# HG changeset patch
# User oheimb
# Date 997282663 -7200
# Node ID 8f32860eac3afd89648e87303a0cd4d487d8ea2b
# Parent  f7157bdc1e7015a9108b55046427daf839a731dd
layout, subscripts

diff -r f7157bdc1e70 -r 8f32860eac3a src/HOL/NanoJava/AxSem.thy
--- 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
diff -r f7157bdc1e70 -r 8f32860eac3a src/HOL/NanoJava/Decl.thy
--- 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 *)
 
 
diff -r f7157bdc1e70 -r 8f32860eac3a src/HOL/NanoJava/Equivalence.thy
--- 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)
diff -r f7157bdc1e70 -r 8f32860eac3a src/HOL/NanoJava/OpSem.thy
--- 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>
diff -r f7157bdc1e70 -r 8f32860eac3a src/HOL/NanoJava/Term.thy
--- 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