text:
(*  Title:      HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
    Author:     Olaf Müller
*)

section {* Compositionality on Trace level *}

theory CompoTraces
imports CompoScheds ShortExecutions
begin

consts

 mksch      ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq"
 par_traces ::"['a trace_module,'a trace_module] => 'a trace_module"

defs

mksch_def:
  "mksch A B == (fix$(LAM h tr schA schB. case tr of
       nil => nil
    | x##xs =>
      (case x of
        UU => UU
      | Def y =>
         (if y:act A then
             (if y:act B then
                   ((Takewhile (%a. a:int A)$schA)
                      @@ (Takewhile (%a. a:int B)$schB)
                           @@ (y>>(h$xs
                                    $(TL$(Dropwhile (%a. a:int A)$schA))
                                    $(TL$(Dropwhile (%a. a:int B)$schB))
                    )))
              else
                 ((Takewhile (%a. a:int A)$schA)
                  @@ (y>>(h$xs
                           $(TL$(Dropwhile (%a. a:int A)$schA))
                           $schB)))
              )
          else
             (if y:act B then
                 ((Takewhile (%a. a:int B)$schB)
                     @@ (y>>(h$xs
                              $schA
                              $(TL$(Dropwhile (%a. a:int B)$schB))
                              )))
             else
               UU
             )
         )
       )))"

par_traces_def:
  "par_traces TracesA TracesB ==
       let trA = fst TracesA; sigA = snd TracesA;
           trB = fst TracesB; sigB = snd TracesB
       in
       (    {tr. Filter (%a. a:actions sigA)$tr : trA}
        Int {tr. Filter (%a. a:actions sigB)$tr : trB}
        Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
        asig_comp sigA sigB)"

axiomatization where

finiteR_mksch:
  "Finite (mksch A B$tr$x$y) \<Longrightarrow> Finite tr"

lemma finiteR_mksch': "\<not> Finite tr \<Longrightarrow> \<not> Finite (mksch A B$tr$x$y)"
  by (blast intro: finiteR_mksch)

declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (K NONE))) *}

subsection "mksch rewrite rules"

lemma mksch_unfold:
"mksch A B = (LAM tr schA schB. case tr of
       nil => nil
    | x##xs =>
      (case x of
        UU => UU
      | Def y =>
         (if y:act A then
             (if y:act B then
                   ((Takewhile (%a. a:int A)$schA)
                         @@(Takewhile (%a. a:int B)$schB)
                              @@(y>>(mksch A B$xs
                                       $(TL$(Dropwhile (%a. a:int A)$schA))
                                       $(TL$(Dropwhile (%a. a:int B)$schB))
                    )))
              else
                 ((Takewhile (%a. a:int A)$schA)
                      @@ (y>>(mksch A B$xs
                              $(TL$(Dropwhile (%a. a:int A)$schA))
                              $schB)))
              )
          else
             (if y:act B then
                 ((Takewhile (%a. a:int B)$schB)
                       @@ (y>>(mksch A B$xs
                              $schA
                              $(TL$(Dropwhile (%a. a:int B)$schB))
                              )))
             else
               UU
             )
         )
       ))"
apply (rule trans)
apply (rule fix_eq2)
apply (rule mksch_def)
apply (rule beta_cfun)
apply simp
done

lemma mksch_UU: "mksch A B$UU$schA$schB = UU"
apply (subst mksch_unfold)
apply simp
done

lemma mksch_nil: "mksch A B$nil$schA$schB = nil"
apply (subst mksch_unfold)
apply simp
done

lemma mksch_cons1: "[|x:act A;x~:act B|]
    ==> mksch A B$(x>>tr)$schA$schB =
          (Takewhile (%a. a:int A)$schA)
          @@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))
                              $schB))"
apply (rule trans)
apply (subst mksch_unfold)
apply (simp add: Consq_def If_and_if)
apply (simp add: Consq_def)
done

lemma mksch_cons2: "[|x~:act A;x:act B|]
    ==> mksch A B$(x>>tr)$schA$schB =
         (Takewhile (%a. a:int B)$schB)
          @@ (x>>(mksch A B$tr$schA$(TL$(Dropwhile (%a. a:int B)$schB))
                             ))"
apply (rule trans)
apply (subst mksch_unfold)
apply (simp add: Consq_def If_and_if)
apply (simp add: Consq_def)
done

lemma mksch_cons3: "[|x:act A;x:act B|]
    ==> mksch A B$(x>>tr)$schA$schB =
             (Takewhile (%a. a:int A)$schA)
          @@ ((Takewhile (%a. a:int B)$schB)
          @@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))
                             $(TL$(Dropwhile (%a. a:int B)$schB))))
              )"
apply (rule trans)
apply (subst mksch_unfold)
apply (simp add: Consq_def If_and_if)
apply (simp add: Consq_def)
done

lemmas compotr_simps = mksch_UU mksch_nil mksch_cons1 mksch_cons2 mksch_cons3

declare compotr_simps [simp]

subsection {* COMPOSITIONALITY on TRACE Level *}

subsubsection "Lemmata for ==>"

(* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of
   the compatibility of IOA, in particular out of the condition that internals are
   really hidden. *)

lemma compatibility_consequence1: "(eB & ~eA --> ~A) -->
          (A & (eA | eB)) = (eA & A)"
apply fast
done

(* very similar to above, only the commutativity of | is used to make a slight change *)

lemma compatibility_consequence2: "(eB & ~eA --> ~A) -->
          (A & (eB | eA)) = (eA & A)"
apply fast
done

subsubsection "Lemmata for <=="

(* Lemma for substitution of looping assumption in another specific assumption *)
lemma subst_lemma1: "[| f << (g x) ; x=(h x) |] ==> f << g (h x)"
by (erule subst)

(* Lemma for substitution of looping assumption in another specific assumption *)
lemma subst_lemma2: "[| (f x) = y >> g; x=(h x) |] ==> (f (h x)) = y >> g"
by (erule subst)

lemma ForallAorB_mksch [rule_format]:
  "!!A B. compatible A B ==>
    ! schA schB. Forall (%x. x:act (A||B)) tr
    --> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)"
apply (tactic {* Seq_induct_tac @{context} "tr"
  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
apply auto
apply (simp add: actions_of_par)
apply (case_tac "a:act A")
apply (case_tac "a:act B")
(* a:A, a:B *)
apply simp
apply (rule Forall_Conc_impl [THEN mp])
apply (simp add: intA_is_not_actB int_is_act)
apply (rule Forall_Conc_impl [THEN mp])
apply (simp add: intA_is_not_actB int_is_act)
(* a:A,a~:B *)
apply simp
apply (rule Forall_Conc_impl [THEN mp])
apply (simp add: intA_is_not_actB int_is_act)
apply (case_tac "a:act B")
(* a~:A, a:B *)
apply simp
apply (rule Forall_Conc_impl [THEN mp])
apply (simp add: intA_is_not_actB int_is_act)
(* a~:A,a~:B *)
apply auto
done

lemma ForallBnAmksch [rule_format (no_asm)]: "!!A B. compatible B A  ==>
    ! schA schB.  (Forall (%x. x:act B & x~:act A) tr
    --> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))"
apply (tactic {* Seq_induct_tac @{context} "tr"
  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
apply auto
apply (rule Forall_Conc_impl [THEN mp])
apply (simp add: intA_is_not_actB int_is_act)
done

lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==>
    ! schA schB.  (Forall (%x. x:act A & x~:act B) tr
    --> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))"
apply (tactic {* Seq_induct_tac @{context} "tr"
  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
apply auto
apply (rule Forall_Conc_impl [THEN mp])
apply (simp add: intA_is_not_actB int_is_act)
done

(* safe-tac makes too many case distinctions with this lemma in the next proof *)
declare FiniteConc [simp del]

lemma FiniteL_mksch [rule_format (no_asm)]: "[| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==>
    ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y &
           Filter (%a. a:ext A)$x = Filter (%a. a:act A)$tr &
           Filter (%a. a:ext B)$y = Filter (%a. a:act B)$tr &
           Forall (%x. x:ext (A||B)) tr
           --> Finite (mksch A B$tr$x$y)"

apply (erule Seq_Finite_ind)
apply simp
(* main case *)
apply simp
apply auto

(* a: act A; a: act B *)
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
back
apply (erule conjE)+
(* Finite (tw iA x) and Finite (tw iB y) *)
apply (simp add: not_ext_is_int_or_not_act FiniteConc)
(* now for conclusion IH applicable, but assumptions have to be transformed *)
apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $s" in subst_lemma2)
apply assumption
apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $s" in subst_lemma2)
apply assumption
(* IH *)
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)

(* a: act B; a~: act A *)
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])

apply (erule conjE)+
(* Finite (tw iB y) *)
apply (simp add: not_ext_is_int_or_not_act FiniteConc)
(* now for conclusion IH applicable, but assumptions have to be transformed *)
apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $s" in subst_lemma2)
apply assumption
(* IH *)
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)

(* a~: act B; a: act A *)
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])

apply (erule conjE)+
(* Finite (tw iA x) *)
apply (simp add: not_ext_is_int_or_not_act FiniteConc)
(* now for conclusion IH applicable, but assumptions have to be transformed *)
apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $s" in subst_lemma2)
apply assumption
(* IH *)
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)

(* a~: act B; a~: act A *)
apply (fastforce intro!: ext_is_act simp: externals_of_par)
done

declare FiniteConc [simp]

declare FilterConc [simp del]

lemma reduceA_mksch1 [rule_format (no_asm)]: " [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>
 ! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &
     Filter (%a. a:ext B)$y = Filter (%a. a:act B)$(bs @@ z)
     --> (? y1 y2.  (mksch A B$(bs @@ z)$x$y) = (y1 @@ (mksch A B$z$x$y2)) &
                    Forall (%x. x:act B & x~:act A) y1 &
                    Finite y1 & y = (y1 @@ y2) &
                    Filter (%a. a:ext B)$y1 = bs)"
apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
apply (erule Seq_Finite_ind)
apply (rule allI)+
apply (rule impI)
apply (rule_tac x = "nil" in exI)
apply (rule_tac x = "y" in exI)
apply simp
(* main case *)
apply (rule allI)+
apply (rule impI)
apply simp
apply (erule conjE)+
apply simp
(* divide_Seq on s *)
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
apply (erule conjE)+
(* transform assumption f eB y = f B (s@z) *)
apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $ (s@@z) " in subst_lemma2)
apply assumption
apply (simp add: not_ext_is_int_or_not_act FilterConc)
(* apply IH *)
apply (erule_tac x = "TL$ (Dropwhile (%a. a:int B) $y) " in allE)
apply (simp add: ForallTL ForallDropwhile FilterConc)
apply (erule exE)+
apply (erule conjE)+
apply (simp add: FilterConc)
(* for replacing IH in conclusion *)
apply (rotate_tac -2)
(* instantiate y1a and y2a *)
apply (rule_tac x = "Takewhile (%a. a:int B) $y @@ a>>y1" in exI)
apply (rule_tac x = "y2" in exI)
(* elminate all obligations up to two depending on Conc_assoc *)
apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
apply (simp (no_asm) add: Conc_assoc FilterConc)
done

lemmas reduceA_mksch = conjI [THEN [6] conjI [THEN [5] reduceA_mksch1]]

lemma reduceB_mksch1 [rule_format]:
" [| Finite a_s; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>
 ! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) a_s &
     Filter (%a. a:ext A)$x = Filter (%a. a:act A)$(a_s @@ z)
     --> (? x1 x2.  (mksch A B$(a_s @@ z)$x$y) = (x1 @@ (mksch A B$z$x2$y)) &
                    Forall (%x. x:act A & x~:act B) x1 &
                    Finite x1 & x = (x1 @@ x2) &
                    Filter (%a. a:ext A)$x1 = a_s)"
apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
apply (erule Seq_Finite_ind)
apply (rule allI)+
apply (rule impI)
apply (rule_tac x = "nil" in exI)
apply (rule_tac x = "x" in exI)
apply simp
(* main case *)
apply (rule allI)+
apply (rule impI)
apply simp
apply (erule conjE)+
apply simp
(* divide_Seq on s *)
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
apply (erule conjE)+
(* transform assumption f eA x = f A (s@z) *)
apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $ (s@@z) " in subst_lemma2)
apply assumption
apply (simp add: not_ext_is_int_or_not_act FilterConc)
(* apply IH *)
apply (erule_tac x = "TL$ (Dropwhile (%a. a:int A) $x) " in allE)
apply (simp add: ForallTL ForallDropwhile FilterConc)
apply (erule exE)+
apply (erule conjE)+
apply (simp add: FilterConc)
(* for replacing IH in conclusion *)
apply (rotate_tac -2)
(* instantiate y1a and y2a *)
apply (rule_tac x = "Takewhile (%a. a:int A) $x @@ a>>x1" in exI)
apply (rule_tac x = "x2" in exI)
(* elminate all obligations up to two depending on Conc_assoc *)
apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
apply (simp (no_asm) add: Conc_assoc FilterConc)
done

lemmas reduceB_mksch = conjI [THEN [6] conjI [THEN [5] reduceB_mksch1]]

declare FilterConc [simp]

subsection "Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr"

lemma FilterA_mksch_is_tr:
"!! A B. [| compatible A B; compatible B A;
            is_asig(asig_of A); is_asig(asig_of B) |] ==>
  ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &
  Forall (%x. x:ext (A||B)) tr &
  Filter (%a. a:act A)$tr << Filter (%a. a:ext A)$schA &
  Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB
  --> Filter (%a. a:ext (A||B))$(mksch A B$tr$schA$schB) = tr"

apply (tactic {* Seq_induct_tac @{context} "tr"
  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
(* main case *)
(* splitting into 4 cases according to a:A, a:B *)
apply auto

(* Case a:A, a:B *)
apply (frule divide_Seq)
apply (frule divide_Seq)
back
apply (erule conjE)+
(* filtering internals of A in schA and of B in schB is nil *)
apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
(* conclusion of IH ok, but assumptions of IH have to be transformed *)
apply (drule_tac x = "schA" in subst_lemma1)
apply assumption
apply (drule_tac x = "schB" in subst_lemma1)
apply assumption
(* IH *)
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)

(* Case a:A, a~:B *)
apply (frule divide_Seq)
apply (erule conjE)+
(* filtering internals of A is nil *)
apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
apply (drule_tac x = "schA" in subst_lemma1)
apply assumption
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)

(* Case a:B, a~:A *)
apply (frule divide_Seq)
apply (erule conjE)+
(* filtering internals of A is nil *)
apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
apply (drule_tac x = "schB" in subst_lemma1)
back
apply assumption
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)

(* Case a~:A, a~:B *)
apply (fastforce intro!: ext_is_act simp: externals_of_par)
done

subsection" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof"

lemma FilterAmksch_is_schA: "!! A B. [| compatible A B; compatible B A;
  is_asig(asig_of A); is_asig(asig_of B) |] ==>
  Forall (%x. x:ext (A||B)) tr &
  Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &
  Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &
  Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &
  LastActExtsch A schA & LastActExtsch B schB
  --> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA"
apply (intro strip)
apply (rule seq.take_lemma)
apply (rule mp)
prefer 2 apply assumption
back back back back
apply (rule_tac x = "schA" in spec)
apply (rule_tac x = "schB" in spec)
apply (rule_tac x = "tr" in spec)
apply (tactic "thin_tac' 5 1")
apply (rule nat_less_induct)
apply (rule allI)+
apply (rename_tac tr schB schA)
apply (intro strip)
apply (erule conjE)+

apply (case_tac "Forall (%x. x:act B & x~:act A) tr")

apply (rule seq_take_lemma [THEN iffD2, THEN spec])
apply (tactic "thin_tac' 5 1")

apply (case_tac "Finite tr")

(* both sides of this equation are nil *)
apply (subgoal_tac "schA=nil")
apply (simp (no_asm_simp))
(* first side: mksch = nil *)
apply (auto intro!: ForallQFilterPnil ForallBnAmksch FiniteL_mksch)[1]
(* second side: schA = nil *)
apply (erule_tac A = "A" in LastActExtimplnil)
apply (simp (no_asm_simp))
apply (erule_tac Q = "%x. x:act B & x~:act A" in ForallQFilterPnil)
apply assumption
apply fast

(* case ~ Finite s *)

(* both sides of this equation are UU *)
apply (subgoal_tac "schA=UU")
apply (simp (no_asm_simp))
(* first side: mksch = UU *)
apply (auto intro!: ForallQFilterPUU finiteR_mksch' ForallBnAmksch)[1]
(* schA = UU *)
apply (erule_tac A = "A" in LastActExtimplUU)
apply (simp (no_asm_simp))
apply (erule_tac Q = "%x. x:act B & x~:act A" in ForallQFilterPUU)
apply assumption
apply fast

(* case" ~ Forall (%x.x:act B & x~:act A) s" *)

apply (drule divide_Seq3)

apply (erule exE)+
apply (erule conjE)+
apply hypsubst

(* bring in lemma reduceA_mksch *)
apply (frule_tac x = "schA" and y = "schB" and A = "A" and B = "B" in reduceA_mksch)
apply assumption+
apply (erule exE)+
apply (erule conjE)+

(* use reduceA_mksch to rewrite conclusion *)
apply hypsubst
apply simp

(* eliminate the B-only prefix *)

apply (subgoal_tac " (Filter (%a. a :act A) $y1) = nil")
apply (erule_tac [2] ForallQFilterPnil)
prefer 2 apply assumption
prefer 2 apply fast

(* Now real recursive step follows (in y) *)

apply simp
apply (case_tac "x:act A")
apply (case_tac "x~:act B")
apply (rotate_tac -2)
apply simp

apply (subgoal_tac "Filter (%a. a:act A & a:ext B) $y1=nil")
apply (rotate_tac -1)
apply simp
(* eliminate introduced subgoal 2 *)
apply (erule_tac [2] ForallQFilterPnil)
prefer 2 apply assumption
prefer 2 apply fast

(* bring in divide Seq for s *)
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
apply (erule conjE)+

(* subst divide_Seq in conclusion, but only at the righest occurrence *)
apply (rule_tac t = "schA" in ssubst)
back
back
back
apply assumption

(* reduce trace_takes from n to strictly smaller k *)
apply (rule take_reduction)

(* f A (tw iA) = tw ~eA *)
apply (simp add: int_is_act not_ext_is_int_or_not_act)
apply (rule refl)
apply (simp add: int_is_act not_ext_is_int_or_not_act)
apply (rotate_tac -11)

(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)

(* assumption Forall tr *)
(* assumption schB *)
apply (simp add: ext_and_act)
(* assumption schA *)
apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
apply assumption
apply (simp add: int_is_not_ext)
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
apply (drule_tac sch = "schA" and P = "%a. a:int A" in LastActExtsmall1)
apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
apply assumption

(* assumption Forall schA *)
apply (drule_tac s = "schA" and P = "Forall (%x. x:act A) " in subst)
apply assumption
apply (simp add: int_is_act)

(* case x:actions(asig_of A) & x: actions(asig_of B) *)

apply (rotate_tac -2)
apply simp

apply (subgoal_tac "Filter (%a. a:act A & a:ext B) $y1=nil")
apply (rotate_tac -1)
apply simp
(* eliminate introduced subgoal 2 *)
apply (erule_tac [2] ForallQFilterPnil)
prefer 2 apply (assumption)
prefer 2 apply (fast)

(* bring in divide Seq for s *)
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
apply (erule conjE)+

(* subst divide_Seq in conclusion, but only at the rightmost occurrence *)
apply (rule_tac t = "schA" in ssubst)
back
back
back
apply assumption

(* f A (tw iA) = tw ~eA *)
apply (simp add: int_is_act not_ext_is_int_or_not_act)

(* rewrite assumption forall and schB *)
apply (rotate_tac 13)
apply (simp add: ext_and_act)

(* divide_Seq for schB2 *)
apply (frule_tac y = "y2" in sym [THEN eq_imp_below, THEN divide_Seq])
apply (erule conjE)+
(* assumption schA *)
apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
apply assumption
apply (simp add: int_is_not_ext)

(* f A (tw iB schB2) = nil *)
apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)

(* reduce trace_takes from n to strictly smaller k *)
apply (rule take_reduction)
apply (rule refl)
apply (rule refl)

(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)

(* assumption schB *)
apply (drule_tac x = "y2" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
apply assumption
apply (simp add: intA_is_not_actB int_is_not_ext)

(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
apply (drule_tac sch = "schA" and P = "%a. a:int A" in LastActExtsmall1)
apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
apply assumption
apply (drule_tac sch = "y2" and P = "%a. a:int B" in LastActExtsmall1)

(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
apply (simp add: ForallTL ForallDropwhile)

(* case x~:A & x:B  *)
(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
apply (case_tac "x:act B")
apply fast

(* case x~:A & x~:B  *)
(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
apply (rotate_tac -9)
(* reduce forall assumption from tr to (x>>rs) *)
apply (simp add: externals_of_par)
apply (fast intro!: ext_is_act)

done

subsection" Filter of mksch(tr,schA,schB) to B is schB -- take lemma proof"

lemma FilterBmksch_is_schB: "!! A B. [| compatible A B; compatible B A;
  is_asig(asig_of A); is_asig(asig_of B) |] ==>
  Forall (%x. x:ext (A||B)) tr &
  Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &
  Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &
  Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &
  LastActExtsch A schA & LastActExtsch B schB
  --> Filter (%a. a:act B)$(mksch A B$tr$schA$schB) = schB"
apply (intro strip)
apply (rule seq.take_lemma)
apply (rule mp)
prefer 2 apply assumption
back back back back
apply (rule_tac x = "schA" in spec)
apply (rule_tac x = "schB" in spec)
apply (rule_tac x = "tr" in spec)
apply (tactic "thin_tac' 5 1")
apply (rule nat_less_induct)
apply (rule allI)+
apply (rename_tac tr schB schA)
apply (intro strip)
apply (erule conjE)+

apply (case_tac "Forall (%x. x:act A & x~:act B) tr")

apply (rule seq_take_lemma [THEN iffD2, THEN spec])
apply (tactic "thin_tac' 5 1")

apply (case_tac "Finite tr")

(* both sides of this equation are nil *)
apply (subgoal_tac "schB=nil")
apply (simp (no_asm_simp))
(* first side: mksch = nil *)
apply (auto intro!: ForallQFilterPnil ForallAnBmksch FiniteL_mksch)[1]
(* second side: schA = nil *)
apply (erule_tac A = "B" in LastActExtimplnil)
apply (simp (no_asm_simp))
apply (erule_tac Q = "%x. x:act A & x~:act B" in ForallQFilterPnil)
apply assumption
apply fast

(* case ~ Finite tr *)

(* both sides of this equation are UU *)
apply (subgoal_tac "schB=UU")
apply (simp (no_asm_simp))
(* first side: mksch = UU *)
apply (force intro!: ForallQFilterPUU finiteR_mksch' ForallAnBmksch)
(* schA = UU *)
apply (erule_tac A = "B" in LastActExtimplUU)
apply (simp (no_asm_simp))
apply (erule_tac Q = "%x. x:act A & x~:act B" in ForallQFilterPUU)
apply assumption
apply fast

(* case" ~ Forall (%x.x:act B & x~:act A) s" *)

apply (drule divide_Seq3)

apply (erule exE)+
apply (erule conjE)+
apply hypsubst

(* bring in lemma reduceB_mksch *)
apply (frule_tac y = "schB" and x = "schA" and A = "A" and B = "B" in reduceB_mksch)
apply assumption+
apply (erule exE)+
apply (erule conjE)+

(* use reduceB_mksch to rewrite conclusion *)
apply hypsubst
apply simp

(* eliminate the A-only prefix *)

apply (subgoal_tac "(Filter (%a. a :act B) $x1) = nil")
apply (erule_tac [2] ForallQFilterPnil)
prefer 2 apply (assumption)
prefer 2 apply (fast)

(* Now real recursive step follows (in x) *)

apply simp
apply (case_tac "x:act B")
apply (case_tac "x~:act A")
apply (rotate_tac -2)
apply simp

apply (subgoal_tac "Filter (%a. a:act B & a:ext A) $x1=nil")
apply (rotate_tac -1)
apply simp
(* eliminate introduced subgoal 2 *)
apply (erule_tac [2] ForallQFilterPnil)
prefer 2 apply (assumption)
prefer 2 apply (fast)

(* bring in divide Seq for s *)
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
apply (erule conjE)+

(* subst divide_Seq in conclusion, but only at the rightmost occurrence *)
apply (rule_tac t = "schB" in ssubst)
back
back
back
apply assumption

(* reduce trace_takes from n to strictly smaller k *)
apply (rule take_reduction)

(* f B (tw iB) = tw ~eB *)
apply (simp add: int_is_act not_ext_is_int_or_not_act)
apply (rule refl)
apply (simp add: int_is_act not_ext_is_int_or_not_act)
apply (rotate_tac -11)

(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)

(* assumption schA *)
apply (simp add: ext_and_act)
(* assumption schB *)
apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
apply assumption
apply (simp add: int_is_not_ext)
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
apply (drule_tac sch = "schB" and P = "%a. a:int B" in LastActExtsmall1)
apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
apply assumption

(* assumption Forall schB *)
apply (drule_tac s = "schB" and P = "Forall (%x. x:act B) " in subst)
apply assumption
apply (simp add: int_is_act)

(* case x:actions(asig_of A) & x: actions(asig_of B) *)

apply (rotate_tac -2)
apply simp

apply (subgoal_tac "Filter (%a. a:act B & a:ext A) $x1=nil")
apply (rotate_tac -1)
apply simp
(* eliminate introduced subgoal 2 *)
apply (erule_tac [2] ForallQFilterPnil)
prefer 2 apply (assumption)
prefer 2 apply (fast)

(* bring in divide Seq for s *)
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
apply (erule conjE)+

(* subst divide_Seq in conclusion, but only at the rightmost occurrence *)
apply (rule_tac t = "schB" in ssubst)
back
back
back
apply assumption

(* f B (tw iB) = tw ~eB *)
apply (simp add: int_is_act not_ext_is_int_or_not_act)

(* rewrite assumption forall and schB *)
apply (rotate_tac 13)
apply (simp add: ext_and_act)

(* divide_Seq for schB2 *)
apply (frule_tac y = "x2" in sym [THEN eq_imp_below, THEN divide_Seq])
apply (erule conjE)+
(* assumption schA *)
apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
apply assumption
apply (simp add: int_is_not_ext)

(* f B (tw iA schA2) = nil *)
apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)

(* reduce trace_takes from n to strictly smaller k *)
apply (rule take_reduction)
apply (rule refl)
apply (rule refl)

(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)

(* assumption schA *)
apply (drule_tac x = "x2" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
apply assumption
apply (simp add: intA_is_not_actB int_is_not_ext)

(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
apply (drule_tac sch = "schB" and P = "%a. a:int B" in LastActExtsmall1)
apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
apply assumption
apply (drule_tac sch = "x2" and P = "%a. a:int A" in LastActExtsmall1)

(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
apply (simp add: ForallTL ForallDropwhile)

(* case x~:B & x:A  *)
(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
apply (case_tac "x:act A")
apply fast

(* case x~:B & x~:A  *)
(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
apply (rotate_tac -9)
(* reduce forall assumption from tr to (x>>rs) *)
apply (simp add: externals_of_par)
apply (fast intro!: ext_is_act)

done

subsection "COMPOSITIONALITY on TRACE Level -- Main Theorem"

lemma compositionality_tr:
"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;
            is_asig(asig_of A); is_asig(asig_of B)|]
        ==>  (tr: traces(A||B)) =
             (Filter (%a. a:act A)$tr : traces A &
              Filter (%a. a:act B)$tr : traces B &
              Forall (%x. x:ext(A||B)) tr)"

apply (simp (no_asm) add: traces_def has_trace_def)
apply auto

(* ==> *)
(* There is a schedule of A *)
apply (rule_tac x = "Filter (%a. a:act A) $sch" in bexI)
prefer 2
apply (simp add: compositionality_sch)
apply (simp add: compatibility_consequence1 externals_of_par ext1_ext2_is_not_act1)
(* There is a schedule of B *)
apply (rule_tac x = "Filter (%a. a:act B) $sch" in bexI)
prefer 2
apply (simp add: compositionality_sch)
apply (simp add: compatibility_consequence2 externals_of_par ext1_ext2_is_not_act2)
(* Traces of A||B have only external actions from A or B *)
apply (rule ForallPFilterP)

(* <== *)

(* replace schA and schB by Cut(schA) and Cut(schB) *)
apply (drule exists_LastActExtsch)
apply assumption
apply (drule exists_LastActExtsch)
apply assumption
apply (erule exE)+
apply (erule conjE)+
(* Schedules of A(B) have only actions of A(B) *)
apply (drule scheds_in_sig)
apply assumption
apply (drule scheds_in_sig)
apply assumption

apply (rename_tac h1 h2 schA schB)
(* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
   we need here *)
apply (rule_tac x = "mksch A B$tr$schA$schB" in bexI)

(* External actions of mksch are just the oracle *)
apply (simp add: FilterA_mksch_is_tr)

(* mksch is a schedule -- use compositionality on sch-level *)
apply (simp add: compositionality_sch)
apply (simp add: FilterAmksch_is_schA FilterBmksch_is_schB)
apply (erule ForallAorB_mksch)
apply (erule ForallPForallQ)
apply (erule ext_is_act)
done

subsection {* COMPOSITIONALITY on TRACE Level -- for Modules *}

lemma compositionality_tr_modules:

"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;
            is_asig(asig_of A); is_asig(asig_of B)|]
 ==> Traces (A||B) = par_traces (Traces A) (Traces B)"

apply (unfold Traces_def par_traces_def)
apply (simp add: asig_of_par)
apply (rule set_eqI)
apply (simp add: compositionality_tr externals_of_par)
done

declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym Simplifier.default_mk_sym) *}

end

author: Josh-Tilles

repo: isabelle


text:
header {* Syntax and proof rules for stratified diagrams *}

theory Ribbons_Stratified imports
  Ribbons_Interfaces
  Proofchain
begin

text {* We define the syntax of stratified diagrams. We give proof rules
  for stratified diagrams, and prove them sound with respect to the
  ordinary rules of separation logic. *}

subsection {* Syntax of stratified diagrams *}

datatype sdiagram = SDiagram "(cell \<times> interface) list"
and cell =
  Filler "interface"
| Basic "interface" "command" "interface"
| Exists_sdia "string" "sdiagram"
| Choose_sdia "interface" "sdiagram" "sdiagram" "interface"
| Loop_sdia "interface" "sdiagram" "interface"

datatype_compat sdiagram cell

type_synonym row = "cell \<times> interface"

text {* Extracting the command from a stratified diagram. *}
fun
  com_sdia :: "sdiagram \<Rightarrow> command" and
  com_cell :: "cell \<Rightarrow> command"
where
  "com_sdia (SDiagram \<rho>s) = foldr (op ;;) (map (com_cell \<circ> fst) \<rho>s) Skip"
| "com_cell (Filler P) = Skip"
| "com_cell (Basic P c Q) = c"
| "com_cell (Exists_sdia x D) = com_sdia D"
| "com_cell (Choose_sdia P D E Q) = Choose (com_sdia D) (com_sdia E)"
| "com_cell (Loop_sdia P D Q) = Loop (com_sdia D)"

text {* Extracting the program variables written by a stratified diagram. *}
fun
  wr_sdia :: "sdiagram \<Rightarrow> string set" and
  wr_cell :: "cell \<Rightarrow> string set"
where
  "wr_sdia (SDiagram \<rho>s) = (\<Union>r \<in> set \<rho>s. wr_cell (fst r))"
| "wr_cell (Filler P) = {}"
| "wr_cell (Basic P c Q) = wr_com c"
| "wr_cell (Exists_sdia x D) = wr_sdia D"
| "wr_cell (Choose_sdia P D E Q) = wr_sdia D \<union> wr_sdia E"
| "wr_cell (Loop_sdia P D Q) = wr_sdia D"

text {* The program variables written by a stratified diagram correspond to
  those written by the commands therein. *}
lemma wr_sdia_is_wr_com:
  fixes \<rho>s :: "row list"
  and \<rho> :: row
  shows "(wr_sdia D = wr_com (com_sdia D))"
  and "(wr_cell \<gamma> = wr_com (com_cell \<gamma>))"
  and "(\<Union>\<rho> \<in> set \<rho>s. wr_cell (fst \<rho>))
    = wr_com (foldr (op ;;) (map (\<lambda>(\<gamma>,F). com_cell \<gamma>) \<rho>s) Skip)"
  and "wr_cell (fst \<rho>) = wr_com (com_cell (fst \<rho>))"
apply (induct D and \<gamma> and \<rho>s and \<rho> rule: compat_sdiagram.induct compat_cell.induct
  compat_cell_interface_prod_list.induct compat_cell_interface_prod.induct)
apply (auto simp add: wr_com_skip wr_com_choose
  wr_com_loop wr_com_seq split_def o_def)
done

subsection {* Proof rules for stratified diagrams *}

inductive
  prov_sdia :: "[sdiagram, interface, interface] \<Rightarrow> bool" and
  prov_row :: "[row, interface, interface] \<Rightarrow> bool" and
  prov_cell :: "[cell, interface, interface] \<Rightarrow> bool"
where
  SRibbon: "prov_cell (Filler P) P P"
| SBasic: "prov_triple (asn P, c, asn Q) \<Longrightarrow> prov_cell (Basic P c Q) P Q"
| SExists: "prov_sdia D P Q
    \<Longrightarrow> prov_cell (Exists_sdia x D) (Exists_int x P) (Exists_int x Q)"
| SChoice: "\<lbrakk> prov_sdia D P Q ; prov_sdia E P Q \<rbrakk>
    \<Longrightarrow> prov_cell (Choose_sdia P D E Q) P Q"
| SLoop: "prov_sdia D P P \<Longrightarrow> prov_cell (Loop_sdia P D P) P P"
| SRow: "\<lbrakk> prov_cell \<gamma> P Q ; wr_cell \<gamma> \<inter> rd_int F = {} \<rbrakk>
    \<Longrightarrow> prov_row (\<gamma>, F) (P \<otimes> F) (Q \<otimes> F)"
| SMain: "\<lbrakk> chain_all (\<lambda>(P,\<rho>,Q). prov_row \<rho> P Q) \<Pi> ; 0 < chainlen \<Pi> \<rbrakk>
    \<Longrightarrow> prov_sdia (SDiagram (comlist \<Pi>)) (pre \<Pi>) (post \<Pi>)"

subsection {* Soundness *}

lemma soundness_strat_helper:
  "(prov_sdia D P Q \<longrightarrow> prov_triple (asn P, com_sdia D, asn Q)) \<and>
   (prov_row \<rho> P Q \<longrightarrow> prov_triple (asn P, com_cell (fst \<rho>), asn Q)) \<and>
   (prov_cell \<gamma> P Q \<longrightarrow> prov_triple (asn P, com_cell \<gamma>, asn Q))"
proof (induct rule: prov_sdia_prov_row_prov_cell.induct)
  case (SRibbon P)
  show ?case by (auto simp add: prov_triple.skip)
next
  case (SBasic P c Q)
  thus ?case by auto
next
  case (SExists D P Q x)
  thus ?case by (auto simp add: prov_triple.exists)
next
  case (SChoice D P Q E)
  thus ?case by (auto simp add: prov_triple.choose)
next
  case (SLoop D P)
  thus ?case by (auto simp add: prov_triple.loop)
next
  case (SRow \<gamma> P Q F)
  thus ?case
  by (simp add: prov_triple.frame rd_int_is_rd_ass wr_sdia_is_wr_com(2))
next
  case (SMain \<Pi>)
  thus ?case
  apply (unfold com_sdia.simps)
  apply (intro seq_fold[of _ \<Pi>])
  apply (simp_all add: len_comlist_chainlen)[3]
  apply (induct \<Pi>, simp)
  apply (case_tac i, auto simp add: fst3_simp thd3_simp)
  done
qed

corollary soundness_strat:
  assumes "prov_sdia D P Q"
  shows "prov_triple (asn P, com_sdia D, asn Q)"
using assms soundness_strat_helper by auto

end

repo: AFP

save_path: github-repos/isabelle/Josh-Tilles-AFP


text:
text\<open> 29 October 2021: Exercise for Homework Assignment 08 in CS 511 \<close>
text\<open> Your task to remove the invocations of the pre-defined method
      'blast' by an equivalent sequence of 'apply' steps \<close>

theory HW08_solution
  imports Main
begin

text\<open> 'blast' is invoked three times, once in the proof of each of
      lemmas K1, L1, and M1 below \<close>

(* lemma K1 is the same in Exercise 2.3.9 (k), page 161, in [LCS] *)
lemma K1 : "\<forall> x. (P x \<and> Q x) \<Longrightarrow> (\<forall> x. P x) \<and> (\<forall> x. Q x)"

  apply (rule conjI)
   apply (rule allI)
apply (erule_tac x="x" in allE)
   apply (erule conjE)
   apply assumption
   apply (rule allI)
  apply (erule_tac x="x" in allE)
   apply (erule conjE)
  apply assumption
  done

(* lemma L1 is the same in Exercise 2.3.9 (l), page 161, in [LCS] *)
lemma L1 : "(\<forall> x. P x) \<or> (\<forall> x. Q x) \<Longrightarrow> \<forall> x. (P x \<or> Q x)"
  apply (erule disjE)
   apply (rule allI)
   apply (rule disjI1)
   apply (erule_tac x="x" in allE)
   apply assumption
   apply (rule allI)
   apply (rule disjI2)
   apply (erule_tac x="x" in allE)
   apply assumption
  done

(* lemma M1 is the same in Exercise 2.3.9 (m), page 161, in [LCS] *)
lemma M1 : "\<exists> x. (P x \<and> Q x) \<Longrightarrow> (\<exists> x. P x) \<and> (\<exists> x. Q x)"
  apply (erule exE)
  apply (rule conjI)
   apply (erule conjE)
  apply (erule exI)
   apply (erule conjE)
  apply (erule exI)
  done
end

author: decltypeme


text:
(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory Memcpy
imports
  "CParser.CTranslation"
  "AutoCorres.AutoCorres"
begin

abbreviation "ADDR_MAX \<equiv> UWORD_MAX TYPE(addr_bitsize)"

(* Helper for noticing when you accidentally haven't constrained an of_nat *)
abbreviation "of_nat_addr \<equiv> of_nat::(nat \<Rightarrow> addr)"

lemma byte_ptr_guarded:
    "ptr_val (x::8 word ptr) \<noteq> 0 \<Longrightarrow> c_guard x"
  unfolding c_guard_def c_null_guard_def ptr_aligned_def
  by (clarsimp simp: intvl_Suc)

(* FIXME: MOVE *)
lemma ptr_add_coerce: "ptr_val (((ptr_coerce x)::('a::{c_type}) ptr) +\<^sub>p a) = (ptr_val x) + (of_int a * of_nat (size_of TYPE('a)))"
  apply (case_tac x)
  apply (clarsimp simp: CTypesDefs.ptr_add_def)
  done

(* FIXME: MOVE *)
(* Casting a valid pointer to char* and incrementing it by a value less than
 * the size of the underlying type does not give us NULL.
 *)
lemma ptr_contained:"\<lbrakk> c_guard (x::('a::c_type) ptr); size_of TYPE('a) = sz;
                       0 \<le> i; i < int sz; (y::8 word ptr) = ptr_coerce x\<rbrakk> \<Longrightarrow> c_guard (y +\<^sub>p i)"
  apply (rule byte_ptr_guarded)
  unfolding c_guard_def c_null_guard_def ptr_add_def
  apply simp
  apply (clarsimp simp: CTypesDefs.ptr_add_def intvl_def)
  apply (erule allE [where x="nat i"])
  apply (clarsimp simp: nat_less_iff of_nat_nat)
  done

external_file "memcpy.c"
install_C_file "memcpy.c"

(* FIXME: MOVE *)
lemma squash_auxupd_id[polish]:
  "modify (t_hrs_'_update (hrs_htd_update id)) = skip"
  by (monad_eq simp: skip_def id_def hrs_htd_update_def)

autocorres [no_heap_abs=memcpy memcpy_int] "memcpy.c"

(* Dereference a pointer *)
abbreviation "deref s x \<equiv> h_val (hrs_mem (t_hrs_' s)) x"

(* char* cast *)
abbreviation "byte_cast x \<equiv> ((ptr_coerce x)::8 word ptr)"

context memcpy begin

lemma memcpy_char:
  "\<lbrace> \<lambda>s. c_guard (x::8 word ptr) \<and>
         c_guard (y::8 word ptr) \<and>
         unat sz = size_of TYPE(8 word) \<and>
         P (deref s x) \<and>
         x \<noteq> y\<rbrace>
      memcpy' (ptr_coerce y) (ptr_coerce x) sz
   \<lbrace>\<lambda> _ s. P (deref s y) \<rbrace>!"
  (* Evaluate sz *)
  apply clarsimp

  unfolding memcpy'_def
  apply (clarsimp simp:skip_def)
  apply wp

  (* Unroll the loop twice *)
  apply (subst whileLoop_unroll, wp)
     apply (subst whileLoop_unroll, wp)

  (* The remaining loop is never encountered *)
       apply (rule validNF_false_pre)
      apply wp+

  (* Finally we're left with the single assignment *)
  apply (clarsimp simp:hrs_mem_update h_val_heap_update)
  apply unat_arith
 done

lemma of_nat_prop_exp: "n < 32 \<Longrightarrow> of_nat (2 ^ n) = 2 ^ (of_nat n)"
  by clarsimp

lemma memcpy_word:
  "\<lbrace> \<lambda>s. c_guard (x::32 word ptr) \<and>
         c_guard (y::32 word ptr) \<and>
         unat sz = size_of TYPE(32 word) \<and>
         P (deref s x) \<and>
         x \<noteq> y \<rbrace>
      memcpy' (ptr_coerce y) (ptr_coerce x) sz
   \<lbrace> \<lambda>_ s. P (deref s y) \<rbrace>!"
  apply clarsimp
  unfolding memcpy'_def apply (clarsimp simp:skip_def)
  apply (rule validNF_assume_pre)
  apply (subgoal_tac "{ptr_val x ..+ unat sz} \<inter> {ptr_val y ..+ unat sz} = {}")
   apply (subst whileLoop_add_inv [where
     I="\<lambda>i s.  unat i \<le> unat sz \<and>
                (\<forall>a < i. deref s (byte_cast x +\<^sub>p uint a) = deref s (byte_cast y +\<^sub>p uint a)) \<and>
                P (deref s x)" and
     M="\<lambda>(i, s). unat sz - unat i"])
   apply (wp validNF_whileLoop_inv_measure_twosteps)
      apply clarsimp
      apply (rule conjI, unat_arith)
      apply (rule conjI, clarsimp)
       apply (case_tac "a = i")
        apply (clarsimp)
        apply (erule_tac x=i in allE)
        apply (clarsimp simp:hrs_mem_update h_val_heap_update)
        apply (subst h_val_heap_same)
            apply (rule ptr_retyp_h_t_valid)
            apply simp
           apply (rule ptr_retyp_disjoint)
            apply (rule ptr_retyp_h_t_valid)
            apply simp
           apply (clarsimp simp:ptr_add_def intvl_def CTypesDefs.ptr_add_def)
          apply simp
         apply (clarsimp simp: CTypesDefs.ptr_add_def field_of_t_simple)
         apply (drule field_of_t_simple)
         apply clarsimp
        apply simp
       apply (subgoal_tac "a < i")
        apply (clarsimp simp:hrs_mem_update)
        apply (subst h_val_heap_update_disjoint)

         (* The current goal should be obvious to unat_arith, but for some reason isn't *)
         apply (clarsimp simp:ptr_add_def intvl_def disjoint_iff_not_equal)
         apply (erule_tac x="ptr_val x + a" in allE, clarsimp)
         apply (erule impE)
          apply (rule_tac x="unat a" in exI, clarsimp)
          apply unat_arith

         apply (erule_tac x="ptr_val y + i" and
                          P="\<lambda>ya. (\<exists>k. ya = ptr_val y + of_nat k \<and> k < 4) \<longrightarrow> ptr_val y + i \<noteq> ya" in allE, clarsimp)
         apply (erule_tac x="unat i" in allE, clarsimp)
          apply unat_arith
         apply (clarsimp simp:CTypesDefs.ptr_add_def)
        apply (subst h_val_heap_update_disjoint)
         (* Similar goal to the previous irritation, but this time Isabelle decides to play ball *)
         apply (clarsimp simp:ptr_add_def intvl_def ptr_val_def disjoint_iff_not_equal)
        apply (clarsimp simp:CTypesDefs.ptr_add_def)
       apply (clarsimp simp:CTypesDefs.ptr_add_def)
      apply unat_arith

      apply (rule conjI)
       apply (subst hrs_mem_update)+
       apply (subst h_val_heap_update_disjoint)
        apply (clarsimp simp: disjoint_iff_not_equal)
        apply (clarsimp simp:CTypesDefs.ptr_add_def intvl_def)
        apply (erule_tac x="ptr_val x + of_nat k" in allE)
        apply (erule impE)
         apply (rule_tac x="k" in exI)
         apply simp
        apply (erule_tac x="ptr_val y + i" and
                         P="\<lambda>ya. (\<exists>k. ya = ptr_val y + of_nat k \<and> k < 4) \<longrightarrow> ptr_val x + of_nat k \<noteq> ya" in allE)
        apply (erule impE)
         apply (rule_tac x="unat i" in exI)
         apply simp
         apply unat_arith
        apply simp
       apply simp

      (* Yet more tedium that unat_arith doesn't like *)
      apply (rule conjI)
       apply (rule byte_ptr_guarded,
              clarsimp simp:CTypesDefs.ptr_add_def c_guard_def c_null_guard_def intvl_def,
              (erule_tac x="unat i" in allE)+,
              clarsimp,
              unat_arith)+

     apply wp
     apply unat_arith
    apply clarsimp
    apply (subgoal_tac "deref sa x = deref sa y")
     apply clarsimp
    apply (clarsimp simp: h_val_def)[1]
    apply (rule arg_cong[where f=from_bytes])
    apply (subst numeral_eqs(3))+
    apply simp
    apply (rule_tac x=0 in allE, assumption, erule impE, unat_arith)
    apply (rule_tac x=1 in allE, assumption, erule impE, unat_arith)
    apply (rule_tac x=2 in allE, assumption, erule impE, unat_arith)
    apply (rule_tac x=3 in allE, assumption, erule impE, unat_arith)
    apply (simp add:CTypesDefs.ptr_add_def)
    apply (simp add: add.commute from_bytes_eq)
   apply clarsimp
  apply (clarsimp simp:intvl_def disjoint_iff_not_equal)
  apply (drule_tac x=x and y=y and j="of_nat k" and i="of_nat ka" and n=2 in neq_imp_bytes_disjoint)
        apply assumption
       apply (case_tac "k = 0", clarsimp) (* insert "k > 0" *)
       apply (clarsimp simp:unat_of_nat_len)
      apply (case_tac "ka = 0", clarsimp)
      apply (clarsimp simp:unat_of_nat_len)
     apply assumption
    apply clarsimp+
  done

text \<open>The bytes at the pointer @{term p} are @{term bs}.\<close>
definition
  bytes_at :: "'a globals_scheme \<Rightarrow> 'b::c_type ptr \<Rightarrow> word8 list \<Rightarrow> bool"
where
  "bytes_at s p bs \<equiv> length bs = 0 \<or>
                      (length bs \<le> ADDR_MAX \<and> (\<forall>i \<in> {0..(length bs - 1)}. deref s (byte_cast p +\<^sub>p (of_nat i)) = bs ! i))"

lemma bytes_at_none[simp]: "bytes_at s p []"
  by (clarsimp simp:bytes_at_def)

text \<open>The bytes of typed pointer @{term p} are @{term bs}.\<close>
definition
  bytes_of :: "'a globals_scheme \<Rightarrow> 'b::c_type ptr \<Rightarrow> word8 list \<Rightarrow> bool"
where
  "bytes_of s p bs \<equiv> length bs = size_of TYPE('b) \<and> bytes_at s p bs"

text \<open>The bytes at a char pointer are just it dereferenced.\<close>
lemma bytes_of_char[simp]: "bytes_of s (p::8word ptr) bs = (length bs = 1 \<and> deref s p = hd bs)"
  apply (clarsimp simp:bytes_of_def bytes_at_def)
  apply (rule iffI)
   apply clarsimp
   apply (erule disjE)
    apply clarsimp+
   apply (rule hd_conv_nth[symmetric])
   apply clarsimp+
  apply (subgoal_tac "hd bs = bs ! 0")
   apply simp
  apply (rule hd_conv_nth)
  apply clarsimp
  done

text \<open>A pointer does not wrap around memory.\<close>
definition
  no_wrap :: "'a::c_type ptr \<Rightarrow> nat \<Rightarrow> bool"
where
  "no_wrap p sz \<equiv> 0 \<notin> {ptr_val p ..+ sz}"

text \<open>Two pointers do not overlap.\<close>
definition
  no_overlap :: "'a::c_type ptr \<Rightarrow> 'b::c_type ptr \<Rightarrow> nat \<Rightarrow> bool"
where
  "no_overlap p q sz \<equiv> {ptr_val p ..+ sz} \<inter> {ptr_val q ..+ sz} = {}"

lemma no_overlap_sym: "no_overlap x y = no_overlap y x"
  apply (rule ext)
  apply (clarsimp simp:no_overlap_def)
  by blast

(* FIXME: MOVE *)
lemma h_val_not_id:
  fixes x :: "'a::mem_type ptr"
    and y :: "'b::mem_type ptr"
  shows "{ptr_val x..+size_of TYPE('a)} \<inter> {ptr_val y..+size_of TYPE('b)} = {}
     \<Longrightarrow> h_val (hrs_mem (hrs_mem_update (heap_update x v) s)) y = h_val (hrs_mem s) y"
  apply (subst hrs_mem_heap_update[symmetric])
  apply (subst h_val_heap_update_disjoint)
   apply blast
  apply clarsimp
  done

definition
  update_bytes :: "'a globals_scheme \<Rightarrow> 'b::mem_type ptr \<Rightarrow> word8 list \<Rightarrow> 'a globals_scheme"
where
  "update_bytes s p bs \<equiv> s\<lparr>t_hrs_' := hrs_mem_update (heap_update_list (ptr_val p) bs) (t_hrs_' s)\<rparr>"

lemma the_horse_says_neigh: "(s\<lparr>t_hrs_' := x\<rparr> = s\<lparr>t_hrs_' := y\<rparr>) = (x = y)"
 by (metis (erased, lifting) globals.cases_scheme globals.select_convs(1) globals.update_convs(1))

lemma upto_singleton[simp]:"[x..x] = [x]"
  by (simp add: upto_rec1)

lemma update_bytes_ignore_ptr_coerce[simp]: "update_bytes s (ptr_coerce p) = update_bytes s p"
  by (clarsimp simp:update_bytes_def intro!:ext)

lemma hrs_mem_update_commute:
  "f \<circ> g = g \<circ> f \<Longrightarrow> hrs_mem_update f (hrs_mem_update g s) = hrs_mem_update g (hrs_mem_update f s)"
  by (metis (no_types, lifting) comp_eq_elim hrs_htd_def hrs_htd_mem_update hrs_mem_def hrs_mem_f prod.collapse)

lemma hrs_mem_update_collapse:
  "hrs_mem_update f (hrs_mem_update g s) = hrs_mem_update (f \<circ> g) s"
  by (metis comp_eq_dest_lhs hrs_htd_def hrs_htd_mem_update hrs_mem_def hrs_mem_f prod.collapse)

lemma update_bytes_reorder:
  "{ptr_val p..+length cs} \<inter> {ptr_val q..+length bs} = {} \<Longrightarrow>
      update_bytes (update_bytes s q bs) p cs = update_bytes (update_bytes s p cs) q bs"
  apply (clarsimp simp:update_bytes_def)
  apply (subst the_horse_says_neigh)
  apply (subst hrs_mem_update_commute)
   apply (clarsimp intro!:ext)
   apply (subst heap_update_list_commute)
    apply clarsimp+
  done

lemma lt_step_down: "\<lbrakk>(x::nat) < y; x = y - 1 \<longrightarrow> P; x < y - 1 \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
  by force

(* XXX: This proof makes me sad. *)
lemma under_uint_imp_no_overflow: "x < ADDR_MAX \<Longrightarrow> ((of_nat x)::addr) + 1 \<noteq> 0"
  apply (induct x)
   apply (clarsimp simp:UWORD_MAX_def)+
  apply unat_arith
  apply (clarsimp simp:UWORD_MAX_def)
  apply (cut_tac y=x and z="(of_nat (ADDR_MAX - 1))::addr" in le_unat_uoi)
   apply (clarsimp simp:UWORD_MAX_def)+
  done

lemma heap_update_list_append3:
  "1 + length ys < 2 ^ word_bits \<Longrightarrow>
    heap_update_list s (y # ys) hp = heap_update_list s [y] (heap_update_list (s + 1) ys hp)"
  apply clarsimp
  apply (subst heap_update_list_append2[where xs="[y]", simplified])
   apply clarsimp+
  done

lemma hrs_mem_update_cong': "f = g \<Longrightarrow> hrs_mem_update f s = hrs_mem_update g s"
  by presburger

lemma update_bytes_append: "length bs \<le> ADDR_MAX \<Longrightarrow>
  update_bytes s p (b # bs) = update_bytes (update_bytes s p [b]) (byte_cast p +\<^sub>p 1) bs"
  apply (clarsimp simp:update_bytes_def)
  apply (subst the_horse_says_neigh)
  apply (subst hrs_mem_update_commute)
   apply (rule ext)+
   apply simp
   apply (case_tac "xa = ptr_val p")
    apply (clarsimp simp:fun_upd_def)
    apply (subst heap_update_nmem_same)
     apply (clarsimp simp:intvl_def ptr_add_def)
     apply (subgoal_tac "k < ADDR_MAX")
      prefer 2
      apply unat_arith
     apply (drule under_uint_imp_no_overflow)
     apply unat_arith
    apply clarsimp
   apply (subst heap_update_list_update)
    apply simp
   apply (clarsimp simp:fun_upd_def)
  apply (subst hrs_mem_update_collapse)
  apply (rule hrs_mem_update_cong')
  apply (clarsimp simp:ptr_add_def)
  apply (rule ext)
  apply (cut_tac xs="[b]" and ys=bs and s="ptr_val p" and hp=x in heap_update_list_append)
  apply (clarsimp simp:fun_upd_def intro!:ext)
  apply (rule conjI)
   apply clarsimp
   apply (subst heap_update_nmem_same)
    apply (clarsimp simp:ptr_add_def intvl_def)
    apply (subgoal_tac "k < ADDR_MAX")
     prefer 2
     apply unat_arith
    apply (drule under_uint_imp_no_overflow)
    apply unat_arith
   apply clarsimp
  apply clarsimp
  apply (case_tac "xa \<in> {ptr_val p + 1..+length bs}")
  apply (subst heap_update_mem_same_point)
    apply simp
   apply (subgoal_tac "addr_card = ADDR_MAX + 1")
    apply clarsimp
   apply (clarsimp simp:addr_card UWORD_MAX_def)
  apply (subst heap_update_mem_same_point)
    apply simp
   apply (subgoal_tac "addr_card = ADDR_MAX + 1")
    apply clarsimp
   apply (clarsimp simp:addr_card UWORD_MAX_def)
  apply clarsimp
  apply (subst heap_update_nmem_same)
   apply clarsimp
  apply (subst heap_update_nmem_same)
   apply clarsimp+
  done

lemma update_bytes_postpend: "length bs = x + 1 \<Longrightarrow>
  update_bytes s p bs = update_bytes (update_bytes s p (take x bs)) (byte_cast p +\<^sub>p (of_nat x)) [bs ! x]"
  apply (clarsimp simp:update_bytes_def)
  apply (subst the_horse_says_neigh)
  apply (clarsimp simp:ptr_add_def)
  apply (subst heap_update_list_concat_fold_hrs_mem)
   apply clarsimp+
  by (metis append_eq_conv_conj append_self_conv hd_drop_conv_nth2 lessI take_hd_drop)

lemma h_val_not_id_general:
  fixes y :: "'a::mem_type ptr"
  shows "\<forall>i \<in> {0..+size_of TYPE('a)}. \<forall>g. f g (ptr_val y + i) = g (ptr_val y + i)
     \<Longrightarrow> h_val (hrs_mem (hrs_mem_update f s)) y = h_val (hrs_mem s) y"
  apply (subst hrs_mem_update)
  apply (clarsimp simp:h_val_def)
  apply (subgoal_tac "heap_list (f (hrs_mem s)) (size_of TYPE('a)) (ptr_val y) =
                      heap_list (hrs_mem s) (size_of TYPE('a)) (ptr_val y)")
   apply clarsimp
  apply (cut_tac h="f (hrs_mem s)" and p="ptr_val y" and n="size_of TYPE('a)"
                 and h'="hrs_mem s" in heap_list_h_eq2)
   apply (erule_tac x="x - ptr_val y" in  ballE)
    apply clarsimp
   apply (clarsimp simp:intvl_def)+
  done

lemma h_val_not_id_list:
  fixes y :: "'a::mem_type ptr"
  shows "{x..+length vs} \<inter> {ptr_val y..+size_of TYPE('a)} = {}
     \<Longrightarrow> h_val (hrs_mem (hrs_mem_update (heap_update_list x vs) s)) y = h_val (hrs_mem s) y"
  apply (subst h_val_not_id_general)
   apply clarsimp
   apply (metis (erased, hide_lams) disjoint_iff_not_equal heap_update_nmem_same intvlD intvlI
          monoid_add_class.add.left_neutral)
  apply clarsimp
  done

lemma h_val_id_update_bytes:
  fixes q :: "'a::mem_type ptr"
  shows "{ptr_val q..+size_of TYPE('a)} \<inter> {ptr_val p..+length bs} = {}
          \<Longrightarrow> deref (update_bytes s p bs) q = deref s q"
  apply (clarsimp simp:update_bytes_def)
  apply (subst h_val_not_id_list)
   apply blast
  by simp

lemma bytes_at_len: "bytes_at s p bs \<Longrightarrow> length bs \<le> ADDR_MAX"
  by (clarsimp simp:bytes_at_def, fastforce)

(* Another sad proof. *)
lemma le_uint_max_imp_id: "x \<le> ADDR_MAX \<Longrightarrow> unat ((of_nat x)::addr) = x"
  apply (induct x)
   apply (clarsimp simp: UWORD_MAX_def)+
  apply unat_arith
  apply clarsimp
  done

lemma update_bytes_id: "update_bytes s p [] = s"
  apply (clarsimp simp:update_bytes_def)
  apply (subst heap_update_list_base')
  by (simp add: hrs_mem_update_id3)

lemma a_horse_by_any_other_name: "t_hrs_'_update f s = s\<lparr>t_hrs_' := f (t_hrs_' s)\<rparr>"
  by auto

lemma heap_update_list_singleton: "heap_update_list p [x] = heap_update (Ptr p) x"
  apply (rule ext)
  by (metis heap_update_def ptr_val.simps to_bytes_word8)

lemma update_bytes_eq: "\<lbrakk>s = s'; p = p'; bs = bs'\<rbrakk> \<Longrightarrow> update_bytes s p bs = update_bytes s' p' bs'"
  by clarsimp

text \<open>
  Memcpy does what it says on the box.
\<close>
lemma memcpy_wp':
  fixes src :: "'a::mem_type ptr"
    and dst :: "'b::mem_type ptr"
  shows "\<forall>s0 bs.
  \<lbrace>\<lambda>s. s = s0 \<and> c_guard src \<and> c_guard dst \<and> sz = of_nat (length bs) \<and> bytes_at s src bs \<and>
       no_wrap src (unat sz) \<and> no_wrap dst (unat sz) \<and> no_overlap src dst (unat sz)\<rbrace>
    memcpy' (ptr_coerce dst) (ptr_coerce src) sz
  \<lbrace>\<lambda>r s. r = ptr_coerce dst \<and> bytes_at s dst bs \<and> s = update_bytes s0 dst bs\<rbrace>!"
  apply (rule allI)+
  apply (rule validNF_assume_pre)
  unfolding memcpy'_def
  apply clarsimp
  apply (subst whileLoop_add_inv[where
    I="\<lambda>i s. unat i \<le> unat sz \<and>
             bytes_at s dst (take (unat i) bs) \<and>
             bytes_at s src bs \<and>
             s = update_bytes s0 dst (take (unat i) bs)" and
    M="\<lambda>(i, s). unat sz - unat i"])
  apply wp
    apply clarsimp
    apply (rule conjI)
     apply unat_arith
    apply (rule conjI)
     apply (simp add:bytes_at_def)
     apply (case_tac "bs = []")
      apply (rule disjI1)
      apply clarsimp
     apply (rule disjI2)
     apply clarsimp
     apply (rule conjI)
      apply unat_arith
     apply clarsimp
     apply (case_tac "unat i = ia")
      apply clarsimp
      apply (subgoal_tac "int (unat i) = uint i")
       prefer 2
       apply (subst uint_nat)
       apply simp
      apply simp
      apply (subst h_val_id)
      apply (subst h_val_id_update_bytes)
       apply (clarsimp simp:no_overlap_def ptr_add_def)
       apply (subgoal_tac "{ptr_val src + i..+Suc 0} \<subseteq> {ptr_val src..+unat (of_nat_addr (length bs))}")
        prefer 2
        apply (clarsimp simp:intvl_def)
        apply (rule_tac x="unat i" in exI)
        apply unat_arith
       apply (subgoal_tac "{ptr_val dst..+unat i} \<subseteq> {ptr_val dst..+unat (of_nat_addr (length bs))}")
        prefer 2
        apply (clarsimp simp:intvl_def)
        apply (rule exI, rule conjI, rule refl)
        apply (simp add: unat_of_nat)
       apply blast
      apply (erule_tac x="unat i" and P="\<lambda>x. deref s0 (byte_cast src +\<^sub>p int x) = bs ! x" in ballE)
       apply clarsimp
       apply (subst nth_take)
        apply unat_arith
       apply simp
      apply (erule disjE)
       apply clarsimp+
     apply (erule disjE)
      apply (subgoal_tac "length bs \<noteq> 0")
       prefer 2
       apply clarsimp
      apply (case_tac "unat i = 0")
       apply unat_arith
      apply linarith
     apply (subst h_val_not_id)
      apply (clarsimp simp:ptr_add_def intvl_def)
      (* Isabelle, why do you have to make it so hard? *)
      apply (erule_tac P="unat (of_nat ia) = ia" in notE)
      apply (cut_tac y=ia and z="(of_nat ADDR_MAX)::addr" in le_unat_uoi)
       apply (subgoal_tac "unat ((of_nat ADDR_MAX)::addr) = ADDR_MAX")
        prefer 2
        apply (simp add: unat_of_nat)
       apply (simp add: unat_of_nat)
      apply clarsimp
     apply clarsimp
     apply (erule_tac x=ia and A="{0..min (length bs) (unat i) - Suc 0}" in ballE)
      apply clarsimp
      apply (subst nth_take, unat_arith)+
      apply simp
     apply clarsimp
     apply unat_arith
    apply (rule conjI)
     apply (clarsimp simp:bytes_at_def)
     apply (subst h_val_not_id)
      apply (clarsimp simp:no_overlap_def)
      apply (subgoal_tac "ptr_val (byte_cast dst +\<^sub>p uint i) \<in> {ptr_val dst..+unat (of_nat (length bs))}")
       prefer 2
       apply (clarsimp simp:ptr_add_def intvl_def)
       apply (rule_tac x="unat i" in exI)
       apply clarsimp
       apply unat_arith
      (* More or less symmetric subgoal *)
      apply (subgoal_tac "ptr_val (byte_cast src +\<^sub>p int ia) \<in> {ptr_val src..+unat ((of_nat (length bs))::addr)}")
       prefer 2
       apply (clarsimp simp:ptr_add_def intvl_def)
       apply (rule_tac x=ia in exI)
       apply clarsimp
       apply (subgoal_tac "unat ((of_nat (length bs))::addr) = length bs")
        apply clarsimp
        apply arith
       apply (cut_tac y="length bs" and z="(of_nat ADDR_MAX)::addr" in le_unat_uoi)
        apply (simp add: unat_of_nat)
       apply arith
      apply (clarsimp simp:intvl_def ptr_add_def)
      apply blast
     apply clarsimp
    apply (rule conjI)
     apply (subst h_val_id_update_bytes)
      apply (clarsimp simp:no_overlap_def ptr_add_def)
      apply (subgoal_tac "{ptr_val src + i..+Suc 0} \<subseteq> {ptr_val src..+unat (of_nat_addr (length bs))}")
       prefer 2
       apply (clarsimp simp:intvl_def)
       apply (rule_tac x="unat i" in exI)
       apply unat_arith
      apply (subgoal_tac "{ptr_val dst..+min (length bs) (unat i)} \<subseteq> {ptr_val dst..+unat (of_nat_addr (length bs))}")
       prefer 2
       apply (clarsimp simp:intvl_def)
       apply (rule_tac x=ka in exI)
       apply unat_arith
      apply blast
     apply (subgoal_tac "deref s0 (byte_cast src +\<^sub>p uint i) = bs ! (unat i)")
      apply clarsimp
      apply (subgoal_tac "update_bytes s0 dst (take (unat (i + 1)) bs) =
                          update_bytes (update_bytes s0 dst (take (unat i) bs)) (byte_cast dst +\<^sub>p uint i) [bs ! unat i]")
       apply clarsimp
       apply (subgoal_tac
               "\<forall>s'. t_hrs_'_update (hrs_mem_update (heap_update (byte_cast dst +\<^sub>p uint i) (bs ! unat i))) s' =
                     update_bytes s' (byte_cast dst +\<^sub>p uint i) [bs ! unat i]")
        apply fast
       apply (clarsimp simp:update_bytes_def)
       apply (subst a_horse_by_any_other_name)
       apply (subst the_horse_says_neigh)
       apply (clarsimp simp:ptr_add_def)
       apply (subst heap_update_list_singleton)
       apply simp
      apply (cut_tac s=s0 and p=dst and bs="take (unat (i + 1)) bs" and x="unat i"
                     in update_bytes_postpend)
       apply (subgoal_tac "unat (i + 1) \<le> length bs")
        apply clarsimp
        apply unat_arith
       apply (subgoal_tac "unat i < length bs")
        apply unat_arith
       apply (rule unat_less_helper)
       apply simp
      apply clarsimp
      apply (rule update_bytes_eq)
        apply (subgoal_tac "min (unat i) (unat (i + 1)) = unat i")
         apply clarsimp
        apply clarsimp
        apply unat_arith
       apply (clarsimp simp:ptr_add_def)
      apply clarsimp
      apply (rule nth_take)
      apply unat_arith
     apply (clarsimp simp:bytes_at_def)
     apply (erule disjE)
      apply clarsimp
     apply clarsimp
     apply (erule_tac x="unat i" in ballE)
      apply (subst (asm) uint_nat[symmetric])
      apply simp
     apply clarsimp
     apply (subgoal_tac "unat i < length bs")
      prefer 2
      apply (rule unat_less_helper)
      apply simp
     apply unat_arith
    apply (rule conjI)
     apply unat_arith
    apply (rule conjI)
     apply (rule byte_ptr_guarded)
     apply (clarsimp simp:no_wrap_def intvl_def ptr_add_def)
     apply (erule_tac x="unat i" in allE)
     apply clarsimp
    apply (rule byte_ptr_guarded)
    apply (clarsimp simp:no_wrap_def intvl_def ptr_add_def)
    apply (erule_tac x="unat i" and
                     P="\<lambda>x. ptr_val dst + ((of_nat x)::addr) = 0 \<longrightarrow> \<not> x < unat ((of_nat_addr (length bs))::addr)"
                    in allE)
    apply clarsimp
   apply clarsimp
   apply (rule conjI)
    apply (subgoal_tac "unat i = length bs")
     apply clarsimp
    apply (case_tac "length bs = 0")
     apply clarsimp
    apply (subgoal_tac "length bs \<le> ADDR_MAX")
     prefer 2
     apply (clarsimp simp:bytes_at_def)
    (* XXX: We keep introducing this subgoal; we should do it once and for all up top. *)
    apply (subgoal_tac "unat ((of_nat (length bs))::addr) = length bs")
     prefer 2
     apply (cut_tac y="length bs" and z="(of_nat ADDR_MAX)::addr" in le_unat_uoi)
      apply (clarsimp simp:UWORD_MAX_def)
     apply clarsimp+
    apply unat_arith
   (* insert a bunch a tedium... *)
   apply (subgoal_tac "unat i = length bs")
    prefer 2
    apply (drule bytes_at_len)
    apply (subgoal_tac "unat (of_nat_addr (length bs)) = length bs")
     prefer 2
     apply (rule le_uint_max_imp_id)
     apply simp
    apply unat_arith
   apply clarsimp
  apply (simp add:update_bytes_id)
  done

lemma validNF_make_schematic_post':
  "(\<forall>s0 x. \<lbrace> \<lambda>s. P s0 x s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 x rv s \<rbrace>!) \<Longrightarrow>
   \<lbrace> \<lambda>s. \<exists>s0 x. P s0 x s \<and> (\<forall>rv s'. Q s0 x rv s' \<longrightarrow> Q' rv s') \<rbrace> f \<lbrace> Q'\<rbrace>!"
  by (auto simp add: valid_def validNF_def no_fail_def split: prod.splits)

lemmas memcpy_wp = memcpy_wp'[THEN validNF_make_schematic_post', simplified]

lemma h_val_not_id_update_bytes:
  fixes q :: "'a::mem_type ptr"
  shows "\<lbrakk>ptr_val p = ptr_val q; length bs = size_of TYPE('a)\<rbrakk> \<Longrightarrow>
            deref (update_bytes s p bs) q = from_bytes bs"
  apply (clarsimp simp:update_bytes_def h_val_def)
  apply (subst hrs_mem_update)
  apply (cut_tac p="ptr_val q" and v=bs and h="hrs_mem (t_hrs_' s)" in heap_list_update)
   apply clarsimp
   apply (metis less_imp_le max_size)
  by clarsimp

text \<open>
  Test that we can use memcpy in a compositional proof. The following proof can be done much more
  pleasantly, but we're just trying to check that the memcpy WP lemma is usable.
  TODO: This relies on disabling heap abstraction for the calling function as well. We should be
  able to phrase an exec_concrete WP lemma over memcpy that lets us prove properties about
  heap-abstracted callers. This will need AutoCorres support to connect is_valid_* with
  c_guard/no_overlap/no_wrap.
\<close>

definition
  memcpy_int_spec :: "sword32 ptr \<Rightarrow> sword32 ptr \<Rightarrow> bool"
where
  "memcpy_int_spec dst src \<equiv>
    \<forall>x. \<lbrace>\<lambda>s. deref s src = x \<and>
             {ptr_val src..+4} \<inter> {ptr_val dst..+4} = {} \<and>
             c_guard src \<and> c_guard dst \<and>
             no_wrap src 4 \<and> no_wrap dst 4\<rbrace>
          memcpy_int' dst src
        \<lbrace>\<lambda>_ s. deref s dst = x\<rbrace>!"

lemma memcpy_int_wp'[unfolded memcpy_int_spec_def]: "memcpy_int_spec dst src"
  unfolding memcpy_int_spec_def
  apply (rule allI)
  unfolding memcpy_int'_def
  apply (wp memcpy_wp)
  apply clarsimp
  apply (rule_tac x="[deref s (byte_cast src),
                      deref s (byte_cast src +\<^sub>p 1),
                      deref s (byte_cast src +\<^sub>p 2),
                      deref s (byte_cast src +\<^sub>p 3)]" in exI)
  apply (clarsimp simp:bytes_at_def no_overlap_def UINT_MAX_def)
  apply (rule conjI)
   apply clarsimp
   apply (case_tac "i = 0", clarsimp)
   apply (case_tac "i = 1", clarsimp)
   apply (case_tac "i = 2", clarsimp)
   apply (case_tac "i = 3", clarsimp)
   apply clarsimp
  apply clarsimp
  apply (subst h_val_not_id_update_bytes)
    apply clarsimp+
  apply (clarsimp simp:h_val_def)
  apply (subgoal_tac "heap_list (hrs_mem (t_hrs_' s)) 4 (ptr_val src) =
                      deref s (byte_cast src) # (heap_list (hrs_mem (t_hrs_' s)) 3 (ptr_val src + 1))")
   prefer 2
   apply (clarsimp simp:h_val_def)
   apply (metis Suc_numeral from_bytes_eq heap_list_rec semiring_norm(2) semiring_norm(8))
  apply (subgoal_tac "heap_list (hrs_mem (t_hrs_' s)) 3 (ptr_val src + 1) =
                      deref s (byte_cast src +\<^sub>p 1) # (heap_list (hrs_mem (t_hrs_' s)) 2 (ptr_val src + 2))")
   prefer 2
   apply (clarsimp simp:h_val_def ptr_add_def)
   apply (cut_tac h="hrs_mem (t_hrs_' s)" and p="ptr_val src + 1" and n=2 in heap_list_rec)
   apply clarsimp
   apply (simp add: add.commute from_bytes_eq)
  apply clarsimp
  apply (subgoal_tac "heap_list (hrs_mem (t_hrs_' s)) 2 (ptr_val src + 2) =
                      deref s (byte_cast src +\<^sub>p 2) # (heap_list (hrs_mem (t_hrs_' s)) 1 (ptr_val src + 3))")
   prefer 2
   apply (cut_tac h="hrs_mem (t_hrs_' s)" and p="ptr_val src + 2" and n=3 in heap_list_rec)
   apply (clarsimp simp:h_val_def ptr_add_def from_bytes_eq)
   apply (metis (no_types, hide_lams) Suc_eq_plus1 heap_list_base heap_list_rec is_num_normalize(1)
                monoid_add_class.add.left_neutral one_add_one one_plus_numeral semiring_norm(3))
  apply (clarsimp simp:h_val_def ptr_add_def from_bytes_eq)
  done

text \<open>memcpying a typed variable is equivalent to assignment.\<close>
lemma memcpy_type_wp':
  fixes dst :: "'a::mem_type ptr"
    and src :: "'a::mem_type ptr"
  shows "\<forall>s0 bs.
   \<lbrace>\<lambda>s. s = s0 \<and> c_guard dst \<and> c_guard src \<and> sz = of_nat (size_of TYPE('a)) \<and>
        no_overlap dst src (unat sz) \<and> no_wrap dst (unat sz) \<and> no_wrap src (unat sz) \<and>
        bytes_of s src bs\<rbrace>
     memcpy' (ptr_coerce dst) (ptr_coerce src) sz
   \<lbrace>\<lambda>r s. r = ptr_coerce dst \<and> bytes_of s dst bs \<and> s = update_bytes s0 dst bs\<rbrace>!"
  apply (rule allI)+
  apply (wp memcpy_wp)
  apply clarsimp
  apply (rule_tac x=bs in exI)
  apply clarsimp
  apply (subst no_overlap_sym)
  apply (clarsimp simp:bytes_of_def)
  done

lemmas memcpy_type_wp = memcpy_type_wp'[THEN validNF_make_schematic_post', simplified]

text \<open>Confirm that we can also prove memcpy_int using the previous generic lemma.\<close>
lemma memcpy_int_wp''[unfolded memcpy_int_spec_def]: "memcpy_int_spec dst src"
  unfolding memcpy_int_spec_def memcpy_int'_def
  apply (rule allI)
  apply (wp memcpy_type_wp)
  (* Remainder mostly clagged from the original proof above. *)
  apply clarsimp
  apply (rule conjI, clarsimp simp:no_overlap_def, blast)
  apply (rule_tac x="[deref s (byte_cast src),
                      deref s (byte_cast src +\<^sub>p 1),
                      deref s (byte_cast src +\<^sub>p 2),
                      deref s (byte_cast src +\<^sub>p 3)]" in exI)
  apply (rule conjI)
   apply (clarsimp simp:bytes_of_def bytes_at_def UINT_MAX_def)
   apply (case_tac "i = 0", clarsimp)
   apply (case_tac "i = 1", clarsimp)
   apply (case_tac "i = 2", clarsimp)
   apply (case_tac "i = 3", clarsimp)
   apply clarsimp
  apply clarsimp
  apply (subst h_val_not_id_update_bytes, clarsimp+)
  apply (clarsimp simp:h_val_def)
  apply (subgoal_tac "heap_list (hrs_mem (t_hrs_' s)) 4 (ptr_val src) =
                      deref s (byte_cast src) # (heap_list (hrs_mem (t_hrs_' s)) 3 (ptr_val src + 1))")
   prefer 2
   apply (clarsimp simp:h_val_def from_bytes_eq)
   apply (subst heap_list_rec[symmetric])
   apply simp
  apply (subgoal_tac "heap_list (hrs_mem (t_hrs_' s)) 3 (ptr_val src + 1) =
                      deref s (byte_cast src +\<^sub>p 1) # (heap_list (hrs_mem (t_hrs_' s)) 2 (ptr_val src + 2))")
   prefer 2
   apply (clarsimp simp:h_val_def ptr_add_def)
   apply (cut_tac h="hrs_mem (t_hrs_' s)" and p="ptr_val src + 1" and n=2 in heap_list_rec)
   apply (clarsimp simp: from_bytes_eq)
   apply (metis add.commute)
  apply clarsimp
  apply (subgoal_tac "heap_list (hrs_mem (t_hrs_' s)) 2 (ptr_val src + 2) =
                      deref s (byte_cast src +\<^sub>p 2) # (heap_list (hrs_mem (t_hrs_' s)) 1 (ptr_val src + 3))")
   prefer 2
   apply (cut_tac h="hrs_mem (t_hrs_' s)" and p="ptr_val src + 2" and n=3 in heap_list_rec)
   apply (clarsimp simp:h_val_def ptr_add_def from_bytes_eq)
   apply (metis (no_types, hide_lams) Suc_eq_plus1 heap_list_base heap_list_rec is_num_normalize(1)
                monoid_add_class.add.left_neutral one_add_one one_plus_numeral semiring_norm(3))
  apply (clarsimp simp:h_val_def ptr_add_def from_bytes_eq)
  done

lemma bytes_of_imp_at[simp]: "bytes_of s x bs \<Longrightarrow> bytes_at s x bs"
  by (clarsimp simp:bytes_of_def bytes_at_def)

lemma bytes_at_imp_of:
  fixes x :: "'a::mem_type ptr"
  shows "\<lbrakk>bytes_at s x bs; length bs = size_of TYPE('a)\<rbrakk> \<Longrightarrow> bytes_of s x bs"
  by (clarsimp simp:bytes_of_def bytes_at_def)

text \<open>
  Memcpying from a source to a destination via an intermediary does what it should. This is close to
  the desirable property we want for CAmkES systems; i.e. that copying into your IPC buffer on one
  side and then out on the other gives you back what you put in. Note that the type of the
  intermediate pointer is irrelevant and we don't need to assume that the source and final
  destination do not overlap.
\<close>
lemma memcpy_seq:
  fixes x :: "'a::mem_type ptr"
    and y :: "'b::mem_type ptr"
    and z :: "'a::mem_type ptr"
  shows "\<forall>s0 bs.
   \<lbrace>\<lambda>s. s = s0 \<and> sz = of_nat (size_of TYPE('a)) \<and>
        c_guard x \<and> c_guard y \<and> c_guard z \<and>
        no_wrap x (unat sz) \<and> no_wrap y (unat sz) \<and> no_wrap z (unat sz) \<and>
        no_overlap x y (unat sz) \<and> no_overlap y z (unat sz) \<and>
        bytes_of s x bs\<rbrace>
    do memcpy' (ptr_coerce y) (ptr_coerce x) sz;
       memcpy' (ptr_coerce z) (ptr_coerce y) sz
    od
   \<lbrace>\<lambda>r s. r = ptr_coerce z \<and> bytes_of s z bs\<rbrace>!"
  apply (rule allI)+
  apply (wp memcpy_wp)
  apply clarsimp
  apply (rule_tac x=bs in exI)
  apply clarsimp
  apply (rule conjI, clarsimp simp:bytes_of_def)
  apply clarsimp
  apply (rule_tac x=bs in exI)
  apply (rule conjI, clarsimp simp:bytes_of_def)
  apply clarsimp
  apply (rule bytes_at_imp_of)
   apply (clarsimp simp:bytes_of_def)+
  done

lemma update_ti_eq:
  fixes x :: "'a::mem_type"
    and y :: 'a
  shows "\<lbrakk>length bs = size_of TYPE('a); bs = bs'\<rbrakk>
          \<Longrightarrow> update_ti_t (typ_info_t TYPE('a)) bs x = update_ti_t (typ_info_t TYPE('a)) bs' y"
  by (clarsimp simp:upd)

lemma from_bytes_cong: "x = y \<Longrightarrow> from_bytes x = from_bytes y"
  by simp

declare from_bytes_eq [simp]

text \<open>
  If you dereference a pointer, the value you get is the same as the underlying bytes backing that
  memory.
\<close>
lemma val_eq_bytes:
  fixes x :: "'a::mem_type ptr"
  shows "deref s x = from_bytes (map (\<lambda>off. deref s (byte_cast x +\<^sub>p of_nat off)) [0..<size_of TYPE('a)])"
  apply (clarsimp simp:h_val_def ptr_add_def)
  apply (rule from_bytes_cong)
  apply (rule nth_equalityI)
   apply clarsimp+
  apply (subst heap_list_nth)
   apply clarsimp+
  done

lemma extract_list_elem: "i < n \<Longrightarrow> f i = (map f [0..<n]) ! i"
  apply (induct i)
   apply clarsimp+
  done

lemma update_deref:
  fixes x :: "'a::mem_type ptr"
  shows "size_of TYPE('a) = length bs \<Longrightarrow> deref (update_bytes s x bs) x = from_bytes bs"
  apply (clarsimp simp:update_bytes_def)
  apply (subst hrs_mem_update)
  apply (clarsimp simp:h_val_def)
  apply (subst heap_list_update)
   apply (metis less_imp_le max_size)
  apply clarsimp
  done

text \<open>
  The memcpy_int proof can now be completed more elegantly. Note that the body of this proof is more
  generic than the previous attempts and doesn't involve manually reasoning about each byte.
\<close>
lemma memcpy_int_wp'''[unfolded memcpy_int_spec_def]: "memcpy_int_spec dst src"
  unfolding memcpy_int_spec_def memcpy_int'_def
  apply (rule allI)
  apply (wp memcpy_type_wp)
  apply clarsimp
  apply (rule conjI, clarsimp simp:no_overlap_def, blast)
  apply (rule_tac x="map (\<lambda>i. deref s (byte_cast src +\<^sub>p of_nat i)) [0..<size_of TYPE(32sword)]" in exI)
  apply (rule conjI)
   apply (clarsimp simp:bytes_of_def bytes_at_def UINT_MAX_def)+
  apply (subst update_deref)
   apply clarsimp
  apply (cut_tac s=s and x=src in val_eq_bytes)
  apply clarsimp
  done

lemma bytes_at_heap_list:
  fixes x :: "'a::mem_type ptr"
  shows "\<lbrakk>n \<le> ADDR_MAX; no_wrap x n\<rbrakk>
          \<Longrightarrow> bytes_at s x (heap_list (hrs_mem (t_hrs_' s)) n (ptr_val x))"
  apply (clarsimp simp:bytes_at_def ptr_add_def h_val_def)
  apply (subst heap_list_nth)
   apply unat_arith
  apply clarsimp
  done

text \<open>
  A collection of useful type-generic implications for moving from the abstract heap to the concrete
  heap.
\<close>
definition
  is_valid_imp_c_guard :: "(lifted_globals \<Rightarrow> 'b::mem_type ptr \<Rightarrow> bool) \<Rightarrow> bool"
where
  "is_valid_imp_c_guard is_valid \<equiv> \<forall>s p. is_valid (lift_global_heap s) p \<longrightarrow> c_guard p"
definition
  is_valid_imp_no_null :: "(lifted_globals \<Rightarrow> 'b::mem_type ptr \<Rightarrow> bool) \<Rightarrow> bool"
where
  "is_valid_imp_no_null is_valid \<equiv>
     \<forall>s p. is_valid (lift_global_heap s) p \<longrightarrow> 0 \<notin> {ptr_val p..of_nat (size_of TYPE('b))}"
definition
  is_valid_imp_no_wrap :: "(lifted_globals \<Rightarrow> 'b::mem_type ptr \<Rightarrow> bool) \<Rightarrow> bool"
where
  "is_valid_imp_no_wrap is_valid \<equiv>
     \<forall>s p. is_valid (lift_global_heap s) p \<longrightarrow> no_wrap p (size_of TYPE('b))"
definition
  is_valid_imp_no_overlap :: "(lifted_globals \<Rightarrow> 'b::mem_type ptr \<Rightarrow> bool) \<Rightarrow> bool"
where
  "is_valid_imp_no_overlap is_valid \<equiv>
     \<forall>s p q. is_valid (lift_global_heap s) p \<and> is_valid (lift_global_heap s) q \<and> p \<noteq> q
               \<longrightarrow> no_overlap p q (size_of TYPE('b))"
definition
  is_valid_imp_heap_ptr_valid :: "(lifted_globals \<Rightarrow> 'b::mem_type ptr \<Rightarrow> bool) \<Rightarrow> bool"
where
  "is_valid_imp_heap_ptr_valid is_valid \<equiv>
     \<forall>s p. is_valid (lift_global_heap s) p \<longrightarrow> heap_ptr_valid (hrs_htd (t_hrs_' s)) p"

text \<open>We can easily discharge these for a given type.\<close>
lemma is_valid_w32_imp_c_guard[unfolded is_valid_imp_c_guard_def, simplified]:
    "is_valid_imp_c_guard is_valid_w32"
  unfolding is_valid_imp_c_guard_def
  apply clarsimp
  apply (subst (asm) lifted_globals_ext_simps)
  apply clarsimp
  apply (rule simple_lift_c_guard, force)
  done

lemma is_valid_w32_imp_no_null[unfolded is_valid_imp_no_null_def, simplified]:
    "is_valid_imp_no_null is_valid_w32"
  unfolding is_valid_imp_no_null_def
  apply clarsimp
  apply (subst (asm) lifted_globals_ext_simps)
  apply clarsimp
  apply (drule simple_lift_c_guard)
  apply (clarsimp simp:c_guard_def c_null_guard_def intvl_def)
  by force

lemma is_valid_w32_imp_no_wrap[unfolded is_valid_imp_no_wrap_def, simplified]:
    "is_valid_imp_no_wrap is_valid_w32"
  unfolding is_valid_imp_no_wrap_def no_wrap_def
  apply clarsimp
  apply (subst (asm) lifted_globals_ext_simps)
  apply clarsimp
  apply (drule simple_lift_c_guard)
  apply (clarsimp simp:c_guard_def c_null_guard_def intvl_def)
  done

lemma is_valid_w32_imp_no_overlap[unfolded is_valid_imp_no_overlap_def, simplified]:
    "is_valid_imp_no_overlap is_valid_w32"
  unfolding is_valid_imp_no_overlap_def no_wrap_def
  apply clarsimp
  apply (subst (asm) lifted_globals_ext_simps)+
  apply clarsimp
  apply (drule simple_lift_heap_ptr_valid)+
  apply (clarsimp simp:no_overlap_def)
  apply (cut_tac p=p and q=q and d="hrs_htd (t_hrs_' s)" in heap_ptr_valid_neq_disjoint)
     apply clarsimp+
  done

lemma is_valid_w32_imp_heap_ptr_valid[unfolded is_valid_imp_heap_ptr_valid_def, simplified]:
    "is_valid_imp_heap_ptr_valid is_valid_w32"
  unfolding is_valid_imp_heap_ptr_valid_def
  apply clarsimp
  apply (subst (asm) lifted_globals_ext_simps)
  apply clarsimp
  by (rule simple_lift_heap_ptr_valid, force)

text \<open>
  With that support in place, we can now prove a heap-abstracted call to memcpy of a type in a
  reasonably generic way. Note that we leverage the relationship between
  is_valid_*/lift_global_heap/simple_lift to transfer assumptions across the boundary between the
  abstract and concrete heaps.
\<close>
lemma
  fixes dst :: "32word ptr"
    and src :: "32word ptr"
  shows "\<forall>s0 x.
   \<lbrace>\<lambda>s. s = s0 \<and> is_valid_w32 s dst \<and> is_valid_w32 s src \<and> sz = of_nat (size_of TYPE(32word)) \<and>
        heap_w32 s src = x \<and> dst \<noteq> src\<rbrace>
     exec_concrete lift_global_heap (memcpy' (ptr_coerce dst) (ptr_coerce src) sz)
   \<lbrace>\<lambda>r s. r = ptr_coerce dst \<and> heap_w32 s dst = x\<rbrace>!"
  including nf_no_pre
  apply (rule allI)+
  apply (wp memcpy_wp)
  apply (clarsimp simp:is_valid_w32_imp_c_guard
                       is_valid_w32_imp_no_wrap
                       is_valid_w32_imp_no_overlap)
  apply (rule_tac x="map (\<lambda>i. deref s (byte_cast src +\<^sub>p of_nat i)) [0..<size_of TYPE(32word)]" in exI)
  apply clarsimp
  apply (rule conjI)
   apply (clarsimp simp:bytes_at_def UINT_MAX_def)
  apply clarsimp
  apply (subst lifted_globals_ext_simps(3))+
  apply (clarsimp simp:simple_lift_def is_valid_w32_imp_heap_ptr_valid)
  apply (rule conjI)
   apply clarsimp
   apply (subst update_deref)
    apply clarsimp+
   apply (cut_tac s=s and x=src in val_eq_bytes)
   apply clarsimp
  apply (clarsimp simp:update_bytes_def is_valid_w32_imp_heap_ptr_valid)
  done

text \<open>
  Let's do the same instantiation for a structure. Note that the proof text for the following lemmas
  is identical to the word 32 instantiation above. These could be straightforwardly abstracted into
  a locale which could be automatically interpreted with the use of generated proofs.
\<close>
lemma is_valid_my_structure_imp_c_guard[unfolded is_valid_imp_c_guard_def, simplified]:
    "is_valid_imp_c_guard is_valid_my_structure_C"
  unfolding is_valid_imp_c_guard_def
  apply clarsimp
  apply (subst (asm) lifted_globals_ext_simps)
  apply clarsimp
  apply (rule simple_lift_c_guard, force)
  done

lemma is_valid_my_structure_imp_no_null[unfolded is_valid_imp_no_null_def, simplified]:
    "is_valid_imp_no_null is_valid_my_structure_C"
  unfolding is_valid_imp_no_null_def
  apply clarsimp
  apply (subst (asm) lifted_globals_ext_simps)
  apply clarsimp
  apply (drule simple_lift_c_guard)
  apply (clarsimp simp:c_guard_def c_null_guard_def intvl_def)
  by force

lemma is_valid_my_structure_imp_no_wrap[unfolded is_valid_imp_no_wrap_def, simplified]:
    "is_valid_imp_no_wrap is_valid_my_structure_C"
  unfolding is_valid_imp_no_wrap_def no_wrap_def
  apply clarsimp
  apply (subst (asm) lifted_globals_ext_simps)
  apply clarsimp
  apply (drule simple_lift_c_guard)
  apply (clarsimp simp:c_guard_def c_null_guard_def intvl_def)
  done

lemma is_valid_my_structure_imp_no_overlap[unfolded is_valid_imp_no_overlap_def, simplified]:
    "is_valid_imp_no_overlap is_valid_my_structure_C"
  unfolding is_valid_imp_no_overlap_def no_wrap_def
  apply clarsimp
  apply (subst (asm) lifted_globals_ext_simps)+
  apply clarsimp
  apply (drule simple_lift_heap_ptr_valid)+
  apply (clarsimp simp:no_overlap_def)
  apply (cut_tac p=p and q=q and d="hrs_htd (t_hrs_' s)" in heap_ptr_valid_neq_disjoint)
     apply clarsimp+
  done

lemma is_valid_my_structure_imp_heap_ptr_valid[unfolded is_valid_imp_heap_ptr_valid_def, simplified]:
    "is_valid_imp_heap_ptr_valid is_valid_my_structure_C"
  unfolding is_valid_imp_heap_ptr_valid_def
  apply clarsimp
  apply (subst (asm) lifted_globals_ext_simps)
  apply clarsimp
  by (rule simple_lift_heap_ptr_valid, force)

text \<open>
  Again, we can now trivially transfer Hoare triple properties.
\<close>
lemma
  fixes dst :: "my_structure_C ptr"
    and src :: "my_structure_C ptr"
  shows "\<forall>s0 x.
   \<lbrace>\<lambda>s. s = s0 \<and> is_valid_my_structure_C s dst \<and> is_valid_my_structure_C s src \<and>
        heap_my_structure_C s src = x \<and> dst \<noteq> src\<rbrace>
     memcpy_struct' dst src
   \<lbrace>\<lambda>r s. r = dst \<and> heap_my_structure_C s dst = x\<rbrace>!"
  including nf_no_pre
  apply (rule allI)+
  unfolding memcpy_struct'_def
  apply (wp memcpy_wp)
  apply (clarsimp simp:is_valid_my_structure_imp_c_guard)
  apply (rule_tac x="map (\<lambda>i. deref s (byte_cast src +\<^sub>p of_nat i)) [0..<size_of TYPE(my_structure_C)]" in exI)
  apply (clarsimp simp:is_valid_my_structure_imp_no_wrap is_valid_my_structure_imp_no_overlap)
  apply (rule conjI)
   apply (clarsimp simp:bytes_at_def UINT_MAX_def)
  apply clarsimp
  apply (subst lifted_globals_ext_simps)+
  apply (clarsimp simp:simple_lift_def is_valid_my_structure_imp_heap_ptr_valid)
  apply (rule conjI)
   apply clarsimp
   apply (subst update_deref)
    apply clarsimp
   apply (cut_tac s=s and x=src in val_eq_bytes)
   apply clarsimp
  apply (clarsimp simp:update_bytes_def is_valid_my_structure_imp_heap_ptr_valid)
  done

end

end

author: NICTA


text:
(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section \<open>Cardinality of Partial Equivalence Relations\<close>

theory Card_Partial_Equiv_Relations
imports
  Card_Equiv_Relations
begin

subsection \<open>Definition of Partial Equivalence Relation\<close>

definition partial_equiv :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"
where
  "partial_equiv A R = (R \<subseteq> A \<times> A \<and> sym R \<and> trans R)"

lemma partial_equivI:
  assumes "R \<subseteq> A \<times> A" "sym R" "trans R"
  shows "partial_equiv A R"
using assms unfolding partial_equiv_def by auto

lemma partial_equiv_iff:
  shows "partial_equiv A R \<longleftrightarrow> (\<exists>A' \<subseteq> A. equiv A' R)"
proof
  assume "partial_equiv A R"
  from \<open>partial_equiv A R\<close> have "R `` A \<subseteq> A"
    unfolding partial_equiv_def by blast
  moreover have "equiv (R `` A) R"
  proof (rule equivI)
    from \<open>partial_equiv A R\<close> show "sym R"
      unfolding partial_equiv_def by blast
    from \<open>partial_equiv A R\<close> show "trans R"
      unfolding partial_equiv_def by blast
    show "refl_on (R `` A) R"
    proof (rule refl_onI)
      show "R \<subseteq> R `` A \<times> R `` A"
      proof
        fix p
        assume "p \<in> R"
        obtain x y where "p = (x, y)" by fastforce
        moreover have "x \<in> R `` A"
          using \<open>p \<in> R\<close> \<open>p = (x, y)\<close> \<open>partial_equiv A R\<close>
            partial_equiv_def sym_def by fastforce
        moreover have "y \<in> R `` A"
          using \<open>p \<in> R\<close> \<open>p = (x, y)\<close> \<open>R `` A \<subseteq> A\<close> \<open>x \<in> R `` A\<close> by blast
        ultimately show "p \<in> R `` A \<times> R `` A" by auto
      qed
    next
      fix y
      assume "y \<in> R `` A"
      from this obtain x where "(x, y) \<in> R" by auto
      from \<open>(x, y) \<in> R\<close> have "(y, x) \<in> R"
        using \<open>sym R\<close> by (meson symE)
      from \<open>(x, y) \<in> R\<close> \<open>(y, x) \<in> R\<close> show "(y, y) \<in> R"
        using \<open>trans R\<close> by (meson transE)
    qed
  qed
  ultimately show "\<exists>A'\<subseteq>A. equiv A' R" by blast
next
  assume "\<exists>A'\<subseteq>A. equiv A' R"
  from this obtain A' where "A' \<subseteq> A" and "equiv A' R" by blast
  show "partial_equiv A R"
  proof (rule partial_equivI)
    from \<open>equiv A' R\<close> \<open>A' \<subseteq> A\<close> show "R \<subseteq> A \<times> A"
      using equiv_class_eq_iff by fastforce
    from \<open>equiv A' R\<close> show "sym R"
      using equivE by blast
    from \<open>equiv A' R\<close> show "trans R"
      using equivE by blast
  qed
qed

subsection \<open>Construction of all Partial Equivalence Relations for a Given Set\<close>

definition all_partial_equivs_on :: "'a set \<Rightarrow> (('a \<times> 'a) set) set"
where
  "all_partial_equivs_on A =
    do {
      k \<leftarrow> {0..card A};
      A' \<leftarrow> {A'. A' \<subseteq> A \<and> card A' = k};
      {R. equiv A' R}
    }"

lemma all_partial_equivs_on:
  assumes "finite A"
  shows "all_partial_equivs_on A = {R. partial_equiv A R}"
proof
  show "all_partial_equivs_on A \<subseteq> {R. partial_equiv A R}"
  proof
    fix R
    assume "R \<in> all_partial_equivs_on A"
    from this obtain A' where "A' \<subseteq> A" and "equiv A' R"
      unfolding all_partial_equivs_on_def by auto
    from this have "partial_equiv A R"
      using partial_equiv_iff by blast
    from this show "R \<in> {R. partial_equiv A R}" ..
  qed
next
  show "{R. partial_equiv A R} \<subseteq> all_partial_equivs_on A"
  proof
    fix R
    assume "R \<in> {R. partial_equiv A R}"
    from this obtain A' where "A' \<subseteq> A" and "equiv A' R"
      using partial_equiv_iff by (metis mem_Collect_eq)
    moreover have "card A' \<in> {0..card A}"
      using \<open>A' \<subseteq> A\<close> \<open>finite A\<close> by (simp add: card_mono)
    ultimately show "R \<in> all_partial_equivs_on A"
      unfolding all_partial_equivs_on_def
      by (auto simp del: atLeastAtMost_iff)
  qed
qed

subsection \<open>Injectivity of the Set Construction\<close>

lemma equiv_inject:
  assumes "equiv A R" "equiv B R"
  shows "A = B"
proof -
  from assms have "R \<subseteq> A \<times> A" "R \<subseteq> B \<times> B" by (simp add: equiv_type)+
  moreover from assms have "\<forall>x\<in>A. (x, x) \<in> R" "\<forall>x\<in>B. (x, x) \<in> R"
    by (simp add: eq_equiv_class)+
  ultimately show ?thesis
    using mem_Sigma_iff subset_antisym subset_eq by blast
qed

lemma injectivity:
  assumes "(A' \<subseteq> A \<and> card A' = k) \<and> (A'' \<subseteq> A \<and> card A'' = k')"
  assumes "equiv A' R \<and> equiv A'' R'"
  assumes "R = R'"
  shows "A' = A''" "k = k'"
proof -
  from \<open>R = R'\<close> assms(2) show "A' = A''"
    using equiv_inject by fast
  from this assms(1) show "k = k'" by simp
qed

subsection \<open>Cardinality Theorem of Partial Equivalence Relations\<close>

theorem card_partial_equiv:
  assumes "finite A"
  shows "card {R. partial_equiv A R} = Bell (card A + 1)"
proof -
  let ?expr = "do {
      k \<leftarrow> {0..card A};
      A' \<leftarrow> {A'. A' \<subseteq> A \<and> card A' = k};
      {R. equiv A' R}
    }"
  have "card {R. partial_equiv A R} = card (all_partial_equivs_on A)"
    using \<open>finite A\<close> by (simp add: all_partial_equivs_on)
  also have "card (all_partial_equivs_on A) = card ?expr"
    unfolding all_partial_equivs_on_def ..
  also have "card ?expr = (\<Sum>k = 0..card A. (card A choose k) * Bell k)"
  proof -
    let "?S \<bind> ?comp" = ?expr
    {
      fix k
      assume k: "k \<in> {..card A}"
      let ?expr = "?comp k"
      let "?S \<bind> ?comp" = ?expr
      have "finite ?S" using \<open>finite A\<close> by simp
      moreover {
        fix A'
        assume A': "A' \<in> {A'. A' \<subseteq> A \<and> card A' = k}"
        from this have "A' \<subseteq> A" and "card A' = k" by auto
        let ?expr = "?comp A'"
        have "finite A'"
          using \<open>finite A\<close> \<open>A' \<subseteq> A\<close> by (simp add: finite_subset)
        have "card ?expr = Bell k"
          using \<open>finite A\<close> \<open>finite A'\<close> \<open>A' \<subseteq> A\<close> \<open>card A' = k\<close>
          by (simp add: card_equiv_rel_eq_Bell)
        moreover have "finite ?expr"
          using \<open>finite A'\<close> by (simp add: finite_equiv)
        ultimately have "finite ?expr \<and> card ?expr = Bell k" by blast
      } note inner = this
      moreover have "disjoint_family_on ?comp ?S"
        by (injectivity_solver rule: injectivity(1))
      moreover have "card ?S = card A choose k"
        using \<open>finite A\<close> by (simp add: n_subsets)
      ultimately have "card ?expr = (card A choose k) * Bell k" (is "_ = ?formula")
        by (subst card_bind_constant) auto
      moreover have "finite ?expr"
        using \<open>finite ?S\<close> inner by (auto intro!: finite_bind)
      ultimately have "finite ?expr \<and> card ?expr = ?formula" by blast
    }
    moreover have "finite ?S" by simp
    moreover have "disjoint_family_on ?comp ?S"
      by (injectivity_solver rule: injectivity(2))
    ultimately show "card ?expr = (\<Sum>k = 0..card A. (card A choose k) * Bell k)"
      by (subst card_bind) auto
  qed
  also have "\<dots> = (\<Sum>k\<le>card A. (card A choose k) * Bell k)"
    by (auto intro: sum.cong)
  also have "\<dots> = Bell (card A + 1)"
    using Bell_recursive_eq by simp
  finally show ?thesis .
qed

end

repo: PSL


text:
section \<open>Syntax of the Boogie language\<close>

theory Lang
  imports Main HOL.Real
begin

type_synonym fname = string (* function name *)
type_synonym vname = nat (* variable name, de-bruijn index *)
type_synonym pname = string (* procedure name *)

datatype lit =  LBool bool  | LInt int | LReal real

datatype binop = Eq | Neq | Add | Sub | Mul | Div | RealDiv | Mod | Lt | Le | Gt | Ge | And | Or | Imp | Iff
datatype unop = Not | UMinus

datatype prim_ty
 = TBool | TInt | TReal

type_synonym tcon_id = string (* type constructor id *)

datatype ty
  = TVar nat | (* type variables as de-bruijn indices *)
    TPrim prim_ty | (* primitive types *)
    TCon tcon_id "ty list" (* type constructor *)

primrec type_of_lit :: "lit \<Rightarrow> prim_ty"
  where
    "type_of_lit (LBool _) = TBool"
  | "type_of_lit (LInt _)  = TInt"
  | "type_of_lit (LReal _) = TReal"

datatype expr
  =
    Var vname
  | BVar nat (* de-bruijn index *)
  | Lit lit
  | UnOp unop "expr"
  | BinOp "(expr)" binop "(expr)" ("_ \<guillemotleft>_\<guillemotright> _" [80,0,81] 80)
  | FunExp fname "ty list" "(expr list)" (* second argument: type instantiation *)
  | CondExp expr expr expr
  | Old expr
(* value quantification *)
  | Forall ty expr
  | Exists ty expr
(* type quantification *)
  | ForallT expr
  | ExistsT expr

text \<open>We use a De-Bruijn encoding for bound variables \<^term>\<open>BVar\<close> and names for local/global variables
\<^term>\<open>Var\<close> (where names are natural numbers. While this setup suggests that we use the locally
nameless encoding, this is not the case (see Semantics.thy for more details).\<close>

(* multi-assign and multi-havoc not supported for now *)
datatype cmd
 = Assert expr
 | Assume expr
 | Assign vname expr
 | Havoc vname
 | ProcCall pname "expr list" "vname list"

text \<open>Function declarations: number of type parameters, argument types and return type\<close>
type_synonym fdecl = "(fname \<times> nat \<times> ty list \<times> ty)"
type_synonym fdecls = "fdecl list"

text \<open>Variable declarations: the optional expression represents the where-clause\<close>
type_synonym vdecl = "vname \<times> ty \<times> (expr option)"
type_synonym vdecls = "vdecl list"

text \<open>Type constructor declarations: number of arguments for each constructor\<close>
type_synonym tdecls = "(tcon_id \<times> nat) list"

text \<open>Basic blocks as a list of commands\<close>
type_synonym block = "cmd list"

text \<open>Identify nodes in the CFG by natural numbers. We always use block identifiers from 0 to N-1 when
there N blocks in the CFG\<close>
type_synonym node = "nat"

record mbodyCFG =
  entry :: "node"
  out_edges :: "(node list) list"
  node_to_block :: "block list"

text \<open>
Let N be the number of blocks in the CFG.
CFG of a procedure body is represented by:
  1) A block id indicating the entry of the CFG (\<^term>\<open>entry\<close>)
  2) The outgoing edges for each block. We represent this is as a list of length N (\<^term>\<open>out_edges\<close>).
     The outgoing block ids for the block with id i are given by i-th element in the list.
  3) A mapping from block ids to the corresponding list of commands. We represent this as a list of
     length N, where the list of commands for the block with id i are given by the i-th element in
     the list.
\<close>

text \<open>Procedure pre- and postconditions contain a boolean to indicate whether they are free (true) or
      checked (false).\<close>
record procedure =
  proc_ty_args :: nat
  proc_args :: vdecls
  proc_rets :: vdecls
  proc_modifs :: "vname list"
  proc_pres :: "(expr \<times> bool) list"
  proc_posts :: "(expr \<times> bool) list"
  proc_body :: "(vdecls \<times> mbodyCFG) option"

fun proc_checked_pres :: "procedure \<Rightarrow> expr list"
  where "proc_checked_pres p = map fst (filter (\<lambda>x. \<not> snd(x)) (proc_pres p))"

fun proc_free_pres :: "procedure \<Rightarrow> expr list"
  where "proc_free_pres p = map fst (filter (\<lambda>x. snd(x)) (proc_pres p))"

fun proc_all_pres :: "procedure \<Rightarrow> expr list"
  where "proc_all_pres p = map fst (proc_pres p)"

fun proc_checked_posts :: "procedure \<Rightarrow> expr list"
  where "proc_checked_posts p = map fst (filter (\<lambda>x. \<not> snd(x)) (proc_posts p))"

fun proc_all_posts :: "procedure \<Rightarrow> expr list"
  where "proc_all_posts p = map fst (proc_posts p)"

fun proc_free_posts :: "procedure \<Rightarrow> expr list"
  where "proc_free_posts p = map fst (filter (\<lambda>x. snd(x)) (proc_posts p))"

definition exprs_to_only_checked_spec :: "expr list \<Rightarrow> (expr \<times> bool) list"
  where "exprs_to_only_checked_spec es = map (\<lambda>e. (e, False)) es"
text \<open>For cases where there are no free pre- and postconditions, one can use
 \<^term>\<open>exprs_to_only_checked_spec\<close> to lift expressions to checked pre- and postconditions.
The proof generation currently does not support free specifications.\<close>

lemma exprs_to_only_checked_spec_1: "es = map fst (exprs_to_only_checked_spec es)"
  unfolding exprs_to_only_checked_spec_def
  by (induction es) auto

lemma exprs_to_only_checked_spec_2: "es = map fst (filter (\<lambda>x. \<not> snd x) (exprs_to_only_checked_spec es))"
  unfolding exprs_to_only_checked_spec_def
  by (induction es) auto

type_synonym pdecl = "pname \<times> procedure"

text \<open>An axiom is a boolean expression that can refer to constants.\<close>
type_synonym axiom = expr

record prog =
  prog_ty_constr :: tdecls
  prog_funcs :: fdecls
  prog_consts :: vdecls
  prog_globals :: vdecls
  prog_axioms :: "axiom list"
  prog_procs :: "pdecl list"

text \<open>Type declarations are ignored by the semantics (all possible types are taken into account, which
is more general and the resulting semantics can be reduced to the case where one only quantifies over
those types that can be constructed via the type declarations that appear in the program).\<close>

primrec closed :: "ty \<Rightarrow> bool"
  where
    "closed (TVar i) = False"
  | "closed (TPrim prim_ty) = True"
  | "closed (TCon tcon_id ty_args) = list_all closed ty_args"

end

author: gauravpartha