text:
theory Infinite_TA_Runs
  imports
    TA.Normalized_Zone_Semantics
    TA_Library.Stream_More
    TA_Library.Instantiate_Existentials
begin

type_synonym ('s, 'c, 't) run = "('s * ('c, 't) cval) stream"
type_synonym ('s, 'c, 't) zrun = "('s * ('c, 't) zone) stream"
type_synonym ('a, 's, 'c, 't) trun = "('a, 'c, 't, 's) transition stream"

coinductive is_run for A where
  "A \<turnstile>' \<langle>l, u\<rangle> \<rightarrow> \<langle>l', u'\<rangle> \<Longrightarrow> is_run A ((l', u') ## xs) \<Longrightarrow> is_run A ((l, u) ## (l', u') ## xs)"

coinductive is_trun for A where
  "A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l' \<Longrightarrow> is_trun A ((l', g', a', r', l'') ## xs)
  \<Longrightarrow> is_trun A ((l, g, a, r, l') ## (l', g', a', r', l'') ## xs)"

(* definition "is_run' A xs ts \<equiv> is_run A xs \<and> smap fst xs = smap fst ts" *)

definition zone_step ::
  "('a, 'c, 't :: time, 's) ta \<Rightarrow> ('a, 'c, 't, 's) transition \<Rightarrow> ('c, 't) zone \<Rightarrow> ('c, 't) zone"
where
  "zone_step A \<equiv> \<lambda> (l, g, a, r, l') Z.
    zone_set ((Z\<^sup>\<up> \<inter> {u. u \<turnstile> inv_of A l}) \<inter> {u. u \<turnstile> g}) r \<inter> {u. u \<turnstile> inv_of A l'}"

coinductive is_zrun for A where
  "A \<turnstile> \<langle>l, Z\<rangle> \<leadsto>\<^bsub>\<tau>\<^esub> \<langle>l', Z'\<rangle> \<Longrightarrow> A \<turnstile> \<langle>l', Z'\<rangle> \<leadsto>\<^bsub>\<upharpoonleft>a\<^esub> \<langle>l'', Z''\<rangle> \<Longrightarrow> is_zrun A ((l'', Z'') ## xs)
  \<Longrightarrow> is_zrun A ((l, Z) ## (l'', Z'') ## xs)"

definition step_from ::
  "('a, 'c, 't :: time, 's) ta \<Rightarrow> ('c, 't) cval \<Rightarrow> ('a, 'c, 't, 's) transition \<Rightarrow> ('c, 't) cval \<Rightarrow> bool"
("_ \<turnstile> _ \<rightarrow>\<^bsub>_\<^esub> _" [61,61] 61)
where
"A \<turnstile> u \<rightarrow>\<^bsub>t\<^esub> u' \<equiv> case t of (l, g, a, r, l') \<Rightarrow> \<exists> d \<ge> 0.
  u \<oplus> d \<turnstile> inv_of A l \<and> d \<ge> 0 \<and> A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l' \<and> u \<oplus> d \<turnstile> g \<and> u' \<turnstile> inv_of A l'
  \<and> u' = [r \<rightarrow> 0](u \<oplus> d)"

lemma step_from_cases:
  assumes "A \<turnstile> u \<rightarrow>\<^bsub>t\<^esub> u'"
  obtains l g a r l' d where
    "t = (l, g, a, r, l')"
    "u \<oplus> d \<turnstile> inv_of A l" "d \<ge> 0" "A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l'" "u \<oplus> d \<turnstile> g" "u' \<turnstile> inv_of A l'"
    "u' = [r \<rightarrow> 0](u \<oplus> d)"
  apply atomize_elim
  using assms unfolding step_from_def by (cases t) auto

lemma step_from_step':
  "A \<turnstile>' \<langle>l, u\<rangle> \<rightarrow> \<langle>l', u'\<rangle>" if "A \<turnstile> u \<rightarrow>\<^bsub>(l, g, a, r, l')\<^esub> u'"
  using that by (auto intro: step_a.intros elim!: step_from_cases)

lemma stepz_from_steps:
  "A \<turnstile>' \<langle>l, u\<rangle> \<rightarrow>* \<langle>l'', u''\<rangle>" if "A \<turnstile> u \<rightarrow>\<^bsub>(l, g, a, r, l')\<^esub> u'" "A \<turnstile>' \<langle>l', u'\<rangle> \<rightarrow>* \<langle>l'', u''\<rangle>"
  using that by (blast intro: step_from_step')

lemma step_from_complete:
  "A \<turnstile> u \<rightarrow>\<^bsub>t\<^esub> u' \<Longrightarrow> u \<in> Z \<Longrightarrow> u' \<in> zone_step A t Z"
  by (auto 4 4 simp: zone_delay_def zone_step_def zone_set_def elim!: step_from_cases)

coinductive is_run_from for A where
  "A \<turnstile> u \<rightarrow>\<^bsub>(l, g, a, r, l')\<^esub> u' \<Longrightarrow> is_run_from A ((l', u') ## xs) ts
  \<Longrightarrow> is_run_from A ((l, u) ## (l', u') ## xs) ((l, g, a, r, l') ## ts)"

inductive stepz_from ::
  "('a, 'c, 't, 's) ta \<Rightarrow> ('c, ('t::time)) zone \<Rightarrow> _ \<Rightarrow> ('c, 't) zone \<Rightarrow> bool"
("_ \<turnstile> _ \<leadsto>\<^bsub>_\<^esub> _" [61,61,61,61] 61)
where
  "A \<turnstile> Z \<leadsto>\<^bsub>(l, g, a, r, l')\<^esub> zone_step A (l, g, a, r, l') Z"
  if "A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l'"

coinductive is_zrun_from for A where
  "A \<turnstile> Z \<leadsto>\<^bsub>(l, g, a, r, l')\<^esub> Z' \<Longrightarrow> is_zrun_from A ((l', Z'') ## xs) ts
  \<Longrightarrow> is_zrun_from A ((l, Z) ## (l', Z') ## xs) ((l, g, a, r, l') ## ts)"

lemma
 "\<exists> u' \<in> zone_step A (l, g, a, r, l') Z. A \<turnstile> u \<rightarrow>\<^bsub>(l, g, a, r, l')\<^esub> u'"
 if "A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l'" "zone_step A (l, g, a, r, l') Z \<noteq> {}"
proof -
  define thesis where "thesis = ?thesis"
  from that show ?thesis
    unfolding zone_step_def
 oops

lemma zstep_from_prestable:
  "\<exists> u' \<in> Z'. A \<turnstile> u \<rightarrow>\<^bsub>(l, g, a, r, l')\<^esub> u'" if "A \<turnstile> Z \<leadsto>\<^bsub>(l, g, a, r, l')\<^esub> Z'" "Z' \<noteq> {}" "u \<in> Z"
  using that
  apply cases
    apply simp
  apply (simp add: zone_delay_def zone_step_def zone_set_def step_from_def)
  oops

lemma
 "\<exists> u \<in> Z. A \<turnstile> u \<rightarrow>\<^bsub>(l, g, a, r, l')\<^esub> u'"
 if "u' \<in> zone_step A (l, g, a, r, l') Z" "A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l'"
  using that by (auto simp: zone_delay_def zone_step_def zone_set_def step_from_def)

lemma stepz_from_poststable:
 "\<exists> u \<in> Z. A \<turnstile> u \<rightarrow>\<^bsub>(l, g, a, r, l')\<^esub> u'"
 if "u' \<in> Z'" "A \<turnstile> Z \<leadsto>\<^bsub>(l, g, a, r, l')\<^esub> Z'"
  using that(2,1) by cases (auto simp: zone_delay_def zone_step_def zone_set_def step_from_def)

lemma is_run_from_locs:
  "is_run_from A xs ts \<Longrightarrow> smap fst xs = smap fst ts"
  apply (coinduction arbitrary: xs ts rule: stream.coinduct)
  subgoal for xs ts
    by (inst_existentials "stl xs" "stl ts") (auto elim: is_run_from.cases)
  done
term "(\<lambda> (l, g, a, r, l') (_, u). (l', SOME u'. A \<turnstile> u \<rightarrow>\<^bsub>(l, g, a, r, l')\<^esub> u'))"
term "sscan"
definition
  "gen_run A xs x =
    x ## sscan (\<lambda> (l, g, a, r, l') (_, u). (l', SOME u'. A \<turnstile> u \<rightarrow>\<^bsub>(l, g, a, r, l')\<^esub> u')) xs x"

definition
  "gen_zrun A xs x = x ##
  sscan (
    \<lambda> (l, g, a, r, l') (_, Z).
      (l', zone_set ((Z\<^sup>\<up> \<inter> {u. u \<turnstile> inv_of A l}) \<inter> {u. u \<turnstile> g}) r \<inter> {u. u \<turnstile> inv_of A l'})
  ) xs x"

lemma is_run_from_is_zrun:
  "is_run_from A ((l, u) ## xs) ts \<Longrightarrow> u \<in> Z \<Longrightarrow> is_zrun A (gen_zrun A ts (l, Z))"
proof (coinduction arbitrary: l u Z ts xs)
  case prems: is_zrun
  from is_run_from.cases[OF prems(1)] guess u l g a1 r l2 u2 xs1 ts'
    .
  note guessed = this
  then obtain l' Z' l'' Z'' xs' a where
    "gen_zrun A ts (l, Z) = (l, Z) ## (l'', Z'') ## xs'"
    "A \<turnstile> \<langle>l, Z\<rangle> \<leadsto>\<^bsub>\<tau>\<^esub> \<langle>l', Z'\<rangle>"
    "A \<turnstile> \<langle>l', Z'\<rangle> \<leadsto>\<^bsub>\<upharpoonleft>a\<^esub> \<langle>l'', Z''\<rangle>"
    "(l'', Z'') ## xs' = gen_zrun A (stl ts) (l'', Z'')"
    "Z'' = zone_step A (l, g, a1, r, l2) Z"
    "l2 = l''"
    apply atomize_elim
    unfolding gen_zrun_def zone_step_def
    apply (subst stream.collapse[symmetric])
    apply (simp add: step_z.simps)
    apply (cases "shd ts")
    by (auto elim: step_from_cases)
  with guessed prems(2) show ?case
    apply simp
    apply (inst_existentials l' Z' a l'' Z'' xs')
    by (fastforce dest: step_from_complete)+
qed

lemma is_run_from_abstract:
  "is_run_from A ((l, u) ## xs) ts \<Longrightarrow> u \<in> Z
  \<Longrightarrow> stream_all2 (\<lambda> (l, u) (l', Z). l = l' \<and> u \<in> Z) ((l, u) ## xs) (gen_zrun A ts (l, Z))"
proof (coinduction arbitrary: l u Z ts xs rule: stream.rel_coinduct)
  case prems: Eq_stream
  from is_run_from.cases[OF prems(1)] guess u l g a1 r l2 u2 xs1 ts' .
  note guessed = this
  then obtain l' Z' l'' Z'' xs' a where
    "gen_zrun A ts (l, Z) = (l, Z) ## (l'', Z'') ## xs'"
    "A \<turnstile> \<langle>l, Z\<rangle> \<leadsto>\<^bsub>\<tau>\<^esub> \<langle>l', Z'\<rangle>"
    "A \<turnstile> \<langle>l', Z'\<rangle> \<leadsto>\<^bsub>\<upharpoonleft>a\<^esub> \<langle>l'', Z''\<rangle>"
    "(l'', Z'') ## xs' = gen_zrun A (stl ts) (l'', Z'')"
    "Z'' = zone_step A (l, g, a1, r, l2) Z"
    "l2 = l''"
    apply atomize_elim
    unfolding gen_zrun_def zone_step_def
    apply (subst stream.collapse[symmetric])
    apply (simp add: step_z.simps)
    apply (cases "shd ts")
    by (auto elim: step_from_cases)
  with guessed prems(2) show ?case
    apply simp
    apply (inst_existentials l' Z' a l'' Z'' xs')
    by (fastforce dest: step_from_complete)+
qed

locale Zone_Step_Defs =
  fixes A :: "('a, 'c, 't :: time, 's) ta"
    and step :: "('a, 'c, 't, 's) transition \<Rightarrow> ('c, 't) zone \<Rightarrow> ('c, 't) zone"
begin

inductive stepz_from ::
  "('c, ('t::time)) zone \<Rightarrow> _ \<Rightarrow> ('c, 't) zone \<Rightarrow> bool"
  ("_ \<leadsto>\<^bsub>_\<^esub> _" [61,61,61] 61)
where
  "Z \<leadsto>\<^bsub>(l, g, a, r, l')\<^esub> step (l, g, a, r, l') Z"
  if "A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l'"

inductive is_stepsz_from where
  Single: "is_stepsz_from [x] []" |
  Cons: "Z \<leadsto>\<^bsub>(l, g, a, r, l')\<^esub> Z' \<Longrightarrow> is_stepsz_from ((l', Z') # xs) ts
  \<Longrightarrow> is_stepsz_from ((l, Z) # (l', Z') # xs) ((l, g, a, r, l') # ts)"

lemmas [intro] = is_stepsz_from.intros

coinductive is_zrun_from where
  "Z \<leadsto>\<^bsub>(l, g, a, r, l')\<^esub> Z' \<Longrightarrow> is_zrun_from ((l', Z') ## xs) ts
  \<Longrightarrow> is_zrun_from ((l, Z) ## (l', Z') ## xs) ((l, g, a, r, l') ## ts)"

end (* End of Zone Step Defs *)

locale Zone_Step = Zone_Step_Defs +
  fixes Z\<^sub>0
  assumes poststable: "u' \<in> Z' \<Longrightarrow> Z \<leadsto>\<^bsub>t\<^esub> Z' \<Longrightarrow> \<exists> u. u \<in> Z \<and> A \<turnstile> u \<rightarrow>\<^bsub>t\<^esub> u'"
      and finite_reachable: "finite {Z. (\<lambda> Z Z'. \<exists> t. Z \<leadsto>\<^bsub>t\<^esub> Z')\<^sup>*\<^sup>* Z\<^sub>0 Z}"
      and finite_transitions: "finite {(l, g, a, r, l'). A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l'}"
begin

lemma is_zrun_from_transitions:
  assumes "is_zrun_from xs ts"
  shows "pred_stream (\<lambda> (l, g, a, r, l'). A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l') ts"
  using assms by (coinduction arbitrary: xs ts) (auto elim: stepz_from.cases is_zrun_from.cases)

lemma is_zrun_from_reachable':
  assumes "is_zrun_from ((l, Z) ## xs) ts" "(\<lambda> Z Z'. \<exists> t. Z \<leadsto>\<^bsub>t\<^esub> Z')\<^sup>*\<^sup>* Z\<^sub>0 Z"
  shows
    "pred_stream (\<lambda> (l', Z). (\<lambda> Z Z'. \<exists> t. Z \<leadsto>\<^bsub>t\<^esub> Z')\<^sup>*\<^sup>* Z\<^sub>0 Z \<and> (\<exists> l g a r. A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l')) xs"
  using assms
  by (coinduction arbitrary: l Z xs ts)
     (force elim: is_zrun_from.cases stepz_from.cases intro: rtranclp.intros(2)) (* Slow *)

lemma is_zrun_from_reachable:
  assumes "is_zrun_from ((l\<^sub>0, Z\<^sub>0) ## xs) ts"
  shows
    "pred_stream (\<lambda> (l', Z). (\<lambda> Z Z'. \<exists> t. Z \<leadsto>\<^bsub>t\<^esub> Z')\<^sup>*\<^sup>* Z\<^sub>0 Z \<and> (\<exists> l g a r. A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l')) xs"
  by (rule is_zrun_from_reachable'[OF assms]) blast

lemma is_zrun_from_finite_state_set:
  assumes "is_zrun_from ((l\<^sub>0, Z\<^sub>0) ## xs) ts"
  shows "finite (sset ((l\<^sub>0, Z\<^sub>0) ## xs))"
proof -
  let ?S = "{(l', Z). (\<lambda> Z Z'. \<exists> t. Z \<leadsto>\<^bsub>t\<^esub> Z')\<^sup>*\<^sup>* Z\<^sub>0 Z \<and> (\<exists> l g a r. A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l')}"
  from is_zrun_from_reachable[OF assms] have "sset xs \<subseteq> ?S" unfolding stream.pred_set by auto
  moreover have "finite ?S"
    using finite_reachable finite_transitions [[simproc add: finite_Collect]] by auto
  ultimately show ?thesis by (auto intro: finite_subset)
qed

lemma is_zrun_from_decomp:
  assumes "is_zrun_from (xs @- ys) ts" "xs \<noteq> []"
  shows
    "is_stepsz_from xs (stake (length xs - 1) ts) \<and> is_zrun_from ys (sdrop (length xs) ts)
     \<and> (case last xs of (l, Z) \<Rightarrow> case shd ys of (l', Z') \<Rightarrow> \<exists> g a r. Z \<leadsto>\<^bsub>(l, g, a, r, l')\<^esub> Z' \<and> snth ts (length xs - 1) = (l, g, a, r, l'))"
using assms(2,1)
proof (induction xs arbitrary: ts rule: list_nonempty_induct)
  case (single x)
  then show ?case by (auto elim: is_zrun_from.cases)
next
  case (cons x xs)
  then show ?case by (cases xs; auto 4 4 elim: is_zrun_from.cases)
qed

lemma is_zrun_from_decomp':
  assumes "is_zrun_from (xs @- ys) ts" "xs \<noteq> []"
  shows "\<exists> ts'. is_stepsz_from xs ts' \<and> set ts' \<subseteq> sset ts"
  using is_zrun_from_decomp[OF assms] by (inst_existentials "stake (length xs - 1) ts", blast) rule

lemma is_stepsz_from_append_single:
  assumes
    "is_stepsz_from xs ts"
    "case last xs of (l, Z) \<Rightarrow> Z \<leadsto>\<^bsub>(l, g, a, r, l')\<^esub> Z'"
    "xs \<noteq> []"
  shows "is_stepsz_from (xs @ [(l', Z')]) (ts @ [(fst (last xs), g, a, r, l')])"
  using assms(3,1,2)
  by (induction xs arbitrary: ts rule: list_nonempty_induct) (auto 4 4 elim: is_stepsz_from.cases)

lemma is_stepsz_from_extend_run:
  assumes
    "is_stepsz_from xs ts"
    "case last xs of (l, Z) \<Rightarrow> Z \<leadsto>\<^bsub>(l, g, a, r, l')\<^esub> Z'"
    "is_zrun_from ((l', Z') ## ys) ts'"
    "xs \<noteq> []"
  shows "is_zrun_from (xs @- (l', Z') ## ys) (ts @- (fst (last xs), g, a, r, l') ## ts')"
  using assms(4,1-3)
  by (induction xs arbitrary: ts rule: list_nonempty_induct)
     (auto 4 4 elim: is_stepsz_from.cases intro: is_zrun_from.intros)

lemma is_stepsz_from_cycle:
  assumes
    "is_stepsz_from xs ts"
    "case last xs of (l, Z) \<Rightarrow> case hd xs of (l', Z') \<Rightarrow> Z \<leadsto>\<^bsub>(l, g, a, r, l')\<^esub> Z'"
    "xs \<noteq> []"
  shows "is_zrun_from (cycle xs) (cycle (ts @ [(fst (last xs), g, a, r, fst (hd xs))]))"
  using assms
proof (coinduction arbitrary: g a r xs ts)
  case is_zrun_from
  then show ?case
    apply (rewrite at \<open>cycle xs\<close> stream.collapse[symmetric])
    apply (rewrite at \<open>stl (cycle xs)\<close> stream.collapse[symmetric])
    apply clarsimp
    subgoal for l' Z' l Z
      apply (erule is_stepsz_from.cases)
      subgoal for x
        apply simp
        apply (inst_existentials g a r "cycle [(l, g, a, r, l)]")
          apply (subst cycle_Cons, simp; fail)
         apply assumption
        apply (rule disjI1)
        apply (inst_existentials g a r "[(l, Z)]")
         apply (subst (2) cycle_Cons, simp; fail)
        apply (rule exI[where x = "[]"])
        by auto
      apply simp
      subgoal for _ _ g' a' r' l'' Z'' xs' ts'
        apply (inst_existentials g' a' r' "cycle (ts' @ [(l', g, a, r, l), (l, g', a', r', l'')])")
          apply (subst cycle_Cons, simp; fail)
         apply assumption
        apply (rule disjI1)
        apply (inst_existentials g' a' r' "(l'', Z'') # xs' @ [(l, Z)]")
         apply (subst cycle_Cons, simp; fail)
        apply (inst_existentials "ts' @ [(l', g, a, r, l)]")
        using is_stepsz_from_append_single by fastforce+
      done
    done
qed

lemma is_zrun_from_stl:
  "is_zrun_from (stl xs) (stl ts)" if "is_zrun_from xs ts"
  using that by (auto elim: is_zrun_from.cases)

lemma is_zrun_from_sdrop:
  "is_zrun_from (sdrop n xs) (sdrop n ts)" if "is_zrun_from xs ts"
  using that by (induction n arbitrary: xs ts) (auto intro: is_zrun_from_stl)

paragraph \<open>Infinte Paths in the Simulation Graph contain cycles\<close>

lemma is_zrun_from_finite_state_set_cycle:
  assumes "is_zrun_from ((l\<^sub>0, Z\<^sub>0) ## xs) ts"
  shows
  "\<exists> ys zs ts'.
    is_zrun_from ((l\<^sub>0, Z\<^sub>0) ## ys @- cycle zs) ts'
  \<and> set ys \<union> set zs \<subseteq> {(l\<^sub>0, Z\<^sub>0)} \<union> sset xs \<and> sset ts' \<subseteq> sset ts"
proof -
  from is_zrun_from_finite_state_set[OF assms] have "finite (sset ((l\<^sub>0, Z\<^sub>0) ## xs))" .
  then have "\<not> sdistinct ((l\<^sub>0, Z\<^sub>0) ## xs)"
    by (auto dest: sdistinct_infinite_sset)
  from not_sdistinct_decomp[OF this] guess ws ys x zs .
  then have decomp: "(l\<^sub>0, Z\<^sub>0) ## xs = (ws @ [x]) @- ys @- x ## zs"
    by simp
  then have *: "(l\<^sub>0, Z\<^sub>0) ## tl (ws @ [x]) @- xs = (ws @ [x]) @- xs" for xs
    by (metis append_is_Nil_conv list.simps(3) shift_simps(1,2) stream.exhaust_sel stream.sel(1))
  from is_zrun_from_decomp[OF assms[unfolded decomp]] guess l Z  l' Z'  g a r by auto
  note decomp_first = this
  from is_zrun_from_sdrop[OF assms, of "length (ws @ [x])"] guess by simp
  moreover from decomp have "sdrop (length ws) xs = ys @- x ## zs"
    apply (cases ws)
     apply simp
    apply simp
    by (subst sdrop_shift, simp, simp add: Nitpick.size_list_simp(2))
  ultimately have "is_zrun_from ((ys @ [x]) @- zs) (sdrop (length ws) (stl ts))" by simp
  from is_zrun_from_decomp'[OF this] guess ts' by auto
  from is_stepsz_from_cycle[OF this(1)] decomp_first have
    "is_zrun_from (cycle (ys @ [x]))
     (cycle (ts' @ [(fst (last (ys @ [x])), g, a, r, fst (hd (ys @ [x])))]))"
    by (force split: if_split_asm)
  with
    is_stepsz_from_extend_run[
      of "(ws @ [x])" "(stake (length ws) ts)" g a r l' Z' "stl (cycle (ys @ [x]))"
         "cycle (ts' @ [(fst (last (ys @ [x])), g, a, r, fst (hd (ys @ [x])))])"
    ] decomp_first
  have
    "is_zrun_from ((ws @ [x]) @- cycle (ys @ [x]))
      (stake (
          length (ws @ [x])) ts
          @- cycle (ts' @ [(fst (last (ys @ [x])), g, a, r, fst (hd (ys @ [x])))]
      ))"
    apply (simp split: if_split_asm)
    subgoal premises prems
    proof -
      have "stake (length ws) ts @ [(l', g, a, r, l')] = shd ts # stake (length ws) (stl ts)"
        by (metis prems(2) stake.simps(2) stake_Suc)
      then have
        "stake (length ws) ts @- [(l', g, a, r, l')] @- cycle (ts' @ [(l', g, a, r, l')])
       = shd ts ## stake (length ws) (stl ts) @- cycle (ts' @ [(l', g, a, r, l')])"
        by (simp del: shift.simps(2) add: shift.simps(2)[symmetric] shift_append[symmetric])
      with prems show ?thesis
        using cycle_Cons[of "(l', Z')" "[]", simplified] by auto
    qed
    subgoal premises prems
    proof -
      have
        "ws @- (l, Z) ## (l', Z') ## cycle (tl ys @ [(l, Z), (l', Z')])
       = ws @- (l, Z) ## cycle (ys @ [(l, Z)])"
        unfolding \<open>hd ys = _\<close>[symmetric] using \<open>ys \<noteq> []\<close> by (subst (2) cycle.ctr) simp
      moreover have
        "shd ts ## stake (length ws) (stl ts) @- cycle (ts' @ [(l, g, a, r, l')])
       = stake (length ws) ts @- (l, g, a, r, l') ## cycle (ts' @ [(l, g, a, r, l')])"
        unfolding \<open>ts !! _ = _\<close>[symmetric]  stake_Suc[symmetric] using stake_Suc[of "length ws" ts]
        by simp (metis (no_types) scons_eq_shift shift.simps(1) shift_append)
      ultimately show ?thesis using prems by simp
    qed
    done
  with decomp show ?thesis
    apply (inst_existentials
        "tl (ws @ [x])" "(ys @ [x])"
        "(stake (length (ws @ [x])) ts
      @- cycle (ts' @ [(fst (last (ys @ [x])), g, a, r, fst (hd (ys @ [x])))]))"
        )
      apply (simp add: *)
     apply (cases ws; force)
    apply (auto intro: shd_sset)
      apply (metis (no_types, lifting)
        Cons_eq_append_conv decomp_first(3,4,6) fst_conv hd_append2 list.sel(1) snth_sset
        stream.sel(1)
        )
    using set_sset_stake[of "length ws"] sset_sdrop \<open>set ts' \<subseteq> _\<close> by - (rule stl_sset, fastforce)+
qed

paragraph \<open>Cycles in the Simulation Graph Contain Pre-stable Cycles\<close>

lemma is_stepsz_from_prestable:
  "\<exists> u \<in> Z. A \<turnstile>' \<langle>l, u\<rangle> \<rightarrow>* \<langle>l', u'\<rangle>" if
  "is_stepsz_from xs ts" "hd xs = (l, Z)" "last xs = (l', Z')" "u' \<in> Z'"
using that
proof (induction arbitrary: l Z l' Z')
  case (Single x)
  then show ?case by auto
next
  case (Cons Z l g a r l' Z' xs ts)
  then show ?case
    by (clarsimp split: if_split_asm) (blast intro: stepz_from_steps dest: poststable[rotated])+
qed

lemma
  "\<exists> u \<in> Z. \<exists> l' u'. A \<turnstile>' \<langle>l, u\<rangle> \<rightarrow> \<langle>l', u'\<rangle> \<and> A \<turnstile>' \<langle>l', u'\<rangle> \<rightarrow>* \<langle>l, u\<rangle>" if
  assms: "is_stepsz_from xs ts" "hd xs = last xs" "hd xs = (l, Z)" "Z \<noteq> {}" "length xs > 1"
proof -
  from that obtain g a r l' Z' ts' where tail:
    "xs = (l, Z) # (l', Z') # tl (tl xs)" "Z \<leadsto>\<^bsub>(l, g, a, r, l')\<^esub> Z'"
    "is_stepsz_from ((l', Z') # tl (tl xs)) ts'"
    by - (erule is_stepsz_from.cases, auto)
  obtain u u' where
    "A \<turnstile>' \<langle>l', u\<rangle> \<rightarrow>* \<langle>l, u'\<rangle>" "u \<in> Z'" "u' \<in> Z"
    using is_stepsz_from_prestable[OF tail(3), of l' Z' l Z] \<open>xs = _\<close> assms(2-)
    by atomize_elim (cases "tl (tl xs)", auto)
  moreover from poststable[OF \<open>u \<in> Z'\<close> tail(2)] guess u1 ..
  ultimately show ?thesis
oops

end (* Zone Step *)

end (* Theory *)

author: wimmers

repo: munta

save_path: github-repos/isabelle/wimmers-munta


text:
(*
 * Copyright 2014, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

theory WPC
imports "~~/src/HOL/Main"
keywords "wpc_setup" :: thy_decl

begin

definition
  wpc_helper :: "(('a \<Rightarrow> bool) \<times> 'b set)
                 \<Rightarrow> (('a \<Rightarrow> bool) \<times> 'b set) \<Rightarrow> bool \<Rightarrow> bool" where
 "wpc_helper \<equiv> \<lambda>(P, P') (Q, Q') R. ((\<forall>s. P s \<longrightarrow> Q s) \<and> P' \<subseteq> Q') \<longrightarrow> R"

lemma wpc_conj_process:
  "\<lbrakk> wpc_helper (P, P') (A, A') C; wpc_helper (P, P') (B, B') D \<rbrakk>
       \<Longrightarrow> wpc_helper (P, P') (\<lambda>s. A s \<and> B s, A' \<inter> B') (C \<and> D)"
  by (clarsimp simp add: wpc_helper_def)

lemma wpc_all_process:
  "\<lbrakk> \<And>x. wpc_helper (P, P') (Q x, Q' x) (R x) \<rbrakk>
       \<Longrightarrow> wpc_helper (P, P') (\<lambda>s. \<forall>x. Q x s, {s. \<forall>x. s \<in> Q' x}) (\<forall>x. R x)"
  by (clarsimp simp: wpc_helper_def subset_iff)

lemma wpc_all_process_very_weak:
  "\<lbrakk> \<And>x. wpc_helper (P, P') (Q, Q') (R x) \<rbrakk> \<Longrightarrow> wpc_helper (P, P') (Q, Q') (\<forall>x. R x)"
  by (clarsimp simp: wpc_helper_def)

lemma wpc_imp_process:
  "\<lbrakk> Q \<Longrightarrow> wpc_helper (P, P') (R, R') S \<rbrakk>
        \<Longrightarrow> wpc_helper (P, P') (\<lambda>s. Q \<longrightarrow> R s, {s. Q \<longrightarrow> s \<in> R'}) (Q \<longrightarrow> S)"
  by (clarsimp simp add: wpc_helper_def subset_iff)

lemma wpc_imp_process_weak:
  "\<lbrakk> wpc_helper (P, P') (R, R') S \<rbrakk> \<Longrightarrow> wpc_helper (P, P') (R, R') (Q \<longrightarrow> S)"
  by (clarsimp simp add: wpc_helper_def)

lemmas wpc_processors
  = wpc_conj_process wpc_all_process wpc_imp_process
lemmas wpc_weak_processors
  = wpc_conj_process wpc_all_process wpc_imp_process_weak
lemmas wpc_vweak_processors
  = wpc_conj_process wpc_all_process_very_weak wpc_imp_process_weak

lemma wpc_helperI:
  "wpc_helper (P, P') (P, P') Q \<Longrightarrow> Q"
  by (simp add: wpc_helper_def)

lemma wpc_foo: "\<lbrakk> undefined x; False \<rbrakk> \<Longrightarrow> P x"
  by simp

lemma foo:
  assumes foo_elim: "\<And>P Q h. \<lbrakk> foo Q h; \<And>s. P s \<Longrightarrow> Q s \<rbrakk> \<Longrightarrow> foo P h"
  shows
  "\<lbrakk> \<And>x. foo (Q x) (f x); foo R g \<rbrakk> \<Longrightarrow>
      foo (\<lambda>s. (\<forall>x. Q x s) \<and> (y = None \<longrightarrow> R s))
         (case y of Some x \<Rightarrow> f x | None \<Rightarrow> g)"
  by (auto split: option.split intro: foo_elim)

ML {*

signature WPC = sig
  exception WPCFailed of string * term list * thm list;

  val foo_thm: thm;
  val iffd2_thm: thm;
  val wpc_helperI: thm;

  val instantiate_concl_pred: Proof.context -> cterm -> thm -> thm;

  val detect_term: Proof.context -> thm -> cterm -> (cterm * term) list;
  val detect_terms: Proof.context -> (term -> cterm -> thm -> tactic) -> tactic;

  val split_term: thm list -> Proof.context -> term -> cterm -> thm -> tactic;

  val wp_cases_tac: thm list -> Proof.context -> tactic;
  val wp_debug_tac: thm list -> Proof.context -> tactic;
  val wp_cases_method: thm list -> (Proof.context -> Method.method) context_parser;

end;

structure WPCPredicateAndFinals = Theory_Data
(struct
    type T = (cterm * thm) list
    val empty = []
    val extend = I
    fun merge (xs, ys) =
        (* Order of predicates is important, so we can't reorder *)
        let val tms = map (Thm.term_of o fst) xs
            fun inxs x = exists (fn y => x aconv y) tms
            val ys' = filter (not o inxs o Thm.term_of o fst) ys
        in
            xs @ ys'
        end
end);

structure WeakestPreCases : WPC =
struct

exception WPCFailed of string * term list * thm list;

val iffd2_thm = @{thm "iffD2"};
val wpc_helperI = @{thm "wpc_helperI"};
val foo_thm = @{thm "wpc_foo"};

(* it looks like cterm_instantiate would do the job better,
   but this handles the case where ?'a must be instantiated
   to ?'a \<times> ?'b *)
fun instantiate_concl_pred ctxt pred thm =
let
  val get_concl_pred  = (fst o strip_comb o HOLogic.dest_Trueprop o Thm.concl_of);
  val get_concl_predC = (Thm.cterm_of ctxt o get_concl_pred);

  val get_pred_tvar   = (Thm.ctyp_of ctxt o domain_type o Thm.typ_of o Thm.ctyp_of_cterm);
  val thm_pred        = get_concl_predC thm;
  val thm_pred_tvar   = get_pred_tvar thm_pred;
  val pred_tvar       = get_pred_tvar pred;

  val thm2            = Thm.instantiate ([(thm_pred_tvar, pred_tvar)], []) thm;

  val thm2_pred       = get_concl_predC thm2;
in
  Thm.instantiate ([], [(thm2_pred, pred)]) thm2
end;

fun detect_term ctxt thm tm =
let
  val foo_thm_tm   = instantiate_concl_pred ctxt tm foo_thm;
  val matches      = resolve_tac ctxt [foo_thm_tm] 1 thm;
  val outcomes     = Seq.list_of matches;
  val get_goalterm = (HOLogic.dest_Trueprop o Logic.strip_assums_concl
                       o Envir.beta_eta_contract o hd o Thm.prems_of);
  val get_argument = hd o snd o strip_comb;
in
  map (pair tm o get_argument o get_goalterm) outcomes
end;

fun detect_terms ctxt tactic2 thm =
let
  val pfs           = WPCPredicateAndFinals.get (Proof_Context.theory_of ctxt);
  val detects       = map (fn (tm, rl) => (detect_term ctxt thm tm, rl)) pfs;
  val detects2      = filter (not o null o fst) detects;
  val ((pred, arg), fin)   = case detects2 of
                                [] => raise WPCFailed ("detect_terms: no match", [], [thm])
                               | ((d3, fin) :: _) => (hd d3, fin)
in
  tactic2 arg pred fin thm
end;

fun resolve_single_tac ctxt rules n thm =
  case Seq.chop 2 (resolve_tac ctxt rules n thm)
  of ([], _) => raise WPCFailed
                        ("resolve_single_tac: no rules could apply",
                         [], thm :: rules)
   | (_ :: _ :: _, _) => raise WPCFailed
                        ("resolve_single_tac: multiple rules applied",
                         [], thm :: rules)
   | ([x], _) => Seq.single x;

fun split_term processors ctxt target pred fin t =
let
  val hdTarget      = head_of target;
  val (constNm, _)  = dest_Const hdTarget handle TERM (_, tms)
                       => raise WPCFailed ("split_term: couldn't dest_Const", tms, []);
  val split = case (Ctr_Sugar.ctr_sugar_of_case ctxt constNm) of
      SOME sugar => #split sugar
    | _ => raise WPCFailed ("split_term: not a case", [hdTarget], []);
  val subst         = split RS iffd2_thm;
  val subst2        = instantiate_concl_pred ctxt pred subst;
in
 ((resolve_tac ctxt [subst2] 1)
    THEN
  (resolve_tac ctxt [wpc_helperI] 1)
    THEN
  (REPEAT_ALL_NEW (resolve_tac ctxt processors)
     THEN_ALL_NEW
   resolve_single_tac ctxt [fin]) 1
 ) t
end;

(* n.b. need to concretise the lazy sequence via a list to ensure exceptions
  have been raised already and catch them *)
fun wp_cases_tac processors ctxt thm =
  detect_terms ctxt (split_term processors ctxt) thm
      |> Seq.list_of |> Seq.of_list
    handle WPCFailed _ => no_tac thm;

fun wp_debug_tac processors ctxt  =
  detect_terms ctxt (split_term processors ctxt);

fun wp_cases_method processors = Scan.succeed (fn ctxt =>
  Method.SIMPLE_METHOD (wp_cases_tac processors ctxt));

local structure P = Parse and K = Keyword in

fun add_wpc tm thm lthy = let
  val ctxt = Local_Theory.target_of lthy
  val tm' = (Syntax.read_term ctxt tm) |> Thm.cterm_of ctxt o Logic.varify_global
  val thm' = Proof_Context.get_thm ctxt thm
in
  Local_Theory.background_theory (WPCPredicateAndFinals.map (fn xs => (tm', thm') :: xs)) lthy
end;

val _ =
    Outer_Syntax.command
        @{command_keyword "wpc_setup"}
        "Add wpc stuff"
        (P.term -- P.name >> (fn (tm, thm) => Toplevel.local_theory NONE NONE (add_wpc tm thm)))

end;
end;

*}

ML {*

val wp_cases_tactic_weak = WeakestPreCases.wp_cases_tac @{thms wpc_weak_processors};
val wp_cases_method_strong = WeakestPreCases.wp_cases_method @{thms wpc_processors};
val wp_cases_method_weak   = WeakestPreCases.wp_cases_method @{thms wpc_weak_processors};
val wp_cases_method_vweak  = WeakestPreCases.wp_cases_method @{thms wpc_vweak_processors};

*}

method_setup wpc = {* wp_cases_method_strong *}
  "case splitter for weakest-precondition proofs"

method_setup wpcw = {* wp_cases_method_weak *}
  "weak-form case splitter for weakest-precondition proofs"

definition
  wpc_test :: "'a set \<Rightarrow> ('a \<times> 'b) set \<Rightarrow> 'b set \<Rightarrow> bool"
  where
 "wpc_test P R S \<equiv> (R `` P) \<subseteq> S"

lemma wpc_test_weaken:
  "\<lbrakk> wpc_test Q R S; P \<subseteq> Q \<rbrakk> \<Longrightarrow> wpc_test P R S"
  by (simp add: wpc_test_def, blast)

lemma wpc_helper_validF:
  "wpc_test Q' R S \<Longrightarrow> wpc_helper (P, P') (Q, Q') (wpc_test P' R S)"
  by (simp add: wpc_test_def wpc_helper_def, blast)

setup {*

let
  val tm  = Thm.cterm_of @{context} (Logic.varify_global @{term "\<lambda>R. wpc_test P R S"});
  val thm = @{thm wpc_helper_validF};
in
  WPCPredicateAndFinals.map (fn xs => (tm, thm) :: xs)
end;

*}

lemma set_conj_Int_simp:
  "{s \<in> S. P s} = S \<inter> {s. P s}"
  by auto

lemma case_options_weak_wp:
  "\<lbrakk> wpc_test P R S; \<And>x. wpc_test P' (R' x) S \<rbrakk>
    \<Longrightarrow> wpc_test (P \<inter> P') (case opt of None \<Rightarrow> R | Some x \<Rightarrow> R' x) S"
  apply (rule wpc_test_weaken)
   apply wpcw
    apply assumption
   apply assumption
  apply simp
  done

end

repo: AutoCorres


text:
(*
  File:       Bernoulli.thy
  Author:     Lukas Bulwahn <lukas.bulwahn-at-gmail.com>
  Author:     Manuel Eberl <manuel@pruvisto.org>
*)
section \<open>Bernoulli numbers\<close>

theory Bernoulli
imports Complex_Main
begin

subsection \<open>Preliminaries\<close>

lemma power_numeral_reduce: "a ^ numeral n = a * a ^ pred_numeral n"
  by (simp only: numeral_eq_Suc power_Suc)

lemma fact_diff_Suc: "n < Suc m \<Longrightarrow> fact (Suc m - n) = of_nat (Suc m - n) * fact (m - n)"
  by (subst fact_reduce) auto

lemma of_nat_binomial_Suc:
  assumes "k \<le> n"
  shows   "(of_nat (Suc n choose k) :: 'a :: field_char_0) =
             of_nat (Suc n) / of_nat (Suc n - k) * of_nat (n choose k)"
  using assms by (simp add: binomial_fact divide_simps fact_diff_Suc of_nat_diff del: of_nat_Suc)

lemma integrals_eq:
  assumes "f 0 = g 0"
  assumes "\<And> x. ((\<lambda>x. f x - g x) has_real_derivative 0) (at x)"
  shows "f x = g x"
proof -
  show "f x = g x"
  proof (cases "x \<noteq> 0")
    case True
    from assms DERIV_const_ratio_const[OF this, of "\<lambda>x. f x - g x" 0]
    show ?thesis by auto
  qed (simp add: assms)
qed

lemma sum_diff: "((\<Sum>i\<le>n::nat. f (i + 1) - f i)::'a::field) = f (n + 1) - f 0"
  by (induct n) (auto simp add: field_simps)

lemma Rats_sum: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> \<rat>) \<Longrightarrow> sum f A \<in> \<rat>"
  by (induction A rule: infinite_finite_induct) simp_all

subsection \<open>Bernoulli Numbers and Bernoulli Polynomials\<close>

declare sum.cong [fundef_cong]

fun bernoulli :: "nat \<Rightarrow> real"
where
  "bernoulli 0 = (1::real)"
| "bernoulli (Suc n) =  (-1 / (n + 2)) * (\<Sum>k \<le> n. ((n + 2 choose k) * bernoulli k))"

declare bernoulli.simps[simp del]

lemmas bernoulli_0 [simp] = bernoulli.simps(1)
lemmas bernoulli_Suc = bernoulli.simps(2)
lemma bernoulli_1 [simp]: "bernoulli 1 = -1/2" by (simp add: bernoulli_Suc)
lemma bernoulli_Suc_0 [simp]: "bernoulli (Suc 0) = -1/2" by (simp add: bernoulli_Suc)

text \<open>
  The ``normal'' Bernoulli numbers are the negative Bernoulli numbers $B_n^{-}$ we just defined
  (so called because $B_1^{-} = -\frac{1}{2}$). There is also another convention, the
  positive Bernoulli numbers $B_n^{+}$, which differ from the negative ones only in that
  $B_1^{+} = \frac{1}{2}$. Both conventions have their justification, since a number of theorems
  are easier to state with one than the other.
\<close>
definition bernoulli' where
  "bernoulli' n = (if n = 1 then 1/2 else bernoulli n)"

lemma bernoulli'_0 [simp]: "bernoulli' 0 = 1" by (simp add: bernoulli'_def)

lemma bernoulli'_1 [simp]: "bernoulli' (Suc 0) = 1/2"
  by (simp add: bernoulli'_def)

lemma bernoulli_conv_bernoulli': "n \<noteq> 1 \<Longrightarrow> bernoulli n = bernoulli' n"
  by (simp add: bernoulli'_def)

lemma bernoulli'_conv_bernoulli: "n \<noteq> 1 \<Longrightarrow> bernoulli' n = bernoulli n"
  by (simp add: bernoulli'_def)

lemma bernoulli_conv_bernoulli'_if:
    "n \<noteq> 1 \<Longrightarrow> bernoulli n = (if n = 1 then -1/2 else bernoulli' n)"
  by (simp add: bernoulli'_def)

lemma bernoulli_in_Rats: "bernoulli n \<in> \<rat>"
proof (induction n rule: less_induct)
  case (less n)
  thus ?case
    by (cases n) (auto simp: bernoulli_Suc intro!: Rats_sum Rats_divide)
qed

lemma bernoulli'_in_Rats: "bernoulli' n \<in> \<rat>"
  by (simp add: bernoulli'_def bernoulli_in_Rats)

definition bernpoly :: "nat \<Rightarrow> 'a \<Rightarrow> 'a :: real_algebra_1" where
  "bernpoly n = (\<lambda>x. \<Sum>k \<le> n. of_nat (n choose k) * of_real (bernoulli k) * x ^ (n - k))"

lemma bernoulli_Suc':
  "bernoulli (Suc n) = -1/(real n + 2) * (\<Sum>k\<le>n. real (n + 2 choose (k + 2)) * bernoulli (n - k))"
proof -
  have "bernoulli (Suc n) = - 1 / (real n + 2) * (\<Sum>k\<le>n. real (n + 2 choose k) * bernoulli k)"
    unfolding bernoulli.simps ..
  also have "(\<Sum>k\<le>n. real (n + 2 choose k) * bernoulli k) =
               (\<Sum>k\<le>n. real (n + 2 choose (n - k)) * bernoulli (n - k))"
    by (rule sum.reindex_bij_witness[of _ "\<lambda>k. n - k" "\<lambda>k. n - k"]) simp_all
  also have "\<dots> = (\<Sum>k\<le>n. real (n + 2 choose (k + 2)) * bernoulli (n - k))"
    by (intro sum.cong refl, subst binomial_symmetric) simp_all
  finally show ?thesis .
qed

subsection \<open>Basic Observations on Bernoulli Polynomials\<close>

lemma bernpoly_0 [simp]: "bernpoly n 0 = (of_real (bernoulli n) :: 'a :: real_algebra_1)"
proof (cases n)
  case 0
  then show "bernpoly n 0 = of_real (bernoulli n)"
    unfolding bernpoly_def bernoulli.simps by auto
next
  case (Suc n')
  have "(\<Sum>k\<le>n'. of_nat (Suc n' choose k) * of_real (bernoulli k) * 0 ^ (Suc n' - k)) = (0::'a)"
  proof (intro sum.neutral ballI)
    fix k assume "k \<in> {..n'}"
    thus "of_nat (Suc n' choose k) * of_real (bernoulli k) * (0::'a) ^ (Suc n' - k) = 0"
      by (cases "Suc n' - k") auto
  qed
  with Suc show ?thesis
    unfolding bernpoly_def by simp
qed

lemma continuous_on_bernpoly [continuous_intros]:
  "continuous_on A (bernpoly n :: 'a \<Rightarrow> 'a :: real_normed_algebra_1)"
  unfolding bernpoly_def by (auto intro!: continuous_intros)

lemma isCont_bernpoly [continuous_intros]:
  "isCont (bernpoly n :: 'a \<Rightarrow> 'a :: real_normed_algebra_1) x"
  unfolding bernpoly_def by (auto intro!: continuous_intros)

lemma has_field_derivative_bernpoly:
  "(bernpoly (Suc n) has_field_derivative
     (of_nat (n + 1) * bernpoly n x :: 'a :: real_normed_field)) (at x)"
proof -
  have "(bernpoly (Suc n) has_field_derivative
          (\<Sum>k\<le>n. of_nat (Suc n - k) * x ^ (n - k) * (of_nat (Suc n choose k) *
            of_real (bernoulli k)))) (at x)" (is "(_ has_field_derivative ?D) _")
    unfolding bernpoly_def by (rule DERIV_cong) (fast intro!: derivative_intros, simp)
  also have "?D = of_nat (n + 1) * bernpoly n x" unfolding bernpoly_def
    by (subst sum_distrib_left, intro sum.cong refl, subst of_nat_binomial_Suc) simp_all
  ultimately show ?thesis by (auto simp del: of_nat_Suc One_nat_def)
qed

lemmas has_field_derivative_bernpoly' [derivative_intros] =
  DERIV_chain'[OF _ has_field_derivative_bernpoly]

lemma sum_binomial_times_bernoulli:
  "(\<Sum>k\<le>n. ((Suc n) choose k) * bernoulli k) = (if n = 0 then 1 else 0)"
proof (cases n)
  case (Suc m)
  then show ?thesis
    by (simp add: bernoulli_Suc)
       (simp add: field_simps add_2_eq_Suc'[symmetric] del: add_2_eq_Suc add_2_eq_Suc')
qed simp_all

lemma sum_binomial_times_bernoulli':
  "(\<Sum>k<n. real (n choose k) * bernoulli k) = (if n = 1 then 1 else 0)"
proof (cases n)
  case (Suc m)
  have "(\<Sum>k<n. real (n choose k) * bernoulli k) =
           (\<Sum>k\<le>m. real (Suc m choose k) * bernoulli k)"
    unfolding Suc lessThan_Suc_atMost ..
  also have "\<dots> = (if n = 1 then 1 else 0)"
    by (subst sum_binomial_times_bernoulli) (simp add: Suc)
  finally show ?thesis .
qed simp_all

lemma binomial_unroll:
  "n > 0 \<Longrightarrow> (n choose k) = (if k = 0 then 1 else (n - 1) choose (k - 1) + ((n - 1) choose k))"
  by (auto simp add: gr0_conv_Suc)

lemma sum_unroll:
  "(\<Sum>k\<le>n::nat. f k) = (if n = 0 then f 0 else f n + (\<Sum>k\<le>n - 1. f k))"
  by (cases n) (simp_all add: add_ac)

lemma bernoulli_unroll:
  "n > 0 \<Longrightarrow> bernoulli n = - 1 / (real n + 1) * (\<Sum>k\<le>n - 1. real (n + 1 choose k) * bernoulli k)"
by (cases n) (simp add: bernoulli_Suc)+

lemmas bernoulli_unroll_all = binomial_unroll bernoulli_unroll sum_unroll bernpoly_def

lemma bernpoly_1_1: "bernpoly 1 1 = of_real (1/2)"
proof -
  have *: "(1 :: 'a) = of_real 1" by simp
  have "bernpoly 1 (1::'a) = 1 - of_real (1 / 2)"
    by (simp add: bernoulli_unroll_all)
  also have "\<dots> = of_real (1 - 1 / 2)"
    by (simp only: *  of_real_diff)
  also have "1 - 1 / 2 = (1 / 2 :: real)"
    by simp
  finally show ?thesis .
qed

subsection \<open>Sum of Powers with Bernoulli Polynomials\<close>

(* TODO: Generalisation not possible here because mean-value theorem
   is only available for reals *)
lemma diff_bernpoly:
  fixes x :: real
  shows "bernpoly n (x + 1) - bernpoly n x = of_nat n * x ^ (n - 1)"
proof (induct n arbitrary: x)
  case 0
  show ?case unfolding bernpoly_def by auto
next
  case (Suc n)
  have "bernpoly (Suc n) (0 + 1) - bernpoly (Suc n) (0 :: real) =
          (\<Sum>k\<le>n. of_real (real (Suc n choose k) * bernoulli k))"
    unfolding bernpoly_0 unfolding bernpoly_def by simp
  also have "\<dots> = of_nat (Suc n) * 0 ^ n"
    by (simp only: of_real_sum [symmetric] sum_binomial_times_bernoulli) simp
  finally have const: "bernpoly (Suc n) (0 + 1) - bernpoly (Suc n) 0 = \<dots>"
    by simp

  have hyps': "of_nat (Suc n) * bernpoly n (x + 1) -
                  of_nat (Suc n) * bernpoly n x =
                  of_nat n * of_nat (Suc n) * x ^ (n - Suc 0)" for x :: real
    unfolding right_diff_distrib[symmetric]
    by (subst Suc) (simp_all add: algebra_simps)
  have "((\<lambda>x. bernpoly (Suc n) (x + 1) - bernpoly (Suc n) x - of_nat (Suc n) * x ^ n)
           has_field_derivative 0) (at x)" for x :: real
    by (rule derivative_eq_intros refl)+ (insert hyps'[of x], simp add: algebra_simps)
  from integrals_eq[OF const this] show ?case by simp
qed

lemma bernpoly_of_real: "bernpoly n (of_real x) = of_real (bernpoly n x)"
  by (simp add: bernpoly_def)

lemma bernpoly_1:
  assumes "n \<noteq> 1"
  shows   "bernpoly n 1 = of_real (bernoulli n)"
proof -
  have "bernpoly n 1 = bernoulli n"
  proof (cases "n \<ge> 2")
    case False
    with assms have "n = 0" by auto
    thus ?thesis by (simp add: bernpoly_def)
  next
    case True
    with diff_bernpoly[of n 0] show ?thesis
      by (simp add: power_0_left bernpoly_0)
  qed
  hence "bernpoly n (of_real 1) = of_real (bernoulli n)"
    by (simp only: bernpoly_of_real)
  thus ?thesis by simp
qed

lemma bernpoly_1': "bernpoly n 1 = of_real (bernoulli' n)"
  using bernpoly_1_1 [where ?'a = 'a]
  by (cases "n = 1") (simp_all add: bernpoly_1 bernoulli'_def)

theorem sum_of_powers:
  "(\<Sum>k\<le>n::nat. (real k) ^ m) = (bernpoly (Suc m) (n + 1) - bernpoly (Suc m) 0) / (m + 1)"
proof -
  from diff_bernpoly[of "Suc m", simplified] have "(m + (1::real)) * (\<Sum>k\<le>n. (real k) ^ m) = (\<Sum>k\<le>n. bernpoly (Suc m) (real k + 1) - bernpoly (Suc m) (real k))"
    by (auto simp add: sum_distrib_left intro!: sum.cong)
  also have "... = (\<Sum>k\<le>n. bernpoly (Suc m) (real (k + 1)) - bernpoly (Suc m) (real k))"
    by (simp add: add_ac)
  also have "... = bernpoly (Suc m) (n + 1) - bernpoly (Suc m) 0"
    by (simp only: sum_diff[where f="\<lambda>k. bernpoly (Suc m) (real k)"]) simp
  finally show ?thesis by (auto simp add: field_simps intro!: eq_divide_imp)
qed

subsection \<open>Instances for Square And Cubic Numbers\<close>

theorem sum_of_squares: "real (\<Sum>k\<le>n::nat. k ^ 2) = real (2 * n ^ 3 + 3 * n ^ 2 + n) / 6"
  by (simp only: of_nat_sum of_nat_power sum_of_powers)
     (simp add: bernoulli_unroll_all field_simps power2_eq_square power_numeral_reduce)

corollary sum_of_squares_nat: "(\<Sum>k\<le>n::nat. k ^ 2) = (2 * n ^ 3 + 3 * n ^ 2 + n) div 6"
  by (rule sum_of_powers_nat_aux[OF sum_of_squares]) simp_all

theorem sum_of_cubes: "real (\<Sum>k\<le>n::nat. k ^ 3) = real (n ^ 2 + n) ^ 2 / 4"
  by (simp only: of_nat_sum of_nat_power sum_of_powers)
     (simp add: bernoulli_unroll_all field_simps power2_eq_square power_numeral_reduce)

corollary sum_of_cubes_nat: "(\<Sum>k\<le>n::nat. k ^ 3) = (n ^ 2 + n) ^ 2 div 4"
  by (rule sum_of_powers_nat_aux[OF sum_of_cubes]) simp_all

end

author: isabelle-prover

repo: mirror-afp-devel


text:
theory Crypto_Scheme_NTT

imports Crypto_Scheme
        NTT_Scheme

begin

section \<open>Kyber Algorithm using NTT for Fast Multiplication\<close>

hide_type Matrix.vec

context kyber_ntt
begin

definition mult_ntt:: "'a qr \<Rightarrow> 'a qr \<Rightarrow> 'a qr" (infixl "*\<^bsub>ntt\<^esub>" 70) where
  "mult_ntt f g = inv_ntt_poly (ntt_poly f \<star> ntt_poly g)"

lemma mult_ntt:
  "f*g = f *\<^bsub>ntt\<^esub> g"
  unfolding mult_ntt_def using convolution_thm_ntt_poly by auto

definition scalar_prod_ntt::
  "('a qr, 'k) vec \<Rightarrow> ('a qr, 'k) vec \<Rightarrow> 'a qr" (infixl "\<bullet>\<^bsub>ntt\<^esub>" 70) where
  "scalar_prod_ntt v w =
  (\<Sum>i\<in>(UNIV::'k set). (vec_nth v i) *\<^bsub>ntt\<^esub> (vec_nth w i))"

lemma scalar_prod_ntt:
  "scalar_product v w = scalar_prod_ntt v w"
  unfolding scalar_product_def scalar_prod_ntt_def using mult_ntt by auto

definition mat_vec_mult_ntt::
  "(('a qr, 'k) vec, 'k) vec \<Rightarrow> ('a qr, 'k) vec \<Rightarrow> ('a qr, 'k) vec" (infixl "\<cdot>\<^bsub>ntt\<^esub>" 70) where
  "mat_vec_mult_ntt A v = vec_lambda (\<lambda>i.
  (\<Sum>j\<in>UNIV. (vec_nth (vec_nth A i) j) *\<^bsub>ntt\<^esub> (vec_nth v j)))"

lemma mat_vec_mult_ntt:
  "A *v v = mat_vec_mult_ntt A v"
  unfolding matrix_vector_mult_def mat_vec_mult_ntt_def using mult_ntt by auto

text \<open>Refined algorithm using NTT for multiplications\<close>

definition key_gen_ntt ::
  "nat \<Rightarrow> (('a qr, 'k) vec, 'k) vec \<Rightarrow> ('a qr, 'k) vec \<Rightarrow>
   ('a qr, 'k) vec \<Rightarrow> ('a qr, 'k) vec" where
  "key_gen_ntt dt A s e = compress_vec dt (A \<cdot>\<^bsub>ntt\<^esub> s + e)"

lemma key_gen_ntt:
  "key_gen_ntt dt A s e = key_gen dt A s e"
  unfolding key_gen_ntt_def key_gen_def mat_vec_mult_ntt by auto

definition encrypt_ntt ::
  "('a qr, 'k) vec \<Rightarrow> (('a qr, 'k) vec, 'k) vec \<Rightarrow>
   ('a qr, 'k) vec \<Rightarrow> ('a qr, 'k) vec \<Rightarrow> ('a qr) \<Rightarrow>
    nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a qr \<Rightarrow>
   (('a qr, 'k) vec) * ('a qr)" where
  "encrypt_ntt t A r e1 e2 dt du dv m =
  (compress_vec du ((transpose A) \<cdot>\<^bsub>ntt\<^esub> r + e1),
   compress_poly dv ((decompress_vec dt t) \<bullet>\<^bsub>ntt\<^esub> r +
    e2 + to_module (round((real_of_int q)/2)) *\<^bsub>ntt\<^esub> m)) "

lemma encrypt_ntt:
  "encrypt_ntt t A r e1 e2 dt du dv m = encrypt t A r e1 e2 dt du dv m"
  unfolding encrypt_ntt_def encrypt_def mat_vec_mult_ntt scalar_prod_ntt mult_ntt by auto

definition decrypt_ntt ::
  "('a qr, 'k) vec \<Rightarrow> ('a qr) \<Rightarrow> ('a qr, 'k) vec \<Rightarrow>
  nat \<Rightarrow> nat \<Rightarrow> 'a qr" where
  "decrypt_ntt u v s du dv = compress_poly 1 ((decompress_poly dv v) -
  s \<bullet>\<^bsub>ntt\<^esub> (decompress_vec du u))"

lemma decrypt_ntt:
  "decrypt_ntt u v s du dv = decrypt u v s du dv"
  unfolding decrypt_ntt_def decrypt_def scalar_prod_ntt by auto

text \<open>$(1-\delta)$-correctness for the refined algorithm\<close>

lemma kyber_correct_ntt:
  fixes A s r e e1 e2 dt du dv ct cu cv t u v
  assumes
      t_def:   "t = key_gen_ntt dt A s e"
  and u_v_def: "(u,v) = encrypt_ntt t A r e1 e2 dt du dv m"
  and ct_def:  "ct = compress_error_vec dt (A \<cdot>\<^bsub>ntt\<^esub> s + e)"
  and cu_def:  "cu = compress_error_vec du
                ((transpose A) \<cdot>\<^bsub>ntt\<^esub> r + e1)"
  and cv_def:  "cv = compress_error_poly dv
                ((decompress_vec dt t) \<bullet>\<^bsub>ntt\<^esub> r + e2 +
                 to_module (round((real_of_int q)/2)) *\<^bsub>ntt\<^esub> m)"
  and delta:   "abs_infty_poly (e \<bullet>\<^bsub>ntt\<^esub> r + e2 + cv -
                s \<bullet>\<^bsub>ntt\<^esub> e1 + ct \<bullet>\<^bsub>ntt\<^esub> r -
                s \<bullet>\<^bsub>ntt\<^esub> cu) < round (real_of_int q / 4)"
  and m01:     "set ((coeffs \<circ> of_qr) m) \<subseteq> {0,1}"
  shows "decrypt_ntt u v s du dv = m"
using assms unfolding key_gen_ntt encrypt_ntt decrypt_ntt mat_vec_mult_ntt[symmetric]
scalar_prod_ntt[symmetric] mult_ntt[symmetric] using kyber_correct by auto

end
end


text:
theory HoareLogic
  imports CKA
begin

context ckat begin

definition hoare_triple :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("\<lbrace> _ \<rbrace> _ \<lbrace> _ \<rbrace>" [54,54,54] 53)
  where "\<lbrace>p\<rbrace>x\<lbrace>q\<rbrace> \<equiv> p\<cdot>x = p\<cdot>x\<cdot>q \<and> p \<in> B \<and> q \<in> B"

declare hoare_triple_def [simp]

lemma hoare_equiv: "\<lbrace>p\<rbrace>x\<lbrace>q\<rbrace> = (p \<in> B \<and> q \<in> B \<and> p\<cdot>x \<le> p\<cdot>x\<cdot>q)"
  by (metis eq_iff hoare_triple_def mult_isol mult_oner test_top)

lemma hoare_equiv2: "\<lbrace>p\<rbrace>x\<lbrace>q\<rbrace> = (p \<in> B \<and> q \<in> B \<and> p\<cdot>x \<le> x\<cdot>q)"
  by (metis encoding_eq hoare_triple_def)

theorem composition_rule: "\<lbrakk>\<lbrace>p\<rbrace>x\<lbrace>q\<rbrace>; \<lbrace>q\<rbrace>y\<lbrace>r\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>p\<rbrace>x\<cdot>y\<lbrace>r\<rbrace>"
  by (smt hoare_triple_def mult_assoc)

theorem weakening_rule: "\<lbrakk>p \<in> B; p \<le> p'; \<lbrace>p'\<rbrace>x\<lbrace>q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>p\<rbrace>x\<lbrace>q\<rbrace>"
  by (metis composition_rule encoding_eq hoare_triple_def mult_onel mult_oner)

theorem weakening_rule2: "\<lbrakk>\<lbrace>p\<rbrace>x\<lbrace>q'\<rbrace>; q' \<le> q; q \<in> B\<rbrakk> \<Longrightarrow> \<lbrace>p\<rbrace>x\<lbrace>q\<rbrace>"
  by (smt hoare_equiv hoare_triple_def mult_isol order_trans)

lemma pull_test: "\<lbrakk>p \<in> B; q \<in> B; \<lbrace>p\<cdot>q\<rbrace>x\<lbrace>r\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>p\<rbrace>q\<cdot>x\<lbrace>r\<rbrace>"
  by (metis hoare_triple_def mult_assoc)

theorem skip_rule: "\<lbrace>p\<rbrace>1\<lbrace>q\<rbrace> \<longleftrightarrow> (p \<le> q \<and> p \<in> B \<and> q \<in> B)"
  by (metis hoare_equiv2 mult_1_left mult_1_right)

corollary skip_true: "p \<in> B \<Longrightarrow> \<lbrace>p\<rbrace>1\<lbrace>p\<rbrace>"
  by (metis eq_refl skip_rule)

lemma choice: "\<lbrakk>\<lbrace>p\<rbrace>x\<lbrace>q\<rbrace>; \<lbrace>p\<rbrace>y\<lbrace>q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>p\<rbrace>x+y\<lbrace>q\<rbrace>"
  by (smt hoare_triple_def distrib_right' distrib_left)

lemma failure: "\<lbrakk>p \<in> B; q \<in> B\<rbrakk> \<Longrightarrow> \<lbrace>p\<rbrace>0\<lbrace>q\<rbrace>"
  by (metis annil annir hoare_triple_def)

lemma iteration: "\<lbrace>p\<rbrace>x\<lbrace>p\<rbrace> \<Longrightarrow> \<lbrace>p\<rbrace>x\<^sup>\<star>\<lbrace>p\<rbrace>"
  by (metis hoare_equiv2 star_sim2)

lemma iteration2: "\<lbrace>p\<rbrace>x\<lbrace>p\<rbrace> \<Longrightarrow> \<lbrace>p\<rbrace>x\<^sup>+\<lbrace>p\<rbrace>"
  by (metis composition_rule iteration star_trancl)

theorem concurrency: "\<lbrakk>x = x\<cdot>q'; \<lbrace>p\<rbrace>x\<lbrace>q\<rbrace>; \<lbrace>p'\<rbrace>x'\<lbrace>q'\<rbrace>; x' = x'\<cdot>q\<rbrakk> \<Longrightarrow> \<lbrace>p\<cdot>p'\<rbrace>x\<parallel>x'\<lbrace>q\<cdot>q'\<rbrace>"
  nitpick oops

theorem frame_rule: "\<lbrakk>r \<in> B; x\<cdot>r = x; r\<cdot>x = x; \<lbrace>p\<rbrace>x\<lbrace>q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>p\<parallel>r\<rbrace>x\<lbrace>q\<parallel>r\<rbrace>"
  by (unfold hoare_triple_def, metis par_comm mult_assoc test_par_closed test_eq)

end

end

author: Alasdair


(*
 * Copyright 2014, General Dynamics C4 Systems
 *
 * SPDX-License-Identifier: GPL-2.0-only
 *)

theory ArchTcb_AI
imports Tcb_AI
begin

context Arch begin global_naming ARM

named_theorems Tcb_AI_asms

lemma activate_idle_invs[Tcb_AI_asms]:
  "\<lbrace>invs and ct_idle\<rbrace>
     arch_activate_idle_thread thread
   \<lbrace>\<lambda>rv. invs and ct_idle\<rbrace>"
  by (simp add: arch_activate_idle_thread_def)

lemma empty_fail_getRegister [intro!, simp, Tcb_AI_asms]:
  "empty_fail (getRegister r)"
  by (simp add: getRegister_def)

lemma same_object_also_valid:  (* arch specific *)
  "\<lbrakk> same_object_as cap cap'; s \<turnstile> cap'; wellformed_cap cap;
     cap_asid cap = None \<or> (\<exists>asid. cap_asid cap = Some asid \<and> 0 < asid \<and> asid \<le> 2^asid_bits - 1);
     cap_vptr cap = None; cap_asid_base cap = None \<rbrakk>
     \<Longrightarrow> s \<turnstile> cap"
  apply (cases cap,
         (clarsimp simp: same_object_as_def is_cap_simps cap_asid_def
                         wellformed_cap_def wellformed_acap_def
                         valid_cap_def bits_of_def cap_aligned_def
                   split: cap.split_asm arch_cap.split_asm option.splits)+)
  done

lemma same_object_obj_refs[Tcb_AI_asms]:
  "\<lbrakk> same_object_as cap cap' \<rbrakk>
     \<Longrightarrow> obj_refs cap = obj_refs cap'"
  apply (cases cap, simp_all add: same_object_as_def)
       apply ((clarsimp simp: is_cap_simps bits_of_def same_aobject_as_def
                      split: cap.split_asm )+)
  by (cases "the_arch_cap cap"; cases "the_arch_cap cap'"; simp)

definition
  is_cnode_or_valid_arch :: "cap \<Rightarrow> bool"
where
 "is_cnode_or_valid_arch cap \<equiv>
    is_cnode_cap cap
     \<or> (is_arch_cap cap
          \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap \<noteq> None)
          \<and> (is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None))"

definition (* arch specific *)
  "pt_pd_asid cap \<equiv> case cap of
    ArchObjectCap (PageTableCap _ (Some (asid, _))) \<Rightarrow> Some asid
  | ArchObjectCap (PageDirectoryCap _ (Some asid)) \<Rightarrow> Some asid
  | _ \<Rightarrow> None"

lemmas pt_pd_asid_simps [simp] = (* arch specific *)
  pt_pd_asid_def [split_simps cap.split arch_cap.split option.split prod.split]

lemma checked_insert_is_derived: (* arch specific *)
  "\<lbrakk> same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap;
     obj_refs new_cap = obj_refs old_cap
         \<longrightarrow> table_cap_ref old_cap = table_cap_ref new_cap
            \<and> pt_pd_asid old_cap = pt_pd_asid new_cap\<rbrakk>
     \<Longrightarrow> is_derived m slot new_cap old_cap"
  apply (cases slot)
  apply (frule same_object_as_cap_master)
  apply (frule master_cap_obj_refs)
  apply (frule cap_master_eq_badge_none)
  apply (frule same_master_cap_same_types)
  apply (simp add: is_derived_def)
  apply clarsimp
  apply (auto simp: is_cap_simps cap_master_cap_def
                    is_cnode_or_valid_arch_def vs_cap_ref_def
                    table_cap_ref_def pt_pd_asid_def up_ucast_inj_eq
             split: cap.split_asm arch_cap.split_asm
                    option.split_asm)[1]
  done

lemma is_cnode_or_valid_arch_cap_asid: (* arch specific *)
  "is_cnode_or_valid_arch cap
       \<Longrightarrow> (is_pt_cap cap \<longrightarrow> cap_asid cap \<noteq> None)
             \<and> (is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None)"
  by (auto simp add: is_cnode_or_valid_arch_def
                     is_cap_simps)

lemma checked_insert_tcb_invs[wp]: (* arch specific *)
  "\<lbrace>invs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref)
        and K (is_cnode_or_valid_arch new_cap) and valid_cap new_cap
        and tcb_cap_valid new_cap (target, ref)
        and K (is_pt_cap new_cap \<or> is_pd_cap new_cap
                         \<longrightarrow> cap_asid new_cap \<noteq> None)
        and (cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap
                              \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and>
                                 pt_pd_asid c = pt_pd_asid new_cap) src_slot)\<rbrace>
     check_cap_at new_cap src_slot
      (check_cap_at (cap.ThreadCap target) slot
       (cap_insert new_cap src_slot (target, ref))) \<lbrace>\<lambda>rv. invs\<rbrace>"
  apply (simp add: check_cap_at_def)
  apply (rule hoare_pre)
   apply (wp get_cap_wp)
  apply (clarsimp simp: cte_wp_at_caps_of_state)
  apply (frule caps_of_state_valid_cap[where p=src_slot], fastforce)
  apply (frule caps_of_state_valid_cap[where p=slot], fastforce)
  apply (rule conjI, simp only: ex_cte_cap_wp_to_def)
   apply (rule_tac x=slot in exI)
   apply (clarsimp simp: cte_wp_at_caps_of_state same_object_as_cte_refs)
   apply (clarsimp simp: same_object_as_def2 cap_master_cap_simps
                  dest!: cap_master_cap_eqDs)
   apply (clarsimp simp: valid_cap_def[where c="cap.ThreadCap x" for x])
   apply (erule cte_wp_atE[OF caps_of_state_cteD])
    apply (fastforce simp: obj_at_def is_obj_defs)
   apply clarsimp
  apply (rule conjI)
   apply clarsimp
   apply (subgoal_tac "\<not> is_zombie new_cap")
    apply (simp add: same_object_zombies same_object_obj_refs)
    apply (erule(2) zombies_final_helperE)
      apply fastforce
     apply (fastforce simp add: cte_wp_at_caps_of_state)
    apply assumption
   apply (clarsimp simp: is_cnode_or_valid_arch_def is_cap_simps
                         is_valid_vtable_root_def)
  apply (rule conjI)
   apply (erule(1) checked_insert_is_derived, simp+)
  apply (auto simp: is_cnode_or_valid_arch_def is_cap_simps)
  done

crunch tcb_at[wp, Tcb_AI_asms]: arch_get_sanitise_register_info, arch_post_modify_registers "tcb_at a"
crunch invs[wp, Tcb_AI_asms]: arch_get_sanitise_register_info, arch_post_modify_registers "invs"
crunch ex_nonz_cap_to[wp, Tcb_AI_asms]: arch_get_sanitise_register_info, arch_post_modify_registers "ex_nonz_cap_to a"

lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]:
  assumes x: "P cap.NullCap"
  shows      "\<lbrace>\<lambda>s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>
                finalise_cap cap fin
              \<lbrace>\<lambda>rv s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>"
  apply (cases cap, simp_all)
       apply (wp suspend_caps_of_state hoare_vcg_all_lift
            | simp
            | rule impI
            | rule hoare_drop_imps)+
     apply (clarsimp simp: ball_ran_eq x)
    apply (wp delete_one_caps_of_state
         | rule impI
         | simp add: deleting_irq_handler_def get_irq_slot_def x ball_ran_eq)+
    done

lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_asms]:
  "table_cap_ref (max_free_index_update cap) = table_cap_ref cap"
  by (simp add: free_index_update_def table_cap_ref_def split: cap.splits)

interpretation Tcb_AI_1? : Tcb_AI_1
  where state_ext_t = state_ext_t
  and is_cnode_or_valid_arch = is_cnode_or_valid_arch
by (unfold_locales; fact Tcb_AI_asms)

lemma use_no_cap_to_obj_asid_strg: (* arch specific *)
  "(cte_at p s \<and> no_cap_to_obj_dr_emp cap s \<and> valid_cap cap s \<and> invs s)
         \<longrightarrow> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap
                \<longrightarrow> table_cap_ref c = table_cap_ref cap \<and> pt_pd_asid c = pt_pd_asid cap) p s"
  apply (clarsimp simp: cte_wp_at_caps_of_state
                     no_cap_to_obj_with_diff_ref_def
           simp del: split_paired_All)
  apply (frule caps_of_state_valid_cap, fastforce)
  apply (erule allE)+
  apply (erule (1) impE)+
  apply (simp add: table_cap_ref_def pt_pd_asid_def split: cap.splits arch_cap.splits option.splits prod.splits)
  apply (fastforce simp: table_cap_ref_def valid_cap_simps elim!: asid_low_high_bits)+
  done

lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]:
  "\<lbrace>no_cap_to_obj_dr_emp cap\<rbrace>
     cap_delete slot
   \<lbrace>\<lambda>rv. no_cap_to_obj_dr_emp cap\<rbrace>"
  apply (simp add: cap_delete_def
                   no_cap_to_obj_with_diff_ref_ran_caps_form)
  apply wp
  apply (rule use_spec)
  apply (rule rec_del_all_caps_in_range)
     apply (simp add: table_cap_ref_def[simplified, split_simps cap.split]
              | rule obj_ref_none_no_asid)+
  done

lemma as_user_valid_cap[wp]:
  "\<lbrace>valid_cap c\<rbrace> as_user a b \<lbrace>\<lambda>rv. valid_cap c\<rbrace>"
  by (wp valid_cap_typ)

lemma as_user_ipc_tcb_cap_valid4[wp]:
  "\<lbrace>\<lambda>s. tcb_cap_valid cap (t, tcb_cnode_index 4) s\<rbrace>
    as_user a b
   \<lbrace>\<lambda>rv. tcb_cap_valid cap (t, tcb_cnode_index 4)\<rbrace>"
  apply (simp add: as_user_def set_object_def get_object_def)
  apply (wp | wpc | simp)+
  apply (clarsimp simp: tcb_cap_valid_def obj_at_def
                        pred_tcb_at_def is_tcb
                 dest!: get_tcb_SomeD)
  apply (clarsimp simp: get_tcb_def)
  done

lemma tc_invs[Tcb_AI_asms]:
  "\<lbrace>invs and tcb_at a
       and (case_option \<top> (valid_cap o fst) e)
       and (case_option \<top> (valid_cap o fst) f)
       and (case_option \<top> (case_option \<top> (valid_cap o fst) o snd) g)
       and (case_option \<top> (cte_at o snd) e)
       and (case_option \<top> (cte_at o snd) f)
       and (case_option \<top> (case_option \<top> (cte_at o snd) o snd) g)
       and (case_option \<top> (no_cap_to_obj_dr_emp o fst) e)
       and (case_option \<top> (no_cap_to_obj_dr_emp o fst) f)
       and (case_option \<top> (case_option \<top> (no_cap_to_obj_dr_emp o fst) o snd) g)
       \<comment> \<open>only set prio \<le> mcp of authorising thread\<close>
       and (\<lambda>s. case_option True (\<lambda>(pr, auth). mcpriority_tcb_at (\<lambda>mcp. pr \<le> mcp) auth s) pr)
       \<comment> \<open>only set mcp \<le> mcp of authorising thread\<close>
       and (\<lambda>s. case_option True (\<lambda>(mcp, auth). mcpriority_tcb_at (\<lambda>m. mcp \<le> m) auth s) mcp)
       and K (case_option True (is_cnode_cap o fst) e)
       and K (case_option True (is_valid_vtable_root o fst) f)
       and K (case_option True (\<lambda>v. case_option True
                          ((swp valid_ipc_buffer_cap (fst v)
                             and is_arch_cap and is_cnode_or_valid_arch)
                                o fst) (snd v)) g)
       and K (case_option True (\<lambda>bl. length bl = word_bits) b)\<rbrace>
      invoke_tcb (ThreadControl a sl b mcp pr e f g)
   \<lbrace>\<lambda>rv. invs\<rbrace>"
  apply (rule hoare_gen_asm)+
  apply (simp add: split_def set_mcpriority_def cong: option.case_cong)
  apply (rule hoare_vcg_precond_imp)
   apply wp
      (* takes long: (30 sec) *)
      apply ((simp only: simp_thms cong: conj_cong
        | (strengthen invs_strengthen)+
        | rule wp_split_const_if wp_split_const_if_R
                   hoare_vcg_all_lift_R
                   hoare_vcg_E_elim hoare_vcg_const_imp_lift_R
                   hoare_vcg_R_conj
        | (wp out_invs_trivial case_option_wpE cap_delete_deletes
             cap_delete_valid_cap cap_insert_valid_cap out_cte_at
             cap_insert_cte_at cap_delete_cte_at out_valid_cap
             hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R
             thread_set_tcb_ipc_buffer_cap_cleared_invs
             thread_set_invs_trivial[OF ball_tcb_cap_casesI]
             hoare_vcg_all_lift thread_set_valid_cap out_emptyable
             check_cap_inv [where P="valid_cap c" for c]
             check_cap_inv [where P="tcb_cap_valid c p" for c p]
             check_cap_inv[where P="cte_at p0" for p0]
             check_cap_inv[where P="tcb_at p0" for p0]
             thread_set_cte_at
             thread_set_cte_wp_at_trivial[where Q="\<lambda>x. x", OF ball_tcb_cap_casesI]
             thread_set_no_cap_to_trivial[OF ball_tcb_cap_casesI]
             checked_insert_no_cap_to
             out_no_cap_to_trivial[OF ball_tcb_cap_casesI]
             thread_set_ipc_tcb_cap_valid
             static_imp_wp static_imp_conj_wp)[1]
        | simp add: ran_tcb_cap_cases dom_tcb_cap_cases[simplified]
                    emptyable_def
               del: hoare_True_E_R
        | wpc
        | strengthen use_no_cap_to_obj_asid_strg
                     tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"]
                     tcb_cap_always_valid_strg[where p="tcb_cnode_index (Suc 0)"])+)
  apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] is_nondevice_page_cap_arch_def
                        is_cap_simps is_valid_vtable_root_def is_nondevice_page_cap_simps
                        is_cnode_or_valid_arch_def tcb_cap_valid_def
                        invs_valid_objs cap_asid_def vs_cap_ref_def
                 split: option.split_asm )+
      apply (simp add: case_bool_If valid_ipc_buffer_cap_def is_nondevice_page_cap_simps
                       is_nondevice_page_cap_arch_def
                split: arch_cap.splits if_splits)+
  done

lemma check_valid_ipc_buffer_inv:
  "\<lbrace>P\<rbrace> check_valid_ipc_buffer vptr cap \<lbrace>\<lambda>rv. P\<rbrace>"
  apply (simp add: check_valid_ipc_buffer_def whenE_def
             cong: cap.case_cong arch_cap.case_cong
             split del: if_split)
  apply (rule hoare_pre)
   apply (wp | simp add: whenE_def if_apply_def2 | wpcw)+
  done

lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]:
  "\<lbrace>\<lambda>(s::'state_ext::state_ext state). is_arch_cap cap \<and> is_cnode_or_valid_arch cap
          \<and> valid_ipc_buffer_cap cap vptr
          \<and> is_aligned vptr msg_align_bits
             \<longrightarrow> P s\<rbrace>
     check_valid_ipc_buffer vptr cap
   \<lbrace>\<lambda>rv. P\<rbrace>,-"
  apply (simp add: check_valid_ipc_buffer_def whenE_def
             cong: cap.case_cong arch_cap.case_cong
             split del: if_split)
  apply (rule hoare_pre)
   apply (wp | simp add: whenE_def split del: if_split | wpc)+
  apply (clarsimp simp: is_cap_simps is_cnode_or_valid_arch_def
                        valid_ipc_buffer_cap_def)
  done

lemma derive_no_cap_asid[wp,Tcb_AI_asms]:
  "\<lbrace>(no_cap_to_obj_with_diff_ref cap S)::'state_ext::state_ext state\<Rightarrow>bool\<rbrace>
     derive_cap slot cap
   \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref rv S\<rbrace>,-"
  apply (simp add: derive_cap_def arch_derive_cap_def
             cong: cap.case_cong)
  apply (rule hoare_pre)
   apply (wp | simp | wpc)+
  apply (auto simp add: no_cap_to_obj_with_diff_ref_Null,
         auto simp add: no_cap_to_obj_with_diff_ref_def
                        table_cap_ref_def)
  done

lemma decode_set_ipc_inv[wp,Tcb_AI_asms]:
  "\<lbrace>P::'state_ext::state_ext state \<Rightarrow> bool\<rbrace> decode_set_ipc_buffer args cap slot excaps \<lbrace>\<lambda>rv. P\<rbrace>"
  apply (simp   add: decode_set_ipc_buffer_def whenE_def
                     split_def
          split del: if_split)
  apply (rule hoare_pre, wp check_valid_ipc_buffer_inv)
  apply simp
  done

lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]:
  "no_cap_to_obj_with_diff_ref c S s \<longrightarrow>
    no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s"
  apply (case_tac "update_cap_data P x c = NullCap")
   apply (simp add: no_cap_to_obj_with_diff_ref_Null)
  apply (subgoal_tac "vs_cap_ref (update_cap_data P x c)
                                 = vs_cap_ref c")
   apply (simp add: no_cap_to_obj_with_diff_ref_def
                    update_cap_objrefs)
  apply (clarsimp simp: update_cap_data_closedform
                        table_cap_ref_def
                        arch_update_cap_data_def
                 split: cap.split)
  apply simp
  done

lemma update_cap_valid[Tcb_AI_asms]:
  "valid_cap cap (s::'state_ext::state_ext state) \<Longrightarrow>
   valid_cap (case capdata of
              None \<Rightarrow> cap_rights_update rs cap
            | Some x \<Rightarrow> update_cap_data p x
                     (cap_rights_update rs cap)) s"
  apply (case_tac capdata, simp_all)[1]
  apply (case_tac cap,
         simp_all add: update_cap_data_def cap_rights_update_def
                       is_cap_defs Let_def split_def valid_cap_def
                       badge_update_def the_cnode_cap_def cap_aligned_def
                       arch_update_cap_data_def split: bool.splits)
   apply (simp add: word_bits_def)
  apply (rename_tac arch_cap)
  using valid_validate_vm_rights[simplified valid_vm_rights_def]
  apply (case_tac arch_cap, simp_all add: acap_rights_update_def
                                     split: option.splits prod.splits bool.splits)
  done

crunch pred_tcb_at: switch_to_thread "pred_tcb_at proj P t"
  (wp: crunch_wps simp: crunch_simps)

crunch typ_at[wp]: invoke_tcb "\<lambda>s. P (typ_at T p s)"
  (ignore: check_cap_at setNextPC zipWithM
       wp: hoare_drop_imps mapM_x_wp' check_cap_inv
     simp: crunch_simps)

end

context begin interpretation Arch .
requalify_consts is_cnode_or_valid_arch
requalify_facts invoke_tcb_typ_at
end

global_interpretation Tcb_AI?: Tcb_AI
  where is_cnode_or_valid_arch = ARM.is_cnode_or_valid_arch
 proof goal_cases
  interpret Arch .
  case 1 show ?case
  by (unfold_locales; fact Tcb_AI_asms)
qed

end


text:
theory "Axioms"
imports
  "Syntax"
  "Denotational_Semantics"
  "Ids"
begin

section \<open>Axioms and Axiomatic Proof Rules of Differential Game Logic\<close>

subsection \<open>Axioms\<close>

abbreviation pusall:: "fml"
  where "pusall \<equiv> \<langle>Game hgidc\<rangle>TT"

abbreviation nothing:: "trm"
  where "nothing \<equiv> Number 0"

named_theorems axiom_defs "Axiom definitions"

definition box_axiom :: "fml"
  where [axiom_defs]:
"box_axiom \<equiv> (Box (Game hgid1) pusall) \<leftrightarrow> Not(Diamond (Game hgid1) (Not(pusall)))"

definition assigneq_axiom :: "fml"
  where [axiom_defs]:
"assigneq_axiom \<equiv> (Diamond (Assign xid1 (Const fid1)) pusall) \<leftrightarrow> Exists xid1 (Equals (Var xid1) (Const fid1) && pusall)"

definition stutterd_axiom :: "fml"
  where [axiom_defs]:
"stutterd_axiom \<equiv> (Diamond (Assign xid1 (Var xid1)) pusall) \<leftrightarrow> pusall"

definition test_axiom :: "fml"
  where [axiom_defs]:
"test_axiom \<equiv> Diamond (Test (Pred pid2 nothing)) (Pred pid1 nothing) \<leftrightarrow> (Pred pid2 nothing && Pred pid1 nothing)"

definition choice_axiom :: "fml"
  where [axiom_defs]:
"choice_axiom \<equiv> Diamond (Choice (Game hgid1) (Game hgid2)) pusall \<leftrightarrow> (Diamond (Game hgid1) pusall || Diamond (Game hgid2) pusall)"

definition compose_axiom :: "fml"
  where [axiom_defs]:
"compose_axiom \<equiv> Diamond (Compose (Game hgid1) (Game hgid2)) pusall \<leftrightarrow> Diamond (Game hgid1) (Diamond (Game hgid2) pusall)"

definition iterate_axiom :: "fml"
  where [axiom_defs]:
"iterate_axiom \<equiv> Diamond (Loop (Game hgid1)) pusall \<leftrightarrow> (pusall || Diamond (Game hgid1) (Diamond (Loop (Game hgid1)) pusall))"

definition dual_axiom :: "fml"
  where [axiom_defs]:
"dual_axiom \<equiv> Diamond (Dual (Game hgid1)) pusall \<leftrightarrow> !(Diamond (Game hgid1) (!pusall))"

subsection \<open>Axiomatic Rules\<close>

named_theorems rule_defs "Rule definitions"

definition mon_rule :: "inference"
  where [rule_defs]:
"mon_rule \<equiv> ([(\<langle>Game hgidc\<rangle>TT) \<rightarrow> (\<langle>Game hgidd\<rangle>TT)], (\<langle>Game hgid1\<rangle>(\<langle>Game hgidc\<rangle>TT)) \<rightarrow> (\<langle>Game hgid1\<rangle>(\<langle>Game hgidd\<rangle>TT)))"

definition FP_rule :: "inference"
  where [rule_defs]:
"FP_rule \<equiv> ([((\<langle>Game hgidc\<rangle>TT) || \<langle>Game hgid1\<rangle>\<langle>Game hgidd\<rangle>TT) \<rightarrow> \<langle>Game hgidd\<rangle>TT], (\<langle>Loop (Game hgid1)\<rangle>\<langle>Game hgidc\<rangle>TT) \<rightarrow> (\<langle>Game hgidd\<rangle>TT))"

definition MP_rule :: "inference"
  where [rule_defs]:
"MP_rule \<equiv> ([Pred pid1 nothing , Pred pid1 nothing \<rightarrow> Pred pid2 nothing], Pred pid2 nothing)"

definition gena_rule :: "inference"
  where [rule_defs]:
"gena_rule \<equiv> ([pusall], Exists xid1 pusall)"

subsection \<open>Soundness / Validity Proofs for Axioms\<close>

text \<open>Because an axiom in a uniform substitution calculus is an individual formula,
  proving the validity of that formula suffices to prove soundness\<close>

lemma box_valid: "valid box_axiom"
  unfolding box_axiom_def Box_def Or_def by simp

(*lemma assign_equal: "game_sem I (Assign x (Const f)) (fml_sem I \<phi>) = fml_sem I (Exists x (Equals (Var x) (Const f) && \<phi>))"
  by simp*)

lemma assigneq_valid: "valid assigneq_axiom"
  unfolding assigneq_axiom_def by (auto simp add: valid_equiv)

(*lemma game_sem_stutter: "game_sem I (Assign x (Var x)) X = X"
  by (auto simp add: repv_self)*)

lemma stutterd_valid: "valid stutterd_axiom"
  unfolding stutterd_axiom_def by (auto simp add: valid_equiv)

lemma test_valid: "valid test_axiom"
  unfolding test_axiom_def Or_def using valid_equiv by fastforce

lemma choice_valid: "valid choice_axiom"
  unfolding choice_axiom_def Or_def by (auto simp add: valid_equiv)

lemma compose_valid: "valid compose_axiom"
  unfolding compose_axiom_def Or_def by (simp add: valid_equiv)

lemma dual_valid: "valid dual_axiom"
unfolding dual_axiom_def using valid_equiv fml_sem_not using fml_sem.simps(6) game_sem.simps(7) by presburger

lemma iterate_valid: "valid iterate_axiom"
(*unfolding iterate_axiom_def using valid_equiv fml_sem.simps(6) game_equiv_subst[OF loop_iterate_equiv]*)
proof-
  have "\<forall>I. fml_sem I (Diamond (Loop (Game hgid1)) pusall) = fml_sem I (pusall || Diamond (Game hgid1) (Diamond (Loop (Game hgid1)) pusall))"
  proof
  fix I
    have "fml_sem I (Diamond (Loop (Game hgid1)) pusall) = game_sem I (Loop (Game hgid1)) (fml_sem I pusall)" by (rule fml_sem.simps(6))
    also have "... = game_sem I (Choice Skip (Compose (Game hgid1) (Loop (Game hgid1)))) (fml_sem I pusall)"
    using game_equiv_subst[where I=I and X=\<open>fml_sem I pusall\<close>, OF loop_iterate_equiv[where \<alpha>=\<open>Game hgid1\<close>]] by blast
    also have "... = fml_sem I (Diamond (Choice Skip (Compose (Game hgid1) (Loop (Game hgid1)))) pusall)" by simp
    also have "... = fml_sem I (Diamond Skip pusall || Diamond (Compose (Game hgid1) (Loop (Game hgid1))) pusall)" by simp
    also have "... = fml_sem I (pusall || Diamond (Compose (Game hgid1) (Loop (Game hgid1))) pusall)" by simp
    also have "... = fml_sem I (pusall || Diamond (Game hgid1) (Diamond (Loop (Game hgid1)) pusall))" by simp
    finally show "fml_sem I (Diamond (Loop (Game hgid1)) pusall) = fml_sem I (pusall || Diamond (Game hgid1) (Diamond (Loop (Game hgid1)) pusall))" .
  qed
  then have "valid ((Diamond (Loop (Game hgid1)) pusall) \<leftrightarrow> (pusall || Diamond (Game hgid1) (Diamond (Loop (Game hgid1)) pusall)))" using valid_equiv by (rule rev_iffD2)
  then show "valid iterate_axiom" unfolding iterate_axiom_def by auto
qed

subsection \<open>Local Soundness Proofs for Axiomatic Rules\<close>

lemma mon_locsound: "locally_sound mon_rule"
  unfolding mon_rule_def locally_sound_def using valid_in_impl monotone by simp

lemma FP_locsound: "locally_sound FP_rule"
  unfolding FP_rule_def locally_sound_def using valid_in_impl game_sem_loop by auto

lemma MP_locsound: "locally_sound MP_rule"
  unfolding MP_rule_def locally_sound_def valid_in_def using fml_sem_implies less_Suc_eq by auto

lemma gena_locsound: "locally_sound gena_rule"
  unfolding gena_rule_def locally_sound_def valid_in_def using fml_sem_implies less_Suc_eq by auto

end

repo: PSL


text:
(* Author: Various *)

section \<open>Combination and Cancellation Simprocs for Numeral Expressions\<close>

theory Numeral_Simprocs
imports Divides
begin

ML_file \<open>~~/src/Provers/Arith/assoc_fold.ML\<close>
ML_file \<open>~~/src/Provers/Arith/cancel_numerals.ML\<close>
ML_file \<open>~~/src/Provers/Arith/combine_numerals.ML\<close>
ML_file \<open>~~/src/Provers/Arith/cancel_numeral_factor.ML\<close>
ML_file \<open>~~/src/Provers/Arith/extract_common_term.ML\<close>

lemmas semiring_norm =
  Let_def arith_simps diff_nat_numeral rel_simps
  if_False if_True
  add_0 add_Suc add_numeral_left
  add_neg_numeral_left mult_numeral_left
  numeral_One [symmetric] uminus_numeral_One [symmetric] Suc_eq_plus1
  eq_numeral_iff_iszero not_iszero_Numeral1

declare split_div [of _ _ "numeral k", arith_split] for k
declare split_mod [of _ _ "numeral k", arith_split] for k

text \<open>For \<open>combine_numerals\<close>\<close>

lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
by (simp add: add_mult_distrib)

text \<open>For \<open>cancel_numerals\<close>\<close>

lemma nat_diff_add_eq1:
     "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
by (simp split: nat_diff_split add: add_mult_distrib)

lemma nat_diff_add_eq2:
     "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
by (simp split: nat_diff_split add: add_mult_distrib)

lemma nat_eq_add_iff1:
     "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
by (auto split: nat_diff_split simp add: add_mult_distrib)

lemma nat_eq_add_iff2:
     "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
by (auto split: nat_diff_split simp add: add_mult_distrib)

lemma nat_less_add_iff1:
     "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
by (auto split: nat_diff_split simp add: add_mult_distrib)

lemma nat_less_add_iff2:
     "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
by (auto split: nat_diff_split simp add: add_mult_distrib)

lemma nat_le_add_iff1:
     "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
by (auto split: nat_diff_split simp add: add_mult_distrib)

lemma nat_le_add_iff2:
     "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
by (auto split: nat_diff_split simp add: add_mult_distrib)

text \<open>For \<open>cancel_numeral_factors\<close>\<close>

lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
by auto

lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
by auto

lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
by auto

lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
by auto

lemma nat_mult_dvd_cancel_disj[simp]:
  "(k*m) dvd (k*n) = (k=0 \<or> m dvd (n::nat))"
by (auto simp: dvd_eq_mod_eq_0 mod_mult_mult1)

lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
by(auto)

text \<open>For \<open>cancel_factor\<close>\<close>

lemmas nat_mult_le_cancel_disj = mult_le_cancel1

lemmas nat_mult_less_cancel_disj = mult_less_cancel1

lemma nat_mult_eq_cancel_disj:
  fixes k m n :: nat
  shows "k * m = k * n \<longleftrightarrow> k = 0 \<or> m = n"
  by auto

lemma nat_mult_div_cancel_disj [simp]:
  fixes k m n :: nat
  shows "(k * m) div (k * n) = (if k = 0 then 0 else m div n)"
  by (fact div_mult_mult1_if)

lemma numeral_times_minus_swap:
  fixes x:: "'a::comm_ring_1" shows  "numeral w * -x = x * - numeral w"
  by (simp add: mult.commute)

ML_file \<open>Tools/numeral_simprocs.ML\<close>

simproc_setup semiring_assoc_fold
  ("(a::'a::comm_semiring_1_cancel) * b") =
  \<open>fn phi => Numeral_Simprocs.assoc_fold\<close>

(* TODO: see whether the type class can be generalized further *)
simproc_setup int_combine_numerals
  ("(i::'a::comm_ring_1) + j" | "(i::'a::comm_ring_1) - j") =
  \<open>fn phi => Numeral_Simprocs.combine_numerals\<close>

simproc_setup field_combine_numerals
  ("(i::'a::{field,ring_char_0}) + j"
  |"(i::'a::{field,ring_char_0}) - j") =
  \<open>fn phi => Numeral_Simprocs.field_combine_numerals\<close>

simproc_setup inteq_cancel_numerals
  ("(l::'a::comm_ring_1) + m = n"
  |"(l::'a::comm_ring_1) = m + n"
  |"(l::'a::comm_ring_1) - m = n"
  |"(l::'a::comm_ring_1) = m - n"
  |"(l::'a::comm_ring_1) * m = n"
  |"(l::'a::comm_ring_1) = m * n"
  |"- (l::'a::comm_ring_1) = m"
  |"(l::'a::comm_ring_1) = - m") =
  \<open>fn phi => Numeral_Simprocs.eq_cancel_numerals\<close>

simproc_setup intless_cancel_numerals
  ("(l::'a::linordered_idom) + m < n"
  |"(l::'a::linordered_idom) < m + n"
  |"(l::'a::linordered_idom) - m < n"
  |"(l::'a::linordered_idom) < m - n"
  |"(l::'a::linordered_idom) * m < n"
  |"(l::'a::linordered_idom) < m * n"
  |"- (l::'a::linordered_idom) < m"
  |"(l::'a::linordered_idom) < - m") =
  \<open>fn phi => Numeral_Simprocs.less_cancel_numerals\<close>

simproc_setup intle_cancel_numerals
  ("(l::'a::linordered_idom) + m \<le> n"
  |"(l::'a::linordered_idom) \<le> m + n"
  |"(l::'a::linordered_idom) - m \<le> n"
  |"(l::'a::linordered_idom) \<le> m - n"
  |"(l::'a::linordered_idom) * m \<le> n"
  |"(l::'a::linordered_idom) \<le> m * n"
  |"- (l::'a::linordered_idom) \<le> m"
  |"(l::'a::linordered_idom) \<le> - m") =
  \<open>fn phi => Numeral_Simprocs.le_cancel_numerals\<close>

simproc_setup ring_eq_cancel_numeral_factor
  ("(l::'a::{idom,ring_char_0}) * m = n"
  |"(l::'a::{idom,ring_char_0}) = m * n") =
  \<open>fn phi => Numeral_Simprocs.eq_cancel_numeral_factor\<close>

simproc_setup ring_less_cancel_numeral_factor
  ("(l::'a::linordered_idom) * m < n"
  |"(l::'a::linordered_idom) < m * n") =
  \<open>fn phi => Numeral_Simprocs.less_cancel_numeral_factor\<close>

simproc_setup ring_le_cancel_numeral_factor
  ("(l::'a::linordered_idom) * m <= n"
  |"(l::'a::linordered_idom) <= m * n") =
  \<open>fn phi => Numeral_Simprocs.le_cancel_numeral_factor\<close>

(* TODO: remove comm_ring_1 constraint if possible *)
simproc_setup int_div_cancel_numeral_factors
  ("((l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) * m) div n"
  |"(l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) div (m * n)") =
  \<open>fn phi => Numeral_Simprocs.div_cancel_numeral_factor\<close>

simproc_setup divide_cancel_numeral_factor
  ("((l::'a::{field,ring_char_0}) * m) / n"
  |"(l::'a::{field,ring_char_0}) / (m * n)"
  |"((numeral v)::'a::{field,ring_char_0}) / (numeral w)") =
  \<open>fn phi => Numeral_Simprocs.divide_cancel_numeral_factor\<close>

simproc_setup ring_eq_cancel_factor
  ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") =
  \<open>fn phi => Numeral_Simprocs.eq_cancel_factor\<close>

simproc_setup linordered_ring_le_cancel_factor
  ("(l::'a::linordered_idom) * m <= n"
  |"(l::'a::linordered_idom) <= m * n") =
  \<open>fn phi => Numeral_Simprocs.le_cancel_factor\<close>

simproc_setup linordered_ring_less_cancel_factor
  ("(l::'a::linordered_idom) * m < n"
  |"(l::'a::linordered_idom) < m * n") =
  \<open>fn phi => Numeral_Simprocs.less_cancel_factor\<close>

simproc_setup int_div_cancel_factor
  ("((l::'a::euclidean_semiring_cancel) * m) div n"
  |"(l::'a::euclidean_semiring_cancel) div (m * n)") =
  \<open>fn phi => Numeral_Simprocs.div_cancel_factor\<close>

simproc_setup int_mod_cancel_factor
  ("((l::'a::euclidean_semiring_cancel) * m) mod n"
  |"(l::'a::euclidean_semiring_cancel) mod (m * n)") =
  \<open>fn phi => Numeral_Simprocs.mod_cancel_factor\<close>

simproc_setup dvd_cancel_factor
  ("((l::'a::idom) * m) dvd n"
  |"(l::'a::idom) dvd (m * n)") =
  \<open>fn phi => Numeral_Simprocs.dvd_cancel_factor\<close>

simproc_setup divide_cancel_factor
  ("((l::'a::field) * m) / n"
  |"(l::'a::field) / (m * n)") =
  \<open>fn phi => Numeral_Simprocs.divide_cancel_factor\<close>

ML_file \<open>Tools/nat_numeral_simprocs.ML\<close>

simproc_setup nat_combine_numerals
  ("(i::nat) + j" | "Suc (i + j)") =
  \<open>fn phi => Nat_Numeral_Simprocs.combine_numerals\<close>

simproc_setup nateq_cancel_numerals
  ("(l::nat) + m = n" | "(l::nat) = m + n" |
   "(l::nat) * m = n" | "(l::nat) = m * n" |
   "Suc m = n" | "m = Suc n") =
  \<open>fn phi => Nat_Numeral_Simprocs.eq_cancel_numerals\<close>

simproc_setup natless_cancel_numerals
  ("(l::nat) + m < n" | "(l::nat) < m + n" |
   "(l::nat) * m < n" | "(l::nat) < m * n" |
   "Suc m < n" | "m < Suc n") =
  \<open>fn phi => Nat_Numeral_Simprocs.less_cancel_numerals\<close>

simproc_setup natle_cancel_numerals
  ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" |
   "(l::nat) * m \<le> n" | "(l::nat) \<le> m * n" |
   "Suc m \<le> n" | "m \<le> Suc n") =
  \<open>fn phi => Nat_Numeral_Simprocs.le_cancel_numerals\<close>

simproc_setup natdiff_cancel_numerals
  ("((l::nat) + m) - n" | "(l::nat) - (m + n)" |
   "(l::nat) * m - n" | "(l::nat) - m * n" |
   "Suc m - n" | "m - Suc n") =
  \<open>fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals\<close>

simproc_setup nat_eq_cancel_numeral_factor
  ("(l::nat) * m = n" | "(l::nat) = m * n") =
  \<open>fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor\<close>

simproc_setup nat_less_cancel_numeral_factor
  ("(l::nat) * m < n" | "(l::nat) < m * n") =
  \<open>fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor\<close>

simproc_setup nat_le_cancel_numeral_factor
  ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
  \<open>fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor\<close>

simproc_setup nat_div_cancel_numeral_factor
  ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
  \<open>fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor\<close>

simproc_setup nat_dvd_cancel_numeral_factor
  ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
  \<open>fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor\<close>

simproc_setup nat_eq_cancel_factor
  ("(l::nat) * m = n" | "(l::nat) = m * n") =
  \<open>fn phi => Nat_Numeral_Simprocs.eq_cancel_factor\<close>

simproc_setup nat_less_cancel_factor
  ("(l::nat) * m < n" | "(l::nat) < m * n") =
  \<open>fn phi => Nat_Numeral_Simprocs.less_cancel_factor\<close>

simproc_setup nat_le_cancel_factor
  ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
  \<open>fn phi => Nat_Numeral_Simprocs.le_cancel_factor\<close>

simproc_setup nat_div_cancel_factor
  ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
  \<open>fn phi => Nat_Numeral_Simprocs.div_cancel_factor\<close>

simproc_setup nat_dvd_cancel_factor
  ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
  \<open>fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor\<close>

declaration \<open>
  K (Lin_Arith.add_simprocs
      [\<^simproc>\<open>semiring_assoc_fold\<close>,
       \<^simproc>\<open>int_combine_numerals\<close>,
       \<^simproc>\<open>inteq_cancel_numerals\<close>,
       \<^simproc>\<open>intless_cancel_numerals\<close>,
       \<^simproc>\<open>intle_cancel_numerals\<close>,
       \<^simproc>\<open>field_combine_numerals\<close>,
       \<^simproc>\<open>nat_combine_numerals\<close>,
       \<^simproc>\<open>nateq_cancel_numerals\<close>,
       \<^simproc>\<open>natless_cancel_numerals\<close>,
       \<^simproc>\<open>natle_cancel_numerals\<close>,
       \<^simproc>\<open>natdiff_cancel_numerals\<close>,
       Numeral_Simprocs.field_divide_cancel_numeral_factor])
\<close>

end

author: landonf

repo: isabelle-legacy