# HG changeset patch
# User kleing
# Date 952614596 -3600
# Node ID 6db1309c8241246166c1c8d2113d8d4ce13a4398
# Parent  c7772d3787c3657a5a6c1384a39ebe99de52c6b3
moved more lemmas to Convert (transitivity etc)

diff -r c7772d3787c3 -r 6db1309c8241 src/HOL/MicroJava/BV/Convert.ML
--- 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";
diff -r c7772d3787c3 -r 6db1309c8241 src/HOL/MicroJava/BV/LBVComplete.ML
--- a/src/HOL/MicroJava/BV/LBVComplete.ML	Thu Mar 09 16:07:38 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.ML	Thu Mar 09 16:09:56 2000 +0100
@@ -113,79 +113,6 @@
 qed "rev_append_cons";
 
 
-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";
-
-
-Goal "map f (rev l) = rev (map f l)";
-by (induct_tac "l" 1);
-by Auto_tac;
-qed "map_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, map_rev]));
-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"; 
-
 Goal "G \\<turnstile> b \\<preceq> NT \\<Longrightarrow> b = NT";
 by (exhaust_tac "b" 1);
  by (exhaust_tac "ref_ty" 2);
@@ -198,84 +125,6 @@
 qed "widen_Class";
 
 
-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";
-
 Goal "\\<forall>b. length a = length b \\<longrightarrow> (\\<forall>x\\<in>set (zip a b). x \\<in> widen G) = (G \\<turnstile> (map Some a) <=l (map Some b))";
 by (induct_tac "a" 1);
  by (Clarsimp_tac 1);
@@ -344,11 +193,6 @@
 qed "method_inv_pseudo_mono";
 
 
-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> 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)))";
 by (induct_tac "b" 1);
@@ -370,17 +214,6 @@
 qed "mono_load";
 
 
-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";
-
-
 Goalw[sup_state_def] 
 "\\<lbrakk>G \\<turnstile> (a, b) <=s (ts # ST', y); n < length y\\<rbrakk> \\<Longrightarrow> \
 \ \\<exists> t a'. a = t#a' \\<and> G \\<turnstile> (a', b[n := Some t]) <=s (ST', y[n := Some ts])";