Theory Equivalence

(*  Title:      HOL/NanoJava/Equivalence.thy
    Author:     David von Oheimb
    Copyright   2001 Technische Universitaet Muenchen
*)

section "Equivalence of Operational and Axiomatic Semantics"

theory Equivalence imports OpSem AxSem begin

subsection "Validity"

definition valid :: "[assn,stmt, assn] => bool" ("⊨ {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) where
 "⊨  {P} c {Q} ≡ ∀s   t. P s --> (∃n. s -c  -n→ t) --> Q   t"

definition evalid   :: "[assn,expr,vassn] => bool" ("⊨⇩e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) where
 "⊨⇩e {P} e {Q} ≡ ∀s v t. P s --> (∃n. s -e≻v-n→ t) --> Q v t"

definition nvalid   :: "[nat, triple    ] => bool" ("⊨_: _" [61,61] 60) where
 "⊨n:  t ≡ let (P,c,Q) = t in ∀s   t. s -c  -n→ t --> P s --> Q   t"

definition envalid   :: "[nat,etriple    ] => bool" ("⊨_:⇩e _" [61,61] 60) where
 "⊨n:⇩e t ≡ let (P,e,Q) = t in ∀s v t. s -e≻v-n→ t --> P s --> Q v t"

definition nvalids :: "[nat,       triple set] => bool" ("|⊨_: _" [61,61] 60) where
 "|⊨n: T ≡ ∀t∈T. ⊨n: t"

definition cnvalids :: "[triple set,triple set] => bool" ("_ |⊨/ _" [61,61] 60) where
 "A |⊨  C ≡ ∀n. |⊨n: A --> |⊨n: C"

definition cenvalid  :: "[triple set,etriple   ] => bool" ("_ |⊨⇩e/ _"[61,61] 60) where
 "A |⊨⇩e t ≡ ∀n. |⊨n: A --> ⊨n:⇩e t"

lemma nvalid_def2: "⊨n: (P,c,Q) ≡ ∀s t. s -c-n→ t ⟶ P s ⟶ Q t"
by (simp add: nvalid_def Let_def)

lemma valid_def2: "⊨ {P} c {Q} = (∀n. ⊨n: (P,c,Q))"
apply (simp add: valid_def nvalid_def2)
apply blast
done

lemma envalid_def2: "⊨n:⇩e (P,e,Q) ≡ ∀s v t. s -e≻v-n→ t ⟶ P s ⟶ Q v t"
by (simp add: envalid_def Let_def)

lemma evalid_def2: "⊨⇩e {P} e {Q} = (∀n. ⊨n:⇩e (P,e,Q))"
apply (simp add: evalid_def envalid_def2)
apply blast
done

lemma cenvalid_def2: 
  "A|⊨⇩e (P,e,Q) = (∀n. |⊨n: A ⟶ (∀s v t. s -e≻v-n→ t ⟶ P s ⟶ Q v t))"
by(simp add: cenvalid_def envalid_def2) 


subsection "Soundness"

declare exec_elim_cases [elim!] eval_elim_cases [elim!]

lemma Impl_nvalid_0: "⊨0: (P,Impl M,Q)"
by (clarsimp simp add: nvalid_def2)

lemma Impl_nvalid_Suc: "⊨n: (P,body M,Q) ⟹ ⊨Suc n: (P,Impl M,Q)"
by (clarsimp simp add: nvalid_def2)

lemma nvalid_SucD: "⋀t. ⊨Suc n:t ⟹ ⊨n:t"
by (force simp add: split_paired_all nvalid_def2 intro: exec_mono)

lemma nvalids_SucD: "Ball A (nvalid (Suc n)) ⟹  Ball A (nvalid n)"
by (fast intro: nvalid_SucD)

lemma Loop_sound_lemma [rule_format (no_asm)]: 
"∀s t. s -c-n→ t ⟶ P s ∧ s<x> ≠ Null ⟶ P t ⟹ 
  (s -c0-n0→ t ⟶ P s ⟶ c0 = While (x) c ⟶ n0 = n ⟶ P t ∧ t<x> = Null)"
apply (rule_tac ?P2.1="%s e v n t. True" in exec_eval.induct [THEN conjunct1])
apply clarsimp+
done

lemma Impl_sound_lemma: 
"⟦∀z n. Ball (A ∪ B) (nvalid n) ⟶ Ball (f z ` Ms) (nvalid n); 
  Cm∈Ms; Ball A (nvalid na); Ball B (nvalid na)⟧ ⟹ nvalid na (f z Cm)"
by blast

lemma all_conjunct2: "∀l. P' l ∧ P l ⟹ ∀l. P l"
by fast

lemma all3_conjunct2: 
  "∀a p l. (P' a p l ∧ P a p l) ⟹ ∀a p l. P a p l"
by fast

lemma cnvalid1_eq: 
  "A |⊨ {(P,c,Q)} ≡ ∀n. |⊨n: A ⟶ (∀s t. s -c-n→ t ⟶ P s ⟶ Q t)"
by(simp add: cnvalids_def nvalids_def nvalid_def2)

lemma hoare_sound_main:"⋀t. (A |⊢ C ⟶ A |⊨ C) ∧ (A |⊢⇩e t ⟶ A |⊨⇩e t)"
apply (tactic "split_all_tac \<^context> 1", rename_tac P e Q)
apply (rule hoare_ehoare.induct)
(*18*)
apply (tactic ‹ALLGOALS (REPEAT o dresolve_tac \<^context> [@{thm all_conjunct2}, @{thm all3_conjunct2}])›)
apply (tactic ‹ALLGOALS (REPEAT o Rule_Insts.thin_tac \<^context> "hoare _ _" [])›)
apply (tactic ‹ALLGOALS (REPEAT o Rule_Insts.thin_tac \<^context> "ehoare _ _" [])›)
apply (simp_all only: cnvalid1_eq cenvalid_def2)
                 apply fast
                apply fast
               apply fast
              apply (clarify,tactic "smp_tac \<^context> 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
             apply fast
            apply fast
           apply fast
          apply fast
         apply fast
        apply fast
       apply (clarsimp del: Meth_elim_cases) (* Call *)
      apply (force del: Impl_elim_cases)
     defer
     prefer 4 apply blast (*  Conseq *)
    prefer 4 apply blast (* eConseq *)
   apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def)
   apply blast
  apply blast
 apply blast
apply (rule allI)
apply (rule_tac x=Z in spec)
apply (induct_tac "n")
 apply  (clarify intro!: Impl_nvalid_0)
apply (clarify  intro!: Impl_nvalid_Suc)
apply (drule nvalids_SucD)
apply (simp only: HOL.all_simps)
apply (erule (1) impE)
apply (drule (2) Impl_sound_lemma)
 apply  blast
apply assumption
done

theorem hoare_sound: "{} ⊢ {P} c {Q} ⟹ ⊨ {P} c {Q}"
apply (simp only: valid_def2)
apply (drule hoare_sound_main [THEN conjunct1, rule_format])
apply (unfold cnvalids_def nvalids_def)
apply fast
done

theorem ehoare_sound: "{} ⊢⇩e {P} e {Q} ⟹ ⊨⇩e {P} e {Q}"
apply (simp only: evalid_def2)
apply (drule hoare_sound_main [THEN conjunct2, rule_format])
apply (unfold cenvalid_def nvalids_def)
apply fast
done


subsection "(Relative) Completeness"

definition MGT :: "stmt => state => triple" where
         "MGT  c Z ≡ (λs. Z = s, c, λ  t. ∃n. Z -c-  n→ t)"

definition MGT⇩e   :: "expr => state => etriple" where
         "MGT⇩e e Z ≡ (λs. Z = s, e, λv t. ∃n. Z -e≻v-n→ t)"

lemma MGF_implies_complete:
 "∀Z. {} |⊢ { MGT c Z} ⟹ ⊨  {P} c {Q} ⟹ {} ⊢  {P} c {Q}"
apply (simp only: valid_def2)
apply (unfold MGT_def)
apply (erule hoare_ehoare.Conseq)
apply (clarsimp simp add: nvalid_def2)
done

lemma eMGF_implies_complete:
 "∀Z. {} |⊢⇩e MGT⇩e e Z ⟹ ⊨⇩e {P} e {Q} ⟹ {} ⊢⇩e {P} e {Q}"
apply (simp only: evalid_def2)
apply (unfold MGT⇩e_def)
apply (erule hoare_ehoare.eConseq)
apply (clarsimp simp add: envalid_def2)
done

declare exec_eval.intros[intro!]

lemma MGF_Loop: "∀Z. A ⊢ {(=) Z} c {λt. ∃n. Z -c-n→ t} ⟹ 
  A ⊢ {(=) Z} While (x) c {λt. ∃n. Z -While (x) c-n→ t}"
apply (rule_tac P' = "λZ s. (Z,s) ∈ ({(s,t). ∃n. s<x> ≠ Null ∧ s -c-n→ t})⇧*"
       in hoare_ehoare.Conseq)
apply  (rule allI)
apply  (rule hoare_ehoare.Loop)
apply  (erule hoare_ehoare.Conseq)
apply  clarsimp
apply  (blast intro:rtrancl_into_rtrancl)
apply (erule thin_rl)
apply clarsimp
apply (erule_tac x = Z in allE)
apply clarsimp
apply (erule converse_rtrancl_induct)
apply  blast
apply clarsimp
apply (drule (1) exec_exec_max)
apply (blast del: exec_elim_cases)
done

lemma MGF_lemma: "∀M Z. A |⊢ {MGT (Impl M) Z} ⟹ 
 (∀Z. A |⊢ {MGT c Z}) ∧ (∀Z. A |⊢⇩e MGT⇩e e Z)"
apply (simp add: MGT_def MGT⇩e_def)
apply (rule stmt_expr.induct)
apply (rule_tac [!] allI)

apply (rule Conseq1 [OF hoare_ehoare.Skip])
apply blast

apply (rule hoare_ehoare.Comp)
apply  (erule spec)
apply (erule hoare_ehoare.Conseq)
apply clarsimp
apply (drule (1) exec_exec_max)
apply blast

apply (erule thin_rl)
apply (rule hoare_ehoare.Cond)
apply  (erule spec)
apply (rule allI)
apply (simp)
apply (rule conjI)
apply  (rule impI, erule hoare_ehoare.Conseq, clarsimp, drule (1) eval_exec_max,
        erule thin_rl, erule thin_rl, force)+

apply (erule MGF_Loop)

apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.LAss])
apply fast

apply (erule thin_rl)
apply (rename_tac expr1 u v Z, rule_tac Q = "λa s. ∃n. Z -expr1≻Addr a-n→ s" in hoare_ehoare.FAss)
apply  (drule spec)
apply  (erule eConseq2)
apply  fast
apply (rule allI)
apply (erule hoare_ehoare.eConseq)
apply clarsimp
apply (drule (1) eval_eval_max)
apply blast

apply (simp only: split_paired_all)
apply (rule hoare_ehoare.Meth)
apply (rule allI)
apply (drule spec, drule spec, erule hoare_ehoare.Conseq)
apply blast

apply (simp add: split_paired_all)

apply (rule eConseq1 [OF hoare_ehoare.NewC])
apply blast

apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.Cast])
apply fast

apply (rule eConseq1 [OF hoare_ehoare.LAcc])
apply blast

apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.FAcc])
apply fast

apply (rename_tac expr1 u expr2 Z)
apply (rule_tac R = "λa v s. ∃n1 n2 t. Z -expr1≻a-n1→ t ∧ t -expr2≻v-n2→ s" in
                hoare_ehoare.Call)
apply   (erule spec)
apply  (rule allI)
apply  (erule hoare_ehoare.eConseq)
apply  clarsimp
apply  blast
apply (rule allI)+
apply (rule hoare_ehoare.Meth)
apply (rule allI)
apply (drule spec, drule spec, erule hoare_ehoare.Conseq)
apply (erule thin_rl, erule thin_rl)
apply (clarsimp del: Impl_elim_cases)
apply (drule (2) eval_eval_exec_max)
apply (force del: Impl_elim_cases)
done

lemma MGF_Impl: "{} |⊢ {MGT (Impl M) Z}"
apply (unfold MGT_def)
apply (rule Impl1')
apply  (rule_tac [2] UNIV_I)
apply clarsimp
apply (rule hoare_ehoare.ConjI)
apply clarsimp
apply (rule ssubst [OF Impl_body_eq])
apply (fold MGT_def)
apply (rule MGF_lemma [THEN conjunct1, rule_format])
apply (rule hoare_ehoare.Asm)
apply force
done

theorem hoare_relative_complete: "⊨ {P} c {Q} ⟹ {} ⊢ {P} c {Q}"
apply (rule MGF_implies_complete)
apply  (erule_tac [2] asm_rl)
apply (rule allI)
apply (rule MGF_lemma [THEN conjunct1, rule_format])
apply (rule MGF_Impl)
done

theorem ehoare_relative_complete: "⊨⇩e {P} e {Q} ⟹ {} ⊢⇩e {P} e {Q}"
apply (rule eMGF_implies_complete)
apply  (erule_tac [2] asm_rl)
apply (rule allI)
apply (rule MGF_lemma [THEN conjunct2, rule_format])
apply (rule MGF_Impl)
done

lemma cFalse: "A ⊢ {λs. False} c {Q}"
apply (rule cThin)
apply (rule hoare_relative_complete)
apply (auto simp add: valid_def)
done

lemma eFalse: "A ⊢⇩e {λs. False} e {Q}"
apply (rule eThin)
apply (rule ehoare_relative_complete)
apply (auto simp add: evalid_def)
done

end