--- a/src/ZF/Arith.ML Fri May 17 16:54:25 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,516 +0,0 @@
-(* Title: ZF/Arith.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
-
-Arithmetic operators and their definitions
-
-Proofs about elementary arithmetic: addition, multiplication, etc.
-*)
-
-(*"Difference" is subtraction of natural numbers.
- There are no negative numbers; we have
- m #- n = 0 iff m<=n and m #- n = succ(k) iff m>n.
- Also, rec(m, 0, %z w.z) is pred(m).
-*)
-
-Addsimps [rec_type, nat_0_le];
-bind_thms ("nat_typechecks", [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat]);
-
-Goal "[| 0<k; k: nat |] ==> EX j: nat. k = succ(j)";
-by (etac rev_mp 1);
-by (induct_tac "k" 1);
-by (Simp_tac 1);
-by (Blast_tac 1);
-val lemma = result();
-
-(* [| 0 < k; k: nat; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
-bind_thm ("zero_lt_natE", lemma RS bexE);
-
-
-(** natify: coercion to "nat" **)
-
-Goalw [pred_def] "pred(succ(y)) = y";
-by Auto_tac;
-qed "pred_succ_eq";
-Addsimps [pred_succ_eq];
-
-Goal "natify(succ(x)) = succ(natify(x))";
-by (rtac (natify_def RS def_Vrecursor RS trans) 1);
-by Auto_tac;
-qed "natify_succ";
-
-Goal "natify(0) = 0";
-by (rtac (natify_def RS def_Vrecursor RS trans) 1);
-by Auto_tac;
-qed "natify_0";
-Addsimps [natify_0];
-
-Goal "ALL z. x ~= succ(z) ==> natify(x) = 0";
-by (rtac (natify_def RS def_Vrecursor RS trans) 1);
-by Auto_tac;
-qed "natify_non_succ";
-
-Goal "natify(x) : nat";
-by (eps_ind_tac "x" 1);
-by (case_tac "EX z. x1 = succ(z)" 1);
-by (auto_tac (claset(), simpset() addsimps [natify_succ, natify_non_succ]));
-qed "natify_in_nat";
-AddIffs [natify_in_nat];
-AddTCs [natify_in_nat];
-
-Goal "n : nat ==> natify(n) = n";
-by (induct_tac "n" 1);
-by (auto_tac (claset(), simpset() addsimps [natify_succ]));
-qed "natify_ident";
-Addsimps [natify_ident];
-
-Goal "[|natify(x) = y; x: nat|] ==> x=y";
-by Auto_tac;
-qed "natify_eqE";
-
-
-(*** Collapsing rules: to remove natify from arithmetic expressions ***)
-
-Goal "natify(natify(x)) = natify(x)";
-by (Simp_tac 1);
-qed "natify_idem";
-Addsimps [natify_idem];
-
-(** Addition **)
-
-Goal "natify(m) #+ n = m #+ n";
-by (simp_tac (simpset() addsimps [add_def]) 1);
-qed "add_natify1";
-
-Goal "m #+ natify(n) = m #+ n";
-by (simp_tac (simpset() addsimps [add_def]) 1);
-qed "add_natify2";
-Addsimps [add_natify1, add_natify2];
-
-(** Multiplication **)
-
-Goal "natify(m) #* n = m #* n";
-by (simp_tac (simpset() addsimps [mult_def]) 1);
-qed "mult_natify1";
-
-Goal "m #* natify(n) = m #* n";
-by (simp_tac (simpset() addsimps [mult_def]) 1);
-qed "mult_natify2";
-Addsimps [mult_natify1, mult_natify2];
-
-(** Difference **)
-
-Goal "natify(m) #- n = m #- n";
-by (simp_tac (simpset() addsimps [diff_def]) 1);
-qed "diff_natify1";
-
-Goal "m #- natify(n) = m #- n";
-by (simp_tac (simpset() addsimps [diff_def]) 1);
-qed "diff_natify2";
-Addsimps [diff_natify1, diff_natify2];
-
-(** Remainder **)
-
-Goal "natify(m) mod n = m mod n";
-by (simp_tac (simpset() addsimps [mod_def]) 1);
-qed "mod_natify1";
-
-Goal "m mod natify(n) = m mod n";
-by (simp_tac (simpset() addsimps [mod_def]) 1);
-qed "mod_natify2";
-Addsimps [mod_natify1, mod_natify2];
-
-(** Quotient **)
-
-Goal "natify(m) div n = m div n";
-by (simp_tac (simpset() addsimps [div_def]) 1);
-qed "div_natify1";
-
-Goal "m div natify(n) = m div n";
-by (simp_tac (simpset() addsimps [div_def]) 1);
-qed "div_natify2";
-Addsimps [div_natify1, div_natify2];
-
-
-(*** Typing rules ***)
-
-(** Addition **)
-
-Goal "[| m:nat; n:nat |] ==> raw_add (m, n) : nat";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "raw_add_type";
-
-Goal "m #+ n : nat";
-by (simp_tac (simpset() addsimps [add_def, raw_add_type]) 1);
-qed "add_type";
-AddIffs [add_type];
-AddTCs [add_type];
-
-(** Multiplication **)
-
-Goal "[| m:nat; n:nat |] ==> raw_mult (m, n) : nat";
-by (induct_tac "m" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [raw_add_type])));
-qed "raw_mult_type";
-
-Goal "m #* n : nat";
-by (simp_tac (simpset() addsimps [mult_def, raw_mult_type]) 1);
-qed "mult_type";
-AddIffs [mult_type];
-AddTCs [mult_type];
-
-
-(** Difference **)
-
-Goal "[| m:nat; n:nat |] ==> raw_diff (m, n) : nat";
-by (induct_tac "n" 1);
-by Auto_tac;
-by (fast_tac (claset() addIs [nat_case_type]) 1);
-qed "raw_diff_type";
-
-Goal "m #- n : nat";
-by (simp_tac (simpset() addsimps [diff_def, raw_diff_type]) 1);
-qed "diff_type";
-AddIffs [diff_type];
-AddTCs [diff_type];
-
-Goalw [diff_def] "0 #- n = 0";
-by (rtac (natify_in_nat RS nat_induct) 1);
-by Auto_tac;
-qed "diff_0_eq_0";
-
-(*Must simplify BEFORE the induction: else we get a critical pair*)
-Goal "succ(m) #- succ(n) = m #- n";
-by (simp_tac (simpset() addsimps [natify_succ, diff_def]) 1);
-by (res_inst_tac [("x1","n")] (natify_in_nat RS nat_induct) 1);
-by Auto_tac;
-qed "diff_succ_succ";
-
-(*This defining property is no longer wanted*)
-Delsimps [raw_diff_succ];
-
-(*Natify has weakened this law, compared with the older approach*)
-Goal "m #- 0 = natify(m)";
-by (asm_simp_tac (simpset() addsimps [diff_def]) 1);
-qed "diff_0";
-
-Addsimps [diff_0, diff_0_eq_0, diff_succ_succ];
-
-Goal "m:nat ==> (m #- n) le m";
-by (subgoal_tac "(m #- natify(n)) le m" 1);
-by (res_inst_tac [("m","m"), ("n","natify(n)")] diff_induct 2);
-by (etac leE 6);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [le_iff])));
-qed "diff_le_self";
-
-
-(*** Addition ***)
-
-(*Natify has weakened this law, compared with the older approach*)
-Goal "0 #+ m = natify(m)";
-by (asm_simp_tac (simpset() addsimps [add_def]) 1);
-qed "add_0_natify";
-
-Goal "succ(m) #+ n = succ(m #+ n)";
-by (asm_simp_tac (simpset() addsimps [natify_succ, add_def]) 1);
-qed "add_succ";
-
-Addsimps [add_0_natify, add_succ];
-
-Goal "m: nat ==> 0 #+ m = m";
-by (Asm_simp_tac 1);
-qed "add_0";
-
-(*Associative law for addition*)
-Goal "(m #+ n) #+ k = m #+ (n #+ k)";
-by (subgoal_tac "(natify(m) #+ natify(n)) #+ natify(k) = \
-\ natify(m) #+ (natify(n) #+ natify(k))" 1);
-by (res_inst_tac [("n","natify(m)")] nat_induct 2);
-by Auto_tac;
-qed "add_assoc";
-
-(*The following two lemmas are used for add_commute and sometimes
- elsewhere, since they are safe for rewriting.*)
-Goal "m #+ 0 = natify(m)";
-by (subgoal_tac "natify(m) #+ 0 = natify(m)" 1);
-by (res_inst_tac [("n","natify(m)")] nat_induct 2);
-by Auto_tac;
-qed "add_0_right_natify";
-
-Goalw [add_def] "m #+ succ(n) = succ(m #+ n)";
-by (res_inst_tac [("n","natify(m)")] nat_induct 1);
-by (auto_tac (claset(), simpset() addsimps [natify_succ]));
-qed "add_succ_right";
-
-Addsimps [add_0_right_natify, add_succ_right];
-
-Goal "m: nat ==> m #+ 0 = m";
-by Auto_tac;
-qed "add_0_right";
-
-(*Commutative law for addition*)
-Goal "m #+ n = n #+ m";
-by (subgoal_tac "natify(m) #+ natify(n) = natify(n) #+ natify(m)" 1);
-by (res_inst_tac [("n","natify(m)")] nat_induct 2);
-by Auto_tac;
-qed "add_commute";
-
-(*for a/c rewriting*)
-Goal "m#+(n#+k)=n#+(m#+k)";
-by (rtac (add_commute RS trans) 1);
-by (rtac (add_assoc RS trans) 1);
-by (rtac (add_commute RS subst_context) 1);
-qed "add_left_commute";
-
-(*Addition is an AC-operator*)
-bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]);
-
-(*Cancellation law on the left*)
-Goal "[| raw_add(k, m) = raw_add(k, n); k:nat |] ==> m=n";
-by (etac rev_mp 1);
-by (induct_tac "k" 1);
-by Auto_tac;
-qed "raw_add_left_cancel";
-
-Goalw [add_def] "k #+ m = k #+ n ==> natify(m) = natify(n)";
-by (dtac raw_add_left_cancel 1);
-by Auto_tac;
-qed "add_left_cancel_natify";
-
-Goal "[| i = j; i #+ m = j #+ n; m:nat; n:nat |] ==> m = n";
-by (force_tac (claset() addSDs [add_left_cancel_natify], simpset()) 1);
-qed "add_left_cancel";
-
-(*Thanks to Sten Agerholm*)
-Goal "k#+m le k#+n ==> natify(m) le natify(n)";
-by (res_inst_tac [("P", "natify(k)#+m le natify(k)#+n")] rev_mp 1);
-by (res_inst_tac [("n","natify(k)")] nat_induct 2);
-by Auto_tac;
-qed "add_le_elim1_natify";
-
-Goal "[| k#+m le k#+n; m: nat; n: nat |] ==> m le n";
-by (dtac add_le_elim1_natify 1);
-by Auto_tac;
-qed "add_le_elim1";
-
-Goal "k#+m < k#+n ==> natify(m) < natify(n)";
-by (res_inst_tac [("P", "natify(k)#+m < natify(k)#+n")] rev_mp 1);
-by (res_inst_tac [("n","natify(k)")] nat_induct 2);
-by Auto_tac;
-qed "add_lt_elim1_natify";
-
-Goal "[| k#+m < k#+n; m: nat; n: nat |] ==> m < n";
-by (dtac add_lt_elim1_natify 1);
-by Auto_tac;
-qed "add_lt_elim1";
-
-
-(*** Monotonicity of Addition ***)
-
-(*strict, in 1st argument; proof is by rule induction on 'less than'.
- Still need j:nat, for consider j = omega. Then we can have i<omega,
- which is the same as i:nat, but natify(j)=0, so the conclusion fails.*)
-Goal "[| i<j; j:nat |] ==> i#+k < j#+k";
-by (ftac lt_nat_in_nat 1);
-by (assume_tac 1);
-by (etac succ_lt_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI])));
-qed "add_lt_mono1";
-
-(*strict, in both arguments*)
-Goal "[| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
-by (rtac (add_lt_mono1 RS lt_trans) 1);
-by (REPEAT (assume_tac 1));
-by (EVERY [stac add_commute 1,
- stac add_commute 1,
- rtac add_lt_mono1 1]);
-by (REPEAT (assume_tac 1));
-qed "add_lt_mono";
-
-(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
-val lt_mono::ford::prems = Goal
- "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \
-\ !!i. i:k ==> Ord(f(i)); \
-\ i le j; j:k \
-\ |] ==> f(i) le f(j)";
-by (cut_facts_tac prems 1);
-by (blast_tac (le_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
-qed "Ord_lt_mono_imp_le_mono";
-
-(*le monotonicity, 1st argument*)
-Goal "[| i le j; j:nat |] ==> i#+k le j#+k";
-by (res_inst_tac [("f", "%j. j#+k")] Ord_lt_mono_imp_le_mono 1);
-by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1));
-qed "add_le_mono1";
-
-(* le monotonicity, BOTH arguments*)
-Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
-by (rtac (add_le_mono1 RS le_trans) 1);
-by (REPEAT (assume_tac 1));
-by (EVERY [stac add_commute 1,
- stac add_commute 1,
- rtac add_le_mono1 1]);
-by (REPEAT (assume_tac 1));
-qed "add_le_mono";
-
-(** Subtraction is the inverse of addition. **)
-
-Goal "(n#+m) #- n = natify(m)";
-by (subgoal_tac "(natify(n) #+ m) #- natify(n) = natify(m)" 1);
-by (res_inst_tac [("n","natify(n)")] nat_induct 2);
-by Auto_tac;
-qed "diff_add_inverse";
-
-Goal "(m#+n) #- n = natify(m)";
-by (simp_tac (simpset() addsimps [inst "m" "m" add_commute,
- diff_add_inverse]) 1);
-qed "diff_add_inverse2";
-
-Goal "(k#+m) #- (k#+n) = m #- n";
-by (subgoal_tac "(natify(k) #+ natify(m)) #- (natify(k) #+ natify(n)) = \
-\ natify(m) #- natify(n)" 1);
-by (res_inst_tac [("n","natify(k)")] nat_induct 2);
-by Auto_tac;
-qed "diff_cancel";
-
-Goal "(m#+k) #- (n#+k) = m #- n";
-by (simp_tac (simpset() addsimps [inst "n" "k" add_commute, diff_cancel]) 1);
-qed "diff_cancel2";
-
-Goal "n #- (n#+m) = 0";
-by (subgoal_tac "natify(n) #- (natify(n) #+ natify(m)) = 0" 1);
-by (res_inst_tac [("n","natify(n)")] nat_induct 2);
-by Auto_tac;
-qed "diff_add_0";
-
-
-(** Lemmas for the CancelNumerals simproc **)
-
-Goal "(u #+ m = u #+ n) <-> (0 #+ m = natify(n))";
-by Auto_tac;
-by (blast_tac (claset() addDs [add_left_cancel_natify]) 1);
-by (asm_full_simp_tac (simpset() addsimps [add_def]) 1);
-qed "eq_add_iff";
-
-Goal "(u #+ m < u #+ n) <-> (0 #+ m < natify(n))";
-by (auto_tac (claset(), simpset() addsimps [add_lt_elim1_natify]));
-by (dtac add_lt_mono1 1);
-by (auto_tac (claset(), simpset() addsimps [inst "m" "u" add_commute]));
-qed "less_add_iff";
-
-Goal "((u #+ m) #- (u #+ n)) = ((0 #+ m) #- n)";
-by (asm_simp_tac (simpset() addsimps [diff_cancel]) 1);
-qed "diff_add_eq";
-
-(*To tidy up the result of a simproc. Only the RHS will be simplified.*)
-Goal "u = u' ==> (t==u) == (t==u')";
-by Auto_tac;
-qed "eq_cong2";
-
-Goal "u <-> u' ==> (t==u) == (t==u')";
-by Auto_tac;
-qed "iff_cong2";
-
-
-(*** Multiplication [the simprocs need these laws] ***)
-
-Goal "0 #* m = 0";
-by (simp_tac (simpset() addsimps [mult_def]) 1);
-qed "mult_0";
-
-Goal "succ(m) #* n = n #+ (m #* n)";
-by (simp_tac (simpset() addsimps [add_def, mult_def, natify_succ,
- raw_mult_type]) 1);
-qed "mult_succ";
-
-Addsimps [mult_0, mult_succ];
-
-(*right annihilation in product*)
-Goalw [mult_def] "m #* 0 = 0";
-by (res_inst_tac [("n","natify(m)")] nat_induct 1);
-by Auto_tac;
-qed "mult_0_right";
-
-(*right successor law for multiplication*)
-Goal "m #* succ(n) = m #+ (m #* n)";
-by (subgoal_tac "natify(m) #* succ(natify(n)) = \
-\ natify(m) #+ (natify(m) #* natify(n))" 1);
-by (full_simp_tac (simpset() addsimps [natify_succ, add_def, mult_def]) 1);
-by (res_inst_tac [("n","natify(m)")] nat_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac)));
-qed "mult_succ_right";
-
-Addsimps [mult_0_right, mult_succ_right];
-
-Goal "1 #* n = natify(n)";
-by Auto_tac;
-qed "mult_1_natify";
-
-Goal "n #* 1 = natify(n)";
-by Auto_tac;
-qed "mult_1_right_natify";
-
-Addsimps [mult_1_natify, mult_1_right_natify];
-
-Goal "n : nat ==> 1 #* n = n";
-by (Asm_simp_tac 1);
-qed "mult_1";
-
-Goal "n : nat ==> n #* 1 = n";
-by (Asm_simp_tac 1);
-qed "mult_1_right";
-
-(*Commutative law for multiplication*)
-Goal "m #* n = n #* m";
-by (subgoal_tac "natify(m) #* natify(n) = natify(n) #* natify(m)" 1);
-by (res_inst_tac [("n","natify(m)")] nat_induct 2);
-by Auto_tac;
-qed "mult_commute";
-
-(*addition distributes over multiplication*)
-Goal "(m #+ n) #* k = (m #* k) #+ (n #* k)";
-by (subgoal_tac "(natify(m) #+ natify(n)) #* natify(k) = \
-\ (natify(m) #* natify(k)) #+ (natify(n) #* natify(k))" 1);
-by (res_inst_tac [("n","natify(m)")] nat_induct 2);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_assoc RS sym])));
-qed "add_mult_distrib";
-
-(*Distributive law on the left*)
-Goal "k #* (m #+ n) = (k #* m) #+ (k #* n)";
-by (subgoal_tac "natify(k) #* (natify(m) #+ natify(n)) = \
-\ (natify(k) #* natify(m)) #+ (natify(k) #* natify(n))" 1);
-by (res_inst_tac [("n","natify(m)")] nat_induct 2);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
-qed "add_mult_distrib_left";
-
-(*Associative law for multiplication*)
-Goal "(m #* n) #* k = m #* (n #* k)";
-by (subgoal_tac "(natify(m) #* natify(n)) #* natify(k) = \
-\ natify(m) #* (natify(n) #* natify(k))" 1);
-by (res_inst_tac [("n","natify(m)")] nat_induct 2);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_mult_distrib])));
-qed "mult_assoc";
-
-(*for a/c rewriting*)
-Goal "m #* (n #* k) = n #* (m #* k)";
-by (rtac (mult_commute RS trans) 1);
-by (rtac (mult_assoc RS trans) 1);
-by (rtac (mult_commute RS subst_context) 1);
-qed "mult_left_commute";
-
-bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
-
-
-Goal "[| m:nat; n:nat |] \
-\ ==> (m < succ(n)) <-> (m = 0 | (EX j:nat. m = succ(j) & j < n))";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "lt_succ_eq_0_disj";
-
-Goal "[| j:nat; k:nat |] ==> ALL i:nat. (i < j #- k) <-> (i #+ k < j)";
-by (eres_inst_tac [("m", "k")] diff_induct 1);
-by Auto_tac;
-qed_spec_mp "less_diff_conv";
-
--- a/src/ZF/Arith.thy Fri May 17 16:54:25 2002 +0200
+++ b/src/ZF/Arith.thy Sat May 18 20:08:17 2002 +0200
@@ -4,62 +4,581 @@
Copyright 1992 University of Cambridge
Arithmetic operators and their definitions
+
+Proofs about elementary arithmetic: addition, multiplication, etc.
*)
-Arith = Univ +
+(*"Difference" is subtraction of natural numbers.
+ There are no negative numbers; we have
+ m #- n = 0 iff m<=n and m #- n = succ(k) iff m>n.
+ Also, rec(m, 0, %z w.z) is pred(m).
+*)
+
+theory Arith = Univ:
constdefs
- pred :: i=>i (*inverse of succ*)
+ pred :: "i=>i" (*inverse of succ*)
"pred(y) == THE x. y = succ(x)"
- natify :: i=>i (*coerces non-nats to nats*)
+ natify :: "i=>i" (*coerces non-nats to nats*)
"natify == Vrecursor(%f a. if a = succ(pred(a)) then succ(f`pred(a))
else 0)"
consts
- raw_add, raw_diff, raw_mult :: [i,i]=>i
+ raw_add :: "[i,i]=>i"
+ raw_diff :: "[i,i]=>i"
+ raw_mult :: "[i,i]=>i"
primrec
"raw_add (0, n) = n"
"raw_add (succ(m), n) = succ(raw_add(m, n))"
primrec
- raw_diff_0 "raw_diff(m, 0) = m"
- raw_diff_succ "raw_diff(m, succ(n)) =
- nat_case(0, %x. x, raw_diff(m, n))"
+ raw_diff_0: "raw_diff(m, 0) = m"
+ raw_diff_succ: "raw_diff(m, succ(n)) =
+ nat_case(0, %x. x, raw_diff(m, n))"
primrec
"raw_mult(0, n) = 0"
"raw_mult(succ(m), n) = raw_add (n, raw_mult(m, n))"
-
+
constdefs
- add :: [i,i]=>i (infixl "#+" 65)
+ add :: "[i,i]=>i" (infixl "#+" 65)
"m #+ n == raw_add (natify(m), natify(n))"
- diff :: [i,i]=>i (infixl "#-" 65)
+ diff :: "[i,i]=>i" (infixl "#-" 65)
"m #- n == raw_diff (natify(m), natify(n))"
- mult :: [i,i]=>i (infixl "#*" 70)
+ mult :: "[i,i]=>i" (infixl "#*" 70)
"m #* n == raw_mult (natify(m), natify(n))"
- raw_div :: [i,i]=>i
- "raw_div (m, n) ==
+ raw_div :: "[i,i]=>i"
+ "raw_div (m, n) ==
transrec(m, %j f. if j<n | n=0 then 0 else succ(f`(j#-n)))"
- raw_mod :: [i,i]=>i
- "raw_mod (m, n) ==
+ raw_mod :: "[i,i]=>i"
+ "raw_mod (m, n) ==
transrec(m, %j f. if j<n | n=0 then j else f`(j#-n))"
- div :: [i,i]=>i (infixl "div" 70)
+ div :: "[i,i]=>i" (infixl "div" 70)
"m div n == raw_div (natify(m), natify(n))"
- mod :: [i,i]=>i (infixl "mod" 70)
+ mod :: "[i,i]=>i" (infixl "mod" 70)
"m mod n == raw_mod (natify(m), natify(n))"
syntax (xsymbols)
- "mult" :: [i, i] => i (infixr "#\\<times>" 70)
+ "mult" :: "[i,i] => i" (infixr "#\<times>" 70)
syntax (HTML output)
- "mult" :: [i, i] => i (infixr "#\\<times>" 70)
+ "mult" :: "[i, i] => i" (infixr "#\<times>" 70)
+
+
+declare rec_type [simp]
+ nat_0_le [simp]
+
+
+lemma zero_lt_lemma: "[| 0<k; k: nat |] ==> EX j: nat. k = succ(j)"
+apply (erule rev_mp)
+apply (induct_tac "k", auto)
+done
+
+(* [| 0 < k; k: nat; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
+lemmas zero_lt_natE = zero_lt_lemma [THEN bexE, standard]
+
+
+(** natify: coercion to "nat" **)
+
+lemma pred_succ_eq [simp]: "pred(succ(y)) = y"
+by (unfold pred_def, auto)
+
+lemma natify_succ: "natify(succ(x)) = succ(natify(x))"
+by (rule natify_def [THEN def_Vrecursor, THEN trans], auto)
+
+lemma natify_0 [simp]: "natify(0) = 0"
+by (rule natify_def [THEN def_Vrecursor, THEN trans], auto)
+
+lemma natify_non_succ: "ALL z. x ~= succ(z) ==> natify(x) = 0"
+by (rule natify_def [THEN def_Vrecursor, THEN trans], auto)
+
+lemma natify_in_nat [iff,TC]: "natify(x) : nat"
+apply (rule_tac a=x in eps_induct)
+apply (case_tac "EX z. x = succ(z)")
+apply (auto simp add: natify_succ natify_non_succ)
+done
+
+lemma natify_ident [simp]: "n : nat ==> natify(n) = n"
+apply (induct_tac "n")
+apply (auto simp add: natify_succ)
+done
+
+lemma natify_eqE: "[|natify(x) = y; x: nat|] ==> x=y"
+by auto
+
+
+(*** Collapsing rules: to remove natify from arithmetic expressions ***)
+
+lemma natify_idem [simp]: "natify(natify(x)) = natify(x)"
+by simp
+
+(** Addition **)
+
+lemma add_natify1 [simp]: "natify(m) #+ n = m #+ n"
+by (simp add: add_def)
+
+lemma add_natify2 [simp]: "m #+ natify(n) = m #+ n"
+by (simp add: add_def)
+
+(** Multiplication **)
+
+lemma mult_natify1 [simp]: "natify(m) #* n = m #* n"
+by (simp add: mult_def)
+
+lemma mult_natify2 [simp]: "m #* natify(n) = m #* n"
+by (simp add: mult_def)
+
+(** Difference **)
+
+lemma diff_natify1 [simp]: "natify(m) #- n = m #- n"
+by (simp add: diff_def)
+
+lemma diff_natify2 [simp]: "m #- natify(n) = m #- n"
+by (simp add: diff_def)
+
+(** Remainder **)
+
+lemma mod_natify1 [simp]: "natify(m) mod n = m mod n"
+by (simp add: mod_def)
+
+lemma mod_natify2 [simp]: "m mod natify(n) = m mod n"
+by (simp add: mod_def)
+
+
+(** Quotient **)
+
+lemma div_natify1 [simp]: "natify(m) div n = m div n"
+by (simp add: div_def)
+
+lemma div_natify2 [simp]: "m div natify(n) = m div n"
+by (simp add: div_def)
+
+
+(*** Typing rules ***)
+
+(** Addition **)
+
+lemma raw_add_type: "[| m:nat; n:nat |] ==> raw_add (m, n) : nat"
+by (induct_tac "m", auto)
+
+lemma add_type [iff,TC]: "m #+ n : nat"
+by (simp add: add_def raw_add_type)
+
+(** Multiplication **)
+
+lemma raw_mult_type: "[| m:nat; n:nat |] ==> raw_mult (m, n) : nat"
+apply (induct_tac "m")
+apply (simp_all add: raw_add_type)
+done
+
+lemma mult_type [iff,TC]: "m #* n : nat"
+by (simp add: mult_def raw_mult_type)
+
+
+(** Difference **)
+
+lemma raw_diff_type: "[| m:nat; n:nat |] ==> raw_diff (m, n) : nat"
+apply (induct_tac "n", auto)
+apply (fast intro: nat_case_type)
+done
+
+lemma diff_type [iff,TC]: "m #- n : nat"
+by (simp add: diff_def raw_diff_type)
+
+lemma diff_0_eq_0 [simp]: "0 #- n = 0"
+apply (unfold diff_def)
+apply (rule natify_in_nat [THEN nat_induct], auto)
+done
+
+(*Must simplify BEFORE the induction: else we get a critical pair*)
+lemma diff_succ_succ [simp]: "succ(m) #- succ(n) = m #- n"
+apply (simp add: natify_succ diff_def)
+apply (rule_tac x1 = "n" in natify_in_nat [THEN nat_induct], auto)
+done
+
+(*This defining property is no longer wanted*)
+declare raw_diff_succ [simp del]
+
+(*Natify has weakened this law, compared with the older approach*)
+lemma diff_0 [simp]: "m #- 0 = natify(m)"
+by (simp add: diff_def)
+
+lemma diff_le_self: "m:nat ==> (m #- n) le m"
+apply (subgoal_tac " (m #- natify (n)) le m")
+apply (rule_tac [2] m = "m" and n = "natify (n) " in diff_induct)
+apply (erule_tac [6] leE)
+apply (simp_all add: le_iff)
+done
+
+
+(*** Addition ***)
+
+(*Natify has weakened this law, compared with the older approach*)
+lemma add_0_natify [simp]: "0 #+ m = natify(m)"
+by (simp add: add_def)
+
+lemma add_succ [simp]: "succ(m) #+ n = succ(m #+ n)"
+by (simp add: natify_succ add_def)
+
+lemma add_0: "m: nat ==> 0 #+ m = m"
+by simp
+
+(*Associative law for addition*)
+lemma add_assoc: "(m #+ n) #+ k = m #+ (n #+ k)"
+apply (subgoal_tac "(natify(m) #+ natify(n)) #+ natify(k) =
+ natify(m) #+ (natify(n) #+ natify(k))")
+apply (rule_tac [2] n = "natify(m)" in nat_induct)
+apply auto
+done
+
+(*The following two lemmas are used for add_commute and sometimes
+ elsewhere, since they are safe for rewriting.*)
+lemma add_0_right_natify [simp]: "m #+ 0 = natify(m)"
+apply (subgoal_tac "natify(m) #+ 0 = natify(m)")
+apply (rule_tac [2] n = "natify(m)" in nat_induct)
+apply auto
+done
+
+lemma add_succ_right [simp]: "m #+ succ(n) = succ(m #+ n)"
+apply (unfold add_def)
+apply (rule_tac n = "natify(m) " in nat_induct)
+apply (auto simp add: natify_succ)
+done
+
+lemma add_0_right: "m: nat ==> m #+ 0 = m"
+by auto
+
+(*Commutative law for addition*)
+lemma add_commute: "m #+ n = n #+ m"
+apply (subgoal_tac "natify(m) #+ natify(n) = natify(n) #+ natify(m) ")
+apply (rule_tac [2] n = "natify(m) " in nat_induct)
+apply auto
+done
+
+(*for a/c rewriting*)
+lemma add_left_commute: "m#+(n#+k)=n#+(m#+k)"
+apply (rule add_commute [THEN trans])
+apply (rule add_assoc [THEN trans])
+apply (rule add_commute [THEN subst_context])
+done
+
+(*Addition is an AC-operator*)
+lemmas add_ac = add_assoc add_commute add_left_commute
+
+(*Cancellation law on the left*)
+lemma raw_add_left_cancel:
+ "[| raw_add(k, m) = raw_add(k, n); k:nat |] ==> m=n"
+apply (erule rev_mp)
+apply (induct_tac "k", auto)
+done
+
+lemma add_left_cancel_natify: "k #+ m = k #+ n ==> natify(m) = natify(n)"
+apply (unfold add_def)
+apply (drule raw_add_left_cancel, auto)
+done
+
+lemma add_left_cancel:
+ "[| i = j; i #+ m = j #+ n; m:nat; n:nat |] ==> m = n"
+by (force dest!: add_left_cancel_natify)
+
+(*Thanks to Sten Agerholm*)
+lemma add_le_elim1_natify: "k#+m le k#+n ==> natify(m) le natify(n)"
+apply (rule_tac P = "natify(k) #+m le natify(k) #+n" in rev_mp)
+apply (rule_tac [2] n = "natify(k) " in nat_induct)
+apply auto
+done
+
+lemma add_le_elim1: "[| k#+m le k#+n; m: nat; n: nat |] ==> m le n"
+by (drule add_le_elim1_natify, auto)
+
+lemma add_lt_elim1_natify: "k#+m < k#+n ==> natify(m) < natify(n)"
+apply (rule_tac P = "natify(k) #+m < natify(k) #+n" in rev_mp)
+apply (rule_tac [2] n = "natify(k) " in nat_induct)
+apply auto
+done
+
+lemma add_lt_elim1: "[| k#+m < k#+n; m: nat; n: nat |] ==> m < n"
+by (drule add_lt_elim1_natify, auto)
+
+
+(*** Monotonicity of Addition ***)
+
+(*strict, in 1st argument; proof is by rule induction on 'less than'.
+ Still need j:nat, for consider j = omega. Then we can have i<omega,
+ which is the same as i:nat, but natify(j)=0, so the conclusion fails.*)
+lemma add_lt_mono1: "[| i<j; j:nat |] ==> i#+k < j#+k"
+apply (frule lt_nat_in_nat, assumption)
+apply (erule succ_lt_induct)
+apply (simp_all add: leI)
+done
+
+(*strict, in both arguments*)
+lemma add_lt_mono:
+ "[| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l"
+apply (rule add_lt_mono1 [THEN lt_trans], assumption+)
+apply (subst add_commute, subst add_commute, rule add_lt_mono1, assumption+)
+done
+
+(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
+lemma Ord_lt_mono_imp_le_mono:
+ assumes lt_mono: "!!i j. [| i<j; j:k |] ==> f(i) < f(j)"
+ and ford: "!!i. i:k ==> Ord(f(i))"
+ and leij: "i le j"
+ and jink: "j:k"
+ shows "f(i) le f(j)"
+apply (insert leij jink)
+apply (blast intro!: leCI lt_mono ford elim!: leE)
+done
+
+(*le monotonicity, 1st argument*)
+lemma add_le_mono1: "[| i le j; j:nat |] ==> i#+k le j#+k"
+apply (rule_tac f = "%j. j#+k" in Ord_lt_mono_imp_le_mono, typecheck)
+apply (blast intro: add_lt_mono1 add_type [THEN nat_into_Ord])+
+done
+
+(* le monotonicity, BOTH arguments*)
+lemma add_le_mono: "[| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l"
+apply (rule add_le_mono1 [THEN le_trans], assumption+)
+apply (subst add_commute, subst add_commute, rule add_le_mono1, assumption+)
+done
+
+(** Subtraction is the inverse of addition. **)
+
+lemma diff_add_inverse: "(n#+m) #- n = natify(m)"
+apply (subgoal_tac " (natify(n) #+ m) #- natify(n) = natify(m) ")
+apply (rule_tac [2] n = "natify(n) " in nat_induct)
+apply auto
+done
+
+lemma diff_add_inverse2: "(m#+n) #- n = natify(m)"
+by (simp add: add_commute [of m] diff_add_inverse)
+
+lemma diff_cancel: "(k#+m) #- (k#+n) = m #- n"
+apply (subgoal_tac "(natify(k) #+ natify(m)) #- (natify(k) #+ natify(n)) =
+ natify(m) #- natify(n) ")
+apply (rule_tac [2] n = "natify(k) " in nat_induct)
+apply auto
+done
+
+lemma diff_cancel2: "(m#+k) #- (n#+k) = m #- n"
+by (simp add: add_commute [of _ k] diff_cancel)
+
+lemma diff_add_0: "n #- (n#+m) = 0"
+apply (subgoal_tac "natify(n) #- (natify(n) #+ natify(m)) = 0")
+apply (rule_tac [2] n = "natify(n) " in nat_induct)
+apply auto
+done
+
+
+(** Lemmas for the CancelNumerals simproc **)
+
+lemma eq_add_iff: "(u #+ m = u #+ n) <-> (0 #+ m = natify(n))"
+apply auto
+apply (blast dest: add_left_cancel_natify)
+apply (simp add: add_def)
+done
+
+lemma less_add_iff: "(u #+ m < u #+ n) <-> (0 #+ m < natify(n))"
+apply (auto simp add: add_lt_elim1_natify)
+apply (drule add_lt_mono1)
+apply (auto simp add: add_commute [of u])
+done
+
+lemma diff_add_eq: "((u #+ m) #- (u #+ n)) = ((0 #+ m) #- n)"
+by (simp add: diff_cancel)
+
+(*To tidy up the result of a simproc. Only the RHS will be simplified.*)
+lemma eq_cong2: "u = u' ==> (t==u) == (t==u')"
+by auto
+
+lemma iff_cong2: "u <-> u' ==> (t==u) == (t==u')"
+by auto
+
+
+(*** Multiplication [the simprocs need these laws] ***)
+
+lemma mult_0 [simp]: "0 #* m = 0"
+by (simp add: mult_def)
+
+lemma mult_succ [simp]: "succ(m) #* n = n #+ (m #* n)"
+by (simp add: add_def mult_def natify_succ raw_mult_type)
+
+(*right annihilation in product*)
+lemma mult_0_right [simp]: "m #* 0 = 0"
+apply (unfold mult_def)
+apply (rule_tac n = "natify(m) " in nat_induct)
+apply auto
+done
+
+(*right successor law for multiplication*)
+lemma mult_succ_right [simp]: "m #* succ(n) = m #+ (m #* n)"
+apply (subgoal_tac "natify(m) #* succ (natify(n)) =
+ natify(m) #+ (natify(m) #* natify(n))")
+apply (simp (no_asm_use) add: natify_succ add_def mult_def)
+apply (rule_tac n = "natify(m) " in nat_induct)
+apply (simp_all add: add_ac)
+done
+
+lemma mult_1_natify [simp]: "1 #* n = natify(n)"
+by auto
+
+lemma mult_1_right_natify [simp]: "n #* 1 = natify(n)"
+by auto
+
+lemma mult_1: "n : nat ==> 1 #* n = n"
+by simp
+
+lemma mult_1_right: "n : nat ==> n #* 1 = n"
+by simp
+
+(*Commutative law for multiplication*)
+lemma mult_commute: "m #* n = n #* m"
+apply (subgoal_tac "natify(m) #* natify(n) = natify(n) #* natify(m) ")
+apply (rule_tac [2] n = "natify(m) " in nat_induct)
+apply auto
+done
+
+(*addition distributes over multiplication*)
+lemma add_mult_distrib: "(m #+ n) #* k = (m #* k) #+ (n #* k)"
+apply (subgoal_tac "(natify(m) #+ natify(n)) #* natify(k) =
+ (natify(m) #* natify(k)) #+ (natify(n) #* natify(k))")
+apply (rule_tac [2] n = "natify(m) " in nat_induct)
+apply (simp_all add: add_assoc [symmetric])
+done
+
+(*Distributive law on the left*)
+lemma add_mult_distrib_left: "k #* (m #+ n) = (k #* m) #+ (k #* n)"
+apply (subgoal_tac "natify(k) #* (natify(m) #+ natify(n)) =
+ (natify(k) #* natify(m)) #+ (natify(k) #* natify(n))")
+apply (rule_tac [2] n = "natify(m) " in nat_induct)
+apply (simp_all add: add_ac)
+done
+
+(*Associative law for multiplication*)
+lemma mult_assoc: "(m #* n) #* k = m #* (n #* k)"
+apply (subgoal_tac "(natify(m) #* natify(n)) #* natify(k) =
+ natify(m) #* (natify(n) #* natify(k))")
+apply (rule_tac [2] n = "natify(m) " in nat_induct)
+apply (simp_all add: add_mult_distrib)
+done
+
+(*for a/c rewriting*)
+lemma mult_left_commute: "m #* (n #* k) = n #* (m #* k)"
+apply (rule mult_commute [THEN trans])
+apply (rule mult_assoc [THEN trans])
+apply (rule mult_commute [THEN subst_context])
+done
+
+lemmas mult_ac = mult_assoc mult_commute mult_left_commute
+
+
+lemma lt_succ_eq_0_disj:
+ "[| m:nat; n:nat |]
+ ==> (m < succ(n)) <-> (m = 0 | (EX j:nat. m = succ(j) & j < n))"
+by (induct_tac "m", auto)
+
+lemma less_diff_conv [rule_format]:
+ "[| j:nat; k:nat |] ==> ALL i:nat. (i < j #- k) <-> (i #+ k < j)"
+by (erule_tac m = "k" in diff_induct, auto)
+
+lemmas nat_typechecks = rec_type nat_0I nat_1I nat_succI Ord_nat
+
+ML
+{*
+val pred_def = thm "pred_def";
+val raw_div_def = thm "raw_div_def";
+val raw_mod_def = thm "raw_mod_def";
+val div_def = thm "div_def";
+val mod_def = thm "mod_def";
+
+val zero_lt_lemma = thm "zero_lt_lemma";
+val zero_lt_natE = thm "zero_lt_natE";
+val pred_succ_eq = thm "pred_succ_eq";
+val natify_succ = thm "natify_succ";
+val natify_0 = thm "natify_0";
+val natify_non_succ = thm "natify_non_succ";
+val natify_in_nat = thm "natify_in_nat";
+val natify_ident = thm "natify_ident";
+val natify_eqE = thm "natify_eqE";
+val natify_idem = thm "natify_idem";
+val add_natify1 = thm "add_natify1";
+val add_natify2 = thm "add_natify2";
+val mult_natify1 = thm "mult_natify1";
+val mult_natify2 = thm "mult_natify2";
+val diff_natify1 = thm "diff_natify1";
+val diff_natify2 = thm "diff_natify2";
+val mod_natify1 = thm "mod_natify1";
+val mod_natify2 = thm "mod_natify2";
+val div_natify1 = thm "div_natify1";
+val div_natify2 = thm "div_natify2";
+val raw_add_type = thm "raw_add_type";
+val add_type = thm "add_type";
+val raw_mult_type = thm "raw_mult_type";
+val mult_type = thm "mult_type";
+val raw_diff_type = thm "raw_diff_type";
+val diff_type = thm "diff_type";
+val diff_0_eq_0 = thm "diff_0_eq_0";
+val diff_succ_succ = thm "diff_succ_succ";
+val diff_0 = thm "diff_0";
+val diff_le_self = thm "diff_le_self";
+val add_0_natify = thm "add_0_natify";
+val add_succ = thm "add_succ";
+val add_0 = thm "add_0";
+val add_assoc = thm "add_assoc";
+val add_0_right_natify = thm "add_0_right_natify";
+val add_succ_right = thm "add_succ_right";
+val add_0_right = thm "add_0_right";
+val add_commute = thm "add_commute";
+val add_left_commute = thm "add_left_commute";
+val raw_add_left_cancel = thm "raw_add_left_cancel";
+val add_left_cancel_natify = thm "add_left_cancel_natify";
+val add_left_cancel = thm "add_left_cancel";
+val add_le_elim1_natify = thm "add_le_elim1_natify";
+val add_le_elim1 = thm "add_le_elim1";
+val add_lt_elim1_natify = thm "add_lt_elim1_natify";
+val add_lt_elim1 = thm "add_lt_elim1";
+val add_lt_mono1 = thm "add_lt_mono1";
+val add_lt_mono = thm "add_lt_mono";
+val Ord_lt_mono_imp_le_mono = thm "Ord_lt_mono_imp_le_mono";
+val add_le_mono1 = thm "add_le_mono1";
+val add_le_mono = thm "add_le_mono";
+val diff_add_inverse = thm "diff_add_inverse";
+val diff_add_inverse2 = thm "diff_add_inverse2";
+val diff_cancel = thm "diff_cancel";
+val diff_cancel2 = thm "diff_cancel2";
+val diff_add_0 = thm "diff_add_0";
+val eq_add_iff = thm "eq_add_iff";
+val less_add_iff = thm "less_add_iff";
+val diff_add_eq = thm "diff_add_eq";
+val eq_cong2 = thm "eq_cong2";
+val iff_cong2 = thm "iff_cong2";
+val mult_0 = thm "mult_0";
+val mult_succ = thm "mult_succ";
+val mult_0_right = thm "mult_0_right";
+val mult_succ_right = thm "mult_succ_right";
+val mult_1_natify = thm "mult_1_natify";
+val mult_1_right_natify = thm "mult_1_right_natify";
+val mult_1 = thm "mult_1";
+val mult_1_right = thm "mult_1_right";
+val mult_commute = thm "mult_commute";
+val add_mult_distrib = thm "add_mult_distrib";
+val add_mult_distrib_left = thm "add_mult_distrib_left";
+val mult_assoc = thm "mult_assoc";
+val mult_left_commute = thm "mult_left_commute";
+val lt_succ_eq_0_disj = thm "lt_succ_eq_0_disj";
+val less_diff_conv = thm "less_diff_conv";
+
+val add_ac = thms "add_ac";
+val mult_ac = thms "mult_ac";
+val nat_typechecks = thms "nat_typechecks";
+*}
end
--- a/src/ZF/Integ/IntDiv.ML Fri May 17 16:54:25 2002 +0200
+++ b/src/ZF/Integ/IntDiv.ML Sat May 18 20:08:17 2002 +0200
@@ -57,14 +57,14 @@
by Auto_tac;
qed "zneg_or_0_add_zneg_or_0_imp_zneg_or_0";
-
Goal "[| #0 $< k; k \\<in> int |] ==> 0 < zmagnitude(k)";
by (dtac zero_zless_imp_znegative_zminus 1);
by (dtac zneg_int_of 2);
by (auto_tac (claset(), simpset() addsimps [inst "x" "k" zminus_equation]));
by (subgoal_tac "0 < zmagnitude($# succ(x))" 1);
by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset_of Arith.thy addsimps [zmagnitude_int_of]) 1);
+by (asm_full_simp_tac (FOL_ss addsimps [zmagnitude_int_of]) 1);
+by (Asm_full_simp_tac 1);
qed "zero_lt_zmagnitude";
--- a/src/ZF/IsaMakefile Fri May 17 16:54:25 2002 +0200
+++ b/src/ZF/IsaMakefile Sat May 18 20:08:17 2002 +0200
@@ -28,7 +28,7 @@
FOL:
@cd $(SRC)/FOL; $(ISATOOL) make FOL
-$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.ML Arith.thy ArithSimp.ML \
+$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.ML \
ArithSimp.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy \
CardinalArith.ML CardinalArith.thy Cardinal_AC.thy \
Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy Finite.ML Finite.thy \
@@ -45,9 +45,9 @@
Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \
Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \
Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \
- Trancl.ML Trancl.thy Univ.ML Univ.thy Update.ML Update.thy WF.ML \
+ Trancl.ML Trancl.thy Univ.thy Update.ML Update.thy WF.ML \
WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML domrange.ML \
- domrange.thy equalities.ML equalities.thy func.ML func.thy \
+ domrange.thy equalities.ML equalities.thy func.thy \
ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML \
subset.ML subset.thy thy_syntax.ML upair.ML upair.thy
@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
--- a/src/ZF/OrderType.thy Fri May 17 16:54:25 2002 +0200
+++ b/src/ZF/OrderType.thy Sat May 18 20:08:17 2002 +0200
@@ -180,8 +180,7 @@
lemma ordermap_mono:
"[| <w,x>: r; wf[A](r); w: A; x: A |]
==> ordermap(A,r)`w : ordermap(A,r)`x"
-apply (erule_tac x1 = x in ordermap_unfold [THEN ssubst], assumption)
-apply blast
+apply (erule_tac x1 = x in ordermap_unfold [THEN ssubst], assumption, blast)
done
(*linearity of r is crucial here*)
--- a/src/ZF/Univ.ML Fri May 17 16:54:25 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,765 +0,0 @@
-(* Title: ZF/Univ
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-The cumulative hierarchy and a small universe for recursive types
-*)
-
-(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
-Goal "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
-by (stac (Vfrom_def RS def_transrec) 1);
-by (Simp_tac 1);
-qed "Vfrom";
-
-(** Monotonicity **)
-
-Goal "A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)";
-by (eps_ind_tac "i" 1);
-by (rtac (impI RS allI) 1);
-by (stac Vfrom 1);
-by (stac Vfrom 1);
-by (etac Un_mono 1);
-by (rtac UN_mono 1);
-by (assume_tac 1);
-by (rtac Pow_mono 1);
-by (etac (bspec RS spec RS mp) 1);
-by (assume_tac 1);
-by (rtac subset_refl 1);
-qed_spec_mp "Vfrom_mono";
-
-
-(** A fundamental equality: Vfrom does not require ordinals! **)
-
-Goal "Vfrom(A,x) <= Vfrom(A,rank(x))";
-by (eps_ind_tac "x" 1);
-by (stac Vfrom 1);
-by (stac Vfrom 1);
-by (blast_tac (claset() addSIs [rank_lt RS ltD]) 1);
-qed "Vfrom_rank_subset1";
-
-Goal "Vfrom(A,rank(x)) <= Vfrom(A,x)";
-by (eps_ind_tac "x" 1);
-by (stac Vfrom 1);
-by (stac Vfrom 1);
-by (rtac (subset_refl RS Un_mono) 1);
-by (rtac UN_least 1);
-(*expand rank(x1) = (UN y:x1. succ(rank(y))) in assumptions*)
-by (etac (rank RS equalityD1 RS subsetD RS UN_E) 1);
-by (rtac subset_trans 1);
-by (etac UN_upper 2);
-by (rtac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1);
-by (etac (ltI RS le_imp_subset) 1);
-by (rtac (Ord_rank RS Ord_succ) 1);
-by (etac bspec 1);
-by (assume_tac 1);
-qed "Vfrom_rank_subset2";
-
-Goal "Vfrom(A,rank(x)) = Vfrom(A,x)";
-by (rtac equalityI 1);
-by (rtac Vfrom_rank_subset2 1);
-by (rtac Vfrom_rank_subset1 1);
-qed "Vfrom_rank_eq";
-
-
-(*** Basic closure properties ***)
-
-Goal "y:x ==> 0 : Vfrom(A,x)";
-by (stac Vfrom 1);
-by (Blast_tac 1);
-qed "zero_in_Vfrom";
-
-Goal "i <= Vfrom(A,i)";
-by (eps_ind_tac "i" 1);
-by (stac Vfrom 1);
-by (Blast_tac 1);
-qed "i_subset_Vfrom";
-
-Goal "A <= Vfrom(A,i)";
-by (stac Vfrom 1);
-by (rtac Un_upper1 1);
-qed "A_subset_Vfrom";
-
-bind_thm ("A_into_Vfrom", A_subset_Vfrom RS subsetD);
-
-Goal "a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
-by (stac Vfrom 1);
-by (Blast_tac 1);
-qed "subset_mem_Vfrom";
-
-(** Finite sets and ordered pairs **)
-
-Goal "a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";
-by (rtac subset_mem_Vfrom 1);
-by Safe_tac;
-qed "singleton_in_Vfrom";
-
-Goal "[| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))";
-by (rtac subset_mem_Vfrom 1);
-by Safe_tac;
-qed "doubleton_in_Vfrom";
-
-Goalw [Pair_def]
- "[| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> \
-\ <a,b> : Vfrom(A,succ(succ(i)))";
-by (REPEAT (ares_tac [doubleton_in_Vfrom] 1));
-qed "Pair_in_Vfrom";
-
-Goal "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))";
-by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1));
-by (rtac (Vfrom_mono RSN (2,subset_trans)) 2);
-by (REPEAT (ares_tac [subset_refl, subset_succI] 1));
-qed "succ_in_Vfrom";
-
-(*** 0, successor and limit equations fof Vfrom ***)
-
-Goal "Vfrom(A,0) = A";
-by (stac Vfrom 1);
-by (Blast_tac 1);
-qed "Vfrom_0";
-
-Goal "Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
-by (rtac (Vfrom RS trans) 1);
-by (rtac (succI1 RS RepFunI RS Union_upper RSN
- (2, equalityI RS subst_context)) 1);
-by (rtac UN_least 1);
-by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
-by (etac (ltI RS le_imp_subset) 1);
-by (etac Ord_succ 1);
-qed "Vfrom_succ_lemma";
-
-Goal "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
-by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1);
-by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1);
-by (stac rank_succ 1);
-by (rtac (Ord_rank RS Vfrom_succ_lemma) 1);
-qed "Vfrom_succ";
-
-(*The premise distinguishes this from Vfrom(A,0); allowing X=0 forces
- the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
-Goal "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
-by (stac Vfrom 1);
-by (rtac equalityI 1);
-(*first inclusion*)
-by (rtac Un_least 1);
-by (rtac (A_subset_Vfrom RS subset_trans) 1);
-by (rtac UN_upper 1);
-by (assume_tac 1);
-by (rtac UN_least 1);
-by (etac UnionE 1);
-by (rtac subset_trans 1);
-by (etac UN_upper 2 THEN stac Vfrom 1 THEN
- etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
-(*opposite inclusion*)
-by (rtac UN_least 1);
-by (stac Vfrom 1);
-by (Blast_tac 1);
-qed "Vfrom_Union";
-
-(*** Vfrom applied to Limit ordinals ***)
-
-(*NB. limit ordinals are non-empty;
- Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *)
-val [limiti] = goal (the_context ())
- "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))";
-by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1);
-by (stac (limiti RS Limit_Union_eq) 1);
-by (rtac refl 1);
-qed "Limit_Vfrom_eq";
-
-Goal "[| a: Vfrom(A,j); Limit(i); j<i |] ==> a : Vfrom(A,i)";
-by (rtac (Limit_Vfrom_eq RS equalityD2 RS subsetD) 1);
-by (REPEAT (ares_tac [ltD RS UN_I] 1));
-qed "Limit_VfromI";
-
-val prems = Goal
- "[| a: Vfrom(A,i); ~R ==> Limit(i); \
-\ !!x. [| x<i; a: Vfrom(A,x) |] ==> R \
-\ |] ==> R";
-by (rtac classical 1);
-by (rtac (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E) 1);
-by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1));
-qed "Limit_VfromE";
-
-bind_thm ("zero_in_VLimit", Limit_has_0 RS ltD RS zero_in_Vfrom);
-
-val [major,limiti] = goal (the_context ())
- "[| a: Vfrom(A,i); Limit(i) |] ==> {a} : Vfrom(A,i)";
-by (rtac ([major,limiti] MRS Limit_VfromE) 1);
-by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
-by (etac (limiti RS Limit_has_succ) 1);
-qed "singleton_in_VLimit";
-
-bind_thm ("Vfrom_UnI1", Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD));
-bind_thm ("Vfrom_UnI2", Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD));
-
-(*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*)
-val [aprem,bprem,limiti] = goal (the_context ())
- "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) |] ==> \
-\ {a,b} : Vfrom(A,i)";
-by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
-by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
-by (rtac ([doubleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
-by (etac Vfrom_UnI1 1);
-by (etac Vfrom_UnI2 1);
-by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
-qed "doubleton_in_VLimit";
-
-val [aprem,bprem,limiti] = goal (the_context ())
- "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) |] ==> \
-\ <a,b> : Vfrom(A,i)";
-(*Infer that a, b occur at ordinals x,xa < i.*)
-by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
-by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
-by (rtac ([Pair_in_Vfrom, limiti] MRS Limit_VfromI) 1);
-(*Infer that succ(succ(x Un xa)) < i *)
-by (etac Vfrom_UnI1 1);
-by (etac Vfrom_UnI2 1);
-by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
-qed "Pair_in_VLimit";
-
-Goal "Limit(i) ==> Vfrom(A,i)*Vfrom(A,i) <= Vfrom(A,i)";
-by (REPEAT (ares_tac [subsetI,Pair_in_VLimit] 1
- ORELSE eresolve_tac [SigmaE, ssubst] 1));
-qed "product_VLimit";
-
-bind_thm ("Sigma_subset_VLimit",
- [Sigma_mono, product_VLimit] MRS subset_trans);
-
-bind_thm ("nat_subset_VLimit",
- [nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans);
-
-Goal "[| n: nat; Limit(i) |] ==> n : Vfrom(A,i)";
-by (REPEAT (ares_tac [nat_subset_VLimit RS subsetD] 1));
-qed "nat_into_VLimit";
-
-(** Closure under disjoint union **)
-
-bind_thm ("zero_in_VLimit", Limit_has_0 RS ltD RS zero_in_Vfrom);
-
-Goal "Limit(i) ==> 1 : Vfrom(A,i)";
-by (REPEAT (ares_tac [nat_into_VLimit, nat_0I, nat_succI] 1));
-qed "one_in_VLimit";
-
-Goalw [Inl_def]
- "[| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)";
-by (REPEAT (ares_tac [zero_in_VLimit, Pair_in_VLimit] 1));
-qed "Inl_in_VLimit";
-
-Goalw [Inr_def]
- "[| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)";
-by (REPEAT (ares_tac [one_in_VLimit, Pair_in_VLimit] 1));
-qed "Inr_in_VLimit";
-
-Goal "Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)";
-by (blast_tac (claset() addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
-qed "sum_VLimit";
-
-bind_thm ("sum_subset_VLimit", [sum_mono, sum_VLimit] MRS subset_trans);
-
-
-
-(*** Properties assuming Transset(A) ***)
-
-Goal "Transset(A) ==> Transset(Vfrom(A,i))";
-by (eps_ind_tac "i" 1);
-by (stac Vfrom 1);
-by (blast_tac (claset() addSIs [Transset_Union_family, Transset_Un,
- Transset_Pow]) 1);
-qed "Transset_Vfrom";
-
-Goal "Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
-by (rtac (Vfrom_succ RS trans) 1);
-by (rtac (Un_upper2 RSN (2,equalityI)) 1);
-by (rtac (subset_refl RSN (2,Un_least)) 1);
-by (rtac (A_subset_Vfrom RS subset_trans) 1);
-by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1);
-qed "Transset_Vfrom_succ";
-
-Goalw [Pair_def,Transset_def] "[| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
-by (Blast_tac 1);
-qed "Transset_Pair_subset";
-
-Goal "[| <a,b> <= Vfrom(A,i); Transset(A); Limit(i) |] ==> \
-\ <a,b> : Vfrom(A,i)";
-by (etac (Transset_Pair_subset RS conjE) 1);
-by (etac Transset_Vfrom 1);
-by (REPEAT (ares_tac [Pair_in_VLimit] 1));
-qed "Transset_Pair_subset_VLimit";
-
-Goal "[| X: Vfrom(A,j); Transset(A) |] ==> Union(X) : Vfrom(A, succ(j))";
-by (dtac Transset_Vfrom 1);
-by (rtac subset_mem_Vfrom 1);
-by (rewtac Transset_def);
-by (Blast_tac 1);
-qed "Union_in_Vfrom";
-
-Goal "[| X: Vfrom(A,i); Limit(i); Transset(A) |] ==> Union(X) : Vfrom(A,i)";
-by (rtac (Limit_VfromE) 1 THEN REPEAT (assume_tac 1));
-by (blast_tac (claset() addIs [Limit_has_succ, Limit_VfromI, Union_in_Vfrom]) 1);
-qed "Union_in_VLimit";
-
-
-(*** Closure under product/sum applied to elements -- thus Vfrom(A,i)
- is a model of simple type theory provided A is a transitive set
- and i is a limit ordinal
-***)
-
-(*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*)
-val [aprem,bprem,limiti,step] = Goal
- "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); \
-\ !!x y j. [| j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) \
-\ |] ==> EX k. h(x,y): Vfrom(A,k) & k<i |] ==> \
-\ h(a,b) : Vfrom(A,i)";
-(*Infer that a, b occur at ordinals x,xa < i.*)
-by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
-by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
-by (res_inst_tac [("j1", "x Un xa Un 2")] (step RS exE) 1);
-by (blast_tac (claset() addIs [Limit_VfromI, limiti]) 5);
-by (etac (Vfrom_UnI2 RS Vfrom_UnI1) 4);
-by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3);
-by (rtac (succI1 RS UnI2) 2);
-by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1));
-qed "in_VLimit";
-
-(** products **)
-
-Goal "[| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==> \
-\ a*b : Vfrom(A, succ(succ(succ(j))))";
-by (dtac Transset_Vfrom 1);
-by (rtac subset_mem_Vfrom 1);
-by (rewtac Transset_def);
-by (blast_tac (claset() addIs [Pair_in_Vfrom]) 1);
-qed "prod_in_Vfrom";
-
-val [aprem,bprem,limiti,transset] = goal (the_context ())
- "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \
-\ a*b : Vfrom(A,i)";
-by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
-by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset,
- limiti RS Limit_has_succ] 1));
-qed "prod_in_VLimit";
-
-(** Disjoint sums, aka Quine ordered pairs **)
-
-Goalw [sum_def]
- "[| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A); 1:j |] ==> \
-\ a+b : Vfrom(A, succ(succ(succ(j))))";
-by (dtac Transset_Vfrom 1);
-by (rtac subset_mem_Vfrom 1);
-by (rewtac Transset_def);
-by (blast_tac (claset() addIs [zero_in_Vfrom, Pair_in_Vfrom,
- i_subset_Vfrom RS subsetD]) 1);
-qed "sum_in_Vfrom";
-
-val [aprem,bprem,limiti,transset] = goal (the_context ())
- "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \
-\ a+b : Vfrom(A,i)";
-by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
-by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset,
- limiti RS Limit_has_succ] 1));
-qed "sum_in_VLimit";
-
-(** function space! **)
-
-Goalw [Pi_def]
- "[| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==> \
-\ a->b : Vfrom(A, succ(succ(succ(succ(j)))))";
-by (dtac Transset_Vfrom 1);
-by (rtac subset_mem_Vfrom 1);
-by (rtac (Collect_subset RS subset_trans) 1);
-by (stac Vfrom 1);
-by (rtac (subset_trans RS subset_trans) 1);
-by (rtac Un_upper2 3);
-by (rtac (succI1 RS UN_upper) 2);
-by (rtac Pow_mono 1);
-by (rewtac Transset_def);
-by (blast_tac (claset() addIs [Pair_in_Vfrom]) 1);
-qed "fun_in_Vfrom";
-
-val [aprem,bprem,limiti,transset] = goal (the_context ())
- "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \
-\ a->b : Vfrom(A,i)";
-by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
-by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset,
- limiti RS Limit_has_succ] 1));
-qed "fun_in_VLimit";
-
-Goalw [Pi_def]
- "[| a: Vfrom(A,j); Transset(A) |] ==> Pow(a) : Vfrom(A, succ(succ(j)))";
-by (dtac Transset_Vfrom 1);
-by (rtac subset_mem_Vfrom 1);
-by (rewtac Transset_def);
-by (stac Vfrom 1);
-by (Blast_tac 1);
-qed "Pow_in_Vfrom";
-
-Goal "[| a: Vfrom(A,i); Limit(i); Transset(A) |] ==> Pow(a) : Vfrom(A,i)";
-by (blast_tac (claset() addEs [Limit_VfromE]
- addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1);
-qed "Pow_in_VLimit";
-
-
-(*** The set Vset(i) ***)
-
-Goal "Vset(i) = (UN j:i. Pow(Vset(j)))";
-by (stac Vfrom 1);
-by (Blast_tac 1);
-qed "Vset";
-
-bind_thm ("Vset_succ", Transset_0 RS Transset_Vfrom_succ);
-
-bind_thm ("Transset_Vset", Transset_0 RS Transset_Vfrom);
-
-(** Characterisation of the elements of Vset(i) **)
-
-Goal "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
-by (etac trans_induct 1);
-by (stac Vset 1);
-by Safe_tac;
-by (stac rank 1);
-by (rtac UN_succ_least_lt 1);
-by (Blast_tac 2);
-by (REPEAT (ares_tac [ltI] 1));
-qed_spec_mp "VsetD";
-
-Goal "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
-by (etac trans_induct 1);
-by (rtac allI 1);
-by (stac Vset 1);
-by (blast_tac (claset() addSIs [rank_lt RS ltD]) 1);
-val lemma = result();
-
-Goal "rank(x)<i ==> x : Vset(i)";
-by (etac ltE 1);
-by (etac (lemma RS spec RS mp) 1);
-by (assume_tac 1);
-qed "VsetI";
-
-(*Merely a lemma for the result following*)
-Goal "Ord(i) ==> b : Vset(i) <-> rank(b) < i";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1));
-qed "Vset_Ord_rank_iff";
-
-Goal "b : Vset(a) <-> rank(b) < rank(a)";
-by (rtac (Vfrom_rank_eq RS subst) 1);
-by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1);
-qed "Vset_rank_iff";
-Addsimps [Vset_rank_iff];
-
-(*This is rank(rank(a)) = rank(a) *)
-Addsimps [Ord_rank RS rank_of_Ord];
-
-Goal "Ord(i) ==> rank(Vset(i)) = i";
-by (stac rank 1);
-by (rtac equalityI 1);
-by Safe_tac;
-by (EVERY' [rtac UN_I,
- etac (i_subset_Vfrom RS subsetD),
- etac (Ord_in_Ord RS rank_of_Ord RS ssubst),
- assume_tac,
- rtac succI1] 3);
-by (REPEAT (eresolve_tac [asm_rl, VsetD RS ltD, Ord_trans] 1));
-qed "rank_Vset";
-
-(** Lemmas for reasoning about sets in terms of their elements' ranks **)
-
-Goal "a <= Vset(rank(a))";
-by (rtac subsetI 1);
-by (etac (rank_lt RS VsetI) 1);
-qed "arg_subset_Vset_rank";
-
-val [iprem] = Goal
- "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b";
-by (rtac ([subset_refl, arg_subset_Vset_rank] MRS
- Int_greatest RS subset_trans) 1);
-by (rtac (Ord_rank RS iprem) 1);
-qed "Int_Vset_subset";
-
-(** Set up an environment for simplification **)
-
-Goalw [Inl_def] "rank(a) < rank(Inl(a))";
-by (rtac rank_pair2 1);
-qed "rank_Inl";
-
-Goalw [Inr_def] "rank(a) < rank(Inr(a))";
-by (rtac rank_pair2 1);
-qed "rank_Inr";
-
-bind_thms ("rank_rls", [rank_Inl, rank_Inr, rank_pair1, rank_pair2]);
-bind_thms ("rank_trans_rls", rank_rls @ (rank_rls RLN (2, [lt_trans])));
-
-val rank_ss = simpset() addsimps [VsetI] addsimps rank_trans_rls;
-
-(** Recursion over Vset levels! **)
-
-(*NOT SUITABLE FOR REWRITING: recursive!*)
-Goalw [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
-by (stac transrec 1);
-by (Simp_tac 1);
-by (rtac (refl RS lam_cong RS subst_context) 1);
-by (Asm_full_simp_tac 1);
-qed "Vrec";
-
-(*This form avoids giant explosions in proofs. NOTE USE OF == *)
-val rew::prems = Goal
- "[| !!x. h(x)==Vrec(x,H) |] ==> \
-\ h(a) = H(a, lam x: Vset(rank(a)). h(x))";
-by (rewtac rew);
-by (rtac Vrec 1);
-qed "def_Vrec";
-
-(*NOT SUITABLE FOR REWRITING: recursive!*)
-Goalw [Vrecursor_def]
- "Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x), a)";
-by (stac transrec 1);
-by (Simp_tac 1);
-by (rtac (refl RS lam_cong RS subst_context) 1);
-by (Asm_full_simp_tac 1);
-qed "Vrecursor";
-
-(*This form avoids giant explosions in proofs. NOTE USE OF == *)
-Goal "h == Vrecursor(H) ==> h(a) = H(lam x: Vset(rank(a)). h(x), a)";
-by (Asm_simp_tac 1);
-by (rtac Vrecursor 1);
-qed "def_Vrecursor";
-
-
-(*** univ(A) ***)
-
-Goalw [univ_def] "A<=B ==> univ(A) <= univ(B)";
-by (etac Vfrom_mono 1);
-by (rtac subset_refl 1);
-qed "univ_mono";
-
-Goalw [univ_def] "Transset(A) ==> Transset(univ(A))";
-by (etac Transset_Vfrom 1);
-qed "Transset_univ";
-
-(** univ(A) as a limit **)
-
-Goalw [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))";
-by (rtac (Limit_nat RS Limit_Vfrom_eq) 1);
-qed "univ_eq_UN";
-
-Goal "c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))";
-by (rtac (subset_UN_iff_eq RS iffD1) 1);
-by (etac (univ_eq_UN RS subst) 1);
-qed "subset_univ_eq_Int";
-
-val [aprem, iprem] = Goal
- "[| a <= univ(X); \
-\ !!i. i:nat ==> a Int Vfrom(X,i) <= b \
-\ |] ==> a <= b";
-by (stac (aprem RS subset_univ_eq_Int) 1);
-by (rtac UN_least 1);
-by (etac iprem 1);
-qed "univ_Int_Vfrom_subset";
-
-val prems = Goal
- "[| a <= univ(X); b <= univ(X); \
-\ !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \
-\ |] ==> a = b";
-by (rtac equalityI 1);
-by (ALLGOALS
- (resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN'
- eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN'
- rtac Int_lower1));
-qed "univ_Int_Vfrom_eq";
-
-(** Closure properties **)
-
-Goalw [univ_def] "0 : univ(A)";
-by (rtac (nat_0I RS zero_in_Vfrom) 1);
-qed "zero_in_univ";
-
-Goalw [univ_def] "A <= univ(A)";
-by (rtac A_subset_Vfrom 1);
-qed "A_subset_univ";
-
-bind_thm ("A_into_univ", A_subset_univ RS subsetD);
-
-(** Closure under unordered and ordered pairs **)
-
-Goalw [univ_def] "a: univ(A) ==> {a} : univ(A)";
-by (REPEAT (ares_tac [singleton_in_VLimit, Limit_nat] 1));
-qed "singleton_in_univ";
-
-Goalw [univ_def]
- "[| a: univ(A); b: univ(A) |] ==> {a,b} : univ(A)";
-by (REPEAT (ares_tac [doubleton_in_VLimit, Limit_nat] 1));
-qed "doubleton_in_univ";
-
-Goalw [univ_def]
- "[| a: univ(A); b: univ(A) |] ==> <a,b> : univ(A)";
-by (REPEAT (ares_tac [Pair_in_VLimit, Limit_nat] 1));
-qed "Pair_in_univ";
-
-Goalw [univ_def]
- "[| X: univ(A); Transset(A) |] ==> Union(X) : univ(A)";
-by (REPEAT (ares_tac [Union_in_VLimit, Limit_nat] 1));
-qed "Union_in_univ";
-
-Goalw [univ_def] "univ(A)*univ(A) <= univ(A)";
-by (rtac (Limit_nat RS product_VLimit) 1);
-qed "product_univ";
-
-
-(** The natural numbers **)
-
-Goalw [univ_def] "nat <= univ(A)";
-by (rtac i_subset_Vfrom 1);
-qed "nat_subset_univ";
-
-(* n:nat ==> n:univ(A) *)
-bind_thm ("nat_into_univ", (nat_subset_univ RS subsetD));
-
-(** instances for 1 and 2 **)
-
-Goalw [univ_def] "1 : univ(A)";
-by (rtac (Limit_nat RS one_in_VLimit) 1);
-qed "one_in_univ";
-
-(*unused!*)
-Goal "2 : univ(A)";
-by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
-qed "two_in_univ";
-
-Goalw [bool_def] "bool <= univ(A)";
-by (blast_tac (claset() addSIs [zero_in_univ,one_in_univ]) 1);
-qed "bool_subset_univ";
-
-bind_thm ("bool_into_univ", (bool_subset_univ RS subsetD));
-
-
-(** Closure under disjoint union **)
-
-Goalw [univ_def] "a: univ(A) ==> Inl(a) : univ(A)";
-by (etac (Limit_nat RSN (2,Inl_in_VLimit)) 1);
-qed "Inl_in_univ";
-
-Goalw [univ_def] "b: univ(A) ==> Inr(b) : univ(A)";
-by (etac (Limit_nat RSN (2,Inr_in_VLimit)) 1);
-qed "Inr_in_univ";
-
-Goalw [univ_def] "univ(C)+univ(C) <= univ(C)";
-by (rtac (Limit_nat RS sum_VLimit) 1);
-qed "sum_univ";
-
-bind_thm ("sum_subset_univ", [sum_mono, sum_univ] MRS subset_trans);
-
-
-(** Closure under binary union -- use Un_least **)
-(** Closure under Collect -- use (Collect_subset RS subset_trans) **)
-(** Closure under RepFun -- use RepFun_subset **)
-
-
-(*** Finite Branching Closure Properties ***)
-
-(** Closure under finite powerset **)
-
-Goal "[| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
-by (etac Fin_induct 1);
-by (blast_tac (claset() addSDs [Limit_has_0]) 1);
-by Safe_tac;
-by (etac Limit_VfromE 1);
-by (assume_tac 1);
-by (blast_tac (claset() addSIs [Un_least_lt] addIs [Vfrom_UnI1, Vfrom_UnI2]) 1);
-qed "Fin_Vfrom_lemma";
-
-Goal "Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
-by (rtac subsetI 1);
-by (dtac Fin_Vfrom_lemma 1);
-by Safe_tac;
-by (resolve_tac [Vfrom RS ssubst] 1);
-by (blast_tac (claset() addSDs [ltD]) 1);
-qed "Fin_VLimit";
-
-bind_thm ("Fin_subset_VLimit", [Fin_mono, Fin_VLimit] MRS subset_trans);
-
-Goalw [univ_def] "Fin(univ(A)) <= univ(A)";
-by (rtac (Limit_nat RS Fin_VLimit) 1);
-qed "Fin_univ";
-
-(** Closure under finite powers (functions from a fixed natural number) **)
-
-Goal "[| n: nat; Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)";
-by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
-by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit,
- nat_subset_VLimit, subset_refl] 1));
-qed "nat_fun_VLimit";
-
-bind_thm ("nat_fun_subset_VLimit", [Pi_mono, nat_fun_VLimit] MRS subset_trans);
-
-Goalw [univ_def] "n: nat ==> n -> univ(A) <= univ(A)";
-by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1);
-qed "nat_fun_univ";
-
-
-(** Closure under finite function space **)
-
-(*General but seldom-used version; normally the domain is fixed*)
-Goal "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)";
-by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1);
-by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1));
-qed "FiniteFun_VLimit1";
-
-Goalw [univ_def] "univ(A) -||> univ(A) <= univ(A)";
-by (rtac (Limit_nat RS FiniteFun_VLimit1) 1);
-qed "FiniteFun_univ1";
-
-(*Version for a fixed domain*)
-Goal "[| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)";
-by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1);
-by (etac FiniteFun_VLimit1 1);
-qed "FiniteFun_VLimit";
-
-Goalw [univ_def]
- "W <= univ(A) ==> W -||> univ(A) <= univ(A)";
-by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1);
-qed "FiniteFun_univ";
-
-Goal "[| f: W -||> univ(A); W <= univ(A) |] ==> f : univ(A)";
-by (eresolve_tac [FiniteFun_univ RS subsetD] 1);
-by (assume_tac 1);
-qed "FiniteFun_in_univ";
-
-(*Remove <= from the rule above*)
-bind_thm ("FiniteFun_in_univ'", subsetI RSN (2, FiniteFun_in_univ));
-
-
-(**** For QUniv. Properties of Vfrom analogous to the "take-lemma" ****)
-
-(*** Intersecting a*b with Vfrom... ***)
-
-(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*)
-Goal "[| {a,b} : Vfrom(X,succ(i)); Transset(X) |] \
-\ ==> a: Vfrom(X,i) & b: Vfrom(X,i)";
-by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1);
-by (assume_tac 1);
-by (Fast_tac 1);
-qed "doubleton_in_Vfrom_D";
-
-(*This weaker version says a, b exist at the same level*)
-bind_thm ("Vfrom_doubleton_D", Transset_Vfrom RS Transset_doubleton_D);
-
-(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
- implies a, b : Vfrom(X,i), which is useless for induction.
- Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
- implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
- The combination gives a reduction by precisely one level, which is
- most convenient for proofs.
-**)
-
-Goalw [Pair_def]
- "[| <a,b> : Vfrom(X,succ(i)); Transset(X) |] \
-\ ==> a: Vfrom(X,i) & b: Vfrom(X,i)";
-by (blast_tac (claset() addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
-qed "Pair_in_Vfrom_D";
-
-Goal "Transset(X) ==> \
-\ (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";
-by (blast_tac (claset() addSDs [Pair_in_Vfrom_D]) 1);
-qed "product_Int_Vfrom_subset";
-
--- a/src/ZF/Univ.thy Fri May 17 16:54:25 2002 +0200
+++ b/src/ZF/Univ.thy Sat May 18 20:08:17 2002 +0200
@@ -11,30 +11,885 @@
But Ind_Syntax.univ refers to the constant "Univ.univ"
*)
-Univ = Epsilon + Sum + Finite + mono +
+theory Univ = Epsilon + Sum + Finite + mono:
-consts
- Vfrom :: [i,i]=>i
- Vset :: i=>i
- Vrec :: [i, [i,i]=>i] =>i
- Vrecursor :: [[i,i]=>i, i] =>i
- univ :: i=>i
+constdefs
+ Vfrom :: "[i,i]=>i"
+ "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
+syntax Vset :: "i=>i"
translations
"Vset(x)" == "Vfrom(0,x)"
-defs
- Vfrom_def "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
+constdefs
+ Vrec :: "[i, [i,i]=>i] =>i"
+ "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
+ H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
+
+ Vrecursor :: "[[i,i]=>i, i] =>i"
+ "Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
+ H(lam w:Vset(x). g`rank(w)`w, z)) ` a"
+
+ univ :: "i=>i"
+ "univ(A) == Vfrom(A,nat)"
+
+
+text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
+lemma Vfrom: "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))"
+apply (subst Vfrom_def [THEN def_transrec])
+apply simp
+done
+
+subsubsection{* Monotonicity *}
+
+lemma Vfrom_mono [rule_format]:
+ "A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)"
+apply (rule_tac a=i in eps_induct)
+apply (rule impI [THEN allI])
+apply (subst Vfrom)
+apply (subst Vfrom)
+apply (erule Un_mono)
+apply (erule UN_mono, blast)
+done
+
+
+subsubsection{* A fundamental equality: Vfrom does not require ordinals! *}
+
+lemma Vfrom_rank_subset1: "Vfrom(A,x) <= Vfrom(A,rank(x))"
+apply (rule_tac a=x in eps_induct)
+apply (subst Vfrom)
+apply (subst Vfrom)
+apply (blast intro!: rank_lt [THEN ltD])
+done
+
+lemma Vfrom_rank_subset2: "Vfrom(A,rank(x)) <= Vfrom(A,x)"
+apply (rule_tac a=x in eps_induct)
+apply (subst Vfrom)
+apply (subst Vfrom)
+apply (rule subset_refl [THEN Un_mono])
+apply (rule UN_least)
+txt{*expand rank(x1) = (UN y:x1. succ(rank(y))) in assumptions*}
+apply (erule rank [THEN equalityD1, THEN subsetD, THEN UN_E])
+apply (rule subset_trans)
+apply (erule_tac [2] UN_upper)
+apply (rule subset_refl [THEN Vfrom_mono, THEN subset_trans, THEN Pow_mono])
+apply (erule ltI [THEN le_imp_subset])
+apply (rule Ord_rank [THEN Ord_succ])
+apply (erule bspec, assumption)
+done
+
+lemma Vfrom_rank_eq: "Vfrom(A,rank(x)) = Vfrom(A,x)"
+apply (rule equalityI)
+apply (rule Vfrom_rank_subset2)
+apply (rule Vfrom_rank_subset1)
+done
+
+
+subsection{* Basic closure properties *}
+
+lemma zero_in_Vfrom: "y:x ==> 0 : Vfrom(A,x)"
+by (subst Vfrom, blast)
+
+lemma i_subset_Vfrom: "i <= Vfrom(A,i)"
+apply (rule_tac a=i in eps_induct)
+apply (subst Vfrom, blast)
+done
+
+lemma A_subset_Vfrom: "A <= Vfrom(A,i)"
+apply (subst Vfrom)
+apply (rule Un_upper1)
+done
+
+lemmas A_into_Vfrom = A_subset_Vfrom [THEN subsetD]
+
+lemma subset_mem_Vfrom: "a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))"
+by (subst Vfrom, blast)
+
+subsubsection{* Finite sets and ordered pairs *}
+
+lemma singleton_in_Vfrom: "a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))"
+by (rule subset_mem_Vfrom, safe)
+
+lemma doubleton_in_Vfrom:
+ "[| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))"
+by (rule subset_mem_Vfrom, safe)
+
+lemma Pair_in_Vfrom:
+ "[| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> <a,b> : Vfrom(A,succ(succ(i)))"
+apply (unfold Pair_def)
+apply (blast intro: doubleton_in_Vfrom)
+done
+
+lemma succ_in_Vfrom: "a <= Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))"
+apply (intro subset_mem_Vfrom succ_subsetI, assumption)
+apply (erule subset_trans)
+apply (rule Vfrom_mono [OF subset_refl subset_succI])
+done
+
+subsection{* 0, successor and limit equations fof Vfrom *}
+
+lemma Vfrom_0: "Vfrom(A,0) = A"
+by (subst Vfrom, blast)
+
+lemma Vfrom_succ_lemma: "Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
+apply (rule Vfrom [THEN trans])
+apply (rule equalityI [THEN subst_context,
+ OF _ succI1 [THEN RepFunI, THEN Union_upper]])
+apply (rule UN_least)
+apply (rule subset_refl [THEN Vfrom_mono, THEN Pow_mono])
+apply (erule ltI [THEN le_imp_subset])
+apply (erule Ord_succ)
+done
+
+lemma Vfrom_succ: "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
+apply (rule_tac x1 = "succ (i)" in Vfrom_rank_eq [THEN subst])
+apply (rule_tac x1 = "i" in Vfrom_rank_eq [THEN subst])
+apply (subst rank_succ)
+apply (rule Ord_rank [THEN Vfrom_succ_lemma])
+done
+
+(*The premise distinguishes this from Vfrom(A,0); allowing X=0 forces
+ the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
+lemma Vfrom_Union: "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))"
+apply (subst Vfrom)
+apply (rule equalityI)
+txt{*first inclusion*}
+apply (rule Un_least)
+apply (rule A_subset_Vfrom [THEN subset_trans])
+apply (rule UN_upper, assumption)
+apply (rule UN_least)
+apply (erule UnionE)
+apply (rule subset_trans)
+apply (erule_tac [2] UN_upper,
+ subst Vfrom, erule subset_trans [OF UN_upper Un_upper2])
+txt{*opposite inclusion*}
+apply (rule UN_least)
+apply (subst Vfrom, blast)
+done
+
+subsection{* Vfrom applied to Limit ordinals *}
+
+(*NB. limit ordinals are non-empty:
+ Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *)
+lemma Limit_Vfrom_eq:
+ "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))"
+apply (rule Limit_has_0 [THEN ltD, THEN Vfrom_Union, THEN subst], assumption)
+apply (simp add: Limit_Union_eq)
+done
+
+lemma Limit_VfromI: "[| a: Vfrom(A,j); Limit(i); j<i |] ==> a : Vfrom(A,i)"
+apply (rule Limit_Vfrom_eq [THEN equalityD2, THEN subsetD], assumption)
+apply (blast intro: ltD)
+done
+
+lemma Limit_VfromE:
+ "[| a: Vfrom(A,i); ~R ==> Limit(i);
+ !!x. [| x<i; a: Vfrom(A,x) |] ==> R
+ |] ==> R"
+apply (rule classical)
+apply (rule Limit_Vfrom_eq [THEN equalityD1, THEN subsetD, THEN UN_E])
+prefer 2 apply assumption
+apply blast
+apply (blast intro: ltI Limit_is_Ord)
+done
+
+lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
+
+lemma singleton_in_VLimit:
+ "[| a: Vfrom(A,i); Limit(i) |] ==> {a} : Vfrom(A,i)"
+apply (erule Limit_VfromE, assumption)
+apply (erule singleton_in_Vfrom [THEN Limit_VfromI], assumption)
+apply (blast intro: Limit_has_succ)
+done
+
+lemmas Vfrom_UnI1 =
+ Un_upper1 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard]
+lemmas Vfrom_UnI2 =
+ Un_upper2 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard]
+
+text{*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*}
+lemma doubleton_in_VLimit:
+ "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) |] ==> {a,b} : Vfrom(A,i)"
+apply (erule Limit_VfromE, assumption)
+apply (erule Limit_VfromE, assumption)
+apply (blast intro: Limit_VfromI [OF doubleton_in_Vfrom]
+ Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt)
+done
+
+lemma Pair_in_VLimit:
+ "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) |] ==> <a,b> : Vfrom(A,i)"
+txt{*Infer that a, b occur at ordinals x,xa < i.*}
+apply (erule Limit_VfromE, assumption)
+apply (erule Limit_VfromE, assumption)
+txt{*Infer that succ(succ(x Un xa)) < i *}
+apply (blast intro: Limit_VfromI [OF Pair_in_Vfrom]
+ Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt)
+done
+
+lemma product_VLimit: "Limit(i) ==> Vfrom(A,i) * Vfrom(A,i) <= Vfrom(A,i)"
+by (blast intro: Pair_in_VLimit)
+
+lemmas Sigma_subset_VLimit =
+ subset_trans [OF Sigma_mono product_VLimit]
+
+lemmas nat_subset_VLimit =
+ subset_trans [OF nat_le_Limit [THEN le_imp_subset] i_subset_Vfrom]
+
+lemma nat_into_VLimit: "[| n: nat; Limit(i) |] ==> n : Vfrom(A,i)"
+by (blast intro: nat_subset_VLimit [THEN subsetD])
+
+subsubsection{* Closure under disjoint union *}
+
+lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
+
+lemma one_in_VLimit: "Limit(i) ==> 1 : Vfrom(A,i)"
+by (blast intro: nat_into_VLimit)
+
+lemma Inl_in_VLimit:
+ "[| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)"
+apply (unfold Inl_def)
+apply (blast intro: zero_in_VLimit Pair_in_VLimit)
+done
+
+lemma Inr_in_VLimit:
+ "[| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)"
+apply (unfold Inr_def)
+apply (blast intro: one_in_VLimit Pair_in_VLimit)
+done
+
+lemma sum_VLimit: "Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)"
+by (blast intro!: Inl_in_VLimit Inr_in_VLimit)
+
+lemmas sum_subset_VLimit = subset_trans [OF sum_mono sum_VLimit]
+
+
+
+subsection{* Properties assuming Transset(A) *}
+
+lemma Transset_Vfrom: "Transset(A) ==> Transset(Vfrom(A,i))"
+apply (rule_tac a=i in eps_induct)
+apply (subst Vfrom)
+apply (blast intro!: Transset_Union_family Transset_Un Transset_Pow)
+done
+
+lemma Transset_Vfrom_succ:
+ "Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))"
+apply (rule Vfrom_succ [THEN trans])
+apply (rule equalityI [OF _ Un_upper2])
+apply (rule Un_least [OF _ subset_refl])
+apply (rule A_subset_Vfrom [THEN subset_trans])
+apply (erule Transset_Vfrom [THEN Transset_iff_Pow [THEN iffD1]])
+done
+
+lemma Transset_Pair_subset: "[| <a,b> <= C; Transset(C) |] ==> a: C & b: C"
+by (unfold Pair_def Transset_def, blast)
+
+lemma Transset_Pair_subset_VLimit:
+ "[| <a,b> <= Vfrom(A,i); Transset(A); Limit(i) |]
+ ==> <a,b> : Vfrom(A,i)"
+apply (erule Transset_Pair_subset [THEN conjE])
+apply (erule Transset_Vfrom)
+apply (blast intro: Pair_in_VLimit)
+done
+
+lemma Union_in_Vfrom:
+ "[| X: Vfrom(A,j); Transset(A) |] ==> Union(X) : Vfrom(A, succ(j))"
+apply (drule Transset_Vfrom)
+apply (rule subset_mem_Vfrom)
+apply (unfold Transset_def, blast)
+done
+
+lemma Union_in_VLimit:
+ "[| X: Vfrom(A,i); Limit(i); Transset(A) |] ==> Union(X) : Vfrom(A,i)"
+apply (rule Limit_VfromE, assumption+)
+apply (blast intro: Limit_has_succ Limit_VfromI Union_in_Vfrom)
+done
+
+
+(*** Closure under product/sum applied to elements -- thus Vfrom(A,i)
+ is a model of simple type theory provided A is a transitive set
+ and i is a limit ordinal
+***)
+
+text{*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*}
+lemma in_VLimit:
+ "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i);
+ !!x y j. [| j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) |]
+ ==> EX k. h(x,y): Vfrom(A,k) & k<i |]
+ ==> h(a,b) : Vfrom(A,i)"
+txt{*Infer that a, b occur at ordinals x,xa < i.*}
+apply (erule Limit_VfromE, assumption)
+apply (erule Limit_VfromE, assumption, atomize)
+apply (drule_tac x=a in spec)
+apply (drule_tac x=b in spec)
+apply (drule_tac x="x Un xa Un 2" in spec)
+txt{*FIXME: can do better using simprule about Un and <*}
+apply (simp add: Vfrom_UnI2 [THEN Vfrom_UnI1] Vfrom_UnI1 [THEN Vfrom_UnI1])
+apply (blast intro: Limit_has_0 Limit_has_succ Un_least_lt Limit_VfromI)
+done
+
+subsubsection{* products *}
+
+lemma prod_in_Vfrom:
+ "[| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |]
+ ==> a*b : Vfrom(A, succ(succ(succ(j))))"
+apply (drule Transset_Vfrom)
+apply (rule subset_mem_Vfrom)
+apply (unfold Transset_def)
+apply (blast intro: Pair_in_Vfrom)
+done
+
+lemma prod_in_VLimit:
+ "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |]
+ ==> a*b : Vfrom(A,i)"
+apply (erule in_VLimit, assumption+)
+apply (blast intro: prod_in_Vfrom Limit_has_succ)
+done
+
+subsubsection{* Disjoint sums, aka Quine ordered pairs *}
+
+lemma sum_in_Vfrom:
+ "[| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A); 1:j |]
+ ==> a+b : Vfrom(A, succ(succ(succ(j))))"
+apply (unfold sum_def)
+apply (drule Transset_Vfrom)
+apply (rule subset_mem_Vfrom)
+apply (unfold Transset_def)
+apply (blast intro: zero_in_Vfrom Pair_in_Vfrom i_subset_Vfrom [THEN subsetD])
+done
+
+lemma sum_in_VLimit:
+ "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |]
+ ==> a+b : Vfrom(A,i)"
+apply (erule in_VLimit, assumption+)
+apply (blast intro: sum_in_Vfrom Limit_has_succ)
+done
+
+subsubsection{* function space! *}
+
+lemma fun_in_Vfrom:
+ "[| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==>
+ a->b : Vfrom(A, succ(succ(succ(succ(j)))))"
+apply (unfold Pi_def)
+apply (drule Transset_Vfrom)
+apply (rule subset_mem_Vfrom)
+apply (rule Collect_subset [THEN subset_trans])
+apply (subst Vfrom)
+apply (rule subset_trans [THEN subset_trans])
+apply (rule_tac [3] Un_upper2)
+apply (rule_tac [2] succI1 [THEN UN_upper])
+apply (rule Pow_mono)
+apply (unfold Transset_def)
+apply (blast intro: Pair_in_Vfrom)
+done
+
+lemma fun_in_VLimit:
+ "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |]
+ ==> a->b : Vfrom(A,i)"
+apply (erule in_VLimit, assumption+)
+apply (blast intro: fun_in_Vfrom Limit_has_succ)
+done
+
+lemma Pow_in_Vfrom:
+ "[| a: Vfrom(A,j); Transset(A) |] ==> Pow(a) : Vfrom(A, succ(succ(j)))"
+apply (drule Transset_Vfrom)
+apply (rule subset_mem_Vfrom)
+apply (unfold Transset_def)
+apply (subst Vfrom, blast)
+done
+
+lemma Pow_in_VLimit:
+ "[| a: Vfrom(A,i); Limit(i); Transset(A) |] ==> Pow(a) : Vfrom(A,i)"
+by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom Limit_VfromI)
+
+
+subsection{* The set Vset(i) *}
+
+lemma Vset: "Vset(i) = (UN j:i. Pow(Vset(j)))"
+by (subst Vfrom, blast)
+
+lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ, standard]
+lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom, standard]
+
+subsubsection{* Characterisation of the elements of Vset(i) *}
+
+lemma VsetD [rule_format]: "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i"
+apply (erule trans_induct)
+apply (subst Vset, safe)
+apply (subst rank)
+apply (blast intro: ltI UN_succ_least_lt)
+done
+
+lemma VsetI_lemma [rule_format]:
+ "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)"
+apply (erule trans_induct)
+apply (rule allI)
+apply (subst Vset)
+apply (blast intro!: rank_lt [THEN ltD])
+done
+
+lemma VsetI: "rank(x)<i ==> x : Vset(i)"
+by (blast intro: VsetI_lemma elim: ltE)
+
+text{*Merely a lemma for the next result*}
+lemma Vset_Ord_rank_iff: "Ord(i) ==> b : Vset(i) <-> rank(b) < i"
+by (blast intro: VsetD VsetI)
+
+lemma Vset_rank_iff [simp]: "b : Vset(a) <-> rank(b) < rank(a)"
+apply (rule Vfrom_rank_eq [THEN subst])
+apply (rule Ord_rank [THEN Vset_Ord_rank_iff])
+done
+
+text{*This is rank(rank(a)) = rank(a) *}
+declare Ord_rank [THEN rank_of_Ord, simp]
+
+lemma rank_Vset: "Ord(i) ==> rank(Vset(i)) = i"
+apply (subst rank)
+apply (rule equalityI, safe)
+apply (blast intro: VsetD [THEN ltD])
+apply (blast intro: VsetD [THEN ltD] Ord_trans)
+apply (blast intro: i_subset_Vfrom [THEN subsetD]
+ Ord_in_Ord [THEN rank_of_Ord, THEN ssubst])
+done
+
+subsubsection{* Lemmas for reasoning about sets in terms of their elements' ranks *}
- Vrec_def
- "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
- H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
+lemma arg_subset_Vset_rank: "a <= Vset(rank(a))"
+apply (rule subsetI)
+apply (erule rank_lt [THEN VsetI])
+done
+
+lemma Int_Vset_subset:
+ "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b"
+apply (rule subset_trans)
+apply (rule Int_greatest [OF subset_refl arg_subset_Vset_rank])
+apply (blast intro: Ord_rank)
+done
+
+subsubsection{* Set up an environment for simplification *}
+
+lemma rank_Inl: "rank(a) < rank(Inl(a))"
+apply (unfold Inl_def)
+apply (rule rank_pair2)
+done
+
+lemma rank_Inr: "rank(a) < rank(Inr(a))"
+apply (unfold Inr_def)
+apply (rule rank_pair2)
+done
+
+lemmas rank_rls = rank_Inl rank_Inr rank_pair1 rank_pair2
+
+subsubsection{* Recursion over Vset levels! *}
+
+text{*NOT SUITABLE FOR REWRITING: recursive!*}
+lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"
+apply (unfold Vrec_def)
+apply (subst transrec)
+apply simp
+apply (rule refl [THEN lam_cong, THEN subst_context], simp)
+done
+
+text{*This form avoids giant explosions in proofs. NOTE USE OF == *}
+lemma def_Vrec:
+ "[| !!x. h(x)==Vrec(x,H) |] ==>
+ h(a) = H(a, lam x: Vset(rank(a)). h(x))"
+apply simp
+apply (rule Vrec)
+done
+
+text{*NOT SUITABLE FOR REWRITING: recursive!*}
+lemma Vrecursor:
+ "Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x), a)"
+apply (unfold Vrecursor_def)
+apply (subst transrec, simp)
+apply (rule refl [THEN lam_cong, THEN subst_context], simp)
+done
+
+text{*This form avoids giant explosions in proofs. NOTE USE OF == *}
+lemma def_Vrecursor:
+ "h == Vrecursor(H) ==> h(a) = H(lam x: Vset(rank(a)). h(x), a)"
+apply simp
+apply (rule Vrecursor)
+done
+
+
+subsection{* univ(A) *}
+
+lemma univ_mono: "A<=B ==> univ(A) <= univ(B)"
+apply (unfold univ_def)
+apply (erule Vfrom_mono)
+apply (rule subset_refl)
+done
+
+lemma Transset_univ: "Transset(A) ==> Transset(univ(A))"
+apply (unfold univ_def)
+apply (erule Transset_Vfrom)
+done
+
+subsubsection{* univ(A) as a limit *}
+
+lemma univ_eq_UN: "univ(A) = (UN i:nat. Vfrom(A,i))"
+apply (unfold univ_def)
+apply (rule Limit_nat [THEN Limit_Vfrom_eq])
+done
+
+lemma subset_univ_eq_Int: "c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))"
+apply (rule subset_UN_iff_eq [THEN iffD1])
+apply (erule univ_eq_UN [THEN subst])
+done
+
+lemma univ_Int_Vfrom_subset:
+ "[| a <= univ(X);
+ !!i. i:nat ==> a Int Vfrom(X,i) <= b |]
+ ==> a <= b"
+apply (subst subset_univ_eq_Int, assumption)
+apply (rule UN_least, simp)
+done
+
+lemma univ_Int_Vfrom_eq:
+ "[| a <= univ(X); b <= univ(X);
+ !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i)
+ |] ==> a = b"
+apply (rule equalityI)
+apply (rule univ_Int_Vfrom_subset, assumption)
+apply (blast elim: equalityCE)
+apply (rule univ_Int_Vfrom_subset, assumption)
+apply (blast elim: equalityCE)
+done
+
+subsubsection{* Closure properties *}
+
+lemma zero_in_univ: "0 : univ(A)"
+apply (unfold univ_def)
+apply (rule nat_0I [THEN zero_in_Vfrom])
+done
+
+lemma A_subset_univ: "A <= univ(A)"
+apply (unfold univ_def)
+apply (rule A_subset_Vfrom)
+done
+
+lemmas A_into_univ = A_subset_univ [THEN subsetD, standard]
+
+subsubsection{* Closure under unordered and ordered pairs *}
+
+lemma singleton_in_univ: "a: univ(A) ==> {a} : univ(A)"
+apply (unfold univ_def)
+apply (blast intro: singleton_in_VLimit Limit_nat)
+done
+
+lemma doubleton_in_univ:
+ "[| a: univ(A); b: univ(A) |] ==> {a,b} : univ(A)"
+apply (unfold univ_def)
+apply (blast intro: doubleton_in_VLimit Limit_nat)
+done
+
+lemma Pair_in_univ:
+ "[| a: univ(A); b: univ(A) |] ==> <a,b> : univ(A)"
+apply (unfold univ_def)
+apply (blast intro: Pair_in_VLimit Limit_nat)
+done
+
+lemma Union_in_univ:
+ "[| X: univ(A); Transset(A) |] ==> Union(X) : univ(A)"
+apply (unfold univ_def)
+apply (blast intro: Union_in_VLimit Limit_nat)
+done
+
+lemma product_univ: "univ(A)*univ(A) <= univ(A)"
+apply (unfold univ_def)
+apply (rule Limit_nat [THEN product_VLimit])
+done
+
+
+subsubsection{* The natural numbers *}
+
+lemma nat_subset_univ: "nat <= univ(A)"
+apply (unfold univ_def)
+apply (rule i_subset_Vfrom)
+done
+
+text{* n:nat ==> n:univ(A) *}
+lemmas nat_into_univ = nat_subset_univ [THEN subsetD, standard]
+
+subsubsection{* instances for 1 and 2 *}
+
+lemma one_in_univ: "1 : univ(A)"
+apply (unfold univ_def)
+apply (rule Limit_nat [THEN one_in_VLimit])
+done
+
+text{*unused!*}
+lemma two_in_univ: "2 : univ(A)"
+by (blast intro: nat_into_univ)
+
+lemma bool_subset_univ: "bool <= univ(A)"
+apply (unfold bool_def)
+apply (blast intro!: zero_in_univ one_in_univ)
+done
+
+lemmas bool_into_univ = bool_subset_univ [THEN subsetD, standard]
+
+
+subsubsection{* Closure under disjoint union *}
+
+lemma Inl_in_univ: "a: univ(A) ==> Inl(a) : univ(A)"
+apply (unfold univ_def)
+apply (erule Inl_in_VLimit [OF _ Limit_nat])
+done
+
+lemma Inr_in_univ: "b: univ(A) ==> Inr(b) : univ(A)"
+apply (unfold univ_def)
+apply (erule Inr_in_VLimit [OF _ Limit_nat])
+done
+
+lemma sum_univ: "univ(C)+univ(C) <= univ(C)"
+apply (unfold univ_def)
+apply (rule Limit_nat [THEN sum_VLimit])
+done
+
+lemmas sum_subset_univ = subset_trans [OF sum_mono sum_univ]
+
+
+subsubsection{* Closure under binary union -- use Un_least *}
+subsubsection{* Closure under Collect -- use (Collect_subset RS subset_trans) *}
+subsubsection{* Closure under RepFun -- use RepFun_subset *}
+
+
+subsection{* Finite Branching Closure Properties *}
+
+subsubsection{* Closure under finite powerset *}
+
+lemma Fin_Vfrom_lemma:
+ "[| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i"
+apply (erule Fin_induct)
+apply (blast dest!: Limit_has_0, safe)
+apply (erule Limit_VfromE, assumption)
+apply (blast intro!: Un_least_lt intro: Vfrom_UnI1 Vfrom_UnI2)
+done
- Vrecursor_def
- "Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
- H(lam w:Vset(x). g`rank(w)`w, z)) ` a"
+lemma Fin_VLimit: "Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)"
+apply (rule subsetI)
+apply (drule Fin_Vfrom_lemma, safe)
+apply (rule Vfrom [THEN ssubst])
+apply (blast dest!: ltD)
+done
+
+lemmas Fin_subset_VLimit = subset_trans [OF Fin_mono Fin_VLimit]
+
+lemma Fin_univ: "Fin(univ(A)) <= univ(A)"
+apply (unfold univ_def)
+apply (rule Limit_nat [THEN Fin_VLimit])
+done
+
+subsubsection{* Closure under finite powers (functions from a fixed natural number) *}
+
+lemma nat_fun_VLimit:
+ "[| n: nat; Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)"
+apply (erule nat_fun_subset_Fin [THEN subset_trans])
+apply (blast del: subsetI
+ intro: subset_refl Fin_subset_VLimit Sigma_subset_VLimit nat_subset_VLimit)
+done
+
+lemmas nat_fun_subset_VLimit = subset_trans [OF Pi_mono nat_fun_VLimit]
+
+lemma nat_fun_univ: "n: nat ==> n -> univ(A) <= univ(A)"
+apply (unfold univ_def)
+apply (erule nat_fun_VLimit [OF _ Limit_nat])
+done
+
+
+subsubsection{* Closure under finite function space *}
+
+text{*General but seldom-used version; normally the domain is fixed*}
+lemma FiniteFun_VLimit1:
+ "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)"
+apply (rule FiniteFun.dom_subset [THEN subset_trans])
+apply (blast del: subsetI
+ intro: Fin_subset_VLimit Sigma_subset_VLimit subset_refl)
+done
+
+lemma FiniteFun_univ1: "univ(A) -||> univ(A) <= univ(A)"
+apply (unfold univ_def)
+apply (rule Limit_nat [THEN FiniteFun_VLimit1])
+done
+
+text{*Version for a fixed domain*}
+lemma FiniteFun_VLimit:
+ "[| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)"
+apply (rule subset_trans)
+apply (erule FiniteFun_mono [OF _ subset_refl])
+apply (erule FiniteFun_VLimit1)
+done
+
+lemma FiniteFun_univ:
+ "W <= univ(A) ==> W -||> univ(A) <= univ(A)"
+apply (unfold univ_def)
+apply (erule FiniteFun_VLimit [OF _ Limit_nat])
+done
+
+lemma FiniteFun_in_univ:
+ "[| f: W -||> univ(A); W <= univ(A) |] ==> f : univ(A)"
+by (erule FiniteFun_univ [THEN subsetD], assumption)
+
+text{*Remove <= from the rule above*}
+lemmas FiniteFun_in_univ' = FiniteFun_in_univ [OF _ subsetI]
+
+
+subsection{** For QUniv. Properties of Vfrom analogous to the "take-lemma" **}
+
+subsection{* Intersecting a*b with Vfrom... *}
+
+text{*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*}
+lemma doubleton_in_Vfrom_D:
+ "[| {a,b} : Vfrom(X,succ(i)); Transset(X) |]
+ ==> a: Vfrom(X,i) & b: Vfrom(X,i)"
+by (drule Transset_Vfrom_succ [THEN equalityD1, THEN subsetD, THEN PowD],
+ assumption, fast)
+
+text{*This weaker version says a, b exist at the same level*}
+lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D, standard]
+
+(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
+ implies a, b : Vfrom(X,i), which is useless for induction.
+ Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
+ implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
+ The combination gives a reduction by precisely one level, which is
+ most convenient for proofs.
+**)
+
+lemma Pair_in_Vfrom_D:
+ "[| <a,b> : Vfrom(X,succ(i)); Transset(X) |]
+ ==> a: Vfrom(X,i) & b: Vfrom(X,i)"
+apply (unfold Pair_def)
+apply (blast dest!: doubleton_in_Vfrom_D Vfrom_doubleton_D)
+done
+
+lemma product_Int_Vfrom_subset:
+ "Transset(X) ==>
+ (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))"
+by (blast dest!: Pair_in_Vfrom_D)
+
+
+ML
+{*
- univ_def "univ(A) == Vfrom(A,nat)"
+val Vfrom = thm "Vfrom";
+val Vfrom_mono = thm "Vfrom_mono";
+val Vfrom_rank_subset1 = thm "Vfrom_rank_subset1";
+val Vfrom_rank_subset2 = thm "Vfrom_rank_subset2";
+val Vfrom_rank_eq = thm "Vfrom_rank_eq";
+val zero_in_Vfrom = thm "zero_in_Vfrom";
+val i_subset_Vfrom = thm "i_subset_Vfrom";
+val A_subset_Vfrom = thm "A_subset_Vfrom";
+val subset_mem_Vfrom = thm "subset_mem_Vfrom";
+val singleton_in_Vfrom = thm "singleton_in_Vfrom";
+val doubleton_in_Vfrom = thm "doubleton_in_Vfrom";
+val Pair_in_Vfrom = thm "Pair_in_Vfrom";
+val succ_in_Vfrom = thm "succ_in_Vfrom";
+val Vfrom_0 = thm "Vfrom_0";
+val Vfrom_succ_lemma = thm "Vfrom_succ_lemma";
+val Vfrom_succ = thm "Vfrom_succ";
+val Vfrom_Union = thm "Vfrom_Union";
+val Limit_Vfrom_eq = thm "Limit_Vfrom_eq";
+val Limit_VfromI = thm "Limit_VfromI";
+val Limit_VfromE = thm "Limit_VfromE";
+val zero_in_VLimit = thm "zero_in_VLimit";
+val singleton_in_VLimit = thm "singleton_in_VLimit";
+val Vfrom_UnI1 = thm "Vfrom_UnI1";
+val Vfrom_UnI2 = thm "Vfrom_UnI2";
+val doubleton_in_VLimit = thm "doubleton_in_VLimit";
+val Pair_in_VLimit = thm "Pair_in_VLimit";
+val product_VLimit = thm "product_VLimit";
+val Sigma_subset_VLimit = thm "Sigma_subset_VLimit";
+val nat_subset_VLimit = thm "nat_subset_VLimit";
+val nat_into_VLimit = thm "nat_into_VLimit";
+val zero_in_VLimit = thm "zero_in_VLimit";
+val one_in_VLimit = thm "one_in_VLimit";
+val Inl_in_VLimit = thm "Inl_in_VLimit";
+val Inr_in_VLimit = thm "Inr_in_VLimit";
+val sum_VLimit = thm "sum_VLimit";
+val sum_subset_VLimit = thm "sum_subset_VLimit";
+val Transset_Vfrom = thm "Transset_Vfrom";
+val Transset_Vfrom_succ = thm "Transset_Vfrom_succ";
+val Transset_Pair_subset = thm "Transset_Pair_subset";
+val Transset_Pair_subset_VLimit = thm "Transset_Pair_subset_VLimit";
+val Union_in_Vfrom = thm "Union_in_Vfrom";
+val Union_in_VLimit = thm "Union_in_VLimit";
+val in_VLimit = thm "in_VLimit";
+val prod_in_Vfrom = thm "prod_in_Vfrom";
+val prod_in_VLimit = thm "prod_in_VLimit";
+val sum_in_Vfrom = thm "sum_in_Vfrom";
+val sum_in_VLimit = thm "sum_in_VLimit";
+val fun_in_Vfrom = thm "fun_in_Vfrom";
+val fun_in_VLimit = thm "fun_in_VLimit";
+val Pow_in_Vfrom = thm "Pow_in_Vfrom";
+val Pow_in_VLimit = thm "Pow_in_VLimit";
+val Vset = thm "Vset";
+val Vset_succ = thm "Vset_succ";
+val Transset_Vset = thm "Transset_Vset";
+val VsetD = thm "VsetD";
+val VsetI_lemma = thm "VsetI_lemma";
+val VsetI = thm "VsetI";
+val Vset_Ord_rank_iff = thm "Vset_Ord_rank_iff";
+val Vset_rank_iff = thm "Vset_rank_iff";
+val rank_Vset = thm "rank_Vset";
+val arg_subset_Vset_rank = thm "arg_subset_Vset_rank";
+val Int_Vset_subset = thm "Int_Vset_subset";
+val rank_Inl = thm "rank_Inl";
+val rank_Inr = thm "rank_Inr";
+val Vrec = thm "Vrec";
+val def_Vrec = thm "def_Vrec";
+val Vrecursor = thm "Vrecursor";
+val def_Vrecursor = thm "def_Vrecursor";
+val univ_mono = thm "univ_mono";
+val Transset_univ = thm "Transset_univ";
+val univ_eq_UN = thm "univ_eq_UN";
+val subset_univ_eq_Int = thm "subset_univ_eq_Int";
+val univ_Int_Vfrom_subset = thm "univ_Int_Vfrom_subset";
+val univ_Int_Vfrom_eq = thm "univ_Int_Vfrom_eq";
+val zero_in_univ = thm "zero_in_univ";
+val A_subset_univ = thm "A_subset_univ";
+val A_into_univ = thm "A_into_univ";
+val singleton_in_univ = thm "singleton_in_univ";
+val doubleton_in_univ = thm "doubleton_in_univ";
+val Pair_in_univ = thm "Pair_in_univ";
+val Union_in_univ = thm "Union_in_univ";
+val product_univ = thm "product_univ";
+val nat_subset_univ = thm "nat_subset_univ";
+val nat_into_univ = thm "nat_into_univ";
+val one_in_univ = thm "one_in_univ";
+val two_in_univ = thm "two_in_univ";
+val bool_subset_univ = thm "bool_subset_univ";
+val bool_into_univ = thm "bool_into_univ";
+val Inl_in_univ = thm "Inl_in_univ";
+val Inr_in_univ = thm "Inr_in_univ";
+val sum_univ = thm "sum_univ";
+val sum_subset_univ = thm "sum_subset_univ";
+val Fin_Vfrom_lemma = thm "Fin_Vfrom_lemma";
+val Fin_VLimit = thm "Fin_VLimit";
+val Fin_subset_VLimit = thm "Fin_subset_VLimit";
+val Fin_univ = thm "Fin_univ";
+val nat_fun_VLimit = thm "nat_fun_VLimit";
+val nat_fun_subset_VLimit = thm "nat_fun_subset_VLimit";
+val nat_fun_univ = thm "nat_fun_univ";
+val FiniteFun_VLimit1 = thm "FiniteFun_VLimit1";
+val FiniteFun_univ1 = thm "FiniteFun_univ1";
+val FiniteFun_VLimit = thm "FiniteFun_VLimit";
+val FiniteFun_univ = thm "FiniteFun_univ";
+val FiniteFun_in_univ = thm "FiniteFun_in_univ";
+val FiniteFun_in_univ' = thm "FiniteFun_in_univ'";
+val doubleton_in_Vfrom_D = thm "doubleton_in_Vfrom_D";
+val Vfrom_doubleton_D = thm "Vfrom_doubleton_D";
+val Pair_in_Vfrom_D = thm "Pair_in_Vfrom_D";
+val product_Int_Vfrom_subset = thm "product_Int_Vfrom_subset";
+
+val rank_rls = thms "rank_rls";
+val rank_ss = simpset() addsimps [VsetI]
+ addsimps rank_rls @ (rank_rls RLN (2, [lt_trans]));
+
+*}
end
--- a/src/ZF/func.ML Fri May 17 16:54:25 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,479 +0,0 @@
-(* Title: ZF/func
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Functions in Zermelo-Fraenkel Set Theory
-*)
-
-(*** The Pi operator -- dependent function space ***)
-
-Goalw [Pi_def]
- "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)";
-by (Blast_tac 1);
-qed "Pi_iff";
-
-(*For upward compatibility with the former definition*)
-Goalw [Pi_def, function_def]
- "f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)";
-by (Blast_tac 1);
-qed "Pi_iff_old";
-
-Goal "f: Pi(A,B) ==> function(f)";
-by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
-qed "fun_is_function";
-
-(*Functions are relations*)
-Goalw [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";
-by (Blast_tac 1);
-qed "fun_is_rel";
-
-val prems = Goalw [Pi_def]
- "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')";
-by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1);
-qed "Pi_cong";
-
-(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
- flex-flex pairs and the "Check your prover" error. Most
- Sigmas and Pis are abbreviated as * or -> *)
-
-(*Weakening one function type to another; see also Pi_type*)
-Goalw [Pi_def] "[| f: A->B; B<=D |] ==> f: A->D";
-by (Best_tac 1);
-qed "fun_weaken_type";
-
-(*** Function Application ***)
-
-Goalw [Pi_def, function_def] "[| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c";
-by (Blast_tac 1);
-qed "apply_equality2";
-
-Goalw [apply_def, function_def] "[| <a,b>: f; function(f) |] ==> f`a = b";
-by (Blast_tac 1);
-qed "function_apply_equality";
-
-Goalw [Pi_def] "[| <a,b>: f; f: Pi(A,B) |] ==> f`a = b";
-by (blast_tac (claset() addIs [function_apply_equality]) 1);
-qed "apply_equality";
-
-(*Applying a function outside its domain yields 0*)
-Goalw [apply_def] "a ~: domain(f) ==> f`a = 0";
-by (rtac the_0 1);
-by (Blast_tac 1);
-qed "apply_0";
-
-Goal "[| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>";
-by (ftac fun_is_rel 1);
-by (blast_tac (claset() addDs [apply_equality]) 1);
-qed "Pi_memberD";
-
-Goal "[| function(f); a : domain(f)|] ==> <a,f`a>: f";
-by (asm_full_simp_tac (simpset() addsimps [function_def, apply_def]) 1);
-by (rtac theI2 1);
-by Auto_tac;
-qed "function_apply_Pair";
-
-Goal "[| f: Pi(A,B); a:A |] ==> <a,f`a>: f";
-by (asm_full_simp_tac (simpset() addsimps [Pi_iff]) 1);
-by (blast_tac (claset() addIs [function_apply_Pair]) 1);
-qed "apply_Pair";
-
-(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
-Goal "[| f: Pi(A,B); a:A |] ==> f`a : B(a)";
-by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1);
-by (REPEAT (ares_tac [apply_Pair] 1));
-qed "apply_type";
-AddTCs [apply_type];
-
-(*This version is acceptable to the simplifier*)
-Goal "[| f: A->B; a:A |] ==> f`a : B";
-by (REPEAT (ares_tac [apply_type] 1));
-qed "apply_funtype";
-
-Goal "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
-by (ftac fun_is_rel 1);
-by (blast_tac (claset() addSIs [apply_Pair, apply_equality]) 1);
-qed "apply_iff";
-
-(*Refining one Pi type to another*)
-val pi_prem::prems = Goal
- "[| f: Pi(A,C); !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)";
-by (cut_facts_tac [pi_prem] 1);
-by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
-by (blast_tac (claset() addIs prems addSDs [pi_prem RS Pi_memberD]) 1);
-qed "Pi_type";
-
-(*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*)
-Goal "(f : Pi(A, %x. {y:B(x). P(x,y)})) \
-\ <-> f : Pi(A,B) & (ALL x: A. P(x, f`x))";
-by (blast_tac (claset() addIs [Pi_type] addDs [apply_type]) 1);
-qed "Pi_Collect_iff";
-
-val [major,minor] = Goal
- "[| f : Pi(A,B); !!x. x:A ==> B(x)<=C(x) |] ==> f : Pi(A,C)";
-by (fast_tac (claset() addSIs [major RS Pi_type, minor RS subsetD,
- major RS apply_type]) 1);
-qed "Pi_weaken_type";
-
-
-(** Elimination of membership in a function **)
-
-Goal "[| <a,b> : f; f: Pi(A,B) |] ==> a : A";
-by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1));
-qed "domain_type";
-
-Goal "[| <a,b> : f; f: Pi(A,B) |] ==> b : B(a)";
-by (etac (fun_is_rel RS subsetD RS SigmaD2) 1);
-by (assume_tac 1);
-qed "range_type";
-
-Goal "[| <a,b>: f; f: Pi(A,B) |] ==> a:A & b:B(a) & f`a = b";
-by (blast_tac (claset() addIs [domain_type, range_type, apply_equality]) 1);
-qed "Pair_mem_PiD";
-
-(*** Lambda Abstraction ***)
-
-Goalw [lam_def] "a:A ==> <a,b(a)> : (lam x:A. b(x))";
-by (etac RepFunI 1);
-qed "lamI";
-
-val major::prems = Goalw [lam_def]
- "[| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P \
-\ |] ==> P";
-by (rtac (major RS RepFunE) 1);
-by (REPEAT (ares_tac prems 1));
-qed "lamE";
-
-Goal "[| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";
-by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1));
-qed "lamD";
-
-val prems = Goalw [lam_def, Pi_def, function_def]
- "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)";
-by (blast_tac (claset() addIs prems) 1);
-qed "lam_type";
-AddTCs [lam_type];
-
-Goal "(lam x:A. b(x)) : A -> {b(x). x:A}";
-by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
-qed "lam_funtype";
-
-Goal "a : A ==> (lam x:A. b(x)) ` a = b(a)";
-by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1));
-qed "beta";
-
-Goalw [lam_def] "(lam x:0. b(x)) = 0";
-by (Simp_tac 1);
-qed "lam_empty";
-
-Goalw [lam_def] "domain(Lambda(A,b)) = A";
-by (Blast_tac 1);
-qed "domain_lam";
-
-Addsimps [beta, lam_empty, domain_lam];
-
-(*congruence rule for lambda abstraction*)
-val prems = Goalw [lam_def]
- "[| A=A'; !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')";
-by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1);
-qed "lam_cong";
-
-Addcongs [lam_cong];
-
-val [major] = Goal
- "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)";
-by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1);
-by (rtac ballI 1);
-by (stac beta 1);
-by (assume_tac 1);
-by (etac (major RS theI) 1);
-qed "lam_theI";
-
-Goal "[| (lam x:A. f(x)) = (lam x:A. g(x)); a:A |] ==> f(a)=g(a)";
-by (fast_tac (claset() addSIs [lamI] addEs [equalityE, lamE]) 1);
-qed "lam_eqE";
-
-
-(*Empty function spaces*)
-Goalw [Pi_def, function_def] "Pi(0,A) = {0}";
-by (Blast_tac 1);
-qed "Pi_empty1";
-Addsimps [Pi_empty1];
-
-(*The singleton function*)
-Goalw [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
-by (Blast_tac 1);
-qed "singleton_fun";
-Addsimps [singleton_fun];
-
-Goalw [Pi_def, function_def] "(A->0) = (if A=0 then {0} else 0)";
-by (Force_tac 1);
-qed "Pi_empty2";
-Addsimps [Pi_empty2];
-
-Goal "(A->X)=0 \\<longleftrightarrow> X=0 & (A \\<noteq> 0)";
-by Auto_tac;
-by (fast_tac (claset() addSIs [equals0I] addIs [lam_type]) 1);
-qed "fun_space_empty_iff";
-AddIffs [fun_space_empty_iff];
-
-
-(** Extensionality **)
-
-(*Semi-extensionality!*)
-val prems = Goal
- "[| f : Pi(A,B); g: Pi(C,D); A<=C; \
-\ !!x. x:A ==> f`x = g`x |] ==> f<=g";
-by (rtac subsetI 1);
-by (eresolve_tac (prems RL [Pi_memberD RS bexE]) 1);
-by (etac ssubst 1);
-by (resolve_tac (prems RL [ssubst]) 1);
-by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1));
-qed "fun_subset";
-
-val prems = Goal
- "[| f : Pi(A,B); g: Pi(A,D); \
-\ !!x. x:A ==> f`x = g`x |] ==> f=g";
-by (REPEAT (ares_tac (prems @ (prems RL [sym]) @
- [subset_refl,equalityI,fun_subset]) 1));
-qed "fun_extension";
-
-Goal "f : Pi(A,B) ==> (lam x:A. f`x) = f";
-by (rtac fun_extension 1);
-by (REPEAT (ares_tac [lam_type,apply_type,beta] 1));
-qed "eta";
-
-Addsimps [eta];
-
-Goal "[| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g";
-by (blast_tac (claset() addIs [fun_extension]) 1);
-qed "fun_extension_iff";
-
-(*thanks to Mark Staples*)
-Goal "[| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)";
-by (rtac iffI 1);
-by (asm_full_simp_tac ZF_ss 2);
-by (rtac fun_extension 1);
-by (REPEAT (atac 1));
-by (dtac (apply_Pair RSN (2,subsetD)) 1);
-by (REPEAT (atac 1));
-by (rtac (apply_equality RS sym) 1);
-by (REPEAT (atac 1)) ;
-qed "fun_subset_eq";
-
-
-(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
-val prems = Goal
- "[| f: Pi(A,B); \
-\ !!b. [| ALL x:A. b(x):B(x); f = (lam x:A. b(x)) |] ==> P \
-\ |] ==> P";
-by (resolve_tac prems 1);
-by (rtac (eta RS sym) 2);
-by (REPEAT (ares_tac (prems@[ballI,apply_type]) 1));
-qed "Pi_lamE";
-
-
-(** Images of functions **)
-
-Goalw [lam_def] "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}";
-by (Blast_tac 1);
-qed "image_lam";
-
-Goal "[| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}";
-by (etac (eta RS subst) 1);
-by (asm_full_simp_tac (simpset() addsimps [image_lam, subset_iff]) 1);
-qed "image_fun";
-
-Goal "[| f: Pi(A,B); x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)";
-by (blast_tac (claset() addDs [apply_equality, apply_Pair]) 1);
-qed "Pi_image_cons";
-
-
-(*** properties of "restrict" ***)
-
-Goalw [restrict_def]
- "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) <= f";
-by (blast_tac (claset() addIs [apply_Pair]) 1);
-qed "restrict_subset";
-
-Goalw [restrict_def, function_def]
- "function(f) ==> function(restrict(f,A))";
-by (Blast_tac 1);
-qed "function_restrictI";
-
-Goal "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) : Pi(A,B)";
-by (asm_full_simp_tac
- (simpset() addsimps [Pi_iff, function_def, restrict_def]) 1);
-by (Blast_tac 1);
-qed "restrict_type2";
-
-(*Fails with the new definition of restrict
- "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)";
-qed "restrict_type";
-*)
-
-(*FIXME: move to FOL?*)
-Goal "EX x. a = x";
-by Auto_tac;
-qed "ex_equals_triv";
-
-Goal "a : A ==> restrict(f,A) ` a = f`a";
-by (asm_full_simp_tac
- (simpset() addsimps [apply_def, restrict_def, ex_equals_triv]) 1);
-qed "restrict";
-
-Goalw [restrict_def] "restrict(f,0) = 0";
-by (Simp_tac 1);
-qed "restrict_empty";
-Addsimps [restrict_empty];
-
-Goalw [restrict_def, lam_def] "domain(restrict(Lambda(A,f),C)) = A Int C";
-by (rtac equalityI 1);
-by (auto_tac (claset(), simpset() addsimps [domain_iff]));
-qed "domain_restrict_lam";
-Addsimps [domain_restrict_lam];
-
-Goalw [restrict_def] "restrict(restrict(r,A),B) = restrict(r, A Int B)";
-by (Blast_tac 1);
-qed "restrict_restrict";
-Addsimps [restrict_restrict];
-
-Goalw [restrict_def] "domain(restrict(f,C)) = domain(f) Int C";
-by (auto_tac (claset(), simpset() addsimps [domain_def]));
-qed "domain_restrict";
-Addsimps [domain_restrict];
-
-Goal "f <= Sigma(A,B) ==> restrict(f,A) = f";
-by (asm_full_simp_tac (simpset() addsimps [restrict_def]) 1);
-by (Blast_tac 1);
-qed "restrict_idem";
-Addsimps [restrict_idem];
-
-Goal "restrict(f,A) ` a = (if a : A then f`a else 0)";
-by (asm_full_simp_tac (simpset() addsimps [restrict, apply_0]) 1);
-qed "restrict_if";
-Addsimps [restrict_if];
-
-(*No longer true and no longer needed
-val prems = Goalw [restrict_def]
- "[| A=B; !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)";
-qed "restrict_eqI";
-*)
-
-Goalw [restrict_def, lam_def]
- "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
-by Auto_tac;
-qed "restrict_lam_eq";
-
-Goal "f : cons(a, b) -> B ==> f = cons(<a, f ` a>, restrict(f, b))";
-by (rtac equalityI 1);
-by (blast_tac (claset() addIs [apply_Pair, impOfSubs restrict_subset]) 2);
-by (auto_tac (claset() addSDs [Pi_memberD],
- simpset() addsimps [restrict_def, lam_def]));
-qed "fun_cons_restrict_eq";
-
-
-(*** Unions of functions ***)
-
-(** The Union of a set of COMPATIBLE functions is a function **)
-
-Goalw [function_def]
- "[| ALL x:S. function(x); \
-\ ALL x:S. ALL y:S. x<=y | y<=x |] ==> \
-\ function(Union(S))";
-by (fast_tac (ZF_cs addSDs [bspec RS bspec]) 1);
- (*by (Blast_tac 1); takes too long...*)
-qed "function_Union";
-
-Goalw [Pi_def]
- "[| ALL f:S. EX C D. f:C->D; \
-\ ALL f:S. ALL y:S. f<=y | y<=f |] ==> \
-\ Union(S) : domain(Union(S)) -> range(Union(S))";
-by (blast_tac (subset_cs addSIs [rel_Union, function_Union]) 1);
-qed "fun_Union";
-
-
-(** The Union of 2 disjoint functions is a function **)
-
-bind_thms ("Un_rls", [Un_subset_iff, SUM_Un_distrib1, prod_Un_distrib2,
- Un_upper1 RSN (2, subset_trans),
- Un_upper2 RSN (2, subset_trans)]);
-
-Goal "[| f: A->B; g: C->D; A Int C = 0 |] \
-\ ==> (f Un g) : (A Un C) -> (B Un D)";
-(*Prove the product and domain subgoals using distributive laws*)
-by (asm_full_simp_tac (simpset() addsimps [Pi_iff,extension]@Un_rls) 1);
-by (rewtac function_def);
-by (Blast_tac 1);
-qed "fun_disjoint_Un";
-
-Goal "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \
-\ (f Un g)`a = f`a";
-by (rtac (apply_Pair RS UnI1 RS apply_equality) 1);
-by (REPEAT (ares_tac [fun_disjoint_Un] 1));
-qed "fun_disjoint_apply1";
-
-Goal "[| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> \
-\ (f Un g)`c = g`c";
-by (rtac (apply_Pair RS UnI2 RS apply_equality) 1);
-by (REPEAT (ares_tac [fun_disjoint_Un] 1));
-qed "fun_disjoint_apply2";
-
-(** Domain and range of a function/relation **)
-
-Goalw [Pi_def] "f : Pi(A,B) ==> domain(f)=A";
-by (Blast_tac 1);
-qed "domain_of_fun";
-
-Goal "[| f : Pi(A,B); a: A |] ==> f`a : range(f)";
-by (etac (apply_Pair RS rangeI) 1);
-by (assume_tac 1);
-qed "apply_rangeI";
-
-Goal "f : Pi(A,B) ==> f : A->range(f)";
-by (REPEAT (ares_tac [Pi_type, apply_rangeI] 1));
-qed "range_of_fun";
-
-(*** Extensions of functions ***)
-
-Goal "[| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
-by (forward_tac [singleton_fun RS fun_disjoint_Un] 1);
-by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2);
-by (Blast_tac 1);
-qed "fun_extend";
-
-Goal "[| f: A->B; c~:A; b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B";
-by (blast_tac (claset() addIs [fun_extend RS fun_weaken_type]) 1);
-qed "fun_extend3";
-
-Goal "[| f: A->B; a:A; c~:A |] ==> cons(<c,b>,f)`a = f`a";
-by (rtac (apply_Pair RS consI2 RS apply_equality) 1);
-by (rtac fun_extend 3);
-by (REPEAT (assume_tac 1));
-qed "fun_extend_apply1";
-
-Goal "[| f: A->B; c~:A |] ==> cons(<c,b>,f)`c = b";
-by (rtac (consI1 RS apply_equality) 1);
-by (rtac fun_extend 1);
-by (REPEAT (assume_tac 1));
-qed "fun_extend_apply2";
-
-bind_thm ("singleton_apply", [singletonI, singleton_fun] MRS apply_equality);
-Addsimps [singleton_apply];
-
-(*For Finite.ML. Inclusion of right into left is easy*)
-Goal "c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})";
-by (rtac equalityI 1);
-by (safe_tac (claset() addSEs [fun_extend3]));
-(*Inclusion of left into right*)
-by (subgoal_tac "restrict(x, A) : A -> B" 1);
-by (blast_tac (claset() addIs [restrict_type2]) 2);
-by (rtac UN_I 1 THEN assume_tac 1);
-by (rtac (apply_funtype RS UN_I) 1 THEN REPEAT (ares_tac [consI1] 1));
-by (Simp_tac 1);
-by (rtac fun_extension 1 THEN REPEAT (ares_tac [fun_extend] 1));
-by (etac consE 1);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps [restrict, fun_extend_apply1,
- fun_extend_apply2])));
-qed "cons_fun_eq";
--- a/src/ZF/func.thy Fri May 17 16:54:25 2002 +0200
+++ b/src/ZF/func.thy Sat May 18 20:08:17 2002 +0200
@@ -1,3 +1,470 @@
-(*Dummy theory to document dependencies *)
+(* Title: ZF/func.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1991 University of Cambridge
+
+Functions in Zermelo-Fraenkel Set Theory
+*)
+
+theory func = domrange + equalities:
+
+(*** The Pi operator -- dependent function space ***)
+
+lemma Pi_iff:
+ "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)"
+by (unfold Pi_def, blast)
+
+(*For upward compatibility with the former definition*)
+lemma Pi_iff_old:
+ "f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)"
+by (unfold Pi_def function_def, blast)
+
+lemma fun_is_function: "f: Pi(A,B) ==> function(f)"
+by (simp only: Pi_iff)
+
+(*Functions are relations*)
+lemma fun_is_rel: "f: Pi(A,B) ==> f <= Sigma(A,B)"
+by (unfold Pi_def, blast)
+
+lemma Pi_cong:
+ "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')"
+by (simp add: Pi_def cong add: Sigma_cong)
+
+(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
+ flex-flex pairs and the "Check your prover" error. Most
+ Sigmas and Pis are abbreviated as * or -> *)
+
+(*Weakening one function type to another; see also Pi_type*)
+lemma fun_weaken_type: "[| f: A->B; B<=D |] ==> f: A->D"
+by (unfold Pi_def, best)
+
+(*** Function Application ***)
+
+lemma apply_equality2: "[| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c"
+by (unfold Pi_def function_def, blast)
+
+lemma function_apply_equality: "[| <a,b>: f; function(f) |] ==> f`a = b"
+by (unfold apply_def function_def, blast)
+
+lemma apply_equality: "[| <a,b>: f; f: Pi(A,B) |] ==> f`a = b"
+apply (unfold Pi_def)
+apply (blast intro: function_apply_equality)
+done
+
+(*Applying a function outside its domain yields 0*)
+lemma apply_0: "a ~: domain(f) ==> f`a = 0"
+apply (unfold apply_def)
+apply (rule the_0, blast)
+done
+
+lemma Pi_memberD: "[| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>"
+apply (frule fun_is_rel)
+apply (blast dest: apply_equality)
+done
+
+lemma function_apply_Pair: "[| function(f); a : domain(f)|] ==> <a,f`a>: f"
+apply (simp add: function_def apply_def)
+apply (rule theI2, auto)
+done
+
+lemma apply_Pair: "[| f: Pi(A,B); a:A |] ==> <a,f`a>: f"
+apply (simp add: Pi_iff)
+apply (blast intro: function_apply_Pair)
+done
+
+(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
+lemma apply_type [TC]: "[| f: Pi(A,B); a:A |] ==> f`a : B(a)"
+by (blast intro: apply_Pair dest: fun_is_rel)
+
+(*This version is acceptable to the simplifier*)
+lemma apply_funtype: "[| f: A->B; a:A |] ==> f`a : B"
+by (blast dest: apply_type)
+
+lemma apply_iff: "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b"
+apply (frule fun_is_rel)
+apply (blast intro!: apply_Pair apply_equality)
+done
+
+(*Refining one Pi type to another*)
+lemma Pi_type: "[| f: Pi(A,C); !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)"
+apply (simp only: Pi_iff)
+apply (blast dest: function_apply_equality)
+done
+
+(*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*)
+lemma Pi_Collect_iff:
+ "(f : Pi(A, %x. {y:B(x). P(x,y)}))
+ <-> f : Pi(A,B) & (ALL x: A. P(x, f`x))"
+by (blast intro: Pi_type dest: apply_type)
+
+lemma Pi_weaken_type:
+ "[| f : Pi(A,B); !!x. x:A ==> B(x)<=C(x) |] ==> f : Pi(A,C)"
+by (blast intro: Pi_type dest: apply_type)
+
+
+(** Elimination of membership in a function **)
+
+lemma domain_type: "[| <a,b> : f; f: Pi(A,B) |] ==> a : A"
+by (blast dest: fun_is_rel)
+
+lemma range_type: "[| <a,b> : f; f: Pi(A,B) |] ==> b : B(a)"
+by (blast dest: fun_is_rel)
+
+lemma Pair_mem_PiD: "[| <a,b>: f; f: Pi(A,B) |] ==> a:A & b:B(a) & f`a = b"
+by (blast intro: domain_type range_type apply_equality)
+
+(*** Lambda Abstraction ***)
+
+lemma lamI: "a:A ==> <a,b(a)> : (lam x:A. b(x))"
+apply (unfold lam_def)
+apply (erule RepFunI)
+done
+
+lemma lamE:
+ "[| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P
+ |] ==> P"
+by (simp add: lam_def, blast)
+
+lemma lamD: "[| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)"
+by (simp add: lam_def)
+
+lemma lam_type [TC]:
+ "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)"
+by (simp add: lam_def Pi_def function_def, blast)
+
+lemma lam_funtype: "(lam x:A. b(x)) : A -> {b(x). x:A}"
+by (blast intro: lam_type);
+
+lemma beta [simp]: "a : A ==> (lam x:A. b(x)) ` a = b(a)"
+by (blast intro: apply_equality lam_funtype lamI)
+
+lemma lam_empty [simp]: "(lam x:0. b(x)) = 0"
+by (simp add: lam_def)
+
+lemma domain_lam [simp]: "domain(Lambda(A,b)) = A"
+by (simp add: lam_def, blast)
+
+(*congruence rule for lambda abstraction*)
+lemma lam_cong [cong]:
+ "[| A=A'; !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')"
+by (simp only: lam_def cong add: RepFun_cong)
+
+lemma lam_theI:
+ "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)"
+apply (rule_tac x = "lam x: A. THE y. Q (x,y) " in exI)
+apply (rule ballI)
+apply (subst beta, assumption)
+apply (blast intro: theI)
+done
+
+lemma lam_eqE: "[| (lam x:A. f(x)) = (lam x:A. g(x)); a:A |] ==> f(a)=g(a)"
+by (fast intro!: lamI elim: equalityE lamE)
+
+
+(*Empty function spaces*)
+lemma Pi_empty1 [simp]: "Pi(0,A) = {0}"
+by (unfold Pi_def function_def, blast)
+
+(*The singleton function*)
+lemma singleton_fun [simp]: "{<a,b>} : {a} -> {b}"
+by (unfold Pi_def function_def, blast)
+
+lemma Pi_empty2 [simp]: "(A->0) = (if A=0 then {0} else 0)"
+by (unfold Pi_def function_def, force)
+
+lemma fun_space_empty_iff [iff]: "(A->X)=0 \<longleftrightarrow> X=0 & (A \<noteq> 0)"
+apply auto
+apply (fast intro!: equals0I intro: lam_type)
+done
+
+
+(** Extensionality **)
+
+(*Semi-extensionality!*)
+
+lemma fun_subset:
+ "[| f : Pi(A,B); g: Pi(C,D); A<=C;
+ !!x. x:A ==> f`x = g`x |] ==> f<=g"
+by (force dest: Pi_memberD intro: apply_Pair)
+
+lemma fun_extension:
+ "[| f : Pi(A,B); g: Pi(A,D);
+ !!x. x:A ==> f`x = g`x |] ==> f=g"
+by (blast del: subsetI intro: subset_refl sym fun_subset)
+
+lemma eta [simp]: "f : Pi(A,B) ==> (lam x:A. f`x) = f"
+apply (rule fun_extension)
+apply (auto simp add: lam_type apply_type beta)
+done
+
+lemma fun_extension_iff:
+ "[| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g"
+by (blast intro: fun_extension)
+
+(*thm by Mark Staples, proof by lcp*)
+lemma fun_subset_eq: "[| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)"
+by (blast dest: apply_Pair
+ intro: fun_extension apply_equality [symmetric])
+
+
+(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
+lemma Pi_lamE:
+ assumes major: "f: Pi(A,B)"
+ and minor: "!!b. [| ALL x:A. b(x):B(x); f = (lam x:A. b(x)) |] ==> P"
+ shows "P"
+apply (rule minor)
+apply (rule_tac [2] eta [symmetric])
+apply (blast intro: major apply_type)+
+done
+
+
+(** Images of functions **)
+
+lemma image_lam: "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}"
+by (unfold lam_def, blast)
+
+lemma image_fun: "[| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}"
+apply (erule eta [THEN subst])
+apply (simp add: image_lam subset_iff)
+done
+
+lemma Pi_image_cons:
+ "[| f: Pi(A,B); x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)"
+by (blast dest: apply_equality apply_Pair)
+
-func = domrange + equalities
+(*** properties of "restrict" ***)
+
+lemma restrict_subset:
+ "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) <= f"
+apply (unfold restrict_def)
+apply (blast intro: apply_Pair)
+done
+
+lemma function_restrictI:
+ "function(f) ==> function(restrict(f,A))"
+by (unfold restrict_def function_def, blast)
+
+lemma restrict_type2: "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) : Pi(A,B)"
+by (simp add: Pi_iff function_def restrict_def, blast)
+
+lemma restrict: "a : A ==> restrict(f,A) ` a = f`a"
+by (simp add: apply_def restrict_def)
+
+lemma restrict_empty [simp]: "restrict(f,0) = 0"
+apply (unfold restrict_def)
+apply (simp (no_asm))
+done
+
+lemma domain_restrict_lam [simp]: "domain(restrict(Lambda(A,f),C)) = A Int C"
+apply (unfold restrict_def lam_def)
+apply (rule equalityI)
+apply (auto simp add: domain_iff)
+done
+
+lemma restrict_restrict [simp]:
+ "restrict(restrict(r,A),B) = restrict(r, A Int B)"
+by (unfold restrict_def, blast)
+
+lemma domain_restrict [simp]: "domain(restrict(f,C)) = domain(f) Int C"
+apply (unfold restrict_def)
+apply (auto simp add: domain_def)
+done
+
+lemma restrict_idem [simp]: "f <= Sigma(A,B) ==> restrict(f,A) = f"
+by (simp add: restrict_def, blast)
+
+lemma restrict_if [simp]: "restrict(f,A) ` a = (if a : A then f`a else 0)"
+by (simp add: restrict apply_0)
+
+lemma restrict_lam_eq:
+ "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))"
+by (unfold restrict_def lam_def, auto)
+
+lemma fun_cons_restrict_eq:
+ "f : cons(a, b) -> B ==> f = cons(<a, f ` a>, restrict(f, b))"
+apply (rule equalityI)
+prefer 2 apply (blast intro: apply_Pair restrict_subset [THEN subsetD])
+apply (auto dest!: Pi_memberD simp add: restrict_def lam_def)
+done
+
+
+(*** Unions of functions ***)
+
+(** The Union of a set of COMPATIBLE functions is a function **)
+
+lemma function_Union:
+ "[| ALL x:S. function(x);
+ ALL x:S. ALL y:S. x<=y | y<=x |]
+ ==> function(Union(S))"
+by (unfold function_def, blast)
+
+lemma fun_Union:
+ "[| ALL f:S. EX C D. f:C->D;
+ ALL f:S. ALL y:S. f<=y | y<=f |] ==>
+ Union(S) : domain(Union(S)) -> range(Union(S))"
+apply (unfold Pi_def)
+apply (blast intro!: rel_Union function_Union)
+done
+
+
+(** The Union of 2 disjoint functions is a function **)
+
+lemmas Un_rls = Un_subset_iff SUM_Un_distrib1 prod_Un_distrib2
+ subset_trans [OF _ Un_upper1]
+ subset_trans [OF _ Un_upper2]
+
+lemma fun_disjoint_Un:
+ "[| f: A->B; g: C->D; A Int C = 0 |]
+ ==> (f Un g) : (A Un C) -> (B Un D)"
+(*Prove the product and domain subgoals using distributive laws*)
+apply (simp add: Pi_iff extension Un_rls)
+apply (unfold function_def, blast)
+done
+
+lemma fun_disjoint_apply1:
+ "[| a:A; f: A->B; g: C->D; A Int C = 0 |]
+ ==> (f Un g)`a = f`a"
+apply (rule apply_Pair [THEN UnI1, THEN apply_equality], assumption+)
+apply (blast intro: fun_disjoint_Un )
+done
+
+lemma fun_disjoint_apply2:
+ "[| c:C; f: A->B; g: C->D; A Int C = 0 |]
+ ==> (f Un g)`c = g`c"
+apply (rule apply_Pair [THEN UnI2, THEN apply_equality], assumption+)
+apply (blast intro: fun_disjoint_Un )
+done
+
+(** Domain and range of a function/relation **)
+
+lemma domain_of_fun: "f : Pi(A,B) ==> domain(f)=A"
+by (unfold Pi_def, blast)
+
+lemma apply_rangeI: "[| f : Pi(A,B); a: A |] ==> f`a : range(f)"
+by (erule apply_Pair [THEN rangeI], assumption)
+
+lemma range_of_fun: "f : Pi(A,B) ==> f : A->range(f)"
+by (blast intro: Pi_type apply_rangeI)
+
+(*** Extensions of functions ***)
+
+lemma fun_extend:
+ "[| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)"
+apply (frule singleton_fun [THEN fun_disjoint_Un], blast)
+apply (simp add: cons_eq)
+done
+
+lemma fun_extend3:
+ "[| f: A->B; c~:A; b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B"
+by (blast intro: fun_extend [THEN fun_weaken_type])
+
+lemma fun_extend_apply1: "[| f: A->B; a:A; c~:A |] ==> cons(<c,b>,f)`a = f`a"
+apply (rule apply_Pair [THEN consI2, THEN apply_equality])
+apply (rule_tac [3] fun_extend, assumption+)
+done
+
+lemma fun_extend_apply2: "[| f: A->B; c~:A |] ==> cons(<c,b>,f)`c = b"
+apply (rule consI1 [THEN apply_equality])
+apply (rule fun_extend, assumption+)
+done
+
+lemmas singleton_apply = apply_equality [OF singletonI singleton_fun, simp]
+
+(*For Finite.ML. Inclusion of right into left is easy*)
+lemma cons_fun_eq:
+ "c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})"
+apply (rule equalityI)
+apply (safe elim!: fun_extend3)
+(*Inclusion of left into right*)
+apply (subgoal_tac "restrict (x, A) : A -> B")
+ prefer 2 apply (blast intro: restrict_type2)
+apply (rule UN_I, assumption)
+apply (rule apply_funtype [THEN UN_I])
+ apply assumption
+ apply (rule consI1)
+apply (simp (no_asm))
+apply (rule fun_extension)
+ apply assumption
+ apply (blast intro: fun_extend)
+apply (erule consE)
+apply (simp_all add: restrict fun_extend_apply1 fun_extend_apply2)
+done
+
+ML
+{*
+val Pi_iff = thm "Pi_iff";
+val Pi_iff_old = thm "Pi_iff_old";
+val fun_is_function = thm "fun_is_function";
+val fun_is_rel = thm "fun_is_rel";
+val Pi_cong = thm "Pi_cong";
+val fun_weaken_type = thm "fun_weaken_type";
+val apply_equality2 = thm "apply_equality2";
+val function_apply_equality = thm "function_apply_equality";
+val apply_equality = thm "apply_equality";
+val apply_0 = thm "apply_0";
+val Pi_memberD = thm "Pi_memberD";
+val function_apply_Pair = thm "function_apply_Pair";
+val apply_Pair = thm "apply_Pair";
+val apply_type = thm "apply_type";
+val apply_funtype = thm "apply_funtype";
+val apply_iff = thm "apply_iff";
+val Pi_type = thm "Pi_type";
+val Pi_Collect_iff = thm "Pi_Collect_iff";
+val Pi_weaken_type = thm "Pi_weaken_type";
+val domain_type = thm "domain_type";
+val range_type = thm "range_type";
+val Pair_mem_PiD = thm "Pair_mem_PiD";
+val lamI = thm "lamI";
+val lamE = thm "lamE";
+val lamD = thm "lamD";
+val lam_type = thm "lam_type";
+val lam_funtype = thm "lam_funtype";
+val beta = thm "beta";
+val lam_empty = thm "lam_empty";
+val domain_lam = thm "domain_lam";
+val lam_cong = thm "lam_cong";
+val lam_theI = thm "lam_theI";
+val lam_eqE = thm "lam_eqE";
+val Pi_empty1 = thm "Pi_empty1";
+val singleton_fun = thm "singleton_fun";
+val Pi_empty2 = thm "Pi_empty2";
+val fun_space_empty_iff = thm "fun_space_empty_iff";
+val fun_subset = thm "fun_subset";
+val fun_extension = thm "fun_extension";
+val eta = thm "eta";
+val fun_extension_iff = thm "fun_extension_iff";
+val fun_subset_eq = thm "fun_subset_eq";
+val Pi_lamE = thm "Pi_lamE";
+val image_lam = thm "image_lam";
+val image_fun = thm "image_fun";
+val Pi_image_cons = thm "Pi_image_cons";
+val restrict_subset = thm "restrict_subset";
+val function_restrictI = thm "function_restrictI";
+val restrict_type2 = thm "restrict_type2";
+val restrict = thm "restrict";
+val restrict_empty = thm "restrict_empty";
+val domain_restrict_lam = thm "domain_restrict_lam";
+val restrict_restrict = thm "restrict_restrict";
+val domain_restrict = thm "domain_restrict";
+val restrict_idem = thm "restrict_idem";
+val restrict_if = thm "restrict_if";
+val restrict_lam_eq = thm "restrict_lam_eq";
+val fun_cons_restrict_eq = thm "fun_cons_restrict_eq";
+val function_Union = thm "function_Union";
+val fun_Union = thm "fun_Union";
+val fun_disjoint_Un = thm "fun_disjoint_Un";
+val fun_disjoint_apply1 = thm "fun_disjoint_apply1";
+val fun_disjoint_apply2 = thm "fun_disjoint_apply2";
+val domain_of_fun = thm "domain_of_fun";
+val apply_rangeI = thm "apply_rangeI";
+val range_of_fun = thm "range_of_fun";
+val fun_extend = thm "fun_extend";
+val fun_extend3 = thm "fun_extend3";
+val fun_extend_apply1 = thm "fun_extend_apply1";
+val fun_extend_apply2 = thm "fun_extend_apply2";
+val singleton_apply = thm "singleton_apply";
+val cons_fun_eq = thm "cons_fun_eq";
+*}
+
+end