Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Equivalence.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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" ("\\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) where
"\\<^sub>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" ("\_:\<^sub>e _" [61,61] 60) where
"\n:\<^sub>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" ("_ |\\<^sub>e/ _"[61,61] 60) where
"A |\\<^sub>e t \ \n. |\n: A --> \n:\<^sub>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:\<^sub>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: "\\<^sub>e {P} e {Q} = (\n. \n:\<^sub>e (P,e,Q))"
apply (simp add: evalid_def envalid_def2)
apply blast
done

lemma cenvalid_def2:
  "A|\\<^sub>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 \ Null \ P t \
  (s -c0-n0\<rightarrow> t \<longrightarrow> P s \<longrightarrow> c0 = While (x) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> 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\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> 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 |\\<^sub>e t \ A |\\<^sub>e t)"
apply (tactic "split_all_tac \<^context> 1", rename_tac P e Q)
apply (rule hoare_ehoare.induct)
(*18*)
apply (tactic \<open>ALLGOALS (REPEAT o dresolve_tac \<^context> [@{thm all_conjunct2}, @{thm all3_conjunct2}])\<close>)
apply (tactic \<open>ALLGOALS (REPEAT o Rule_Insts.thin_tac \<^context> "hoare _ _" [])\<close>)
apply (tactic \<open>ALLGOALS (REPEAT o Rule_Insts.thin_tac \<^context> "ehoare _ _" [])\<close>)
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: "{} \\<^sub>e {P} e {Q} \ \\<^sub>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\<^sub>e   :: "expr => state => etriple" where
         "MGT\<^sub>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. {} |\\<^sub>e MGT\<^sub>e e Z \ \\<^sub>e {P} e {Q} \ {} \\<^sub>e {P} e {Q}"
apply (simp only: evalid_def2)
apply (unfold MGT\<^sub>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 \<turnstile> {(=) Z} While (x) c {\<lambda>t. \<exists>n. Z -While (x) c-n\<rightarrow> t}"
apply (rule_tac P' = "\Z s. (Z,s) \ ({(s,t). \n. s \ Null \ s -c-n\ t})\<^sup>*"
       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} \
(\<forall>Z. A |\<turnstile> {MGT c Z}) \<and> (\<forall>Z. A |\<turnstile>\<^sub>e MGT\<^sub>e e Z)"
apply (simp add: MGT_def MGT\<^sub>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: "\\<^sub>e {P} e {Q} \ {} \\<^sub>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 \\<^sub>e {\s. False} e {Q}"
apply (rule eThin)
apply (rule ehoare_relative_complete)
apply (auto simp add: evalid_def)
done

end

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.