--- a/src/HOL/MicroJava/BV/LBVSpec.thy Wed Jun 28 19:56:21 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Wed Jun 28 19:57:16 2000 +0200
@@ -7,15 +7,15 @@
header {* Specification of the LBV *}
-theory LBVSpec = BVSpec:;
+theory LBVSpec = BVSpec:
types
certificate = "state_type option list"
class_certificate = "sig \\<Rightarrow> certificate"
- prog_certificate = "cname \\<Rightarrow> class_certificate";
+ prog_certificate = "cname \\<Rightarrow> class_certificate"
consts
- wtl_LS :: "[load_and_store,state_type,state_type,p_count,p_count] \\<Rightarrow> bool";
+ wtl_LS :: "[load_and_store,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
primrec
"wtl_LS (Load idx) s s' max_pc pc =
(let (ST,LT) = s
@@ -43,10 +43,10 @@
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
- (NT # ST , LT) = s')";
+ (NT # ST , LT) = s')"
consts
- wtl_MO :: "[manipulate_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool";
+ wtl_MO :: "[manipulate_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
primrec
"wtl_MO (Getfield F C) G s s' max_pc pc =
(let (ST,LT) = s
@@ -68,21 +68,21 @@
ST = vT # oT # ST' \\<and>
G \\<turnstile> oT \\<preceq> (Class C) \\<and>
G \\<turnstile> vT \\<preceq> T \\<and>
- (ST' , LT) = s'))";
+ (ST' , LT) = s'))"
consts
- wtl_CO :: "[create_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool";
+ wtl_CO :: "[create_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
primrec
"wtl_CO (New C) G s s' max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
is_class G C \\<and>
- ((Class C) # ST , LT) = s')";
+ ((Class C) # ST , LT) = s')"
consts
- wtl_CH :: "[check_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool";
+ wtl_CH :: "[check_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
primrec
"wtl_CH (Checkcast C) G s s' max_pc pc =
(let (ST,LT) = s
@@ -90,10 +90,10 @@
pc+1 < max_pc \\<and>
is_class G C \\<and>
(\\<exists>rt ST'. ST = RefT rt # ST' \\<and>
- (Class C # ST' , LT) = s'))";
+ (Class C # ST' , LT) = s'))"
consts
- wtl_OS :: "[op_stack,state_type,state_type,p_count,p_count] \\<Rightarrow> bool";
+ wtl_OS :: "[op_stack,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
primrec
"wtl_OS Pop s s' max_pc pc =
(let (ST,LT) = s
@@ -128,10 +128,10 @@
in
pc+1 < max_pc \\<and>
(\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and>
- (ts # ts' # ST' , LT) = s'))";
+ (ts # ts' # ST' , LT) = s'))"
consts
- wtl_BR :: "[branch,jvm_prog,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool";
+ wtl_BR :: "[branch,jvm_prog,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
primrec
"wtl_BR (Ifcmpeq branch) G s s' cert max_pc pc =
(let (ST,LT) = s
@@ -149,10 +149,10 @@
in
(nat(int pc+branch)) < max_pc \\<and> cert ! (nat(int pc+branch)) \\<noteq> None \\<and>
G \\<turnstile> (ST , LT) <=s the (cert ! (nat(int pc+branch)))) \\<and>
- (cert ! (pc+1) = Some s'))";
+ (cert ! (pc+1) = Some s'))"
consts
- wtl_MI :: "[meth_inv,jvm_prog,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool";
+ wtl_MI :: "[meth_inv,jvm_prog,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
primrec
"wtl_MI (Invoke mn fpTs) G s s' cert max_pc pc =
(let (ST,LT) = s
@@ -165,20 +165,20 @@
((G \\<turnstile> s' <=s s'') \\<and> (\\<exists>C. X = Class C \\<and>
(\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
(\\<exists>D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
- (rT # ST' , LT) = s')))))))";
+ (rT # ST' , LT) = s')))))))"
consts
- wtl_MR :: "[meth_ret,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool";
+ wtl_MR :: "[meth_ret,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
primrec
"wtl_MR Return G rT s s' cert max_pc pc =
((let (ST,LT) = s
in
(\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT)) \\<and>
- (cert ! (pc+1) = Some s'))";
+ (cert ! (pc+1) = Some s'))"
consts
- 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"
primrec
"wtl_inst (LS ins) G rT s s' cert max_pc pc = wtl_LS ins s s' max_pc pc"
"wtl_inst (CO ins) G rT s s' cert max_pc pc = wtl_CO ins G s s' max_pc pc"
@@ -187,7 +187,7 @@
"wtl_inst (MI ins) G rT s s' cert max_pc pc = wtl_MI ins G s s' cert max_pc pc"
"wtl_inst (MR ins) G rT s s' cert max_pc pc = wtl_MR ins G rT s s' cert max_pc pc"
"wtl_inst (OS ins) G rT s s' cert max_pc pc = wtl_OS ins s s' max_pc pc"
- "wtl_inst (BR ins) G rT s s' cert max_pc pc = wtl_BR ins G s s' cert max_pc pc";
+ "wtl_inst (BR ins) G rT s s' cert max_pc pc = wtl_BR ins G s s' cert max_pc pc"
constdefs
@@ -196,16 +196,16 @@
(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>
- wtl_inst i G rT s0' s1 cert max_pc pc)";
+ 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>
- wtl_inst_list is G rT s1 s2 cert max_pc (pc+1))";
+ 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"
@@ -220,76 +220,76 @@
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";
+ 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";
-by auto;
+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");
-proof (induct i);
-case LS;
- show "?P (LS load_and_store)"; by (induct load_and_store) auto;
-case CO;
- show "?P (CO create_object)"; by (induct create_object) auto;
-case MO;
- show "?P (MO manipulate_object)"; by (induct manipulate_object) auto;
-case CH;
- show "?P (CH check_object)"; by (induct check_object) auto;
-case MI;
- show "?P (MI meth_inv)"; proof (induct meth_inv);
- case Invoke;
- have "\\<exists>x y. s0 = (x,y)"; by (simp);
+ wtl_inst i G rT s0 s1' cert max_pc pc \\<longrightarrow> s1 = s1'" (is "?P i")
+proof (induct i)
+case LS
+ show "?P (LS load_and_store)" by (induct load_and_store) auto
+case CO
+ show "?P (CO create_object)" by (induct create_object) auto
+case MO
+ show "?P (MO manipulate_object)" by (induct manipulate_object) auto
+case CH
+ show "?P (CH check_object)" by (induct check_object) auto
+case MI
+ show "?P (MI meth_inv)" proof (induct meth_inv)
+ case Invoke
+ have "\\<exists>x y. s0 = (x,y)" by (simp)
thus "wtl_inst (MI (Invoke mname list)) G rT s0 s1 cert max_pc pc \\<longrightarrow>
wtl_inst (MI (Invoke mname list)) G rT s0 s1' cert max_pc pc \\<longrightarrow>
- s1 = s1'";
- proof elim;
- apply_end(clarsimp_tac, drule rev_eq, assumption+);
- qed auto;
- qed;
-case MR;
- show "?P (MR meth_ret)"; by (induct meth_ret) auto;
-case OS;
- show "?P (OS op_stack)"; by (induct op_stack) auto;
-case BR;
- show "?P (BR branch)"; by (induct branch) auto;
-qed;
+ s1 = s1'"
+ proof elim
+ apply_end(clarsimp_tac, drule rev_eq, assumption+)
+ qed auto
+ qed
+case MR
+ show "?P (MR meth_ret)" by (induct meth_ret) auto
+case OS
+ show "?P (OS op_stack)" by (induct op_stack) auto
+case BR
+ show "?P (BR branch)" by (induct branch) auto
+qed
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'";
-by (cases "cert!pc") (auto simp add: wtl_inst_unique wtl_inst_option_def);
+ 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");
- case Nil;
- show "?P []"; by simp;
+ wtl_inst_list is G rT s0 s1' cert max_pc pc \\<longrightarrow> s1=s1'" (is "?P is")
+proof (induct "?P" "is")
+ case Nil
+ show "?P []" by simp
- case Cons;
- show "?P (a # list)";
- proof intro;
- fix s0; fix pc;
- let "?o s0 s1" = "wtl_inst_option a G rT s0 s1 cert max_pc pc";
- let "?l l s1 s2 pc" = "wtl_inst_list l G rT s1 s2 cert max_pc pc";
- assume a: "?l (a#list) s0 s1 pc";
- assume b: "?l (a#list) s0 s1' pc";
- with a;
- show "s1 = s1'";
+ case Cons
+ show "?P (a # list)"
+ proof intro
+ fix s0 fix pc
+ let "?o s0 s1" = "wtl_inst_option a G rT s0 s1 cert max_pc pc"
+ let "?l l s1 s2 pc" = "wtl_inst_list l G rT s1 s2 cert max_pc pc"
+ assume a: "?l (a#list) s0 s1 pc"
+ assume b: "?l (a#list) s0 s1' pc"
+ with a
+ show "s1 = s1'"
obtain s s' where "?o s0 s" "?o s0 s'"
and l: "?l list s s1 (Suc pc)"
- and l': "?l list s' s1' (Suc pc)"; by auto;
- have "s=s'"; by(rule wtl_inst_option_unique);
- with l l' Cons;
- show ?thesis; by blast;
- qed;
- qed;
-qed;
+ and l': "?l list s' s1' (Suc pc)" by auto
+ have "s=s'" by(rule wtl_inst_option_unique)
+ with l l' Cons
+ show ?thesis by blast
+ qed
+ qed
+qed
lemma wtl_partial:
"\\<forall> pc' pc s.
@@ -297,159 +297,159 @@
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");
- case Nil;
- show "?P []"; by auto;
+ wtl_inst_list b G rT s1 s' cert mpc (pc+length a))" (is "?P is")
+proof (induct "?P" "is")
+ case Nil
+ show "?P []" by auto
- case Cons;
- show "?P (a#list)";
- proof (intro allI impI);
- fix pc' pc s;
- assume length: "pc' < length (a # list)";
- assume wtl: "wtl_inst_list (a # list) G rT s s' cert mpc pc";
+ case Cons
+ show "?P (a#list)"
+ proof (intro allI impI)
+ 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> \
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'");
- case 0;
- with wtl;
- have "?E [] (a#list) s"; by simp;
- thus ?thesis; by blast;
- next;
- case Suc;
- with wtl;
- show ?thesis;
+ (is "\\<exists> a b s1. ?E a b s1")
+ proof (cases "pc'")
+ case 0
+ with wtl
+ have "?E [] (a#list) s" by simp
+ thus ?thesis by blast
+ next
+ case Suc
+ with wtl
+ show ?thesis
obtain s0 where wtlSuc: "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)"
- and wtlOpt: "wtl_inst_option a G rT s s0 cert mpc pc"; by auto;
- from Cons;
- show ?thesis;
+ and wtlOpt: "wtl_inst_option a G rT s s0 cert mpc pc" by auto
+ from Cons
+ show ?thesis
obtain a' b s1'
where "a' @ b = list" "length a' = nat"
and w:"wtl_inst_list a' G rT s0 s1' cert mpc (Suc pc)"
- and "wtl_inst_list b G rT s1' s' cert mpc (Suc pc + length a')";
- proof (elim allE impE);
- from length Suc; show "nat < length list"; by simp;
- from wtlSuc; show "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)"; .;
- qed (elim exE conjE, auto);
- with Suc wtlOpt;
- have "?E (a#a') b s1'"; by (auto simp del: split_paired_Ex);
- thus ?thesis; by blast;
- qed;
- qed;
- qed;
- qed;
-qed;
+ and "wtl_inst_list b G rT s1' s' cert mpc (Suc pc + length a')"
+ proof (elim allE impE)
+ from length Suc show "nat < length list" by simp
+ from wtlSuc show "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)" .
+ qed (elim exE conjE, auto)
+ with Suc wtlOpt
+ have "?E (a#a') b s1'" by (auto simp del: split_paired_Ex)
+ thus ?thesis by blast
+ qed
+ qed
+ qed
+ qed
+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>
- wtl_inst_list (x@y) G rT s0 s2 cert (length (x@y)) 0";
-proof -;
+ wtl_inst_list (x@y) G rT s0 s2 cert (length (x@y)) 0"
+proof -
assume w:
"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)";
+ "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>
- wtl_inst_list (x@y) G rT s0 s2 cert (pc+length (x@y)) pc" (is "?P x");
-proof (induct "?P" "x");
- case Nil;
- show "?P []"; by simp;
-next;
- case Cons;
- show "?P (a#list)";
- proof intro;
- fix pc s0;
+ wtl_inst_list (x@y) G rT s0 s2 cert (pc+length (x@y)) pc" (is "?P x")
+proof (induct "?P" "x")
+ case Nil
+ show "?P []" by simp
+next
+ case Cons
+ show "?P (a#list)"
+ proof intro
+ fix pc s0
assume y:
- "wtl_inst_list y G rT s1 s2 cert (pc + length ((a # list) @ y)) (pc + length (a # list))";
+ "wtl_inst_list y G rT s1 s2 cert (pc + length ((a # list) @ y)) (pc + length (a # list))"
assume al:
- "wtl_inst_list (a # list) G rT s0 s1 cert (pc + length ((a # list) @ y)) pc";
- thus "wtl_inst_list ((a # list) @ y) G rT s0 s2 cert (pc + length ((a # list) @ y)) pc";
+ "wtl_inst_list (a # list) G rT s0 s1 cert (pc + length ((a # list) @ y)) pc"
+ thus "wtl_inst_list ((a # list) @ y) G rT s0 s2 cert (pc + length ((a # list) @ y)) pc"
obtain s' where
a: "wtl_inst_option a G rT s0 s' cert (Suc pc + length (list@y)) pc" and
- l: "wtl_inst_list list G rT s' s1 cert (Suc pc + length (list@y)) (Suc pc)"; by auto;
- with y Cons;
- have "wtl_inst_list (list @ y) G rT s' s2 cert (Suc pc + length (list @ y)) (Suc pc)";
- by elim (assumption, simp+);
- with a;
- show ?thesis; by (auto simp del: split_paired_Ex);
- qed;
- qed;
-qed;
+ l: "wtl_inst_list list G rT s' s1 cert (Suc pc + length (list@y)) (Suc pc)" by auto
+ with y Cons
+ have "wtl_inst_list (list @ y) G rT s' s2 cert (Suc pc + length (list @ y)) (Suc pc)"
+ by (elim allE impE) (assumption, simp+)
+ with a
+ show ?thesis by (auto simp del: split_paired_Ex)
+ qed
+ qed
+qed
- with w;
- show ?thesis;
- proof elim;
- from w; show "wtl_inst_list x G rT s0 s1 cert (0+length (x @ y)) 0"; by simp;
- qed simp+;
-qed;
+ with w
+ show ?thesis
+ proof (elim allE impE)
+ from w show "wtl_inst_list x G rT s0 s1 cert (0+length (x @ y)) 0" by simp
+ qed simp+
+qed
lemma wtl_cons_appendl:
"\\<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 (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";
+ 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"
assume "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))";
+ "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))"
- hence "wtl_inst_list (i#b) G rT s1 s3 cert (length (a@i#b)) (length a)";
- by (auto simp del: split_paired_Ex);
+ hence "wtl_inst_list (i#b) G rT s1 s3 cert (length (a@i#b)) (length a)"
+ by (auto simp del: split_paired_Ex)
- with a;
- show ?thesis; by (rule wtl_append1);
-qed;
+ with a
+ show ?thesis by (rule wtl_append1)
+qed
lemma "wtl_append":
"\\<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 (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))";
+ 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>
- wtl_inst_list (a@[i]) G rT s0 s2 cert (pc+length (a@i#b)) pc" (is "?P a");
- proof (induct "?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");
- proof intro;
- fix s0 pc;
- assume y: "?y s0 pc";
- assume z: "?z s0 pc";
- assume "?x s0 pc";
- thus "?p s0 pc";
+ wtl_inst_list (a@[i]) G rT s0 s2 cert (pc+length (a@i#b)) pc" (is "?P a")
+ proof (induct "?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")
+ proof intro
+ fix s0 pc
+ assume y: "?y s0 pc"
+ assume z: "?z s0 pc"
+ assume "?x s0 pc"
+ thus "?p s0 pc"
obtain s0' where opt: "wtl_inst_option a G rT s0 s0' cert (pc + length ((a # list) @ i # b)) pc"
- and list: "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)";
- by (auto simp del: split_paired_Ex);
- with y z Cons;
- have "wtl_inst_list (list @ [i]) G rT s0' s2 cert (Suc pc + length (list @ i # b)) (Suc pc)";
- proof elim;
- from list; show "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)"; .;
- qed auto;
- with opt;
- show ?thesis; by (auto simp del: split_paired_Ex);
- qed;
- qed;
- qed;
- with a i b;
- show ?thesis;
- proof elim;
- from a; show "wtl_inst_list a G rT s0 s1 cert (0+length (a@i#b)) 0"; by simp;
- qed auto;
-qed;
+ and list: "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)"
+ by (auto simp del: split_paired_Ex)
+ with y z Cons
+ have "wtl_inst_list (list @ [i]) G rT s0' s2 cert (Suc pc + length (list @ i # b)) (Suc pc)"
+ proof (elim allE impE)
+ from list show "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)" .
+ qed auto
+ with opt
+ show ?thesis by (auto simp del: split_paired_Ex)
+ qed
+ qed
+ qed
+ with a i b
+ show ?thesis
+ proof (elim allE impE)
+ from a show "wtl_inst_list a G rT s0 s1 cert (0+length (a@i#b)) 0" by simp
+ qed auto
+qed
-end;
+end