# HG changeset patch # User paulson # Date 1021745297 -7200 # Node ID e320a52ff71121198c576afc98850a29f390f8eb # Parent 660a71e712afa7c83e0bd6d1aee69a2dd811e341 converted Arith, Univ, func to Isar format! diff -r 660a71e712af -r e320a52ff711 src/ZF/Arith.ML --- 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 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 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 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 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"; - diff -r 660a71e712af -r e320a52ff711 src/ZF/Arith.thy --- 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 ji - "raw_mod (m, n) == + raw_mod :: "[i,i]=>i" + "raw_mod (m, n) == transrec(m, %j f. if ji (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 "#\\" 70) + "mult" :: "[i,i] => i" (infixr "#\" 70) syntax (HTML output) - "mult" :: [i, i] => i (infixr "#\\" 70) + "mult" :: "[i, i] => i" (infixr "#\" 70) + + +declare rec_type [simp] + nat_0_le [simp] + + +lemma zero_lt_lemma: "[| 0 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 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 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 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 diff -r 660a71e712af -r e320a52ff711 src/ZF/Integ/IntDiv.ML --- 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 \\ 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"; diff -r 660a71e712af -r e320a52ff711 src/ZF/IsaMakefile --- 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 diff -r 660a71e712af -r e320a52ff711 src/ZF/OrderType.thy --- 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: "[| : 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*) diff -r 660a71e712af -r e320a52ff711 src/ZF/Univ.ML --- 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) |] ==> \ -\ : 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 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 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) |] ==> \ -\ : 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] "[| <= C; Transset(C) |] ==> a: C & b: C"; -by (Blast_tac 1); -qed "Transset_Pair_subset"; - -Goal "[| <= Vfrom(A,i); Transset(A); Limit(i) |] ==> \ -\ : 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 EX k. h(x,y): Vfrom(A,k) & k \ -\ 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) 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) |] ==> : 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 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 : Vfrom(X,i) - implies a, b : Vfrom(X,i), which is useless for induction. - Using only the stronger theorem would prove : 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] - "[| : 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"; - diff -r 660a71e712af -r e320a52ff711 src/ZF/Univ.thy --- 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) |] ==> : 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 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 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) |] ==> : 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: "[| <= C; Transset(C) |] ==> a: C & b: C" +by (unfold Pair_def Transset_def, blast) + +lemma Transset_Pair_subset_VLimit: + "[| <= Vfrom(A,i); Transset(A); Limit(i) |] + ==> : 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 EX k. h(x,y): Vfrom(A,k) & k 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) 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) |] ==> : 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 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 : Vfrom(X,i) + implies a, b : Vfrom(X,i), which is useless for induction. + Using only the stronger theorem would prove : 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: + "[| : 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 diff -r 660a71e712af -r e320a52ff711 src/ZF/func.ML --- 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. : 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] "[| : f; : f; f: Pi(A,B) |] ==> b=c"; -by (Blast_tac 1); -qed "apply_equality2"; - -Goalw [apply_def, function_def] "[| : f; function(f) |] ==> f`a = b"; -by (Blast_tac 1); -qed "function_apply_equality"; - -Goalw [Pi_def] "[| : 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 = "; -by (ftac fun_is_rel 1); -by (blast_tac (claset() addDs [apply_equality]) 1); -qed "Pi_memberD"; - -Goal "[| function(f); a : domain(f)|] ==> : 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 |] ==> : 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) ==> : 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 "[| : f; f: Pi(A,B) |] ==> a : A"; -by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1)); -qed "domain_type"; - -Goal "[| : 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 "[| : 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 ==> : (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= |] ==> P \ -\ |] ==> P"; -by (rtac (major RS RepFunE) 1); -by (REPEAT (ares_tac prems 1)); -qed "lamE"; - -Goal "[| : (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}"; -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 \\ X=0 & (A \\ 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(, 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(,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(,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(,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(,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(, 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"; diff -r 660a71e712af -r e320a52ff711 src/ZF/func.thy --- 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. : 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: "[| : f; : f; f: Pi(A,B) |] ==> b=c" +by (unfold Pi_def function_def, blast) + +lemma function_apply_equality: "[| : f; function(f) |] ==> f`a = b" +by (unfold apply_def function_def, blast) + +lemma apply_equality: "[| : 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 = " +apply (frule fun_is_rel) +apply (blast dest: apply_equality) +done + +lemma function_apply_Pair: "[| function(f); a : domain(f)|] ==> : f" +apply (simp add: function_def apply_def) +apply (rule theI2, auto) +done + +lemma apply_Pair: "[| f: Pi(A,B); a: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) ==> : 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: "[| : f; f: Pi(A,B) |] ==> a : A" +by (blast dest: fun_is_rel) + +lemma range_type: "[| : f; f: Pi(A,B) |] ==> b : B(a)" +by (blast dest: fun_is_rel) + +lemma Pair_mem_PiD: "[| : 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 ==> : (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= |] ==> P + |] ==> P" +by (simp add: lam_def, blast) + +lemma lamD: "[| : (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}" +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 \ X=0 & (A \ 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(, 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(,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(,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(,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(,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(, 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