# HG changeset patch
# User nipkow
# Date 947516849 -3600
# Node ID 759f712f8f061bda27096fd682211401f6278545
# Parent  c802042066e86ba680d72d8f949ebeedd2bdac36
int:nat->int is pushed inwards.

diff -r c802042066e8 -r 759f712f8f06 src/HOL/Integ/NatBin.ML
--- a/src/HOL/Integ/NatBin.ML	Mon Jan 10 16:06:43 2000 +0100
+++ b/src/HOL/Integ/NatBin.ML	Mon Jan 10 16:07:29 2000 +0100
@@ -462,3 +462,6 @@
 Addsimps [eq_number_of_Suc, Suc_eq_number_of, 
 	  less_number_of_Suc, less_Suc_number_of, 
 	  le_number_of_Suc, le_Suc_number_of];
+
+(* Pusch int(.) inwards: *)
+Addsimps [int_Suc,zadd_int RS sym];
diff -r c802042066e8 -r 759f712f8f06 src/HOL/MicroJava/J/Conform.ML
--- a/src/HOL/MicroJava/J/Conform.ML	Mon Jan 10 16:06:43 2000 +0100
+++ b/src/HOL/MicroJava/J/Conform.ML	Mon Jan 10 16:07:29 2000 +0100
@@ -135,16 +135,15 @@
 qed_spec_mp "non_np_objD'";
 
 Goal "wf_prog wf_mb G \\<Longrightarrow> \\<forall>Ts Ts'. list_all2 (conf G h) vs Ts \\<longrightarrow> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') Ts Ts' \\<longrightarrow>  list_all2 (conf G h) vs Ts'";
-by( induct_tac "vs" 1);
-by(  ALLGOALS Clarsimp_tac);
-by(  ALLGOALS (forward_tac [list_all2_lengthD RS sym]));
-by(  ALLGOALS (full_simp_tac (simpset()addsimps[length_Suc_conv])));
-by(  Safe_tac);
-by(  rotate_tac ~1 1);
-by(  ALLGOALS (forward_tac [list_all2_lengthD RS sym]));
-by(  ALLGOALS (full_simp_tac (simpset()addsimps[length_Suc_conv])));
-by(  ALLGOALS Clarify_tac);
-by( fast_tac (claset() addEs [conf_widen]) 1);
+by(induct_tac "vs" 1);
+ by(ALLGOALS Clarsimp_tac);
+by(forward_tac [list_all2_lengthD RS sym] 1);
+by(full_simp_tac (simpset()addsimps[length_Suc_conv]) 1);
+by(Safe_tac);
+by(forward_tac [list_all2_lengthD RS sym] 1);
+by(full_simp_tac (simpset()addsimps[length_Suc_conv]) 1);
+by(Clarify_tac 1);
+by(fast_tac (claset() addEs [conf_widen]) 1);
 qed_spec_mp "conf_list_gext_widen";
 
 
diff -r c802042066e8 -r 759f712f8f06 src/HOL/MicroJava/J/JBasis.ML
--- a/src/HOL/MicroJava/J/JBasis.ML	Mon Jan 10 16:06:43 2000 +0100
+++ b/src/HOL/MicroJava/J/JBasis.ML	Mon Jan 10 16:07:29 2000 +0100
@@ -67,6 +67,10 @@
 		rotate_tac ~1,asm_full_simp_tac 
 	(simpset() delsimps [split_paired_All,split_paired_Ex])];
 
+Goal "{y. x = Some y} \\<subseteq> {the x}";
+by Auto_tac;
+qed "some_subset_the";
+
 fun ex_ftac thm = EVERY' [forward_tac [thm], REPEAT o (etac exE), rotate_tac ~1,
   asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])];
 
@@ -135,21 +139,6 @@
 	auto_tac(claset_of Prod.thy,simpset_of Prod.thy)]);
 
 
-section "list_all2";
-
-val list_all2_lengthD = prove_goalw thy [list_all2_def] 
- "\\<And>X. list_all2 P as bs \\<Longrightarrow> length as = length bs" (K [Auto_tac]);
-
-val list_all2_Nil = prove_goalw thy [list_all2_def] 
- "list_all2 P [] []" (K [Auto_tac]);
-Addsimps[list_all2_Nil];
-AddSIs[list_all2_Nil];
-
-val list_all2_Cons = prove_goalw thy [list_all2_def] 
- "\\<And>X. list_all2 P (a#as) (b#bs) = (P a b \\<and> list_all2 P as bs)" (K [Auto_tac]);
-AddIffs[list_all2_Cons];
-
-
 (* More about Maps *)
 
 val override_SomeD = prove_goalw thy [override_def] "(s \\<oplus> t) k = Some x \\<Longrightarrow> \
diff -r c802042066e8 -r 759f712f8f06 src/HOL/MicroJava/J/JBasis.thy
--- a/src/HOL/MicroJava/J/JBasis.thy	Mon Jan 10 16:06:43 2000 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy	Mon Jan 10 16:07:29 2000 +0100
@@ -13,7 +13,4 @@
   unique  :: "('a \\<times> 'b) list \\<Rightarrow> bool"
  "unique  \\<equiv> nodups \\<circ> map fst"
 
-  list_all2 :: "('a \\<Rightarrow> 'b \\<Rightarrow> bool) \\<Rightarrow> ('a list \\<Rightarrow> 'b list \\<Rightarrow> bool)"
- "list_all2 P xs ys \\<equiv> length xs = length ys \\<and> (\\<forall> (x,y)\\<in>set (zip xs ys). P x y)"
-
 end