# Theory Equivalence

Up to index of Isabelle/HOL/NanoJava

theory Equivalence
imports OpSem AxSem
begin

    (*  Title:      HOL/NanoJava/Equivalence.thy
        ID:         $Id: Equivalence.thy,v 1.13 2005/06/17 14:13:09 haftmann Exp $
        Author:     David von Oheimb
        Copyright   2001 Technische Universitaet Muenchen
    *)

    header "Equivalence of Operational and Axiomatic Semantics"

    theory Equivalence imports OpSem AxSem begin

    subsection "Validity"

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

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

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

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

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

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

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

    syntax (xsymbols)
       valid  :: "[assn,stmt, assn] => bool" ( "\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
      evalid  :: "[assn,expr,vassn] => bool" ("\<Turnstile>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
      nvalid  :: "[nat, triple          ] => bool" ("\<Turnstile>_: _"  [61,61] 60)
     envalid  :: "[nat,etriple          ] => bool" ("\<Turnstile>_:e _" [61,61] 60)
      nvalids :: "[nat,       triple set] => bool" ("|\<Turnstile>_: _"  [61,61] 60)
     cnvalids :: "[triple set,triple set] => bool" ("_ |\<Turnstile>/ _" [61,61] 60)
    cenvalid  :: "[triple set,etriple   ] => bool" ("_ |\<Turnstile>e/ _"[61,61] 60)

    lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) ≡ ∀s t. s -c-n-> t --> P s --> Q t"
    by (simp add: nvalid_def Let_def)

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

    lemma envalid_def2: "\<Turnstile>n:e (P,e,Q) ≡ ∀s v t. s -e\<succ>v-n-> t --> P s --> Q v t"
    by (simp add: envalid_def Let_def)

    lemma evalid_def2: "\<Turnstile>e {P} e {Q} = (∀n. \<Turnstile>n:e (P,e,Q))"
    apply (simp add: evalid_def envalid_def2)
    apply blast
    done

    lemma cenvalid_def2:
      "A|\<Turnstile>e (P,e,Q) = (∀n. |\<Turnstile>n: A --> (∀s v t. s -e\<succ>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: "\<Turnstile>0: (P,Impl M,Q)"
    by (clarsimp simp add: nvalid_def2)

    lemma Impl_nvalid_Suc: "\<Turnstile>n: (P,body M,Q) ==> \<Turnstile>Suc n: (P,Impl M,Q)"
    by (clarsimp simp add: nvalid_def2)

    lemma nvalid_SucD: "!!t. \<Turnstile>Suc n:t ==> \<Turnstile>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 |\<Turnstile> {(P,c,Q)} ≡ ∀n. |\<Turnstile>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 |\<turnstile> C --> A |\<Turnstile> C) ∧ (A |\<turnstile>e t --> A |\<Turnstile>e t)"
    apply (tactic "split_all_tac 1", rename_tac P e Q)
    apply (rule hoare_ehoare.induct)
    (*18*)
    apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *})
    apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x :  hoare") *})
    apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : ehoare") *})
    apply (simp_all only: cnvalid1_eq cenvalid_def2)
                     apply fast
                    apply fast
                   apply fast
                  apply (clarify,tactic "smp_tac 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: all_simps)
    apply (erule (1) impE)
    apply (drule (2) Impl_sound_lemma)
     apply  blast
    apply assumption
    done

    theorem hoare_sound: "{} \<turnstile> {P} c {Q} ==> \<Turnstile> {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: "{} \<turnstile>e {P} e {Q} ==> \<Turnstile>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"

    constdefs MGT    :: "stmt => state =>  triple"
             "MGT  c Z ≡ (λs. Z = s, c, λ  t. ∃n. Z -c-  n-> t)"
              MGTe   :: "expr => state => etriple"
             "MGTe e Z ≡ (λs. Z = s, e, λv t. ∃n. Z -e>v-n-> t)"
    syntax (xsymbols)
             MGTe    :: "expr => state => etriple" ("MGTe")
    syntax (HTML output)
             MGTe    :: "expr => state => etriple" ("MGTe")

    lemma MGF_implies_complete:
     "∀Z. {} |\<turnstile> { MGT c Z} ==> \<Turnstile>  {P} c {Q} ==> {} \<turnstile>  {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. {} |\<turnstile>e MGTe e Z ==> \<Turnstile>e {P} e {Q} ==> {} \<turnstile>e {P} e {Q}"
    apply (simp only: evalid_def2)
    apply (unfold MGTe_def)
    apply (erule hoare_ehoare.eConseq)
    apply (clarsimp simp add: envalid_def2)
    done

    declare exec_eval.intros[intro!]

    lemma MGF_Loop: "∀Z. A \<turnstile> {op = Z} c {λt. ∃n. Z -c-n-> t} ==>
      A \<turnstile> {op = 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 |\<turnstile> {MGT (Impl M) Z} ==>
     (∀Z. A |\<turnstile> {MGT c Z}) ∧ (∀Z. A |\<turnstile>e MGTe e Z)"
    apply (simp add: MGT_def MGTe_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 (rule_tac Q = "λa s. ∃n. Z -expr1\<succ>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 (rule_tac R = "λa v s. ∃n1 n2 t. Z -expr1\<succ>a-n1-> t ∧ t -expr2\<succ>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: "{} |\<turnstile> {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: "\<Turnstile> {P} c {Q} ==> {} \<turnstile> {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: "\<Turnstile>e {P} e {Q} ==> {} \<turnstile>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 \<turnstile> {λs. False} c {Q}"
    apply (rule cThin)
    apply (rule hoare_relative_complete)
    apply (auto simp add: valid_def)
    done

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

    end

### Validity

lemma nvalid_def2:

      |=n: (P, c, Q) == ∀s t. s -c-n-> t --> P s --> Q t

lemma valid_def2:

      |= {P} c {Q} = (∀n. |=n: (P, c, Q))

lemma envalid_def2:

      |=n:e (P, e, Q) == ∀s v t. s -e>v-n-> t --> P s --> Q v t

lemma evalid_def2:

      |=e {P} e {Q} = (∀n. |=n:e (P, e, Q))

lemma cenvalid_def2:

      A ||=e (P, e, Q) = (∀n. ||=n: A --> (∀s v t. s -e>v-n-> t --> P s --> Q v t))

### Soundness

lemma Impl_nvalid_0:

      |=0: (P, Impl M, Q)

lemma Impl_nvalid_Suc:

      |=n: (P, body M, Q) ==> |=Suc n: (P, Impl M, Q)

lemma nvalid_SucD:

      |=Suc n: t ==> |=n: t

lemma nvalids_SucD:

      Ball A (nvalid (Suc n)) ==> Ball A (nvalid n)

lemma Loop_sound_lemma:

      [| ∀s t. s -c-n-> t --> P s ∧ s<x> ≠ Null --> P t; s -c0.0-n0.0-> t; P s;
         c0.0 = While (x) c; n0.0 = n |]
      ==> P t ∧ t<x> = Null

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) |]
      ==> |=na: f z Cm

lemma all_conjunct2:

      ∀l. P' l ∧ P l ==> ∀l. P l

lemma all3_conjunct2:

      ∀a p l. P' a p l ∧ P a p l ==> ∀a p l. P a p l

lemma cnvalid1_eq:

      A ||= {(P, c, Q)} == ∀n. ||=n: A --> (∀s t. s -c-n-> t --> P s --> Q t)

lemma hoare_sound_main:

      (A ||- C --> A ||= C) ∧ (A ||-e t --> A ||=e t)

theorem hoare_sound:

      {} |- {P} c {Q} ==> |= {P} c {Q}

theorem ehoare_sound:

      {} |-e {P} e {Q} ==> |=e {P} e {Q}

### (Relative) Completeness

lemma MGF_implies_complete:

      [| ∀Z. {} ||- {MGT c Z}; |= {P} c {Q} |] ==> {} |- {P} c {Q}

lemma eMGF_implies_complete:

      [| ∀Z. {} ||-e MGTe e Z; |=e {P} e {Q} |] ==> {} |-e {P} e {Q}

lemma MGF_Loop:

      ∀Z. A |- {op = Z} c {%t. ∃n. Z -c-n-> t}
      ==> A |- {op = Z} While (x) c {%t. ∃n. Z -While (x) c-n-> t}

lemma MGF_lemma:

      ∀M Z. A ||- {MGT (Impl M) Z} ==> (∀Z. A ||- {MGT c Z}) ∧ (∀Z. A ||-e MGTe e Z)

lemma MGF_Impl:

      {} ||- {MGT (Impl M) Z}

theorem hoare_relative_complete:

      |= {P} c {Q} ==> {} |- {P} c {Q}

theorem ehoare_relative_complete:

      |=e {P} e {Q} ==> {} |-e {P} e {Q}

lemma cFalse:

      A |- {%s. False} c {Q}

lemma eFalse:

      A |-e {%s. False} e {Q}