Theory Hoare

(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2006-2008 Norbert Schirmer
*)

section ‹Auxiliary Definitions/Lemmas to Facilitate Hoare Logic›
theory Hoare imports HoarePartial HoareTotal begin


syntax

"_hoarep_emptyFaults"::
"[('s,'p,'f) body,('s,'p) quadruple set,
   'f set,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
    ("(3_,_/ (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)

"_hoarep_emptyCtx"::
"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
    ("(3_/⊢⇘'/_ (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)

"_hoarep_emptyCtx_emptyFaults"::
"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
    ("(3_/ (_/ (_)/ _,/_))" [61,1000,20,1000,1000]60)

"_hoarep_noAbr"::
"[('s,'p,'f) body,('s,'p) quadruple set,'f set,
    's assn,('s,'p,'f) com, 's assn] => bool"
    ("(3_,_/⊢⇘'/_ (_/ (_)/ _))" [61,60,60,1000,20,1000]60)

"_hoarep_noAbr_emptyFaults"::
"[('s,'p,'f) body,('s,'p) quadruple set,'s assn,('s,'p,'f) com, 's assn] => bool"
    ("(3_,_/ (_/ (_)/ _))" [61,60,1000,20,1000]60)

"_hoarep_emptyCtx_noAbr"::
"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn] => bool"
    ("(3_/⊢⇘'/_ (_/ (_)/ _))" [61,60,1000,20,1000]60)

"_hoarep_emptyCtx_noAbr_emptyFaults"::
"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn] => bool"
    ("(3_/ (_/ (_)/ _))" [61,1000,20,1000]60)



"_hoaret_emptyFaults"::
"[('s,'p,'f) body,('s,'p) quadruple set,
    's assn,('s,'p,'f) com, 's assn,'s assn] => bool"
    ("(3_,_/t (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)

"_hoaret_emptyCtx"::
"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
    ("(3_/t⇘'/_ (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)

"_hoaret_emptyCtx_emptyFaults"::
"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
    ("(3_/t (_/ (_)/ _,/_))" [61,1000,20,1000,1000]60)

"_hoaret_noAbr"::
"[('s,'p,'f) body,'f set, ('s,'p) quadruple set,
    's assn,('s,'p,'f) com, 's assn] => bool"
    ("(3_,_/t⇘'/_ (_/ (_)/ _))" [61,60,60,1000,20,1000]60)

"_hoaret_noAbr_emptyFaults"::
"[('s,'p,'f) body,('s,'p) quadruple set,'s assn,('s,'p,'f) com, 's assn] => bool"
    ("(3_,_/t (_/ (_)/ _))" [61,60,1000,20,1000]60)

"_hoaret_emptyCtx_noAbr"::
"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn] => bool"
    ("(3_/t⇘'/_ (_/ (_)/ _))" [61,60,1000,20,1000]60)

"_hoaret_emptyCtx_noAbr_emptyFaults"::
"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn] => bool"
    ("(3_/t (_/ (_)/ _))" [61,1000,20,1000]60)


syntax (ASCII)

"_hoarep_emptyFaults"::
"[('s,'p,'f) body,('s,'p) quadruple set,
     's assn,('s,'p,'f) com, 's assn,'s assn]  bool"
   ("(3_,_/|- (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)

"_hoarep_emptyCtx"::
"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
   ("(3_/|-'/_ (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)

"_hoarep_emptyCtx_emptyFaults"::
"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
   ("(3_/|-(_/ (_)/ _,/_))" [61,1000,20,1000,1000]60)

"_hoarep_noAbr"::
"[('s,'p,'f) body,('s,'p) quadruple set,'f set,
   's assn,('s,'p,'f) com, 's assn] => bool"
   ("(3_,_/|-'/_ (_/ (_)/ _))" [61,60,60,1000,20,1000]60)

"_hoarep_noAbr_emptyFaults"::
"[('s,'p,'f) body,('s,'p) quadruple set,'s assn,('s,'p,'f) com, 's assn] => bool"
   ("(3_,_/|-(_/ (_)/ _))" [61,60,1000,20,1000]60)

"_hoarep_emptyCtx_noAbr"::
"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn] => bool"
   ("(3_/|-'/_ (_/ (_)/ _))" [61,60,1000,20,1000]60)

"_hoarep_emptyCtx_noAbr_emptyFaults"::
"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn] => bool"
   ("(3_/|-(_/ (_)/ _))" [61,1000,20,1000]60)

"_hoaret_emptyFault"::
"[('s,'p,'f) body,('s,'p) quadruple set,
     's assn,('s,'p,'f) com, 's assn,'s assn] => bool"
   ("(3_,_/|-t (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)

"_hoaret_emptyCtx"::
"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
   ("(3_/|-t'/_ (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)

"_hoaret_emptyCtx_emptyFaults"::
"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
   ("(3_/|-t(_/ (_)/ _,/_))" [61,1000,20,1000,1000]60)

"_hoaret_noAbr"::
"[('s,'p,'f) body,('s,'p) quadruple set,'f set,
   's assn,('s,'p,'f) com, 's assn] => bool"
   ("(3_,_/|-t'/_ (_/ (_)/ _))" [61,60,60,1000,20,1000]60)

"_hoaret_noAbr_emptyFaults"::
"[('s,'p,'f) body,('s,'p) quadruple set,'s assn,('s,'p,'f) com, 's assn] => bool"
   ("(3_,_/|-t(_/ (_)/ _))" [61,60,1000,20,1000]60)

"_hoaret_emptyCtx_noAbr"::
"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn] => bool"
   ("(3_/|-t'/_ (_/ (_)/ _))" [61,60,1000,20,1000]60)

"_hoaret_emptyCtx_noAbr_emptyFaults"::
"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn] => bool"
   ("(3_/|-t(_/ (_)/ _))" [61,1000,20,1000]60)

translations


 "Γ P c Q,A"  == "Γ⊢⇘/{}P c Q,A"
 "Γ⊢⇘/FP c Q,A"  == "Γ,{}⊢⇘/FP c Q,A"

 "Γ,Θ P c Q"  == "Γ,Θ⊢⇘/{}P c Q"
 "Γ,Θ⊢⇘/FP c Q"  == "Γ,Θ⊢⇘/FP c Q,{}"
 "Γ,Θ P c Q,A" == "Γ,Θ⊢⇘/{}P c Q,A"

 "Γ P c Q"    ==  "Γ⊢⇘/{}P c Q"
 "Γ⊢⇘/FP c Q"  == "Γ,{}⊢⇘/FP c Q"
 "Γ⊢⇘/FP c Q"  <=  "Γ⊢⇘/FP c Q,{}"
 "Γ P c Q"    <=  "Γ P c Q,{}"




 "Γt P c Q,A"   == "Γt⇘/{}P c Q,A"
 "Γt⇘/FP c Q,A"  == "Γ,{}t⇘/FP c Q,A"

 "Γ,Θt P c Q"   == "Γ,Θt⇘/{}P c Q"
 "Γ,Θt⇘/FP c Q" == "Γ,Θt⇘/FP c Q,{}"
 "Γ,Θt P c Q,A"   == "Γ,Θt⇘/{}P c Q,A"

 "Γt P c Q"    == "Γt⇘/{}P c Q"
 "Γt⇘/FP c Q"  == "Γ,{}t⇘/FP c Q"
 "Γt⇘/FP c Q"  <=  "Γt⇘/FP c Q,{}"
 "Γt P c Q"    <=  "Γt P c Q,{}"


term "Γ P c Q"
term "Γ P c Q,A"

term "Γ⊢⇘/FP c Q"
term "Γ⊢⇘/FP c Q,A"

term "Γ,Θ P c Q"
term "Γ,Θ⊢⇘/FP c Q"

term "Γ,Θ P c Q,A"
term "Γ,Θ⊢⇘/FP c Q,A"


term "Γt P c Q"
term "Γt P c Q,A"

term "Γt⇘/FP c Q"
term "Γt⇘/FP c Q,A"

term "Γ,Θ P c Q"
term "Γ,Θt⇘/FP c Q"

term "Γ,Θ P c Q,A"
term "Γ,Θt⇘/FP c Q,A"


locale hoare =
  fixes Γ::"('s,'p,'f) body"


primrec assoc:: "('a ×'b) list  'a  'b "
where
"assoc [] x = undefined" |
"assoc (p#ps) x = (if fst p = x then (snd p) else assoc ps x)"

lemma conjE_simp: "(P  Q  PROP R)  (P  Q  PROP R)"
  by rule simp_all

lemma CollectInt_iff: "{s. P s}  {s. Q s} = {s. P s  Q s}"
  by auto

lemma Compl_Collect:"-(Collect b) = {x. ¬(b x)}"
  by fastforce

lemma Collect_False: "{s. False} = {}"
  by simp

lemma Collect_True: "{s. True} = UNIV"
  by simp

lemma triv_All_eq: "x. P  P"
  by simp

lemma triv_Ex_eq: "x. P  P"
  by simp

lemma Ex_True: "b. b"
   by blast

lemma Ex_False: "b. ¬b"
  by blast

definition mex::"('a  bool)  bool"
  where "mex P = Ex P"

definition meq::"'a  'a  bool"
  where "meq s Z = (s = Z)"

lemma subset_unI1: "A  B  A  B  C"
  by blast

lemma subset_unI2: "A  C  A  B  C"
  by blast

lemma split_paired_UN: "(p. (P p)) = (a b. (P (a,b)))"
  by auto

lemma in_insert_hd: "f  insert f X"
  by simp

lemma lookup_Some_in_dom: "Γ p = Some bdy  p  dom Γ"
  by auto

lemma unit_object: "(u::unit. P u) = P ()"
  by auto

lemma unit_ex: "(u::unit. P u) = P ()"
  by auto

lemma unit_meta: "((u::unit). PROP P u)  PROP P ()"
  by auto

lemma unit_UN: "(z::unit. P z) = P ()"
  by auto

lemma subset_singleton_insert1: "y = x  {y}  insert x A"
  by auto

lemma subset_singleton_insert2: "{y}  A  {y}  insert x A"
  by auto

lemma in_Specs_simp: "(xZ. {(P Z, p, Q Z, A Z)}. Prop x) =
       (Z. Prop (P Z,p,Q Z,A Z))"
  by auto

lemma in_set_Un_simp: "(xA  B. P x) = ((x  A. P x)  (x  B. P x))"
  by auto

lemma split_all_conj: "(x. P x  Q x) = ((x. P x)  (x. Q x))"
  by blast

lemma image_Un_single_simp: "f ` (Z. {P Z}) = (Z. {f (P Z)}) "
  by auto



lemma measure_lex_prod_def':
  "f <*mlex*> r  ({(x,y). (x,y)  measure f  f x=f y  (x,y)   r})"
  by (auto simp add: mlex_prod_def inv_image_def)

lemma in_measure_iff: "(x,y)  measure f = (f x < f y)"
  by (simp add: measure_def inv_image_def)

lemma in_lex_iff:
  "((a,b),(x,y))  r <*lex*> s = ((a,x)  r  (a=x  (b,y)s))"
  by (simp add: lex_prod_def)

lemma in_mlex_iff:
  "(x,y)  f <*mlex*> r = (f x < f y  (f x=f y  (x,y)  r))"
  by (simp add: measure_lex_prod_def' in_measure_iff)

lemma in_inv_image_iff: "(x,y)  inv_image r f = ((f x, f y)  r)"
  by (simp add: inv_image_def)

text ‹This is actually the same as @{thm [source] wf_mlex}. However, this basic
proof took me so long that I'm not willing to delete it.
›
lemma wf_measure_lex_prod [simp,intro]:
  assumes wf_r: "wf r"
  shows "wf (f <*mlex*> r)"
proof (rule ccontr)
  assume " ¬ wf (f <*mlex*> r)"
  then
  obtain g where "i. (g (Suc i), g i)  f <*mlex*> r"
    by (auto simp add: wf_iff_no_infinite_down_chain)
  hence g: "i. (g (Suc i), g i)  measure f 
    f (g (Suc i)) = f (g i)  (g (Suc i), g i)  r"
    by (simp add: measure_lex_prod_def')
  hence le_g: "i. f (g (Suc i))  f (g i)"
    by (auto simp add: in_measure_iff order_le_less)
  have "wf (measure f)"
    by simp
  hence " Q. (x. x  Q)  (zQ. y. (y, z)  measure f  y  Q)"
    by (simp add: wf_eq_minimal)
  from this [rule_format, of "g ` UNIV"]
  have "z. z  range g  (y. (y, z)  measure f  y  range g)"
    by auto
  then obtain z where
    z: "z  range g" and
    min_z: "y. f y < f z  y  range g"
    by (auto simp add: in_measure_iff)
  from z obtain k where
    k: "z = g k"
    by auto
  have "i. k  i  f (g i) = f (g k)"
  proof (intro allI impI)
    fix i
    assume "k  i" then show "f (g i) = f (g k)"
    proof (induct i)
      case 0
      have "k  0" by fact hence "k = 0" by simp
      thus "f (g 0) = f (g k)"
        by simp
    next
      case (Suc n)
      have k_Suc_n: "k  Suc n" by fact
      then show "f (g (Suc n)) = f (g k)"
      proof (cases "k = Suc n")
        case True
        thus ?thesis by simp
      next
        case False
        with k_Suc_n
        have "k  n"
          by simp
        with Suc.hyps
        have n_k: "f (g n) = f (g k)" by simp
        from le_g have le: "f (g (Suc n))  f (g n)"
          by simp
        show ?thesis
        proof (cases "f (g (Suc n)) = f (g n)")
          case True with n_k show ?thesis by simp
        next
          case False
          with le have "f (g (Suc n)) < f (g n)"
            by simp
          with n_k k have "f (g (Suc n)) < f z"
            by simp
          with min_z have "g (Suc n)  range g"
            by blast
          hence False by simp
          thus ?thesis
            by simp
        qed
      qed
    qed
  qed
  with k [symmetric] have "i. k  i  f (g i) = f z"
    by simp
  hence "i. k  i  f (g (Suc i)) = f (g i)"
    by simp
  with g have "i. k  i  (g (Suc i),(g i))  r"
    by (auto simp add: in_measure_iff order_less_le )
  hence "i. (g (Suc (i+k)),(g (i+k)))  r"
    by simp
  then
  have "f. i. (f (Suc i), f i)  r"
    by - (rule exI [where x="λi. g (i+k)"],simp)
  with wf_r show False
    by (simp add: wf_iff_no_infinite_down_chain)
qed

lemmas all_imp_to_ex = all_simps (5)
(*"⋀P Q. (∀x. P x ⟶ Q) = ((∃x. P x) ⟶ Q)"

 Avoid introduction of existential quantification of states on negative
 position.
*)

lemma all_imp_eq_triv: "(x. x = k  Q) = Q"
                       "(x. k = x  Q) = Q"
  by auto

end