--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Mon Aug 14 14:57:29 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Mon Aug 14 18:03:19 2000 +0200
@@ -4,7 +4,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-val defs1 = exec.simps@[split_def,sup_state_def,correct_state_def,
+val defs1 = exec.simps@[split_def,thm "sup_state_def",correct_state_def,
correct_frame_def, thm "wt_instr_def"];
Goalw [correct_state_def,Let_def,correct_frame_def,split_def]
@@ -66,7 +66,7 @@
\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
by (case_tac "phi C sig ! pc" 1);
by (fast_tac (claset()addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
- addss (simpset() addsimps [approx_val_def,sup_PTS_eq,map_eq_Cons]@defs1)) 1);
+ addss (simpset() addsimps [approx_val_def,thm "sup_PTS_eq",map_eq_Cons]@defs1)) 1);
qed "Bipush_correct";
Goal "G \\<turnstile> T' \\<preceq> T \\<Longrightarrow> T' = NT \\<longrightarrow> (T=NT | (\\<exists>C. T = Class C))";
@@ -133,7 +133,7 @@
\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
by (asm_full_simp_tac (simpset() addsimps [raise_xcpt_def]@defs1 addsplits [option.split]) 1);
by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [sup_state_def,map_eq_Cons]) 1);
+by (asm_full_simp_tac (simpset() addsimps [thm "sup_state_def",map_eq_Cons]) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
@@ -164,7 +164,7 @@
\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
by (asm_full_simp_tac (simpset() addsimps [raise_xcpt_def]@defs1 addsplits [option.split]) 1);
by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [sup_state_def,map_eq_Cons]) 1);
+by (asm_full_simp_tac (simpset() addsimps [thm "sup_state_def",map_eq_Cons]) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
@@ -267,7 +267,7 @@
by (forward_tac [thm "wt_jvm_prog_impl_wt_start"] 1);
ba 1;
back();
-by (asm_full_simp_tac (simpset() addsimps [thm "wt_start_def",sup_state_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [thm "wt_start_def",thm "sup_state_def"]) 1);
by (Clarify_tac 1);
(** approx_loc **)
--- a/src/HOL/MicroJava/BV/Convert.ML Mon Aug 14 14:57:29 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,246 +0,0 @@
-(* Title: HOL/MicroJava/BV/Convert.ML
- ID: $Id$
- Author: Cornelia Pusch
- Copyright 1999 Technische Universitaet Muenchen
-*)
-
-
-Goalw[sup_ty_opt_def] "G \\<turnstile> t <=o t";
-by (case_tac "t" 1);
-by Auto_tac;
-qed "sup_ty_opt_refl";
-Addsimps [sup_ty_opt_refl];
-
-Goalw[sup_loc_def] "G \\<turnstile> t <=l t";
-by (induct_tac "t" 1);
-by Auto_tac;
-qed "sup_loc_refl";
-Addsimps [sup_loc_refl];
-
-Goalw[sup_state_def] "G \\<turnstile> s <=s s";
-by Auto_tac;
-qed "sup_state_refl";
-Addsimps [sup_state_refl];
-
-val widen_PrimT_conv1 =
- prove_typerel "(G \\<turnstile> PrimT x \\<preceq> T) = (T = PrimT x)"
- [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = PrimT x"];
-Addsimps [widen_PrimT_conv1];
-
-Goalw [sup_ty_opt_def] "(G \\<turnstile> None <=o any) = (any = None)";
-by(simp_tac (simpset() addsplits [option.split]) 1);
-qed "anyConvNone";
-Addsimps [anyConvNone];
-
-Goalw [sup_ty_opt_def] "(G \\<turnstile> Some ty' <=o Some ty) = (G \\<turnstile> ty' \\<preceq> ty)";
-by(Simp_tac 1);
-qed "SomeanyConvSome";
-Addsimps [SomeanyConvSome];
-
-Goal
-"(G \\<turnstile> Some(PrimT Integer) <=o X) = (X=None \\<or> (X=Some(PrimT Integer)))";
-by (simp_tac (simpset() setloop (split_tac [ty.split,option.split]) addsimps [sup_ty_opt_def]) 1);
-qed "sup_PTS_eq";
-
-
-Goalw [sup_loc_def] "CFS \\<turnstile> [] <=l XT = (XT=[])";
-by(Simp_tac 1);
-qed "sup_loc_Nil";
-AddIffs [sup_loc_Nil];
-
-
-Goalw [sup_loc_def]
-"CFS \\<turnstile> (Y#YT) <=l XT = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> Y <=o X \\<and> CFS \\<turnstile> YT <=l XT')";
-by(simp_tac (simpset() addsimps [list_all2_Cons1]) 1);
-qed "sup_loc_Cons";
-AddIffs [sup_loc_Cons];
-
-
-Goal "\\<forall> b. G \\<turnstile> a <=l b \\<longrightarrow> length a = length b";
-by (induct_tac "a" 1);
- by (Simp_tac 1);
-by (Clarsimp_tac 1);
-qed_spec_mp "sup_loc_length";
-
-Goal "\\<forall> n b. (G \\<turnstile> a <=l b) \\<longrightarrow> n < length a \\<longrightarrow> (G \\<turnstile> (a!n) <=o (b!n))";
-by (induct_tac "a" 1);
- by (Simp_tac 1);
-by (Clarsimp_tac 1);
-by (case_tac "n" 1);
- by (Asm_full_simp_tac 1);
-by (eres_inst_tac [("x","nat")] allE 1);
-by (smp_tac 1 1);
-by (Asm_full_simp_tac 1);
-qed_spec_mp "sup_loc_nth";
-
-Goalw[sup_state_def]
-"(G \\<turnstile> (x, y) <=s (a, b)) \\<Longrightarrow> length x = length a";
-by (Clarsimp_tac 1);
-bd sup_loc_length 1;
-by Auto_tac;
-qed "sup_state_length_fst";
-
-Goalw[sup_state_def]
-"(G \\<turnstile> (x, y) <=s (a, b)) \\<longrightarrow> length y = length b";
-by (clarsimp_tac (claset(), simpset() addsimps [sup_loc_length]) 1);
-qed "sup_state_length_snd";
-
-Goal "\\<forall>b. length a = length b \\<longrightarrow> (G \\<turnstile> (a@x) <=l (b@y)) = ((G \\<turnstile> a <=l b) \\<and> (G \\<turnstile> x <=l y))";
-by (induct_tac "a" 1);
- by (Clarsimp_tac 1);
-by (Clarify_tac 1);
-by (case_tac "b" 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-qed_spec_mp "sup_loc_append";
-
-
-Goalw[sup_state_def]
-"length a = length b \\<Longrightarrow> (G \\<turnstile> (i,a@x) <=s (j,b@y)) = ((G \\<turnstile> (i,a) <=s (j,b)) \\<and> (G \\<turnstile> (i,x) <=s (j,y)))";
-by (auto_tac (claset(), simpset() addsimps [sup_loc_append]));
-qed "sup_state_append_snd";
-
-Goalw[sup_state_def]
-"length a = length b \\<Longrightarrow> (G \\<turnstile> (a@x,i) <=s (b@y,j)) = ((G \\<turnstile> (a,i) <=s (b,j)) \\<and> (G \\<turnstile> (x,i) <=s (y,j)))";
-by (auto_tac (claset(), simpset() addsimps [sup_loc_append]));
-qed "sup_state_append_fst";
-
-
-Goal "\\<forall> b. (G \\<turnstile> (rev a) <=l rev b) = (G \\<turnstile> a <=l b)";
-by (induct_tac "a" 1);
- by (Simp_tac 1);
-by (Clarsimp_tac 1);
-by Safe_tac;
- by (clarsimp_tac (claset(), simpset() addsimps [sup_loc_append, sup_loc_length]) 2);
-by (case_tac "b" 1);
- bd sup_loc_length 1;
- by (Clarsimp_tac 1);
-by (clarsimp_tac (claset(), simpset() addsimps [sup_loc_append, sup_loc_length]) 1);
-by (subgoal_tac "length (rev list) = length (rev lista)" 1);
- bd sup_loc_length 2;
- by (Clarsimp_tac 2);
-by (dres_inst_tac [("G","G"),("x","[a]"),("y","[aa]")] sup_loc_append 1);
-by (Clarsimp_tac 1);
-qed_spec_mp "sup_loc_rev";
-
-Goalw[sup_state_def]
-"(G \\<turnstile> (rev a,x) <=s (rev b,y)) = (G \\<turnstile> (a,x) <=s (b,y))";
-by (auto_tac (claset(), simpset() addsimps [sup_loc_rev, rev_map RS sym]));
-qed "sup_state_rev_fst";
-
-Goal "map x a = Y # YT \\<longrightarrow> map x (tl a) = YT \\<and> x (hd a) = Y \\<and> (\\<exists> y yt. a = y#yt)";
-by (case_tac "a" 1);
-by Auto_tac;
-qed_spec_mp "map_hd_tl";
-
-Goalw[sup_state_def]
-"(G \\<turnstile> (x#xt, a) <=s (yt, b)) = (\\<exists>y yt'. yt=y#yt' \\<and> (G \\<turnstile> x \\<preceq> y) \\<and> (G \\<turnstile> (xt,a) <=s (yt',b)))";
-by Auto_tac;
-bd map_hd_tl 1;
-by Auto_tac;
-qed "sup_state_Cons1";
-
-Goalw [sup_loc_def]
-"CFS \\<turnstile> YT <=l (X#XT) = (\\<exists>Y YT'. YT=Y#YT' \\<and> CFS \\<turnstile> Y <=o X \\<and> CFS \\<turnstile> YT' <=l XT)";
-by(simp_tac (simpset() addsimps [list_all2_Cons2]) 1);
-qed "sup_loc_Cons2";
-
-Goalw[sup_state_def]
-"(G \\<turnstile> (xt, a) <=s (y#yt, b)) = (\\<exists>x xt'. xt=x#xt' \\<and> (G \\<turnstile> x \\<preceq> y) \\<and> (G \\<turnstile> (xt',a) <=s (yt,b)))";
-by (auto_tac (claset(), simpset() addsimps [sup_loc_Cons2]));
-bd map_hd_tl 1;
-by Auto_tac;
-qed "sup_state_Cons2";
-
-Goalw[sup_state_def]
-"G \\<turnstile> (a, x) <=s (b, y) \\<Longrightarrow> G \\<turnstile> (c, x) <=s (c, y)";
-by Auto_tac;
-qed "sup_state_ignore_fst";
-
-Goalw[sup_ty_opt_def]
-"\\<lbrakk>G \\<turnstile> a <=o b; G \\<turnstile> b <=o c\\<rbrakk> \\<Longrightarrow> G \\<turnstile> a <=o c";
-by (case_tac "c" 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-by (case_tac "a" 1);
- by (Clarsimp_tac 1);
- by (case_tac "b" 1);
- by (Clarsimp_tac 1);
- by (Clarsimp_tac 1);
-by (case_tac "b" 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-be widen_trans 1;
-ba 1;
-qed "sup_ty_opt_trans";
-
-Goal "\\<lbrakk>G \\<turnstile> a <=l b; G \\<turnstile> b <=l c\\<rbrakk> \\<Longrightarrow> \\<forall> n. n < length a \\<longrightarrow> G \\<turnstile> a!n <=o c!n";
-by (Clarify_tac 1);
-by (forward_tac [sup_loc_length] 1);
-bd sup_loc_nth 1;
- ba 1;
-bd sup_loc_nth 1;
- by (Force_tac 1);
-bd sup_ty_opt_trans 1;
- ba 1;
-ba 1;
-qed "sup_loc_all_trans";
-
-Goal "\\<forall> b. length a = length b \\<longrightarrow> (\\<forall> n. n < length a \\<longrightarrow> (G \\<turnstile> (a!n) <=o (b!n))) \\<longrightarrow> (G \\<turnstile> a <=l b)";
-by (induct_tac "a" 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-by (case_tac "b=[]" 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
-by (Clarify_tac 1);
-by (res_inst_tac [("x","y")] exI 1);
-by (res_inst_tac [("x","ys")] exI 1);
-by (eres_inst_tac [("x","ys")] allE 1);
-by (Full_simp_tac 1);
-by (Clarify_tac 1);
-be impE 1;
- by (Clarsimp_tac 1);
- by (eres_inst_tac [("x","Suc n")] allE 1);
- by (Clarsimp_tac 1);
-by (eres_inst_tac [("x","0")] allE 1);
-by (Clarsimp_tac 1);
-qed_spec_mp "all_nth_sup_loc";
-
-Goal "\\<lbrakk>G \\<turnstile> a <=l b; G \\<turnstile> b <=l c\\<rbrakk> \\<Longrightarrow> G \\<turnstile> a <=l c";
-by (forward_tac [sup_loc_all_trans] 1);
- ba 1;
-bd sup_loc_length 1;
-bd sup_loc_length 1;
-br all_nth_sup_loc 1;
- by (Clarsimp_tac 1);
-ba 1;
-qed "sup_loc_trans";
-
-Goalw[sup_state_def]
-"\\<lbrakk>G \\<turnstile> a <=s b; G \\<turnstile> b <=s c\\<rbrakk> \\<Longrightarrow> G \\<turnstile> a <=s c";
-by Safe_tac;
- br sup_loc_trans 1;
- ba 1;
- ba 1;
-br sup_loc_trans 1;
- ba 1;
-ba 1;
-qed "sup_state_trans";
-
-Goalw[sup_ty_opt_def] "G \\<turnstile> a <=o Some b \\<Longrightarrow> \\<exists> x. a = Some x";
-by (case_tac "a" 1);
- by Auto_tac;
-qed "sup_ty_opt_some";
-
-
-Goalw[sup_loc_def]
-"\\<forall> n y. (G \\<turnstile> a <=o b) \\<longrightarrow> n < length y \\<longrightarrow> (G \\<turnstile> x <=l y) \\<longrightarrow> (G \\<turnstile> x[n := a] <=l y[n := b])";
-by (induct_tac "x" 1);
- by (Simp_tac 1);
-by (clarsimp_tac ((claset(), simpset()) addIffs [sup_loc_Cons2]) 1);
-by (case_tac "n" 1);
- by (clarsimp_tac (claset(), simpset() addsimps [list_all2_Cons1]) 1);
-by (clarsimp_tac (claset(), simpset() addsimps [list_all2_Cons1]) 1);
-qed_spec_mp "sup_loc_update";
--- a/src/HOL/MicroJava/BV/Convert.thy Mon Aug 14 14:57:29 2000 +0200
+++ b/src/HOL/MicroJava/BV/Convert.thy Mon Aug 14 18:03:19 2000 +0200
@@ -6,27 +6,357 @@
The supertype relation lifted to type options, type lists and state types.
*)
-Convert = JVMExec +
+theory Convert = JVMExec:
types
- locvars_type = ty option list
- opstack_type = ty list
- state_type = "opstack_type \\<times> locvars_type"
+ locvars_type = "ty option list"
+ opstack_type = "ty list"
+ state_type = "opstack_type \<times> locvars_type"
constdefs
- sup_ty_opt :: "['code prog,ty option,ty option] \\<Rightarrow> bool" ("_ \\<turnstile>_ <=o _")
- "G \\<turnstile> a' <=o a \\<equiv>
- case a of
- None \\<Rightarrow> True
- | Some t \\<Rightarrow> case a' of
- None \\<Rightarrow> False
- | Some t' \\<Rightarrow> G \\<turnstile> t' \\<preceq> t"
+ (* lifts a relation to option with None as top element *)
+ lift_top :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a option \<Rightarrow> 'a option \<Rightarrow> bool)"
+ "lift_top P a' a \<equiv> case a of
+ None \<Rightarrow> True
+ | Some t \<Rightarrow> (case a' of None \<Rightarrow> False | Some t' \<Rightarrow> P t' t)"
+
+
+ sup_ty_opt :: "['code prog,ty option,ty option] \<Rightarrow> bool" ("_ \<turnstile>_ <=o _")
+ "sup_ty_opt G \<equiv> lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
+
+ sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool" ("_ \<turnstile> _ <=l _" [71,71] 70)
+ "G \<turnstile> LT <=l LT' \<equiv> list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'"
+
+ sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool" ("_ \<turnstile> _ <=s _" [71,71] 70)
+ "G \<turnstile> s <=s s' \<equiv> (G \<turnstile> map Some (fst s) <=l map Some (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
+
+
+lemma lift_top_refl [simp]:
+ "[| !!x. P x x |] ==> lift_top P x x"
+ by (simp add: lift_top_def split: option.splits)
+
+lemma lift_top_trans [trans]:
+ "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |] ==> lift_top P x z"
+proof -
+ assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z"
+ assume a: "lift_top P x y"
+ assume b: "lift_top P y z"
+
+ { assume "z = None"
+ hence ?thesis by (simp add: lift_top_def)
+ } note z_none = this
+
+ { assume "x = None"
+ with a b
+ have ?thesis
+ by (simp add: lift_top_def split: option.splits)
+ } note x_none = this
+
+ { fix r t
+ assume x: "x = Some r" and z: "z = Some t"
+ with a b
+ obtain s where y: "y = Some s"
+ by (simp add: lift_top_def split: option.splits)
+
+ from a x y
+ have "P r s" by (simp add: lift_top_def)
+ also
+ from b y z
+ have "P s t" by (simp add: lift_top_def)
+ finally
+ have "P r t" .
+
+ with x z
+ have ?thesis by (simp add: lift_top_def)
+ }
+
+ with x_none z_none
+ show ?thesis by blast
+qed
+
+lemma lift_top_None_any [simp]:
+ "lift_top P None any = (any = None)"
+ by (simp add: lift_top_def split: option.splits)
+
+lemma lift_top_Some_Some [simp]:
+ "lift_top P (Some a) (Some b) = P a b"
+ by (simp add: lift_top_def split: option.splits)
+
+lemma lift_top_any_Some [simp]:
+ "lift_top P any (Some b) = (\<exists>a. any = Some a \<and> P a b)"
+ by (simp add: lift_top_def split: option.splits)
+
+lemma lift_top_Some_any:
+ "lift_top P (Some a) any = (any = None \<or> (\<exists>b. any = Some b \<and> P a b))"
+ by (simp add: lift_top_def split: option.splits)
+
+
+
+theorem sup_ty_opt_refl [simp]:
+ "G \<turnstile> t <=o t"
+ by (simp add: sup_ty_opt_def)
+
+theorem sup_loc_refl [simp]:
+ "G \<turnstile> t <=l t"
+ by (induct t, auto simp add: sup_loc_def)
+
+theorem sup_state_refl [simp]:
+ "G \<turnstile> s <=s s"
+ by (simp add: sup_state_def)
+
+
+
+theorem anyConvNone [simp]:
+ "(G \<turnstile> None <=o any) = (any = None)"
+ by (simp add: sup_ty_opt_def)
+
+theorem SomeanyConvSome [simp]:
+ "(G \<turnstile> (Some ty') <=o (Some ty)) = (G \<turnstile> ty' \<preceq> ty)"
+ by (simp add: sup_ty_opt_def)
+
+theorem sup_ty_opt_Some:
+ "G \<turnstile> a <=o (Some b) \<Longrightarrow> \<exists> x. a = Some x"
+ by (clarsimp simp add: sup_ty_opt_def)
+
+lemma widen_PrimT_conv1 [simp]:
+ "[| G \<turnstile> S \<preceq> T; S = PrimT x|] ==> T = PrimT x"
+ by (auto elim: widen.elims)
+
+theorem sup_PTS_eq:
+ "(G \<turnstile> Some (PrimT p) <=o X) = (X=None \<or> X = Some (PrimT p))"
+ by (auto simp add: sup_ty_opt_def lift_top_Some_any)
+
+
+
+theorem sup_loc_Nil [iff]:
+ "(G \<turnstile> [] <=l XT) = (XT=[])"
+ by (simp add: sup_loc_def)
+
+theorem sup_loc_Cons [iff]:
+ "(G \<turnstile> (Y#YT) <=l XT) = (\<exists>X XT'. XT=X#XT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT <=l XT'))"
+ by (simp add: sup_loc_def list_all2_Cons1)
+
+theorem sup_loc_Cons2:
+ "(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))";
+ by (simp add: sup_loc_def list_all2_Cons2)
+
+
+theorem sup_loc_length:
+ "G \<turnstile> a <=l b \<Longrightarrow> length a = length b"
+proof -
+ assume G: "G \<turnstile> a <=l b"
+ have "\<forall> b. (G \<turnstile> a <=l b) \<longrightarrow> length a = length b"
+ by (induct a, auto)
+ with G
+ show ?thesis by blast
+qed
+
+theorem sup_loc_nth:
+ "[| G \<turnstile> a <=l b; n < length a |] ==> G \<turnstile> (a!n) <=o (b!n)"
+proof -
+ assume a: "G \<turnstile> a <=l b" "n < length a"
+ have "\<forall> n b. (G \<turnstile> a <=l b) \<longrightarrow> n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))"
+ (is "?P a")
+ proof (induct a)
+ show "?P []" by simp
+
+ fix x xs assume IH: "?P xs"
+
+ show "?P (x#xs)"
+ proof (intro strip)
+ fix n b
+ assume "G \<turnstile> (x # xs) <=l b" "n < length (x # xs)"
+ with IH
+ show "G \<turnstile> ((x # xs) ! n) <=o (b ! n)"
+ by - (cases n, auto)
+ qed
+ qed
+ with a
+ show ?thesis by blast
+qed
+
+
+theorem all_nth_sup_loc:
+ "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))) \<longrightarrow> (G \<turnstile> a <=l b)"
+ (is "?P a")
+proof (induct a)
+ show "?P []" by simp
- sup_loc :: "['code prog,locvars_type,locvars_type] \\<Rightarrow> bool" ("_ \\<turnstile> _ <=l _" [71,71] 70)
- "G \\<turnstile> LT <=l LT' \\<equiv> list_all2 (%t t'. G \\<turnstile> t <=o t') LT LT'"
+ fix l ls assume IH: "?P ls"
+
+ show "?P (l#ls)"
+ proof (intro strip)
+ fix b
+ assume f: "\<forall>n. n < length (l # ls) \<longrightarrow> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
+ assume l: "length (l#ls) = length b"
+
+ then obtain b' bs where b: "b = b'#bs"
+ by - (cases b, simp, simp add: neq_Nil_conv, rule that)
+
+ with f
+ have "\<forall>n. n < length ls \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"
+ by auto
+
+ with f b l IH
+ show "G \<turnstile> (l # ls) <=l b"
+ by auto
+ qed
+qed
+
+
+theorem sup_loc_append:
+ "[| length a = length b |] ==> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
+proof -
+ assume l: "length a = length b"
+
+ have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
+ (is "?P a")
+ proof (induct a)
+ show "?P []" by simp
+
+ fix l ls assume IH: "?P ls"
+ show "?P (l#ls)"
+ proof (intro strip)
+ fix b
+ assume "length (l#ls) = length (b::ty option list)"
+ with IH
+ show "(G \<turnstile> ((l#ls)@x) <=l (b@y)) = ((G \<turnstile> (l#ls) <=l b) \<and> (G \<turnstile> x <=l y))"
+ by - (cases b, auto)
+ qed
+ qed
+ with l
+ show ?thesis by blast
+qed
+
+theorem sup_loc_rev [simp]:
+ "(G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)"
+proof -
+ have "\<forall>b. (G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)" (is "\<forall>b. ?Q a b" is "?P a")
+ proof (induct a)
+ show "?P []" by simp
+
+ fix l ls assume IH: "?P ls"
+
+ {
+ fix b
+ have "?Q (l#ls) b"
+ proof (cases b)
+ case Nil
+ thus ?thesis by (auto dest: sup_loc_length)
+ next
+ case Cons
+ show ?thesis
+ proof
+ assume "G \<turnstile> (l # ls) <=l b"
+ thus "G \<turnstile> rev (l # ls) <=l rev b"
+ by (clarsimp simp add: Cons IH sup_loc_length sup_loc_append)
+ next
+ assume "G \<turnstile> rev (l # ls) <=l rev b"
+ hence G: "G \<turnstile> (rev ls @ [l]) <=l (rev list @ [a])"
+ by (simp add: Cons)
+
+ hence "length (rev ls) = length (rev list)"
+ by (auto dest: sup_loc_length)
+
+ from this G
+ obtain "G \<turnstile> rev ls <=l rev list" "G \<turnstile> l <=o a"
+ by (simp add: sup_loc_append)
+
+ thus "G \<turnstile> (l # ls) <=l b"
+ by (simp add: Cons IH)
+ qed
+ qed
+ }
+ thus "?P (l#ls)" by blast
+ qed
- sup_state :: "['code prog,state_type,state_type] \\<Rightarrow> bool" ("_ \\<turnstile> _ <=s _" [71,71] 70)
- "G \\<turnstile> s <=s s' \\<equiv> G \\<turnstile> map Some (fst s) <=l map Some (fst s') \\<and> G \\<turnstile> snd s <=l snd s'"
+ thus ?thesis by blast
+qed
+
+
+theorem sup_loc_update [rulify]:
+ "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> (G \<turnstile> x[n := a] <=l y[n := b])"
+ (is "?P x")
+proof (induct x)
+ show "?P []" by simp
+
+ fix l ls assume IH: "?P ls"
+ show "?P (l#ls)"
+ proof (intro strip)
+ fix n y
+ assume "G \<turnstile>a <=o b" "G \<turnstile> (l # ls) <=l y" "n < length y"
+ with IH
+ show "G \<turnstile> (l # ls)[n := a] <=l y[n := b]"
+ by - (cases n, auto simp add: sup_loc_Cons2 list_all2_Cons1)
+ qed
+qed
+
+
+theorem sup_state_length [simp]:
+ "G \<turnstile> s2 <=s s1 \<Longrightarrow> length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
+ by (auto dest: sup_loc_length simp add: sup_state_def);
+
+theorem sup_state_append_snd:
+ "length a = length b \<Longrightarrow> (G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))"
+ by (auto simp add: sup_state_def sup_loc_append)
+
+theorem sup_state_append_fst:
+ "length a = length b \<Longrightarrow> (G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))"
+ by (auto simp add: sup_state_def sup_loc_append)
+
+theorem sup_state_Cons1:
+ "(G \<turnstile> (x#xt, a) <=s (yt, b)) = (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))"
+ by (auto simp add: sup_state_def map_eq_Cons)
+
+theorem sup_state_Cons2:
+ "(G \<turnstile> (xt, a) <=s (y#yt, b)) = (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))"
+ by (auto simp add: sup_state_def map_eq_Cons sup_loc_Cons2)
+
+theorem sup_state_ignore_fst:
+ "G \<turnstile> (a, x) <=s (b, y) \<Longrightarrow> G \<turnstile> (c, x) <=s (c, y)"
+ by (simp add: sup_state_def)
+
+theorem sup_state_rev_fst:
+ "(G \<turnstile> (rev a, x) <=s (rev b, y)) = (G \<turnstile> (a, x) <=s (b, y))"
+proof -
+ have m: "!!f x. map f (rev x) = rev (map f x)" by (simp add: rev_map)
+ show ?thesis by (simp add: m sup_state_def)
+qed
+
+theorem sup_ty_opt_trans [trans]:
+ "\<lbrakk>G \<turnstile> a <=o b; G \<turnstile> b <=o c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=o c"
+ by (auto intro: lift_top_trans widen_trans simp add: sup_ty_opt_def)
+
+
+theorem sup_loc_trans [trans]:
+ "\<lbrakk>G \<turnstile> a <=l b; G \<turnstile> b <=l c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=l c"
+proof -
+ assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c"
+
+ hence "\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (c!n))"
+ proof (intro strip)
+ fix n
+ assume n: "n < length a"
+ with G
+ have "G \<turnstile> (a!n) <=o (b!n)"
+ by - (rule sup_loc_nth)
+ also
+ from n G
+ have "G \<turnstile> ... <=o (c!n)"
+ by - (rule sup_loc_nth, auto dest: sup_loc_length)
+ finally
+ show "G \<turnstile> (a!n) <=o (c!n)" .
+ qed
+
+ with G
+ show ?thesis
+ by (auto intro!: all_nth_sup_loc [rulify] dest!: sup_loc_length)
+qed
+
+
+theorem sup_state_trans [trans]:
+ "\<lbrakk>G \<turnstile> a <=s b; G \<turnstile> b <=s c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=s c"
+ by (auto intro: sup_loc_trans simp add: sup_state_def)
end
--- a/src/HOL/MicroJava/BV/Correct.ML Mon Aug 14 14:57:29 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.ML Mon Aug 14 18:03:19 2000 +0200
@@ -41,7 +41,7 @@
"\\<lbrakk> wf_prog wt G \\<rbrakk> \
\\\<Longrightarrow> approx_val G hp v (Some T) \\<longrightarrow> G\\<turnstile> T\\<preceq>T' \\<longrightarrow> approx_val G hp v (Some T')";
by (case_tac "T" 1);
- by (Asm_simp_tac 1);
+ by (fast_tac (claset() addIs [conf_widen] addss (simpset()addsimps[approx_val_def])) 1);
by (fast_tac (claset() addIs [conf_widen] addss (simpset()addsimps[approx_val_def])) 1);
qed_spec_mp "approx_val_imp_approx_val_assConvertible";
@@ -63,7 +63,7 @@
Goal
"wf_prog wt G \\<Longrightarrow> approx_val G h val us \\<longrightarrow> G \\<turnstile> us <=o us' \\<longrightarrow> approx_val G h val us'";
-by (asm_simp_tac (simpset() addsimps [sup_PTS_eq,approx_val_def] addsplits [option.split,val_.split,ty.split]) 1);
+by (asm_simp_tac (simpset() addsimps [thm "sup_PTS_eq",approx_val_def] addsplits [option.split,val_.split,ty.split]) 1);
by(blast_tac (claset() addIs [conf_widen]) 1);
qed_spec_mp "approx_val_imp_approx_val_sup";
@@ -104,7 +104,7 @@
qed_spec_mp "approx_loc_imp_approx_loc_sup_heap";
-Goalw [sup_loc_def,approx_loc_def,list_all2_def]
+Goalw [thm "sup_loc_def",approx_loc_def,list_all2_def]
"wf_prog wt G \\<Longrightarrow> approx_loc G hp lvars lt \\<longrightarrow> G \\<turnstile> lt <=l lt' \\<longrightarrow> approx_loc G hp lvars lt'";
by (auto_tac (claset() , simpset() addsimps [all_set_conv_all_nth,split_def]));
by (auto_tac (claset() addEs [approx_val_imp_approx_val_sup] , simpset()));
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Mon Aug 14 14:57:29 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Mon Aug 14 18:03:19 2000 +0200
@@ -475,13 +475,15 @@
lemma fits_imp_wtl_method_complete:
-"\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\<rbrakk> \<Longrightarrow> wtl_method G C pTs rT mxl ins cert"
-by (simp add: wt_method_def wtl_method_def del: split_paired_Ex)
- (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def simp del: split_paired_Ex)
+"\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\<rbrakk>
+ \<Longrightarrow> wtl_method G C pTs rT mxl ins cert"
+by (simp add: wt_method_def wtl_method_def)
+ (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def)
lemma wtl_method_complete:
-"\<lbrakk>wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\<rbrakk> \<Longrightarrow> wtl_method G C pTs rT mxl ins (make_cert ins phi)"
+"\<lbrakk>wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\<rbrakk>
+ \<Longrightarrow> wtl_method G C pTs rT mxl ins (make_cert ins phi)"
proof -
assume * : "wt_method G C pTs rT mxl ins phi" "wf_prog wf_mb G"
--- a/src/HOL/MicroJava/BV/Step.thy Mon Aug 14 14:57:29 2000 +0200
+++ b/src/HOL/MicroJava/BV/Step.thy Mon Aug 14 18:03:19 2000 +0200
@@ -10,7 +10,7 @@
theory Step = Convert :
-text "Effect of instruction on the state type"
+text "Effect of instruction on the state type:"
consts
step :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type option"
@@ -39,7 +39,7 @@
"step (i,G,s) = None"
-text "Conditions under which step is applicable"
+text "Conditions under which step is applicable:"
consts
app :: "instr \<times> jvm_prog \<times> ty \<times> state_type \<Rightarrow> bool"
@@ -84,7 +84,7 @@
"app (i,G,rT,s) = False"
-text {* \verb,p_count, of successor instructions *}
+text {* program counter of successor instructions: *}
consts
succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count set"
@@ -134,10 +134,8 @@
text {*
\medskip
-simp rules for @{term app} without patterns, better suited for proofs
-\medskip
+simp rules for \isa{app} without patterns, better suited for proofs:
*}
-
lemma appStore[simp]:
"app (Store idx, G, rT, s) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
--- a/src/HOL/MicroJava/BV/StepMono.thy Mon Aug 14 14:57:29 2000 +0200
+++ b/src/HOL/MicroJava/BV/StepMono.thy Mon Aug 14 18:03:19 2000 +0200
@@ -4,34 +4,13 @@
Copyright 2000 Technische Universitaet Muenchen
*)
-header {* Monotonicity of \texttt{step} and \texttt{app} *}
-
-theory StepMono = Step :
-
+header {* Monotonicity of step and app *}
-lemmas [trans] = sup_state_trans sup_loc_trans widen_trans
-
+theory StepMono = Step:
-lemma sup_state_length:
-"G \<turnstile> s2 <=s s1 \<Longrightarrow> length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
- by (cases s1, cases s2, simp add: sup_state_length_fst sup_state_length_snd)
-
lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
-proof
- show "xb = PrimT p \<Longrightarrow> G \<turnstile> xb \<preceq> PrimT p" by blast
-
- show "G\<turnstile> xb \<preceq> PrimT p \<Longrightarrow> xb = PrimT p"
- proof (cases xb)
- fix prim
- assume "xb = PrimT prim" "G\<turnstile>xb\<preceq>PrimT p"
- thus ?thesis by simp
- next
- fix ref
- assume "G\<turnstile>xb\<preceq>PrimT p" "xb = RefT ref"
- thus ?thesis by simp (rule widen_RefT [elimify], auto)
- qed
-qed
+ by (auto elim: widen.elims)
lemma sup_loc_some [rulify]:
@@ -50,7 +29,7 @@
show "(\<exists>t. (a # list) ! n = Some t) \<and> G \<turnstile>(a # list) ! n <=o Some t"
proof (cases n)
case 0
- with * show ?thesis by (simp add: sup_ty_opt_some)
+ with * show ?thesis by (simp add: sup_ty_opt_Some)
next
case Suc
with Cons *
@@ -159,7 +138,7 @@
with G app
show ?thesis
by - (cases s2,
- auto dest: map_hd_tl simp add: sup_loc_Cons2 sup_loc_length sup_state_def)
+ auto simp add: map_eq_Cons sup_loc_Cons2 sup_loc_length sup_state_def)
next
case Bipush
thus ?thesis by simp