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"
 "Γ⊢⇘/F⇙ P c Q,A"  == "Γ,{}⊢⇘/F⇙ P c Q,A"

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

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




 "Γ⊢⇩t P c Q,A"   == "Γ⊢⇩t⇘/{}⇙ P c Q,A"
 "Γ⊢⇩t⇘/F⇙ P c Q,A"  == "Γ,{}⊢⇩t⇘/F⇙ P c Q,A"

 "Γ,Θ⊢⇩t P c Q"   == "Γ,Θ⊢⇩t⇘/{}⇙ P c Q"
 "Γ,Θ⊢⇩t⇘/F⇙ P c Q" == "Γ,Θ⊢⇩t⇘/F⇙ P c Q,{}"
 "Γ,Θ⊢⇩t P c Q,A"   == "Γ,Θ⊢⇩t⇘/{}⇙ P c Q,A"

 "Γ⊢⇩t P c Q"    == "Γ⊢⇩t⇘/{}⇙ P c Q"
 "Γ⊢⇩t⇘/F⇙ P c Q"  == "Γ,{}⊢⇩t⇘/F⇙ P c Q"
 "Γ⊢⇩t⇘/F⇙ P c Q"  <=  "Γ⊢⇩t⇘/F⇙ P c Q,{}"
 "Γ⊢⇩t P c Q"    <=  "Γ⊢⇩t P c Q,{}"


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

term "Γ⊢⇘/F⇙ P c Q"
term "Γ⊢⇘/F⇙ P c Q,A"

term "Γ,Θ⊢ P c Q"
term "Γ,Θ⊢⇘/F⇙ P c Q"

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


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

term "Γ⊢⇩t⇘/F⇙ P c Q"
term "Γ⊢⇩t⇘/F⇙ P c Q,A"

term "Γ,Θ⊢ P c Q"
term "Γ,Θ⊢⇩t⇘/F⇙ P c Q"

term "Γ,Θ⊢ P c Q,A"
term "Γ,Θ⊢⇩t⇘/F⇙ P 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: "(∀x∈⋃Z. {(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: "(∀x∈A ∪ 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) ⟶ (∃z∈Q. ∀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