# HG changeset patch
# User paulson
# Date 1010502549 -3600
# Node ID 7e6eaaa125f2a3a9ccbdafff8d6175105808c1de
# Parent  9842befead7ad3f9196431aedf4ef639d6d59113
Added some simprules proofs.
Converted theories CardinalArith and OrdQuant to Isar style

diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/AC/AC7_AC9.ML
--- a/src/ZF/AC/AC7_AC9.ML	Tue Jan 08 15:39:47 2002 +0100
+++ b/src/ZF/AC/AC7_AC9.ML	Tue Jan 08 16:09:09 2002 +0100
@@ -161,7 +161,8 @@
 \        B1: C;  B2: C |]  \
 \     ==> B1 eqpoll B2";
 by (blast_tac
-    (claset() addSIs [nat_lepoll_lemma, nat_cons_eqpoll RS eqpoll_trans, 
+    (claset() delrules [eqpoll_refl]
+	      addSIs [nat_lepoll_lemma, nat_cons_eqpoll RS eqpoll_trans, 
                       eqpoll_refl RSN (2, prod_eqpoll_cong)]
               addIs [eqpoll_trans, eqpoll_sym, Sigma_fun_space_eqpoll]) 1);
 val lemma1 = result();
diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/AC/AC_Equiv.ML
--- a/src/ZF/AC/AC_Equiv.ML	Tue Jan 08 15:39:47 2002 +0100
+++ b/src/ZF/AC/AC_Equiv.ML	Tue Jan 08 16:09:09 2002 +0100
@@ -26,7 +26,7 @@
 
 (* used in \\<in> AC10-AC15.ML AC16WO4.ML WO6WO1.ML *)
 (*I don't know where to put this one.*)
-goal Cardinal.thy
+Goal
      "!!m A B. [| A lepoll succ(m); B \\<subseteq> A; B\\<noteq>0 |] ==> A-B lepoll m";
 by (rtac not_emptyE 1 THEN (assume_tac 1));
 by (ftac singleton_subsetI 1);
@@ -65,7 +65,7 @@
 qed "ordertype_Int";
 
 (* used only in AC16_lemmas.ML *)
-goalw CardinalArith.thy [InfCard_def]
+Goalw [InfCard_def]
         "!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)";
 by (asm_simp_tac (simpset() addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1);
 qed "Inf_Card_is_InfCard";
diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/AC/WO6_WO1.ML
--- a/src/ZF/AC/WO6_WO1.ML	Tue Jan 08 15:39:47 2002 +0100
+++ b/src/ZF/AC/WO6_WO1.ML	Tue Jan 08 16:09:09 2002 +0100
@@ -290,6 +290,7 @@
         uu_subset1 RSN (4, rel_is_fun)))] 1
         THEN TRYALL assume_tac);
 by (rtac (eqpoll_sym RS eqpoll_imp_lepoll RSN (2, supset_lepoll_imp_eq)) 1);
+by (REPEAT_FIRST assume_tac);
 by (REPEAT (fast_tac (claset() addSIs [domain_uu_subset]) 1));
 qed "uu_Least_is_fun";
 
diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Tue Jan 08 15:39:47 2002 +0100
+++ b/src/ZF/Cardinal.ML	Tue Jan 08 16:09:09 2002 +0100
@@ -57,6 +57,7 @@
 
 (*A eqpoll A*)
 bind_thm ("eqpoll_refl", id_bij RS bij_imp_eqpoll);
+Addsimps [eqpoll_refl];
 
 Goalw [eqpoll_def] "X eqpoll Y ==> Y eqpoll X";
 by (blast_tac (claset() addIs [bij_converse_bij]) 1);
@@ -75,6 +76,7 @@
 qed "subset_imp_lepoll";
 
 bind_thm ("lepoll_refl", subset_refl RS subset_imp_lepoll);
+Addsimps [lepoll_refl];
 
 bind_thm ("le_imp_lepoll", le_imp_subset RS subset_imp_lepoll);
 
diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Tue Jan 08 15:39:47 2002 +0100
+++ b/src/ZF/CardinalArith.ML	Tue Jan 08 16:09:09 2002 +0100
@@ -11,6 +11,14 @@
 coincide with union (maximum).  Either way we get most laws for free.
 *)
 
+val InfCard_def = thm "InfCard_def";
+val cmult_def = thm "cmult_def";
+val cadd_def = thm "cadd_def";
+val csquare_rel_def = thm "csquare_rel_def";
+val jump_cardinal_def = thm "jump_cardinal_def";
+val csucc_def = thm "csucc_def";
+
+
 (*** Cardinal addition ***)
 
 (** Cardinal addition is commutative **)
diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Tue Jan 08 15:39:47 2002 +0100
+++ b/src/ZF/CardinalArith.thy	Tue Jan 08 16:09:09 2002 +0100
@@ -6,41 +6,100 @@
 Cardinal Arithmetic
 *)
 
-CardinalArith = Cardinal + OrderArith + ArithSimp + Finite + 
-consts
+theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite:
 
-  InfCard       :: i=>o
-  "|*|"         :: [i,i]=>i       (infixl 70)
-  "|+|"         :: [i,i]=>i       (infixl 65)
-  csquare_rel   :: i=>i
-  jump_cardinal :: i=>i
-  csucc         :: i=>i
+constdefs
 
-defs
+  InfCard       :: "i=>o"
+    "InfCard(i) == Card(i) & nat le i"
 
-  InfCard_def  "InfCard(i) == Card(i) & nat le i"
-
-  cadd_def     "i |+| j == |i+j|"
-
-  cmult_def    "i |*| j == |i*j|"
+  cmult         :: "[i,i]=>i"       (infixl "|*|" 70)
+    "i |*| j == |i*j|"
+  
+  cadd          :: "[i,i]=>i"       (infixl "|+|" 65)
+    "i |+| j == |i+j|"
 
-  csquare_rel_def
-  "csquare_rel(K) ==   
-        rvimage(K*K,   
-                lam <x,y>:K*K. <x Un y, x, y>, 
-                rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
+  csquare_rel   :: "i=>i"
+    "csquare_rel(K) ==   
+	  rvimage(K*K,   
+		  lam <x,y>:K*K. <x Un y, x, y>, 
+		  rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
 
   (*This def is more complex than Kunen's but it more easily proved to
     be a cardinal*)
-  jump_cardinal_def
-      "jump_cardinal(K) ==   
+  jump_cardinal :: "i=>i"
+    "jump_cardinal(K) ==   
          UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
-
+  
   (*needed because jump_cardinal(K) might not be the successor of K*)
-  csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
+  csucc         :: "i=>i"
+    "csucc(K) == LEAST L. Card(L) & K<L"
 
 syntax (xsymbols)
-  "op |+|"     :: [i,i] => i          (infixl "\\<oplus>" 65)
-  "op |*|"     :: [i,i] => i          (infixl "\\<otimes>" 70)
+  "op |+|"     :: "[i,i] => i"          (infixl "\<oplus>" 65)
+  "op |*|"     :: "[i,i] => i"          (infixl "\<otimes>" 70)
+
+
+(*** The following really belong in OrderType ***)
+
+lemma oadd_eq_0_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i ++ j) = 0 <-> i=0 & j=0"
+apply (erule trans_induct3 [of j])
+apply (simp_all add: oadd_Limit)
+apply (simp add: Union_empty_iff Limit_def lt_def)
+apply blast
+done
+
+lemma oadd_eq_lt_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> 0 < (i ++ j) <-> 0<i | 0<j"
+by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)
+
+lemma oadd_lt_self: "[| Ord(i);  0<j |] ==> i < i++j"
+apply (rule lt_trans2) 
+apply (erule le_refl) 
+apply (simp only: lt_Ord2  oadd_1 [of i, symmetric]) 
+apply (blast intro: succ_leI oadd_le_mono)
+done
+
+lemma oadd_LimitI: "\<lbrakk>Ord(i); Limit(j)\<rbrakk> \<Longrightarrow> Limit(i ++ j)"
+apply (simp add: oadd_Limit)
+apply (frule Limit_has_1 [THEN ltD])
+apply (rule increasing_LimitI)
+ apply (rule Ord_0_lt)
+  apply (blast intro: Ord_in_Ord [OF Limit_is_Ord])
+ apply (force simp add: Union_empty_iff oadd_eq_0_iff
+                        Limit_is_Ord [of j, THEN Ord_in_Ord])
+apply auto
+apply (rule_tac x="succ(x)" in bexI)
+ apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])
+apply (simp add: Limit_def lt_def) 
+done
+
+(*** The following really belong in Cardinal ***)
+
+lemma lesspoll_not_refl: "~ (i lesspoll i)"
+by (simp add: lesspoll_def) 
+
+lemma lesspoll_irrefl [elim!]: "i lesspoll i ==> P"
+by (simp add: lesspoll_def) 
+
+lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))"
+apply (rule CardI) 
+ apply (simp add: Card_is_Ord) 
+apply (clarify dest!: ltD)
+apply (drule bspec, assumption) 
+apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord) 
+apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
+apply (drule lesspoll_trans1, assumption) 
+apply (subgoal_tac "B lepoll \<Union>A")
+ apply (drule lesspoll_trans1, assumption, blast) 
+apply (blast intro: subset_imp_lepoll) 
+done
+
+lemma Card_UN:
+     "(!!x. x:A ==> Card(K(x))) ==> Card(UN x:A. K(x))" 
+by (blast intro: Card_Union) 
+
+lemma Card_OUN [simp,intro,TC]:
+     "(!!x. x:A ==> Card(K(x))) ==> Card(UN x<A. K(x))"
+by (simp add: OUnion_def Card_0) 
 
 end
diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Tue Jan 08 15:39:47 2002 +0100
+++ b/src/ZF/IsaMakefile	Tue Jan 08 16:09:09 2002 +0100
@@ -39,7 +39,8 @@
   Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy	\
   Main_ZFC.ML Main_ZFC.thy	\
   Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML OrderArith.thy	\
-  OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy Perm.ML Perm.thy	\
+  OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy OrdQuant.ML OrdQuant.thy \
+  Perm.ML Perm.thy	\
   QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML	\
   Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
   Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/Main.thy
--- a/src/ZF/Main.thy	Tue Jan 08 15:39:47 2002 +0100
+++ b/src/ZF/Main.thy	Tue Jan 08 16:09:09 2002 +0100
@@ -16,6 +16,7 @@
   and wf_on_induct_rule = wf_on_induct [rule_format, consumes 2, induct set: wf_on]
 
 (* belongs to theory Ordinal *)
+declare Ord_Least [intro,simp,TC]
 lemmas Ord_induct = Ord_induct [consumes 2]
   and Ord_induct_rule = Ord_induct [rule_format, consumes 2]
   and trans_induct = trans_induct [consumes 1]
diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Tue Jan 08 15:39:47 2002 +0100
+++ b/src/ZF/OrdQuant.thy	Tue Jan 08 16:09:09 2002 +0100
@@ -36,9 +36,9 @@
   "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
 
 
-declare Ord_Un [intro,simp]
-declare Ord_UN [intro,simp]
-declare Ord_Union [intro,simp]
+declare Ord_Un [intro,simp,TC]
+declare Ord_UN [intro,simp,TC]
+declare Ord_Union [intro,simp,TC]
 
 (** These mostly belong to theory Ordinal **)
 
@@ -49,6 +49,17 @@
 apply auto
 done
 
+lemma zero_not_Limit [iff]: "~ Limit(0)"
+by (simp add: Limit_def)
+
+lemma Limit_has_1: "Limit(i) \<Longrightarrow> 1 < i"
+by (blast intro: Limit_has_0 Limit_has_succ)
+
+lemma Limit_Union [rule_format]: "\<lbrakk>I \<noteq> 0;  \<forall>i\<in>I. Limit(i)\<rbrakk> \<Longrightarrow> Limit(\<Union>I)"
+apply (simp add: Limit_def lt_def)
+apply (blast intro!: equalityI)
+done
+
 lemma increasing_LimitI: "\<lbrakk>0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y\<rbrakk> \<Longrightarrow> Limit(l)"
 apply (simp add: Limit_def lt_Ord2)
 apply clarify
diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/OrderType.ML
--- a/src/ZF/OrderType.ML	Tue Jan 08 15:39:47 2002 +0100
+++ b/src/ZF/OrderType.ML	Tue Jan 08 16:09:09 2002 +0100
@@ -364,6 +364,7 @@
     "[| Ord(i);  Ord(j) |] ==> Ord(i++j)";
 by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 1));
 qed "Ord_oadd";
+Addsimps [Ord_oadd]; AddIs [Ord_oadd]; AddTCs [Ord_oadd];
 
 (** Ordinal addition with zero **)
 
@@ -495,9 +496,10 @@
 
 Goal "[| Ord(i);  Ord(j) |] ==> i++succ(j) = succ(i++j)";
                 (*FOL_ss prevents looping*)
-by (asm_simp_tac (FOL_ss addsimps [Ord_oadd, oadd_1 RS sym]) 1);
-by (asm_simp_tac (simpset() addsimps [oadd_1, oadd_assoc, Ord_1]) 1);
+by (asm_simp_tac (FOL_ss delsimps [oadd_1]
+		 addsimps [Ord_oadd, oadd_1 RS sym, oadd_assoc, Ord_1]) 1);
 qed "oadd_succ";
+Addsimps [oadd_succ];
 
 
 (** Ordinal addition with limit ordinals **)
@@ -549,11 +551,13 @@
 qed "oadd_lt_mono";
 
 Goal "[| i' le i;  j' le j |] ==> i'++j' le i++j";
-by (asm_simp_tac (simpset() addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1);
+by (asm_simp_tac (simpset() delsimps [oadd_succ]
+		   addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1);
 qed "oadd_le_mono";
 
 Goal "[| Ord(i); Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k";
-by (asm_simp_tac (simpset() addsimps [oadd_lt_iff2, oadd_succ RS sym, 
+by (asm_simp_tac (simpset() delsimps [oadd_succ]
+			    addsimps [oadd_lt_iff2, oadd_succ RS sym, 
                                   Ord_succ]) 1);
 qed "oadd_le_iff2";
 
@@ -761,9 +765,8 @@
 
 Goal "[| Ord(i);  Ord(j) |] ==> i**succ(j) = (i**j)++i";
                 (*FOL_ss prevents looping*)
-by (asm_simp_tac (FOL_ss addsimps [oadd_1 RS sym]) 1);
-by (asm_simp_tac 
-    (simpset() addsimps [omult_1, oadd_omult_distrib, Ord_1]) 1);
+by (asm_simp_tac (FOL_ss addsimps [oadd_1 RS sym, omult_1, oadd_omult_distrib,
+                                   Ord_1]) 1);
 qed "omult_succ";
 
 (** Associative law **)