(* 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.18 Sekunden
(vorverarbeitet)
¤
|
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.
|
