--- a/src/HOL/MicroJava/BV/Convert.ML Thu Mar 09 16:07:38 2000 +0100
+++ b/src/HOL/MicroJava/BV/Convert.ML Thu Mar 09 16:09:56 2000 +0100
@@ -56,7 +56,6 @@
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);
@@ -86,3 +85,162 @@
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 (exhaust_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 (exhaust_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 (exhaust_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 (exhaust_tac "c" 1);
+ by (Clarsimp_tac 1);
+by (Clarsimp_tac 1);
+by (exhaust_tac "a" 1);
+ by (Clarsimp_tac 1);
+ by (exhaust_tac "b" 1);
+ by (Clarsimp_tac 1);
+ by (Clarsimp_tac 1);
+by (exhaust_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 (exhaust_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 (exhaust_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 (exhaust_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";