--- a/src/HOL/NanoJava/AxSem.thy Wed Aug 08 15:16:38 2001 +0200
+++ b/src/HOL/NanoJava/AxSem.thy Wed Aug 08 16:57:43 2001 +0200
@@ -9,7 +9,7 @@
theory AxSem = State:
types assn = "state => bool"
- vassn = "val \<Rightarrow> assn"
+ vassn = "val => assn"
triple = "assn \<times> stmt \<times> assn"
etriple = "assn \<times> expr \<times> vassn"
translations
@@ -24,9 +24,9 @@
"@hoare" :: "[triple set, triple set ] => bool" ("_ |\<turnstile>/ _" [61,61] 60)
"@hoare1" :: "[triple set, assn,stmt,assn] => bool"
("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
-"@ehoare" :: "[triple set, etriple ] => bool" ("_ |\<turnstile>e/ _"[61,61]60)
+"@ehoare" :: "[triple set, etriple ] => bool" ("_ |\<turnstile>\<^sub>e/ _"[61,61]60)
"@ehoare1" :: "[triple set, assn,expr,vassn]=> bool"
- ("_ \<turnstile>e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
+ ("_ \<turnstile>\<^sub>e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
syntax
"@hoare" :: "[triple set, triple set ] => bool" ("_ ||-/ _" [61,61] 60)
"@hoare1" :: "[triple set, assn,stmt,assn] => bool"
@@ -37,9 +37,9 @@
translations "A |\<turnstile> C" \<rightleftharpoons> "(A,C) \<in> hoare"
"A \<turnstile> {P}c{Q}" \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
- "A |\<turnstile>e t" \<rightleftharpoons> "(A,t) \<in> ehoare"
- "A |\<turnstile>e (P,e,Q)" \<rightleftharpoons> "(A,P,e,Q) \<in> ehoare" (** shouldn't be necess.**)
- "A \<turnstile>e{P}e{Q}" \<rightleftharpoons> "A |\<turnstile>e (P,e,Q)"
+ "A |\<turnstile>\<^sub>e t" \<rightleftharpoons> "(A,t) \<in> ehoare"
+ "A |\<turnstile>\<^sub>e (P,e,Q)" \<rightleftharpoons> "(A,P,e,Q) \<in> ehoare" (** shouldn't be necess.**)
+ "A \<turnstile>\<^sub>e {P}e{Q}" \<rightleftharpoons> "A |\<turnstile>\<^sub>e (P,e,Q)"
inductive hoare ehoare
@@ -124,13 +124,13 @@
apply fast
done
-lemma eConseq1: "\<lbrakk>A \<turnstile>e {P'} e {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile>e {P} e {Q}"
+lemma eConseq1: "\<lbrakk>A \<turnstile>\<^sub>e {P'} e {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}"
apply (rule hoare_ehoare.eConseq)
apply (rule allI, assumption)
apply fast
done
-lemma eConseq2: "\<lbrakk>A \<turnstile>e {P} e {Q'}; \<forall>v t. Q' v t \<longrightarrow> Q v t\<rbrakk> \<Longrightarrow> A \<turnstile>e {P} e {Q}"
+lemma eConseq2: "\<lbrakk>A \<turnstile>\<^sub>e {P} e {Q'}; \<forall>v t. Q' v t \<longrightarrow> Q v t\<rbrakk> \<Longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}"
apply (rule hoare_ehoare.eConseq)
apply (rule allI, assumption)
apply fast
--- a/src/HOL/NanoJava/Decl.thy Wed Aug 08 15:16:38 2001 +0200
+++ b/src/HOL/NanoJava/Decl.thy Wed Aug 08 16:57:43 2001 +0200
@@ -15,7 +15,6 @@
types fdecl (* field declaration *)
= "vnam \<times> ty"
-
record methd (* method declaration *)
= par :: ty
res :: ty
@@ -46,9 +45,6 @@
consts
Prog :: prog (* program as a global value *)
-
-consts
-
Object :: cname (* name of root class *)
--- a/src/HOL/NanoJava/Equivalence.thy Wed Aug 08 15:16:38 2001 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy Wed Aug 08 16:57:43 2001 +0200
@@ -35,12 +35,12 @@
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)
+ evalid :: "[assn,expr,vassn] => bool" ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
nvalid :: "[nat, triple ] => bool" ("\<Turnstile>_: _" [61,61] 60)
- envalid :: "[nat,etriple ] => bool" ("\<Turnstile>_:e _" [61,61] 60)
+ envalid :: "[nat,etriple ] => bool" ("\<Turnstile>_:\<^sub>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)
+cenvalid :: "[triple set,etriple ] => bool" ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60)
lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
@@ -51,16 +51,16 @@
apply blast
done
-lemma envalid_def2: "\<Turnstile>n:e (P,e,Q) \<equiv> \<forall>s v t. s -e\<succ>v-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q v t"
+lemma envalid_def2: "\<Turnstile>n:\<^sub>e (P,e,Q) \<equiv> \<forall>s v t. s -e\<succ>v-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q v t"
by (simp add: envalid_def Let_def)
-lemma evalid_def2: "\<Turnstile>e {P} e {Q} = (\<forall>n. \<Turnstile>n:e (P,e,Q))"
+lemma evalid_def2: "\<Turnstile>\<^sub>e {P} e {Q} = (\<forall>n. \<Turnstile>n:\<^sub>e (P,e,Q))"
apply (simp add: evalid_def envalid_def2)
apply blast
done
lemma cenvalid_def2:
- "A|\<Turnstile>e (P,e,Q) = (\<forall>n. |\<Turnstile>n: A \<longrightarrow> (\<forall>s v t. s -e\<succ>v-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q v t))"
+ "A|\<Turnstile>\<^sub>e (P,e,Q) = (\<forall>n. |\<Turnstile>n: A \<longrightarrow> (\<forall>s v t. s -e\<succ>v-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q v t))"
by(simp add: cenvalid_def envalid_def2)
@@ -103,7 +103,7 @@
"A |\<Turnstile> {(P,c,Q)} \<equiv> \<forall>n. |\<Turnstile>n: A \<longrightarrow> (\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)"
by(simp add: cnvalids_def nvalids_def nvalid_def2)
-lemma hoare_sound_main:"\<And>t. (A |\<turnstile> C \<longrightarrow> A |\<Turnstile> C) \<and> (A |\<turnstile>e t \<longrightarrow> A |\<Turnstile>e t)"
+lemma hoare_sound_main:"\<And>t. (A |\<turnstile> C \<longrightarrow> A |\<Turnstile> C) \<and> (A |\<turnstile>\<^sub>e t \<longrightarrow> A |\<Turnstile>\<^sub>e t)"
apply (tactic "split_all_tac 1", rename_tac P e Q)
apply (rule hoare_ehoare.induct)
apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *})
@@ -149,7 +149,7 @@
apply fast
done
-theorem ehoare_sound: "{} \<turnstile>e {P} e {Q} \<Longrightarrow> \<Turnstile>e {P} e {Q}"
+theorem ehoare_sound: "{} \<turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> \<Turnstile>\<^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)
@@ -160,9 +160,11 @@
subsection "(Relative) Completeness"
constdefs MGT :: "stmt => state => triple"
- "MGT c z \<equiv> (\<lambda>s. z = s, c, \<lambda> t. \<exists>n. z -c- n-> t)"
- eMGT :: "expr => state => etriple"
- "eMGT e z \<equiv> (\<lambda>s. z = s, e, \<lambda>v t. \<exists>n. z -e>v-n-> t)"
+ "MGT c z \<equiv> (\<lambda>s. z = s, c, \<lambda> t. \<exists>n. z -c- n-> t)"
+ MGTe :: "expr => state => etriple"
+ "MGTe e z \<equiv> (\<lambda>s. z = s, e, \<lambda>v t. \<exists>n. z -e>v-n-> t)"
+syntax (xsymbols)
+ MGTe :: "expr => state => etriple" ("MGT\<^sub>e")
lemma MGF_implies_complete:
"\<forall>z. {} |\<turnstile> { MGT c z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
@@ -173,9 +175,9 @@
done
lemma eMGF_implies_complete:
- "\<forall>z. {} |\<turnstile>e eMGT e z \<Longrightarrow> \<Turnstile>e {P} e {Q} \<Longrightarrow> {} \<turnstile>e {P} e {Q}"
+ "\<forall>z. {} |\<turnstile>\<^sub>e MGT\<^sub>e e z \<Longrightarrow> \<Turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> {} \<turnstile>\<^sub>e {P} e {Q}"
apply (simp only: evalid_def2)
-apply (unfold eMGT_def)
+apply (unfold MGTe_def)
apply (erule hoare_ehoare.eConseq)
apply (clarsimp simp add: envalid_def2)
done
@@ -183,8 +185,8 @@
declare exec_eval.intros[intro!]
lemma MGF_Loop: "\<forall>z. A \<turnstile> {op = z} c {\<lambda>t. \<exists>n. z -c-n\<rightarrow> t} \<Longrightarrow>
- A \<turnstile> {op = z} While (e) c {\<lambda>t. \<exists>n. z -While (e) c-n\<rightarrow> t}"
-apply (rule_tac P' = "\<lambda>z s. (z,s) \<in> ({(s,t). \<exists>n. s<e> \<noteq> Null \<and> s -c-n\<rightarrow> t})^*"
+ A \<turnstile> {op = z} While (x) c {\<lambda>t. \<exists>n. z -While (x) c-n\<rightarrow> t}"
+apply (rule_tac P' = "\<lambda>z s. (z,s) \<in> ({(s,t). \<exists>n. s<x> \<noteq> Null \<and> s -c-n\<rightarrow> t})^*"
in hoare_ehoare.Conseq)
apply (rule allI)
apply (rule hoare_ehoare.Loop)
@@ -203,8 +205,8 @@
done
lemma MGF_lemma: "\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z} \<Longrightarrow>
- (\<forall>z. A |\<turnstile> {MGT c z}) \<and> (\<forall>z. A |\<turnstile>e eMGT e z)"
-apply (simp add: MGT_def eMGT_def)
+ (\<forall>z. A |\<turnstile> {MGT c z}) \<and> (\<forall>z. A |\<turnstile>\<^sub>e MGT\<^sub>e e z)"
+apply (simp add: MGT_def MGTe_def)
apply (rule stmt_expr.induct)
apply (rule_tac [!] allI)
@@ -301,7 +303,7 @@
apply (rule MGF_Impl)
done
-theorem ehoare_relative_complete: "\<Turnstile>e {P} e {Q} \<Longrightarrow> {} \<turnstile>e {P} e {Q}"
+theorem ehoare_relative_complete: "\<Turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> {} \<turnstile>\<^sub>e {P} e {Q}"
apply (rule eMGF_implies_complete)
apply (erule_tac [2] asm_rl)
apply (rule allI)
--- a/src/HOL/NanoJava/OpSem.thy Wed Aug 08 15:16:38 2001 +0200
+++ b/src/HOL/NanoJava/OpSem.thy Wed Aug 08 16:57:43 2001 +0200
@@ -22,7 +22,6 @@
"s -e>v-n-> s'" == "(s, e, v, n, s') \<in> eval"
inductive exec eval intros
-
Skip: " s -Skip-n-> s"
Comp: "[| s0 -c1-n-> s1; s1 -c2-n-> s2 |] ==>
@@ -67,21 +66,21 @@
inductive_cases exec_elim_cases':
- "s -Skip -n\<rightarrow> t"
- "s -c1;; c2 -n\<rightarrow> t"
- "s -If(e) c1 Else c2-n\<rightarrow> t"
- "s -While(x) c -n\<rightarrow> t"
- "s -x:==e -n\<rightarrow> t"
- "s -e1..f:==e2 -n\<rightarrow> t"
-inductive_cases Meth_elim_cases: "s -Meth C m-n\<rightarrow> t"
-inductive_cases Impl_elim_cases: "s -Impl C m-n\<rightarrow> t"
+ "s -Skip -n\<rightarrow> t"
+ "s -c1;; c2 -n\<rightarrow> t"
+ "s -If(e) c1 Else c2-n\<rightarrow> t"
+ "s -While(x) c -n\<rightarrow> t"
+ "s -x:==e -n\<rightarrow> t"
+ "s -e1..f:==e2 -n\<rightarrow> t"
+inductive_cases Meth_elim_cases: "s -Meth C m-n\<rightarrow> t"
+inductive_cases Impl_elim_cases: "s -Impl C m-n\<rightarrow> t"
lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases
inductive_cases eval_elim_cases:
- "s -new C \<succ>v-n\<rightarrow> t"
- "s -Cast C e \<succ>v-n\<rightarrow> t"
- "s -LAcc x \<succ>v-n\<rightarrow> t"
- "s -e..f \<succ>v-n\<rightarrow> t"
- "s -{C}e1..m(e2) \<succ>v-n\<rightarrow> t"
+ "s -new C \<succ>v-n\<rightarrow> t"
+ "s -Cast C e \<succ>v-n\<rightarrow> t"
+ "s -LAcc x \<succ>v-n\<rightarrow> t"
+ "s -e..f \<succ>v-n\<rightarrow> t"
+ "s -{C}e1..m(e2) \<succ>v-n\<rightarrow> t"
lemma exec_eval_mono [rule_format]:
"(s -c -n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -c -m\<rightarrow> t)) \<and>
--- a/src/HOL/NanoJava/Term.thy Wed Aug 08 15:16:38 2001 +0200
+++ b/src/HOL/NanoJava/Term.thy Wed Aug 08 16:57:43 2001 +0200
@@ -38,11 +38,5 @@
| Call cname expr mname expr (* method call *)
("{_}_.._'(_')" [99,95,99,95] 95)
-
-lemma pair_imageI [intro]: "(a, b) \<in> A ==> f a b : (%(a, b). f a b) ` A"
-apply (rule_tac x = "(a,b)" in image_eqI)
-apply auto
-done
-
end