--- a/src/HOL/MicroJava/BV/Convert.ML Thu Mar 09 13:54:03 2000 +0100
+++ b/src/HOL/MicroJava/BV/Convert.ML Thu Mar 09 13:55:39 2000 +0100
@@ -43,7 +43,6 @@
qed "sup_PTS_eq";
-
Goalw [sup_loc_def] "CFS \\<turnstile> [] <=l XT = (XT=[])";
by(Simp_tac 1);
qed "sup_loc_Nil";
@@ -56,3 +55,34 @@
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 (exhaust_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";
+