--- a/src/HOL/MicroJava/BV/LBVSpec.thy Sat Aug 19 12:49:19 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Sun Aug 20 17:45:20 2000 +0200
@@ -11,82 +11,82 @@
types
certificate = "state_type option list"
- class_certificate = "sig \\<Rightarrow> certificate"
- prog_certificate = "cname \\<Rightarrow> class_certificate"
+ class_certificate = "sig \<Rightarrow> certificate"
+ prog_certificate = "cname \<Rightarrow> class_certificate"
constdefs
-wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
+wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \<Rightarrow> bool"
-"wtl_inst i G rT s s' cert max_pc pc \\<equiv> app (i,G,rT,s) \\<and>
+"wtl_inst i G rT s s' cert max_pc pc \<equiv> app (i,G,rT,s) \<and>
(let s'' = the (step (i,G,s)) in
- (\\<forall> pc' \\<in> (succs i pc). pc' < max_pc \\<and>
- ((pc' \\<noteq> pc+1) \\<longrightarrow> cert!pc' \\<noteq> None \\<and> G \\<turnstile> s'' <=s the (cert!pc'))) \\<and>
- (if (pc+1) \\<in> (succs i pc) then
+ (\<forall> pc' \<in> (succs i pc). pc' < max_pc \<and>
+ ((pc' \<noteq> pc+1) \<longrightarrow> cert!pc' \<noteq> None \<and> G \<turnstile> s'' <=s the (cert!pc'))) \<and>
+ (if (pc+1) \<in> (succs i pc) then
s' = s''
else
cert ! (pc+1) = Some s'))"
lemma [simp]:
-"succs i pc = {pc+1} \\<Longrightarrow>
- wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \\<and> pc+1 < max_pc \\<and> (s' = the (step (i,G,s))))"
+"succs i pc = {pc+1} \<Longrightarrow>
+ wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \<and> pc+1 < max_pc \<and> (s' = the (step (i,G,s))))"
by (unfold wtl_inst_def, auto)
lemma [simp]:
-"succs i pc = {} \\<Longrightarrow> wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \\<and> cert!(pc+1) = Some s')"
+"succs i pc = {} \<Longrightarrow> wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \<and> cert!(pc+1) = Some s')"
by (unfold wtl_inst_def, auto)
constdefs
-wtl_inst_option :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
-"wtl_inst_option i G rT s0 s1 cert max_pc pc \\<equiv>
+wtl_inst_option :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \<Rightarrow> bool"
+"wtl_inst_option i G rT s0 s1 cert max_pc pc \<equiv>
(case cert!pc of
- None \\<Rightarrow> wtl_inst i G rT s0 s1 cert max_pc pc
- | Some s0' \\<Rightarrow> (G \\<turnstile> s0 <=s s0') \\<and>
+ None \<Rightarrow> wtl_inst i G rT s0 s1 cert max_pc pc
+ | Some s0' \<Rightarrow> (G \<turnstile> s0 <=s s0') \<and>
wtl_inst i G rT s0' s1 cert max_pc pc)"
consts
- wtl_inst_list :: "[instr list,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
+ wtl_inst_list :: "[instr list,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \<Rightarrow> bool"
primrec
"wtl_inst_list [] G rT s0 s2 cert max_pc pc = (s0 = s2)"
"wtl_inst_list (instr#is) G rT s0 s2 cert max_pc pc =
- (\\<exists>s1. wtl_inst_option instr G rT s0 s1 cert max_pc pc \\<and>
+ (\<exists>s1. wtl_inst_option instr G rT s0 s1 cert max_pc pc \<and>
wtl_inst_list is G rT s1 s2 cert max_pc (pc+1))"
constdefs
- wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \\<Rightarrow> bool"
- "wtl_method G C pTs rT mxl ins cert \\<equiv>
+ wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \<Rightarrow> bool"
+ "wtl_method G C pTs rT mxl ins cert \<equiv>
let max_pc = length ins
in
- 0 < max_pc \\<and>
- (\\<exists>s2. wtl_inst_list ins G rT
+ 0 < max_pc \<and>
+ (\<exists>s2. wtl_inst_list ins G rT
([],(Some(Class C))#((map Some pTs))@(replicate mxl None))
s2 cert max_pc 0)"
- wtl_jvm_prog :: "[jvm_prog,prog_certificate] \\<Rightarrow> bool"
- "wtl_jvm_prog G cert \\<equiv>
- wf_prog (\\<lambda>G C (sig,rT,maxl,b).
+ wtl_jvm_prog :: "[jvm_prog,prog_certificate] \<Rightarrow> bool"
+ "wtl_jvm_prog G cert \<equiv>
+ wf_prog (\<lambda>G C (sig,rT,maxl,b).
wtl_method G C (snd sig) rT maxl b (cert C sig)) G"
text {* \medskip *}
-lemma rev_eq: "\\<lbrakk>length a = n; length x = n; rev a @ b # c = rev x @ y # z\\<rbrakk> \\<Longrightarrow> a = x \\<and> b = y \\<and> c = z"
+lemma rev_eq: "\<lbrakk>length a = n; length x = n; rev a @ b # c = rev x @ y # z\<rbrakk> \<Longrightarrow> a = x \<and> b = y \<and> c = z"
by auto
lemma wtl_inst_unique:
-"wtl_inst i G rT s0 s1 cert max_pc pc \\<longrightarrow>
- wtl_inst i G rT s0 s1' cert max_pc pc \\<longrightarrow> s1 = s1'" (is "?P i")
+"wtl_inst i G rT s0 s1 cert max_pc pc \<longrightarrow>
+ wtl_inst i G rT s0 s1' cert max_pc pc \<longrightarrow> s1 = s1'" (is "?P i")
by (unfold wtl_inst_def, auto)
lemma wtl_inst_option_unique:
-"\\<lbrakk>wtl_inst_option i G rT s0 s1 cert max_pc pc;
- wtl_inst_option i G rT s0 s1' cert max_pc pc\\<rbrakk> \\<Longrightarrow> s1 = s1'"
+"\<lbrakk>wtl_inst_option i G rT s0 s1 cert max_pc pc;
+ wtl_inst_option i G rT s0 s1' cert max_pc pc\<rbrakk> \<Longrightarrow> s1 = s1'"
by (cases "cert!pc") (auto simp add: wtl_inst_unique wtl_inst_option_def)
lemma wtl_inst_list_unique:
-"\\<forall> s0 pc. wtl_inst_list is G rT s0 s1 cert max_pc pc \\<longrightarrow>
- wtl_inst_list is G rT s0 s1' cert max_pc pc \\<longrightarrow> s1=s1'" (is "?P is")
-proof (induct "?P" "is")
+"\<forall> s0 pc. wtl_inst_list is G rT s0 s1 cert max_pc pc \<longrightarrow>
+ wtl_inst_list is G rT s0 s1' cert max_pc pc \<longrightarrow> s1=s1'" (is "?P is")
+proof (induct (open) ?P "is")
case Nil
show "?P []" by simp
@@ -110,13 +110,13 @@
qed
lemma wtl_partial:
-"\\<forall> pc' pc s.
- wtl_inst_list is G rT s s' cert mpc pc \\<longrightarrow> \
- pc' < length is \\<longrightarrow> \
- (\\<exists> a b s1. a @ b = is \\<and> length a = pc' \\<and> \
- wtl_inst_list a G rT s s1 cert mpc pc \\<and> \
+"\<forall> pc' pc s.
+ wtl_inst_list is G rT s s' cert mpc pc \<longrightarrow> \
+ pc' < length is \<longrightarrow> \
+ (\<exists> a b s1. a @ b = is \<and> length a = pc' \<and> \
+ wtl_inst_list a G rT s s1 cert mpc pc \<and> \
wtl_inst_list b G rT s1 s' cert mpc (pc+length a))" (is "?P is")
-proof (induct "?P" "is")
+proof (induct (open) ?P "is")
case Nil
show "?P []" by auto
@@ -126,12 +126,12 @@
fix pc' pc s
assume length: "pc' < length (a # list)"
assume wtl: "wtl_inst_list (a # list) G rT s s' cert mpc pc"
- show "\\<exists> a' b s1.
- a' @ b = a#list \\<and> length a' = pc' \\<and> \
- wtl_inst_list a' G rT s s1 cert mpc pc \\<and> \
+ show "\<exists> a' b s1.
+ a' @ b = a#list \<and> length a' = pc' \<and> \
+ wtl_inst_list a' G rT s s1 cert mpc pc \<and> \
wtl_inst_list b G rT s1 s' cert mpc (pc+length a')"
- (is "\\<exists> a b s1. ?E a b s1")
- proof (cases "pc'")
+ (is "\<exists> a b s1. ?E a b s1")
+ proof (cases (open) pc')
case 0
with wtl
have "?E [] (a#list) s" by simp
@@ -158,8 +158,8 @@
qed
lemma "wtl_append1":
-"\\<lbrakk>wtl_inst_list x G rT s0 s1 cert (length (x@y)) 0;
- wtl_inst_list y G rT s1 s2 cert (length (x@y)) (length x)\\<rbrakk> \\<Longrightarrow>
+"\<lbrakk>wtl_inst_list x G rT s0 s1 cert (length (x@y)) 0;
+ wtl_inst_list y G rT s1 s2 cert (length (x@y)) (length x)\<rbrakk> \<Longrightarrow>
wtl_inst_list (x@y) G rT s0 s2 cert (length (x@y)) 0"
proof -
assume w:
@@ -167,11 +167,11 @@
"wtl_inst_list y G rT s1 s2 cert (length (x@y)) (length x)"
have
- "\\<forall> pc s0.
- wtl_inst_list x G rT s0 s1 cert (pc+length (x@y)) pc \\<longrightarrow>
- wtl_inst_list y G rT s1 s2 cert (pc+length (x@y)) (pc+length x) \\<longrightarrow>
+ "\<forall> pc s0.
+ wtl_inst_list x G rT s0 s1 cert (pc+length (x@y)) pc \<longrightarrow>
+ wtl_inst_list y G rT s1 s2 cert (pc+length (x@y)) (pc+length x) \<longrightarrow>
wtl_inst_list (x@y) G rT s0 s2 cert (pc+length (x@y)) pc" (is "?P x")
- proof (induct "?P" "x")
+ proof (induct (open) ?P x)
case Nil
show "?P []" by simp
next
@@ -204,9 +204,9 @@
qed
lemma wtl_cons_appendl:
-"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0;
+"\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0;
wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a);
- wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk> \\<Longrightarrow>
+ wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\<rbrakk> \<Longrightarrow>
wtl_inst_list (a@i#b) G rT s0 s3 cert (length (a@i#b)) 0"
proof -
assume a: "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0"
@@ -222,24 +222,24 @@
qed
lemma "wtl_append":
-"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0;
+"\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0;
wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a);
- wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk> \\<Longrightarrow>
+ wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\<rbrakk> \<Longrightarrow>
wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0"
proof -
assume a: "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0"
assume i: "wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)"
assume b: "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))"
- have "\\<forall> s0 pc. wtl_inst_list a G rT s0 s1 cert (pc+length (a@i#b)) pc \\<longrightarrow>
- wtl_inst_option i G rT s1 s2 cert (pc+length (a@i#b)) (pc + length a) \\<longrightarrow>
- wtl_inst_list b G rT s2 s3 cert (pc+length (a@i#b)) (Suc pc + length a) \\<longrightarrow>
+ have "\<forall> s0 pc. wtl_inst_list a G rT s0 s1 cert (pc+length (a@i#b)) pc \<longrightarrow>
+ wtl_inst_option i G rT s1 s2 cert (pc+length (a@i#b)) (pc + length a) \<longrightarrow>
+ wtl_inst_list b G rT s2 s3 cert (pc+length (a@i#b)) (Suc pc + length a) \<longrightarrow>
wtl_inst_list (a@[i]) G rT s0 s2 cert (pc+length (a@i#b)) pc" (is "?P a")
- proof (induct "?P" "a")
+ proof (induct (open) ?P a)
case Nil
show "?P []" by (simp del: split_paired_Ex)
case Cons
- show "?P (a#list)" (is "\\<forall>s0 pc. ?x s0 pc \\<longrightarrow> ?y s0 pc \\<longrightarrow> ?z s0 pc \\<longrightarrow> ?p s0 pc")
+ show "?P (a#list)" (is "\<forall>s0 pc. ?x s0 pc \<longrightarrow> ?y s0 pc \<longrightarrow> ?z s0 pc \<longrightarrow> ?p s0 pc")
proof intro
fix s0 pc
assume y: "?y s0 pc"
--- a/src/HOL/MicroJava/BV/Step.thy Sat Aug 19 12:49:19 2000 +0200
+++ b/src/HOL/MicroJava/BV/Step.thy Sun Aug 20 17:45:20 2000 +0200
@@ -187,7 +187,7 @@
lemma appIAdd[simp]:
"app (IAdd, G, rT, s) = (\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))" (is "?app s = ?P s")
-proof (cases s)
+proof (cases (open) s)
case Pair
have "?app (a,b) = ?P (a,b)"
proof (cases "a")
@@ -234,7 +234,7 @@
G \<turnstile> X \<preceq> Class C \<and>
(\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and>
method (G,C) (mn,fpTs) \<noteq> None)" (is "?app s = ?P s")
-proof (cases s)
+proof (cases (open) s)
case Pair
have "?app (a,b) \<Longrightarrow> ?P (a,b)"
proof -
--- a/src/HOL/MicroJava/BV/StepMono.thy Sat Aug 19 12:49:19 2000 +0200
+++ b/src/HOL/MicroJava/BV/StepMono.thy Sun Aug 20 17:45:20 2000 +0200
@@ -15,7 +15,7 @@
lemma sup_loc_some [rulify]:
"\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Some t \<longrightarrow> (\<exists>t. b!n = Some t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
-proof (induct "?P" b)
+proof (induct (open) ?P b)
show "?P []" by simp
case Cons
@@ -59,7 +59,7 @@
lemma append_length_n [rulify]:
"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
-proof (induct "?P" "x")
+proof (induct (open) ?P x)
show "?P []" by simp
fix l ls assume Cons: "?P ls"
@@ -122,7 +122,7 @@
assume app: "app (i, G, rT, s1)"
show ?thesis
- proof (cases i)
+ proof (cases (open) i)
case Load
from G
@@ -308,7 +308,7 @@
by (auto dest!: app_step_some);
have "G \<turnstile> (a1',b1') <=s (a2',b2')"
- proof (cases i)
+ proof (cases (open) i)
case Load
with s app1