# HG changeset patch # User paulson # Date 1025379186 -7200 # Node ID 01fa0c8dbc92535f628fd19df2bd6ab937373b53 # Parent 8f394f266025cff4ae68b4f2da000a6a381daed2 conversion of many files to Isar format diff -r 8f394f266025 -r 01fa0c8dbc92 src/ZF/ArithSimp.ML --- a/src/ZF/ArithSimp.ML Fri Jun 28 20:01:09 2002 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,588 +0,0 @@ -(* Title: ZF/ArithSimp.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2000 University of Cambridge - -Arithmetic with simplification -*) - - -Addsimprocs ArithData.nat_cancel; - - -(*** Difference ***) - -Goal "m #- m = 0"; -by (subgoal_tac "natify(m) #- natify(m) = 0" 1); -by (rtac (natify_in_nat RS nat_induct) 2); -by Auto_tac; -qed "diff_self_eq_0"; - -(**Addition is the inverse of subtraction**) - -(*We need m:nat even if we replace the RHS by natify(m), for consider e.g. - n=2, m=omega; then n + (m-n) = 2 + (0-2) = 2 ~= 0 = natify(m).*) -Goal "[| n le m; m:nat |] ==> n #+ (m#-n) = m"; -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1); -by (etac rev_mp 1); -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); -by Auto_tac; -qed "add_diff_inverse"; - -Goal "[| n le m; m:nat |] ==> (m#-n) #+ n = m"; -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1); -by (asm_simp_tac (simpset() addsimps [add_commute, add_diff_inverse]) 1); -qed "add_diff_inverse2"; - -(*Proof is IDENTICAL to that of add_diff_inverse*) -Goal "[| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)"; -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1); -by (etac rev_mp 1); -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); -by (ALLGOALS Asm_simp_tac); -qed "diff_succ"; - -Goal "[| m: nat; n: nat |] ==> 0 < (n #- m) <-> m m #- n < m"; -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1); -by (etac rev_mp 1); -by (etac rev_mp 1); -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self]))); -qed "div_termination"; - -bind_thms ("div_rls", (*for mod and div*) - nat_typechecks @ - [Ord_transrec_type, apply_funtype, div_termination RS ltD, - nat_into_Ord, not_lt_iff_le RS iffD1]); - -val div_ss = simpset() addsimps [div_termination RS ltD, - not_lt_iff_le RS iffD2]; - -Goalw [raw_mod_def] "[| m:nat; n:nat |] ==> raw_mod (m, n) : nat"; -by (rtac Ord_transrec_type 1); -by (auto_tac(claset(), simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff])); -by (REPEAT (ares_tac div_rls 1)); -qed "raw_mod_type"; - -Goalw [mod_def] "m mod n : nat"; -by (simp_tac (simpset() addsimps [mod_def, raw_mod_type]) 1); -qed "mod_type"; -AddTCs [mod_type]; -AddIffs [mod_type]; - - -(** Aribtrary definitions for division by zero. Useful to simplify - certain equations **) - -Goalw [div_def] "a div 0 = 0"; -by (rtac (raw_div_def RS def_transrec RS trans) 1); -by (Asm_simp_tac 1); -qed "DIVISION_BY_ZERO_DIV"; (*NOT for adding to default simpset*) - -Goalw [mod_def] "a mod 0 = natify(a)"; -by (rtac (raw_mod_def RS def_transrec RS trans) 1); -by (Asm_simp_tac 1); -qed "DIVISION_BY_ZERO_MOD"; (*NOT for adding to default simpset*) - -fun div_undefined_case_tac s i = - case_tac s i THEN - asm_full_simp_tac - (simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]) (i+1) THEN - asm_full_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV, - DIVISION_BY_ZERO_MOD]) i; - -Goal "m raw_mod (m,n) = m"; -by (rtac (raw_mod_def RS def_transrec RS trans) 1); -by (asm_simp_tac (simpset() addsimps [div_termination RS ltD]) 1); -qed "raw_mod_less"; - -Goal "[| m m mod n = m"; -by (ftac lt_nat_in_nat 1 THEN assume_tac 1); -by (asm_simp_tac (simpset() addsimps [mod_def, raw_mod_less]) 1); -qed "mod_less"; - -Goal "[| 0 raw_mod (m, n) = raw_mod (m#-n, n)"; -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1); -by (rtac (raw_mod_def RS def_transrec RS trans) 1); -by (asm_simp_tac div_ss 1); -by (Blast_tac 1); -qed "raw_mod_geq"; - -Goal "[| n le m; m:nat |] ==> m mod n = (m#-n) mod n"; -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1); -by (div_undefined_case_tac "n=0" 1); -by (asm_simp_tac (simpset() addsimps [mod_def, raw_mod_geq]) 1); -qed "mod_geq"; - -Addsimps [mod_less]; - - -(*** Division ***) - -Goalw [raw_div_def] "[| m:nat; n:nat |] ==> raw_div (m, n) : nat"; -by (rtac Ord_transrec_type 1); -by (auto_tac(claset(), simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff])); -by (REPEAT (ares_tac div_rls 1)); -qed "raw_div_type"; - -Goalw [div_def] "m div n : nat"; -by (simp_tac (simpset() addsimps [div_def, raw_div_type]) 1); -qed "div_type"; -AddTCs [div_type]; -AddIffs [div_type]; - -Goal "m raw_div (m,n) = 0"; -by (rtac (raw_div_def RS def_transrec RS trans) 1); -by (asm_simp_tac (simpset() addsimps [div_termination RS ltD]) 1); -qed "raw_div_less"; - -Goal "[| m m div n = 0"; -by (ftac lt_nat_in_nat 1 THEN assume_tac 1); -by (asm_simp_tac (simpset() addsimps [div_def, raw_div_less]) 1); -qed "div_less"; - -Goal "[| 0 raw_div(m,n) = succ(raw_div(m#-n, n))"; -by (subgoal_tac "n ~= 0" 1); -by (Blast_tac 2); -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1); -by (rtac (raw_div_def RS def_transrec RS trans) 1); -by (asm_simp_tac div_ss 1); -qed "raw_div_geq"; - -Goal "[| 0 m div n = succ ((m#-n) div n)"; -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1); -by (asm_simp_tac (simpset() addsimps [div_def, raw_div_geq]) 1); -qed "div_geq"; - -Addsimps [div_less, div_geq]; - - -(*A key result*) -Goal "[| m: nat; n: nat |] ==> (m div n)#*n #+ m mod n = m"; -by (div_undefined_case_tac "n=0" 1); -by (etac complete_induct 1); -by (case_tac "x (m div n)#*n #+ m mod n = m"; -by (asm_simp_tac (simpset() addsimps [mod_div_equality_natify]) 1); -qed "mod_div_equality"; - - -(*** Further facts about mod (mainly for mutilated chess board) ***) - -Goal "[| 0 succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))"; -by (etac complete_induct 1); -by (excluded_middle_tac "succ(x) \ -\ succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))"; -by (case_tac "n=0" 1); -by (asm_simp_tac (simpset() addsimps [natify_succ, DIVISION_BY_ZERO_MOD]) 1); -by (subgoal_tac - "natify(succ(m)) mod n = \ -\ (if succ(natify(m) mod n) = n then 0 else succ(natify(m) mod n))" 1); -by (stac natify_succ 2); -by (rtac lemma 2); -by (auto_tac(claset(), - simpset() delsimps [natify_succ] - addsimps [nat_into_Ord RS Ord_0_lt_iff])); -qed "mod_succ"; - -Goal "[| 0 m mod n < n"; -by (subgoal_tac "natify(m) mod n < n" 1); -by (res_inst_tac [("i","natify(m)")] complete_induct 2); -by (case_tac "x k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)"; -by (subgoal_tac "k mod 2: 2" 1); -by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2); -by (dtac ltD 1); -by Auto_tac; -qed "mod2_cases"; - -Goal "succ(succ(m)) mod 2 = m mod 2"; -by (subgoal_tac "m mod 2: 2" 1); -by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2); -by (auto_tac (claset(), simpset() addsimps [mod_succ])); -qed "mod2_succ_succ"; - -Addsimps [mod2_succ_succ]; - -Goal "(m#+m#+n) mod 2 = n mod 2"; -by (subgoal_tac "(natify(m)#+natify(m)#+n) mod 2 = n mod 2" 1); -by (res_inst_tac [("n","natify(m)")] nat_induct 2); -by Auto_tac; -qed "mod2_add_more"; - -Goal "(m#+m) mod 2 = 0"; -by (cut_inst_tac [("n","0")] mod2_add_more 1); -by Auto_tac; -qed "mod2_add_self"; - -Addsimps [mod2_add_more, mod2_add_self]; - - -(**** Additional theorems about "le" ****) - -Goal "m:nat ==> m le (m #+ n)"; -by (Asm_simp_tac 1); -qed "add_le_self"; - -Goal "m:nat ==> m le (n #+ m)"; -by (Asm_simp_tac 1); -qed "add_le_self2"; - -(*** Monotonicity of Multiplication ***) - -Goal "[| i le j; j:nat |] ==> (i#*k) le (j#*k)"; -by (subgoal_tac "natify(i)#*natify(k) le j#*natify(k)" 1); -by (ftac lt_nat_in_nat 2); -by (res_inst_tac [("n","natify(k)")] nat_induct 3); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_le_mono]))); -qed "mult_le_mono1"; - -(* le monotonicity, BOTH arguments*) -Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l"; -by (rtac (mult_le_mono1 RS le_trans) 1); -by (REPEAT (assume_tac 1)); -by (EVERY [stac mult_commute 1, - stac mult_commute 1, - rtac mult_le_mono1 1]); -by (REPEAT (assume_tac 1)); -qed "mult_le_mono"; - -(*strict, in 1st argument; proof is by induction on k>0. - I can't see how to relax the typing conditions.*) -Goal "[| i k#*i < k#*j"; -by (etac zero_lt_natE 1); -by (ftac lt_nat_in_nat 2); -by (ALLGOALS Asm_simp_tac); -by (induct_tac "x" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono]))); -qed "mult_lt_mono2"; - -Goal "[| i i#*k < j#*k"; -by (asm_simp_tac (simpset() addsimps [mult_lt_mono2, - inst "n" "k" mult_commute]) 1); -qed "mult_lt_mono1"; - -Goal "m#+n = 0 <-> natify(m)=0 & natify(n)=0"; -by (subgoal_tac "natify(m) #+ natify(n) = 0 <-> natify(m)=0 & natify(n)=0" 1); -by (res_inst_tac [("n","natify(m)")] natE 2); - by (res_inst_tac [("n","natify(n)")] natE 4); -by Auto_tac; -qed "add_eq_0_iff"; -AddIffs [add_eq_0_iff]; - -Goal "0 < m#*n <-> 0 < natify(m) & 0 < natify(n)"; -by (subgoal_tac "0 < natify(m)#*natify(n) <-> \ -\ 0 < natify(m) & 0 < natify(n)" 1); -by (res_inst_tac [("n","natify(m)")] natE 2); - by (res_inst_tac [("n","natify(n)")] natE 4); - by (res_inst_tac [("n","natify(n)")] natE 3); -by Auto_tac; -qed "zero_lt_mult_iff"; - -Goal "m#*n = 1 <-> natify(m)=1 & natify(n)=1"; -by (subgoal_tac "natify(m) #* natify(n) = 1 <-> natify(m)=1 & natify(n)=1" 1); -by (res_inst_tac [("n","natify(m)")] natE 2); - by (res_inst_tac [("n","natify(n)")] natE 4); -by Auto_tac; -qed "mult_eq_1_iff"; -AddIffs [zero_lt_mult_iff, mult_eq_1_iff]; - -Goal "[|m: nat; n: nat|] ==> (m #* n = 0) <-> (m = 0 | n = 0)"; -by Auto_tac; -by (etac natE 1); -by (etac natE 2); -by Auto_tac; -qed "mult_is_zero"; - -Goal "(m #* n = 0) <-> (natify(m) = 0 | natify(n) = 0)"; -by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] mult_is_zero 1); -by Auto_tac; -qed "mult_is_zero_natify"; -AddIffs [mult_is_zero_natify]; - - -(** Cancellation laws for common factors in comparisons **) - -Goal "[| k: nat; m: nat; n: nat |] ==> (m#*k < n#*k) <-> (0 (0 < natify(k) & natify(m) < natify(n))"; -by (rtac iff_trans 1); -by (rtac lemma 2); -by Auto_tac; -qed "mult_less_cancel2"; - -Goal "(k#*m < k#*n) <-> (0 < natify(k) & natify(m) < natify(n))"; -by (simp_tac (simpset() addsimps [mult_less_cancel2, - inst "m" "k" mult_commute]) 1); -qed "mult_less_cancel1"; -Addsimps [mult_less_cancel1, mult_less_cancel2]; - -Goal "(m#*k le n#*k) <-> (0 < natify(k) --> natify(m) le natify(n))"; -by (asm_simp_tac (simpset() addsimps [not_lt_iff_le RS iff_sym]) 1); -by Auto_tac; -qed "mult_le_cancel2"; - -Goal "(k#*m le k#*n) <-> (0 < natify(k) --> natify(m) le natify(n))"; -by (asm_simp_tac (simpset() addsimps [not_lt_iff_le RS iff_sym]) 1); -by Auto_tac; -qed "mult_le_cancel1"; -Addsimps [mult_le_cancel1, mult_le_cancel2]; - -Goal "k : nat ==> k #* m le k \\ (0 < k \\ natify(m) le 1)"; -by (cut_inst_tac [("k","k"),("m","m"),("n","1")] mult_le_cancel1 1); -by Auto_tac; -qed "mult_le_cancel_le1"; - -Goal "[| Ord(m); Ord(n) |] ==> m=n <-> (m le n & n le m)"; -by (blast_tac (claset() addIs [le_anti_sym]) 1); -qed "Ord_eq_iff_le"; - -Goal "[| k: nat; m: nat; n: nat |] ==> (m#*k = n#*k) <-> (m=n | k=0)"; -by (asm_simp_tac (simpset() addsimps [inst "m" "m#*k" Ord_eq_iff_le, - inst "m" "m" Ord_eq_iff_le]) 1); -by (auto_tac (claset(), simpset() addsimps [Ord_0_lt_iff])); -val lemma = result(); - -Goal "(m#*k = n#*k) <-> (natify(m) = natify(n) | natify(k) = 0)"; -by (rtac iff_trans 1); -by (rtac lemma 2); -by Auto_tac; -qed "mult_cancel2"; - -Goal "(k#*m = k#*n) <-> (natify(m) = natify(n) | natify(k) = 0)"; -by (simp_tac (simpset() addsimps [mult_cancel2, inst "m" "k" mult_commute]) 1); -qed "mult_cancel1"; -Addsimps [mult_cancel1, mult_cancel2]; - - -(** Cancellation law for division **) - -Goal "[| 0 (k#*m) div (k#*n) = m div n"; -by (eres_inst_tac [("i","m")] complete_induct 1); -by (excluded_middle_tac "x (k#*m) div (k#*n) = m div n"; -by (cut_inst_tac [("k","natify(k)"),("m","natify(m)"),("n","natify(n)")] - div_cancel_raw 1); -by Auto_tac; -qed "div_cancel"; - - -(** Distributive law for remainder (mod) **) - -Goal "[| k:nat; m:nat; n:nat |] ==> (k#*m) mod (k#*n) = k #* (m mod n)"; -by (div_undefined_case_tac "k=0" 1); -by (div_undefined_case_tac "n=0" 1); -by (eres_inst_tac [("i","m")] complete_induct 1); -by (case_tac "x nat ==> (m #+ n) mod n = m mod n"; -by (subgoal_tac "(n #+ m) mod n = (n #+ m #- n) mod n" 1); -by (stac (mod_geq RS sym) 2); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute]))); -qed "mod_add_self2_raw"; - -Goal "(m #+ n) mod n = m mod n"; -by (cut_inst_tac [("n","natify(n)")] mod_add_self2_raw 1); -by Auto_tac; -qed "mod_add_self2"; - -Goal "(n#+m) mod n = m mod n"; -by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1); -qed "mod_add_self1"; -Addsimps [mod_add_self1, mod_add_self2]; - - -Goal "k \\ nat ==> (m #+ k#*n) mod n = m mod n"; -by (etac nat_induct 1); -by (ALLGOALS - (asm_simp_tac - (simpset() addsimps [inst "n" "n" add_left_commute]))); -qed "mod_mult_self1_raw"; - -Goal "(m #+ k#*n) mod n = m mod n"; -by (cut_inst_tac [("k","natify(k)")] mod_mult_self1_raw 1); -by Auto_tac; -qed "mod_mult_self1"; - -Goal "(m #+ n#*k) mod n = m mod n"; -by (simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1); -qed "mod_mult_self2"; - -Addsimps [mod_mult_self1, mod_mult_self2]; - -(*Lemma for gcd*) -Goal "m = m#*n ==> natify(n)=1 | m=0"; -by (subgoal_tac "m: nat" 1); -by (etac ssubst 2); -by (rtac disjCI 1); -by (dtac sym 1); -by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I])); -by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 3); -by Auto_tac; -by (subgoal_tac "m #* n = 0" 1); -by (stac (mult_natify2 RS sym) 2); -by (auto_tac (claset(), simpset() delsimps [mult_natify2])); -qed "mult_eq_self_implies_10"; - -Goal "[| m EX k: nat. n = succ(m#+k)"; -by (ftac lt_nat_in_nat 1 THEN assume_tac 1); -by (etac rev_mp 1); -by (induct_tac "n" 1); -by (ALLGOALS (simp_tac (simpset() addsimps [le_iff]))); -by (blast_tac (claset() addSEs [leE] - addSIs [add_0_right RS sym, add_succ_right RS sym]) 1); -qed_spec_mp "less_imp_succ_add"; - -Goal "[| m: nat; n: nat |] ==> (m (EX k: nat. n = succ(m#+k))"; -by (auto_tac (claset() addIs [less_imp_succ_add], simpset())); -qed "less_iff_succ_add"; - -(* on nat *) - -Goal "m #- n = 0 <-> natify(m) le natify(n)"; -by (auto_tac (claset(), simpset() addsimps - [le_iff, diff_self_eq_0])); -by (full_simp_tac (simpset() addsimps [less_iff_succ_add ]) 2); -by (Clarify_tac 2); -by (subgoal_tac "natify(m) #- natify(n) = 0" 3); -by (etac subst 3); -by (ALLGOALS(asm_full_simp_tac (simpset() - addsimps [diff_self_eq_0]))); -by (subgoal_tac "natify(m) #- natify(n) = 0" 2); -by (etac subst 2); -by (etac ssubst 3); -by (rtac (not_le_iff_lt RS iffD1) 1); -by (auto_tac (claset(), simpset() addsimps [le_iff])); -by (subgoal_tac "natify(m) #- natify(n) = 0" 1); -by (Asm_simp_tac 2); -by (thin_tac "m #- n = 0" 1); -by (dtac ([natify_in_nat, natify_in_nat] MRS zero_less_diff RS iffD2) 1); -by Auto_tac; -qed "diff_is_0_iff"; - -Goal "[| a:nat; b:nat |] ==> \ -\ (P(a #- b)) <-> ((a < b -->P(0)) & (ALL d:nat. a = b #+ d --> P(d)))"; -by (case_tac "a le b" 1); -by (subgoal_tac "natify(a) le natify(b)" 1); -by (dtac (diff_is_0_iff RS iffD2) 1); -by Safe_tac; -by (ALLGOALS(Asm_full_simp_tac)); -by (ALLGOALS(rotate_tac ~1)); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [le_iff]))); -by (Clarify_tac 2); -by (ALLGOALS(dtac not_lt_imp_le)); -by (ALLGOALS(Asm_full_simp_tac)); -by (ALLGOALS(dres_inst_tac [("x", "a #- b")] bspec)); -by (ALLGOALS(Asm_simp_tac)); -by (ALLGOALS(dtac add_diff_inverse)); -by (ALLGOALS(rotate_tac ~1)); -by (ALLGOALS(Asm_full_simp_tac)); -qed "nat_diff_split"; - - - diff -r 8f394f266025 -r 01fa0c8dbc92 src/ZF/ArithSimp.thy --- a/src/ZF/ArithSimp.thy Fri Jun 28 20:01:09 2002 +0200 +++ b/src/ZF/ArithSimp.thy Sat Jun 29 21:33:06 2002 +0200 @@ -8,4 +8,585 @@ theory ArithSimp = Arith files "arith_data.ML": + +(*** Difference ***) + +lemma diff_self_eq_0: "m #- m = 0" +apply (subgoal_tac "natify (m) #- natify (m) = 0") +apply (rule_tac [2] natify_in_nat [THEN nat_induct], auto) +done + +(**Addition is the inverse of subtraction**) + +(*We need m:nat even if we replace the RHS by natify(m), for consider e.g. + n=2, m=omega; then n + (m-n) = 2 + (0-2) = 2 ~= 0 = natify(m).*) +lemma add_diff_inverse: "[| n le m; m:nat |] ==> n #+ (m#-n) = m" +apply (frule lt_nat_in_nat, erule nat_succI) +apply (erule rev_mp) +apply (rule_tac m = "m" and n = "n" in diff_induct, auto) +done + +lemma add_diff_inverse2: "[| n le m; m:nat |] ==> (m#-n) #+ n = m" +apply (frule lt_nat_in_nat, erule nat_succI) +apply (simp (no_asm_simp) add: add_commute add_diff_inverse) +done + +(*Proof is IDENTICAL to that of add_diff_inverse*) +lemma diff_succ: "[| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)" +apply (frule lt_nat_in_nat, erule nat_succI) +apply (erule rev_mp) +apply (rule_tac m = "m" and n = "n" in diff_induct) +apply (simp_all (no_asm_simp)) +done + +lemma zero_less_diff [simp]: + "[| m: nat; n: nat |] ==> 0 < (n #- m) <-> m m #- n < m" +apply (frule lt_nat_in_nat, erule nat_succI) +apply (erule rev_mp) +apply (erule rev_mp) +apply (rule_tac m = "m" and n = "n" in diff_induct) +apply (simp_all (no_asm_simp) add: diff_le_self) +done + +(*for mod and div*) +lemmas div_rls = + nat_typechecks Ord_transrec_type apply_funtype + div_termination [THEN ltD] + nat_into_Ord not_lt_iff_le [THEN iffD1] + +lemma raw_mod_type: "[| m:nat; n:nat |] ==> raw_mod (m, n) : nat" +apply (unfold raw_mod_def) +apply (rule Ord_transrec_type) +apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff]) +apply (blast intro: div_rls) +done + +lemma mod_type [TC,iff]: "m mod n : nat" +apply (unfold mod_def) +apply (simp (no_asm) add: mod_def raw_mod_type) +done + + +(** Aribtrary definitions for division by zero. Useful to simplify + certain equations **) + +lemma DIVISION_BY_ZERO_DIV: "a div 0 = 0" +apply (unfold div_def) +apply (rule raw_div_def [THEN def_transrec, THEN trans]) +apply (simp (no_asm_simp)) +done (*NOT for adding to default simpset*) + +lemma DIVISION_BY_ZERO_MOD: "a mod 0 = natify(a)" +apply (unfold mod_def) +apply (rule raw_mod_def [THEN def_transrec, THEN trans]) +apply (simp (no_asm_simp)) +done (*NOT for adding to default simpset*) + +lemma raw_mod_less: "m raw_mod (m,n) = m" +apply (rule raw_mod_def [THEN def_transrec, THEN trans]) +apply (simp (no_asm_simp) add: div_termination [THEN ltD]) +done + +lemma mod_less [simp]: "[| m m mod n = m" +apply (frule lt_nat_in_nat, assumption) +apply (simp (no_asm_simp) add: mod_def raw_mod_less) +done + +lemma raw_mod_geq: + "[| 0 raw_mod (m, n) = raw_mod (m#-n, n)" +apply (frule lt_nat_in_nat, erule nat_succI) +apply (rule raw_mod_def [THEN def_transrec, THEN trans]) +apply (simp add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2], blast) +done + + +lemma mod_geq: "[| n le m; m:nat |] ==> m mod n = (m#-n) mod n" +apply (frule lt_nat_in_nat, erule nat_succI) +apply (case_tac "n=0") + apply (simp add: DIVISION_BY_ZERO_MOD) +apply (simp add: mod_def raw_mod_geq nat_into_Ord [THEN Ord_0_lt_iff]) +done + + +(*** Division ***) + +lemma raw_div_type: "[| m:nat; n:nat |] ==> raw_div (m, n) : nat" +apply (unfold raw_div_def) +apply (rule Ord_transrec_type) +apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff]) +apply (blast intro: div_rls) +done + +lemma div_type [TC,iff]: "m div n : nat" +apply (unfold div_def) +apply (simp (no_asm) add: div_def raw_div_type) +done + +lemma raw_div_less: "m raw_div (m,n) = 0" +apply (rule raw_div_def [THEN def_transrec, THEN trans]) +apply (simp (no_asm_simp) add: div_termination [THEN ltD]) +done + +lemma div_less [simp]: "[| m m div n = 0" +apply (frule lt_nat_in_nat, assumption) +apply (simp (no_asm_simp) add: div_def raw_div_less) +done + +lemma raw_div_geq: "[| 0 raw_div(m,n) = succ(raw_div(m#-n, n))" +apply (subgoal_tac "n ~= 0") +prefer 2 apply blast +apply (frule lt_nat_in_nat, erule nat_succI) +apply (rule raw_div_def [THEN def_transrec, THEN trans]) +apply (simp add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2] ) +done + +lemma div_geq [simp]: + "[| 0 m div n = succ ((m#-n) div n)" +apply (frule lt_nat_in_nat, erule nat_succI) +apply (simp (no_asm_simp) add: div_def raw_div_geq) +done + +declare div_less [simp] div_geq [simp] + + +(*A key result*) +lemma mod_div_lemma: "[| m: nat; n: nat |] ==> (m div n)#*n #+ m mod n = m" +apply (case_tac "n=0") + apply (simp add: DIVISION_BY_ZERO_MOD) +apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff]) +apply (erule complete_induct) +apply (case_tac "x (m div n)#*n #+ m mod n = m" +apply (simp (no_asm_simp) add: mod_div_equality_natify) +done + + +(*** Further facts about mod (mainly for mutilated chess board) ***) + +lemma mod_succ_lemma: + "[| 0 succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))" +apply (erule complete_induct) +apply (case_tac "succ (x) succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))" +apply (case_tac "n=0") + apply (simp (no_asm_simp) add: natify_succ DIVISION_BY_ZERO_MOD) +apply (subgoal_tac "natify (succ (m)) mod n = (if succ (natify (m) mod n) = n then 0 else succ (natify (m) mod n))") + prefer 2 + apply (subst natify_succ) + apply (rule mod_succ_lemma) + apply (auto simp del: natify_succ simp add: nat_into_Ord [THEN Ord_0_lt_iff]) +done + +lemma mod_less_divisor: "[| 0 m mod n < n" +apply (subgoal_tac "natify (m) mod n < n") +apply (rule_tac [2] i = "natify (m) " in complete_induct) +apply (case_tac [3] "x k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)" +apply (subgoal_tac "k mod 2: 2") + prefer 2 apply (simp add: mod_less_divisor [THEN ltD]) +apply (drule ltD, auto) +done + +lemma mod2_succ_succ [simp]: "succ(succ(m)) mod 2 = m mod 2" +apply (subgoal_tac "m mod 2: 2") + prefer 2 apply (simp add: mod_less_divisor [THEN ltD]) +apply (auto simp add: mod_succ) +done + +lemma mod2_add_more [simp]: "(m#+m#+n) mod 2 = n mod 2" +apply (subgoal_tac " (natify (m) #+natify (m) #+n) mod 2 = n mod 2") +apply (rule_tac [2] n = "natify (m) " in nat_induct) +apply auto +done + +lemma mod2_add_self [simp]: "(m#+m) mod 2 = 0" +by (cut_tac n = "0" in mod2_add_more, auto) + + +(**** Additional theorems about "le" ****) + +lemma add_le_self: "m:nat ==> m le (m #+ n)" +apply (simp (no_asm_simp)) +done + +lemma add_le_self2: "m:nat ==> m le (n #+ m)" +apply (simp (no_asm_simp)) +done + +(*** Monotonicity of Multiplication ***) + +lemma mult_le_mono1: "[| i le j; j:nat |] ==> (i#*k) le (j#*k)" +apply (subgoal_tac "natify (i) #*natify (k) le j#*natify (k) ") +apply (frule_tac [2] lt_nat_in_nat) +apply (rule_tac [3] n = "natify (k) " in nat_induct) +apply (simp_all add: add_le_mono) +done + +(* le monotonicity, BOTH arguments*) +lemma mult_le_mono: "[| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l" +apply (rule mult_le_mono1 [THEN le_trans], assumption+) +apply (subst mult_commute, subst mult_commute, rule mult_le_mono1, assumption+) +done + +(*strict, in 1st argument; proof is by induction on k>0. + I can't see how to relax the typing conditions.*) +lemma mult_lt_mono2: "[| i k#*i < k#*j" +apply (erule zero_lt_natE) +apply (frule_tac [2] lt_nat_in_nat) +apply (simp_all (no_asm_simp)) +apply (induct_tac "x") +apply (simp_all (no_asm_simp) add: add_lt_mono) +done + +lemma mult_lt_mono1: "[| i i#*k < j#*k" +apply (simp (no_asm_simp) add: mult_lt_mono2 mult_commute [of _ k]) +done + +lemma add_eq_0_iff [iff]: "m#+n = 0 <-> natify(m)=0 & natify(n)=0" +apply (subgoal_tac "natify (m) #+ natify (n) = 0 <-> natify (m) =0 & natify (n) =0") +apply (rule_tac [2] n = "natify (m) " in natE) + apply (rule_tac [4] n = "natify (n) " in natE) +apply auto +done + +lemma zero_lt_mult_iff [iff]: "0 < m#*n <-> 0 < natify(m) & 0 < natify(n)" +apply (subgoal_tac "0 < natify (m) #*natify (n) <-> 0 < natify (m) & 0 < natify (n) ") +apply (rule_tac [2] n = "natify (m) " in natE) + apply (rule_tac [4] n = "natify (n) " in natE) + apply (rule_tac [3] n = "natify (n) " in natE) +apply auto +done + +lemma mult_eq_1_iff [iff]: "m#*n = 1 <-> natify(m)=1 & natify(n)=1" +apply (subgoal_tac "natify (m) #* natify (n) = 1 <-> natify (m) =1 & natify (n) =1") +apply (rule_tac [2] n = "natify (m) " in natE) + apply (rule_tac [4] n = "natify (n) " in natE) +apply auto +done + + +lemma mult_is_zero: "[|m: nat; n: nat|] ==> (m #* n = 0) <-> (m = 0 | n = 0)" +apply auto +apply (erule natE) +apply (erule_tac [2] natE, auto) +done + +lemma mult_is_zero_natify [iff]: + "(m #* n = 0) <-> (natify(m) = 0 | natify(n) = 0)" +apply (cut_tac m = "natify (m) " and n = "natify (n) " in mult_is_zero) +apply auto +done + + +(** Cancellation laws for common factors in comparisons **) + +lemma mult_less_cancel_lemma: + "[| k: nat; m: nat; n: nat |] ==> (m#*k < n#*k) <-> (0 (0 < natify(k) & natify(m) < natify(n))" +apply (rule iff_trans) +apply (rule_tac [2] mult_less_cancel_lemma, auto) +done + +lemma mult_less_cancel1 [simp]: + "(k#*m < k#*n) <-> (0 < natify(k) & natify(m) < natify(n))" +apply (simp (no_asm) add: mult_less_cancel2 mult_commute [of k]) +done + +lemma mult_le_cancel2 [simp]: "(m#*k le n#*k) <-> (0 < natify(k) --> natify(m) le natify(n))" +apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym]) +apply auto +done + +lemma mult_le_cancel1 [simp]: "(k#*m le k#*n) <-> (0 < natify(k) --> natify(m) le natify(n))" +apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym]) +apply auto +done + +lemma mult_le_cancel_le1: "k : nat ==> k #* m le k \ (0 < k \ natify(m) le 1)" +by (cut_tac k = "k" and m = "m" and n = "1" in mult_le_cancel1, auto) + +lemma Ord_eq_iff_le: "[| Ord(m); Ord(n) |] ==> m=n <-> (m le n & n le m)" +by (blast intro: le_anti_sym) + +lemma mult_cancel2_lemma: + "[| k: nat; m: nat; n: nat |] ==> (m#*k = n#*k) <-> (m=n | k=0)" +apply (simp (no_asm_simp) add: Ord_eq_iff_le [of "m#*k"] Ord_eq_iff_le [of m]) +apply (auto simp add: Ord_0_lt_iff) +done + +lemma mult_cancel2 [simp]: + "(m#*k = n#*k) <-> (natify(m) = natify(n) | natify(k) = 0)" +apply (rule iff_trans) +apply (rule_tac [2] mult_cancel2_lemma, auto) +done + +lemma mult_cancel1 [simp]: + "(k#*m = k#*n) <-> (natify(m) = natify(n) | natify(k) = 0)" +apply (simp (no_asm) add: mult_cancel2 mult_commute [of k]) +done + + +(** Cancellation law for division **) + +lemma div_cancel_raw: + "[| 0 (k#*m) div (k#*n) = m div n" +apply (erule_tac i = "m" in complete_induct) +apply (case_tac "x (k#*m) div (k#*n) = m div n" +apply (cut_tac k = "natify (k) " and m = "natify (m)" and n = "natify (n)" + in div_cancel_raw) +apply auto +done + + +(** Distributive law for remainder (mod) **) + +lemma mult_mod_distrib_raw: + "[| k:nat; m:nat; n:nat |] ==> (k#*m) mod (k#*n) = k #* (m mod n)" +apply (case_tac "k=0") + apply (simp add: DIVISION_BY_ZERO_MOD) +apply (case_tac "n=0") + apply (simp add: DIVISION_BY_ZERO_MOD) +apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff]) +apply (erule_tac i = "m" in complete_induct) +apply (case_tac "x nat ==> (m #+ n) mod n = m mod n" +apply (subgoal_tac " (n #+ m) mod n = (n #+ m #- n) mod n") +apply (simp add: add_commute) +apply (subst mod_geq [symmetric], auto) +done + +lemma mod_add_self2 [simp]: "(m #+ n) mod n = m mod n" +apply (cut_tac n = "natify (n) " in mod_add_self2_raw) +apply auto +done + +lemma mod_add_self1 [simp]: "(n#+m) mod n = m mod n" +apply (simp (no_asm_simp) add: add_commute mod_add_self2) +done + +lemma mod_mult_self1_raw: "k \ nat ==> (m #+ k#*n) mod n = m mod n" +apply (erule nat_induct) +apply (simp_all (no_asm_simp) add: add_left_commute [of _ n]) +done + +lemma mod_mult_self1 [simp]: "(m #+ k#*n) mod n = m mod n" +apply (cut_tac k = "natify (k) " in mod_mult_self1_raw) +apply auto +done + +lemma mod_mult_self2 [simp]: "(m #+ n#*k) mod n = m mod n" +apply (simp (no_asm) add: mult_commute mod_mult_self1) +done + +(*Lemma for gcd*) +lemma mult_eq_self_implies_10: "m = m#*n ==> natify(n)=1 | m=0" +apply (subgoal_tac "m: nat") + prefer 2 + apply (erule ssubst) + apply simp +apply (rule disjCI) +apply (drule sym) +apply (rule Ord_linear_lt [of "natify(n)" 1]) +apply simp_all + apply (subgoal_tac "m #* n = 0", simp) + apply (subst mult_natify2 [symmetric]) + apply (simp del: mult_natify2) +apply (drule nat_into_Ord [THEN Ord_0_lt, THEN [2] mult_lt_mono2], auto) +done + +lemma less_imp_succ_add [rule_format]: + "[| m EX k: nat. n = succ(m#+k)" +apply (frule lt_nat_in_nat, assumption) +apply (erule rev_mp) +apply (induct_tac "n") +apply (simp_all (no_asm) add: le_iff) +apply (blast elim!: leE intro!: add_0_right [symmetric] add_succ_right [symmetric]) +done + +lemma less_iff_succ_add: + "[| m: nat; n: nat |] ==> (m (EX k: nat. n = succ(m#+k))" +by (auto intro: less_imp_succ_add) + +(* on nat *) + +lemma diff_is_0_lemma: + "[| m: nat; n: nat |] ==> m #- n = 0 <-> m le n" +apply (rule_tac m = "m" and n = "n" in diff_induct, simp_all) +done + +lemma diff_is_0_iff: "m #- n = 0 <-> natify(m) le natify(n)" +by (simp add: diff_is_0_lemma [symmetric]) + +lemma nat_lt_imp_diff_eq_0: + "[| a:nat; b:nat; a a #- b = 0" +by (simp add: diff_is_0_iff le_iff) + +lemma nat_diff_split: + "[| a:nat; b:nat |] ==> + (P(a #- b)) <-> ((a < b -->P(0)) & (ALL d:nat. a = b #+ d --> P(d)))" +apply (case_tac "a < b") + apply (force simp add: nat_lt_imp_diff_eq_0) +apply (rule iffI, simp_all) + apply clarify + apply (rotate_tac -1) + apply simp +apply (drule_tac x="a#-b" in bspec) +apply (simp_all add: Ordinal.not_lt_iff_le add_diff_inverse) +done + +ML +{* +val diff_self_eq_0 = thm "diff_self_eq_0"; +val add_diff_inverse = thm "add_diff_inverse"; +val add_diff_inverse2 = thm "add_diff_inverse2"; +val diff_succ = thm "diff_succ"; +val zero_less_diff = thm "zero_less_diff"; +val diff_mult_distrib = thm "diff_mult_distrib"; +val diff_mult_distrib2 = thm "diff_mult_distrib2"; +val div_termination = thm "div_termination"; +val raw_mod_type = thm "raw_mod_type"; +val mod_type = thm "mod_type"; +val DIVISION_BY_ZERO_DIV = thm "DIVISION_BY_ZERO_DIV"; +val DIVISION_BY_ZERO_MOD = thm "DIVISION_BY_ZERO_MOD"; +val raw_mod_less = thm "raw_mod_less"; +val mod_less = thm "mod_less"; +val raw_mod_geq = thm "raw_mod_geq"; +val mod_geq = thm "mod_geq"; +val raw_div_type = thm "raw_div_type"; +val div_type = thm "div_type"; +val raw_div_less = thm "raw_div_less"; +val div_less = thm "div_less"; +val raw_div_geq = thm "raw_div_geq"; +val div_geq = thm "div_geq"; +val mod_div_equality_natify = thm "mod_div_equality_natify"; +val mod_div_equality = thm "mod_div_equality"; +val mod_succ = thm "mod_succ"; +val mod_less_divisor = thm "mod_less_divisor"; +val mod_1_eq = thm "mod_1_eq"; +val mod2_cases = thm "mod2_cases"; +val mod2_succ_succ = thm "mod2_succ_succ"; +val mod2_add_more = thm "mod2_add_more"; +val mod2_add_self = thm "mod2_add_self"; +val add_le_self = thm "add_le_self"; +val add_le_self2 = thm "add_le_self2"; +val mult_le_mono1 = thm "mult_le_mono1"; +val mult_le_mono = thm "mult_le_mono"; +val mult_lt_mono2 = thm "mult_lt_mono2"; +val mult_lt_mono1 = thm "mult_lt_mono1"; +val add_eq_0_iff = thm "add_eq_0_iff"; +val zero_lt_mult_iff = thm "zero_lt_mult_iff"; +val mult_eq_1_iff = thm "mult_eq_1_iff"; +val mult_is_zero = thm "mult_is_zero"; +val mult_is_zero_natify = thm "mult_is_zero_natify"; +val mult_less_cancel2 = thm "mult_less_cancel2"; +val mult_less_cancel1 = thm "mult_less_cancel1"; +val mult_le_cancel2 = thm "mult_le_cancel2"; +val mult_le_cancel1 = thm "mult_le_cancel1"; +val mult_le_cancel_le1 = thm "mult_le_cancel_le1"; +val Ord_eq_iff_le = thm "Ord_eq_iff_le"; +val mult_cancel2 = thm "mult_cancel2"; +val mult_cancel1 = thm "mult_cancel1"; +val div_cancel_raw = thm "div_cancel_raw"; +val div_cancel = thm "div_cancel"; +val mult_mod_distrib_raw = thm "mult_mod_distrib_raw"; +val mod_mult_distrib2 = thm "mod_mult_distrib2"; +val mult_mod_distrib = thm "mult_mod_distrib"; +val mod_add_self2_raw = thm "mod_add_self2_raw"; +val mod_add_self2 = thm "mod_add_self2"; +val mod_add_self1 = thm "mod_add_self1"; +val mod_mult_self1_raw = thm "mod_mult_self1_raw"; +val mod_mult_self1 = thm "mod_mult_self1"; +val mod_mult_self2 = thm "mod_mult_self2"; +val mult_eq_self_implies_10 = thm "mult_eq_self_implies_10"; +val less_imp_succ_add = thm "less_imp_succ_add"; +val less_iff_succ_add = thm "less_iff_succ_add"; +val diff_is_0_iff = thm "diff_is_0_iff"; +val nat_lt_imp_diff_eq_0 = thm "nat_lt_imp_diff_eq_0"; +val nat_diff_split = thm "nat_diff_split"; +*} + end diff -r 8f394f266025 -r 01fa0c8dbc92 src/ZF/Inductive.thy --- a/src/ZF/Inductive.thy Fri Jun 28 20:01:09 2002 +0200 +++ b/src/ZF/Inductive.thy Sat Jun 29 21:33:06 2002 +0200 @@ -6,7 +6,7 @@ (Co)Inductive Definitions for Zermelo-Fraenkel Set Theory. *) -theory Inductive = Fixedpt + mono +theory Inductive = Fixedpt + mono + QPair files "ind_syntax.ML" "Tools/cartprod.ML" diff -r 8f394f266025 -r 01fa0c8dbc92 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Fri Jun 28 20:01:09 2002 +0200 +++ b/src/ZF/IsaMakefile Sat Jun 29 21:33:06 2002 +0200 @@ -28,7 +28,7 @@ FOL: @cd $(SRC)/FOL; $(ISATOOL) make FOL -$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.ML \ +$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy \ ArithSimp.thy Bool.thy Cardinal.thy \ CardinalArith.thy Cardinal_AC.thy \ Datatype.ML Datatype.thy Epsilon.thy Finite.thy \ @@ -45,8 +45,8 @@ Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \ Trancl.thy Univ.thy Update.thy \ WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy \ - ind_syntax.ML mono.ML mono.thy pair.thy simpdata.ML \ - subset.ML subset.thy thy_syntax.ML upair.ML upair.thy + ind_syntax.ML mono.thy pair.thy simpdata.ML \ + thy_syntax.ML upair.thy @$(ISATOOL) usedir -b -r $(OUT)/FOL ZF diff -r 8f394f266025 -r 01fa0c8dbc92 src/ZF/QPair.ML --- a/src/ZF/QPair.ML Fri Jun 28 20:01:09 2002 +0200 +++ b/src/ZF/QPair.ML Sat Jun 29 21:33:06 2002 +0200 @@ -328,3 +328,30 @@ Goal "C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C"; by (Blast_tac 1); qed "Part_qsum_equality"; + + +(*** Monotonicity ***) + +Goalw [QPair_def] "[| a<=c; b<=d |] ==> <= "; +by (REPEAT (ares_tac [sum_mono] 1)); +qed "QPair_mono"; + +Goal "[| A<=C; ALL x:A. B(x) <= D(x) |] ==> \ +\ QSigma(A,B) <= QSigma(C,D)"; +by (Blast_tac 1); +qed "QSigma_mono_lemma"; +bind_thm ("QSigma_mono", ballI RSN (2,QSigma_mono_lemma)); + +Goalw [QInl_def] "a<=b ==> QInl(a) <= QInl(b)"; +by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1)); +qed "QInl_mono"; + +Goalw [QInr_def] "a<=b ==> QInr(a) <= QInr(b)"; +by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1)); +qed "QInr_mono"; + +Goal "[| A<=C; B<=D |] ==> A <+> B <= C <+> D"; +by (Blast_tac 1); +qed "qsum_mono"; + + diff -r 8f394f266025 -r 01fa0c8dbc92 src/ZF/QPair.thy --- a/src/ZF/QPair.thy Fri Jun 28 20:01:09 2002 +0200 +++ b/src/ZF/QPair.thy Sat Jun 29 21:33:06 2002 +0200 @@ -11,7 +11,7 @@ 1966. *) -QPair = Sum + +QPair = Sum + mono + consts QPair :: "[i, i] => i" ("<(_;/ _)>") diff -r 8f394f266025 -r 01fa0c8dbc92 src/ZF/arith_data.ML --- a/src/ZF/arith_data.ML Fri Jun 28 20:01:09 2002 +0200 +++ b/src/ZF/arith_data.ML Sat Jun 29 21:33:06 2002 +0200 @@ -218,6 +218,10 @@ end; +(*Install the simprocs!*) +Addsimprocs ArithData.nat_cancel; + + (*examples: print_depth 22; set timing; diff -r 8f394f266025 -r 01fa0c8dbc92 src/ZF/equalities.thy --- a/src/ZF/equalities.thy Fri Jun 28 20:01:09 2002 +0200 +++ b/src/ZF/equalities.thy Sat Jun 29 21:33:06 2002 +0200 @@ -3,13 +3,14 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge -Converse, domain, range of a relation or function. -And set theory equalities involving Union, Intersection, Inclusion, etc. - (Thanks also to Philippe de Groote.) +Basic equations (and inclusions) involving union, intersection, +converse, domain, range, etc. + +Thanks also to Philippe de Groote. *) -theory equalities = pair + subset: +theory equalities = pair: (*FIXME: move to ZF.thy or even to FOL.thy??*) lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))" @@ -23,6 +24,33 @@ lemma the_eq_trivial [simp]: "(THE x. x = a) = a" by blast +(** Monotonicity of implications -- some could go to FOL **) + +lemma in_mono: "A<=B ==> x:A --> x:B" +by blast + +lemma conj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)" +by fast (*or (IntPr.fast_tac 1)*) + +lemma disj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)" +by fast (*or (IntPr.fast_tac 1)*) + +lemma imp_mono: "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)" +by fast (*or (IntPr.fast_tac 1)*) + +lemma imp_refl: "P-->P" +by (rule impI, assumption) + +(*The quantifier monotonicity rules are also intuitionistically valid*) +lemma ex_mono: + "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))" +by blast + +lemma all_mono: + "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))" +by blast + + lemma the_eq_0 [simp]: "(THE x. False) = 0" by (blast intro: the_0) @@ -77,143 +105,27 @@ by blast -(*** domain ***) - -lemma domain_iff: "a: domain(r) <-> (EX y. : r)" -by (unfold domain_def, blast) +(** cons; Finite Sets **) -lemma domainI [intro]: ": r ==> a: domain(r)" -by (unfold domain_def, blast) - -lemma domainE [elim!]: - "[| a : domain(r); !!y. : r ==> P |] ==> P" -by (unfold domain_def, blast) - -lemma domain_subset: "domain(Sigma(A,B)) <= A" +lemma cons_subsetI: "[| a:C; B<=C |] ==> cons(a,B) <= C" by blast -(*** range ***) - -lemma rangeI [intro]: ": r ==> b : range(r)" -apply (unfold range_def) -apply (erule converseI [THEN domainI]) -done - -lemma rangeE [elim!]: "[| b : range(r); !!x. : r ==> P |] ==> P" -by (unfold range_def, blast) - -lemma range_subset: "range(A*B) <= B" -apply (unfold range_def) -apply (subst converse_prod) -apply (rule domain_subset) -done - - -(*** field ***) - -lemma fieldI1: ": r ==> a : field(r)" -by (unfold field_def, blast) - -lemma fieldI2: ": r ==> b : field(r)" -by (unfold field_def, blast) - -lemma fieldCI [intro]: - "(~ :r ==> : r) ==> a : field(r)" -apply (unfold field_def, blast) -done - -lemma fieldE [elim!]: - "[| a : field(r); - !!x. : r ==> P; - !!x. : r ==> P |] ==> P" -by (unfold field_def, blast) - -lemma field_subset: "field(A*B) <= A Un B" -by blast - -lemma domain_subset_field: "domain(r) <= field(r)" -apply (unfold field_def) -apply (rule Un_upper1) -done - -lemma range_subset_field: "range(r) <= field(r)" -apply (unfold field_def) -apply (rule Un_upper2) -done - -lemma domain_times_range: "r <= Sigma(A,B) ==> r <= domain(r)*range(r)" +lemma subset_consI: "B <= cons(a,B)" by blast -lemma field_times_field: "r <= Sigma(A,B) ==> r <= field(r)*field(r)" -by blast - -lemma relation_field_times_field: "relation(r) ==> r <= field(r)*field(r)" -by (simp add: relation_def, blast) - - -(*** Image of a set under a function/relation ***) - -lemma image_iff: "b : r``A <-> (EX x:A. :r)" -by (unfold image_def, blast) - -lemma image_singleton_iff: "b : r``{a} <-> :r" -by (rule image_iff [THEN iff_trans], blast) - -lemma imageI [intro]: "[| : r; a:A |] ==> b : r``A" -by (unfold image_def, blast) - -lemma imageE [elim!]: - "[| b: r``A; !!x.[| : r; x:A |] ==> P |] ==> P" -apply (unfold image_def, blast) -done - -lemma image_subset: "r <= A*B ==> r``C <= B" +lemma cons_subset_iff [iff]: "cons(a,B)<=C <-> a:C & B<=C" by blast - -(*** Inverse image of a set under a function/relation ***) - -lemma vimage_iff: - "a : r-``B <-> (EX y:B. :r)" -apply (unfold vimage_def image_def converse_def, blast) -done - -lemma vimage_singleton_iff: "a : r-``{b} <-> :r" -by (rule vimage_iff [THEN iff_trans], blast) - -lemma vimageI [intro]: "[| : r; b:B |] ==> a : r-``B" -by (unfold vimage_def, blast) +(*A safe special case of subset elimination, adding no new variables + [| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *) +lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE, standard] -lemma vimageE [elim!]: - "[| a: r-``B; !!x.[| : r; x:B |] ==> P |] ==> P" -apply (unfold vimage_def, blast) -done - -lemma vimage_subset: "r <= A*B ==> r-``C <= A" -apply (unfold vimage_def) -apply (erule converse_type [THEN image_subset]) -done - - -(** The Union of a set of relations is a relation -- Lemma for fun_Union **) -lemma rel_Union: "(ALL x:S. EX A B. x <= A*B) ==> - Union(S) <= domain(Union(S)) * range(Union(S))" +lemma subset_empty_iff: "A<=0 <-> A=0" by blast -(** The Union of 2 relations is a relation (Lemma for fun_Un) **) -lemma rel_Un: "[| r <= A*B; s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)" -by blast - -lemma domain_Diff_eq: "[| : r; c~=b |] ==> domain(r-{}) = domain(r)" +lemma subset_cons_iff: "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)" by blast -lemma range_Diff_eq: "[| : r; c~=a |] ==> range(r-{}) = range(r)" -by blast - - - -(** Finite Sets **) - (* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*) lemma cons_eq: "{a} Un B = cons(a,B)" by blast @@ -233,9 +145,50 @@ lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)" by blast -(** Binary Intersection **) +(** singletons **) + +lemma singleton_subsetI: "a:C ==> {a} <= C" +by blast + +lemma singleton_subsetD: "{a} <= C ==> a:C" +by blast + + +(*** succ ***) + +lemma subset_succI: "i <= succ(i)" +by blast + +(*But if j is an ordinal or is transitive, then i:j implies i<=j! + See ordinal/Ord_succ_subsetI*) +lemma succ_subsetI: "[| i:j; i<=j |] ==> succ(i)<=j" +by (unfold succ_def, blast) -(*NOT an equality, but it seems to belong here...*) +lemma succ_subsetE: + "[| succ(i) <= j; [| i:j; i<=j |] ==> P |] ==> P" +apply (unfold succ_def, blast) +done + +lemma succ_subset_iff: "succ(a) <= B <-> (a <= B & a : B)" +by (unfold succ_def, blast) + + +(*** Binary Intersection ***) + +(** Intersection is the greatest lower bound of two sets **) + +lemma Int_subset_iff: "C <= A Int B <-> C <= A & C <= B" +by blast + +lemma Int_lower1: "A Int B <= A" +by blast + +lemma Int_lower2: "A Int B <= B" +by blast + +lemma Int_greatest: "[| C<=A; C<=B |] ==> C <= A Int B" +by blast + lemma Int_cons: "cons(a,B) Int C <= cons(a, B Int C)" by blast @@ -272,7 +225,21 @@ lemma Int_Diff_eq: "C<=A ==> (A-B) Int C = C-B" by blast -(** Binary Union **) +(*** Binary Union ***) + +(** Union is the least upper bound of two sets *) + +lemma Un_subset_iff: "A Un B <= C <-> A <= C & B <= C" +by blast + +lemma Un_upper1: "A <= A Un B" +by blast + +lemma Un_upper2: "B <= A Un B" +by blast + +lemma Un_least: "[| A<=C; B<=C |] ==> A Un B <= C" +by blast lemma Un_cons: "cons(a,B) Un C = cons(a, B Un C)" by blast @@ -310,7 +277,16 @@ lemma Un_eq_Union: "A Un B = Union({A, B})" by blast -(** Simple properties of Diff -- set difference **) +(*** Set difference ***) + +lemma Diff_subset: "A-B <= A" +by blast + +lemma Diff_contains: "[| C<=A; C Int B = 0 |] ==> C <= A-B" +by blast + +lemma subset_Diff_cons_iff: "B <= A - cons(c,C) <-> B<=A-C & c ~: B" +by blast lemma Diff_cancel: "A - A = 0" by blast @@ -378,7 +354,18 @@ by (blast elim!: equalityE) -(** Big Union and Intersection **) +(*** Big Union and Intersection ***) + +(** Big Union is the least upper bound of a set **) + +lemma Union_subset_iff: "Union(A) <= C <-> (ALL x:A. x <= C)" +by blast + +lemma Union_upper: "B:A ==> B <= Union(A)" +by blast + +lemma Union_least: "[| !!x. x:A ==> x<=C |] ==> Union(A) <= C" +by blast lemma Union_cons [simp]: "Union(cons(a,B)) = a Un Union(B)" by blast @@ -395,10 +382,31 @@ lemma Union_empty_iff: "Union(A) = 0 <-> (ALL B:A. B=0)" by blast +(** Big Intersection is the greatest lower bound of a nonempty set **) + +lemma Inter_subset_iff: "a: A ==> C <= Inter(A) <-> (ALL x:A. C <= x)" +by blast + +lemma Inter_lower: "B:A ==> Inter(A) <= B" +by blast + +lemma Inter_greatest: "[| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A)" +by blast + +(** Intersection of a family of sets **) + +lemma INT_lower: "x:A ==> (INT x:A. B(x)) <= B(x)" +by blast + +lemma INT_greatest: + "[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))" +by blast + lemma Inter_0: "Inter(0) = 0" by (unfold Inter_def, blast) -lemma Inter_Un_subset: "[| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)" +lemma Inter_Un_subset: + "[| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)" by blast (* A good challenge: Inter is ill-behaved on the empty set *) @@ -416,7 +424,19 @@ "Inter(cons(a,B)) = (if B=0 then a else a Int Inter(B))" by force -(** Unions and Intersections of Families **) +(*** Unions and Intersections of Families ***) + +lemma subset_UN_iff_eq: "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))" +by (blast elim!: equalityE) + +lemma UN_subset_iff: "(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)" +by blast + +lemma UN_upper: "x:A ==> B(x) <= (UN x:A. B(x))" +by (erule RepFunI [THEN Union_upper]) + +lemma UN_least: "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C" +by blast lemma Union_eq_UN: "Union(A) = (UN x:A. x)" by blast @@ -436,7 +456,7 @@ lemma INT_Un: "(INT i:I Un J. A(i)) = (if I=0 then INT j:J. A(j) else if J=0 then INT i:I. A(i) else ((INT i:I. A(i)) Int (INT j:J. A(j))))" -apply auto +apply simp apply (blast intro!: equalityI) done @@ -562,6 +582,19 @@ (** Domain **) +lemma domain_iff: "a: domain(r) <-> (EX y. : r)" +by (unfold domain_def, blast) + +lemma domainI [intro]: ": r ==> a: domain(r)" +by (unfold domain_def, blast) + +lemma domainE [elim!]: + "[| a : domain(r); !!y. : r ==> P |] ==> P" +by (unfold domain_def, blast) + +lemma domain_subset: "domain(Sigma(A,B)) <= A" +by blast + lemma domain_of_prod: "b:B ==> domain(A*B) = A" by blast @@ -580,9 +613,6 @@ lemma domain_Diff_subset: "domain(A) - domain(B) <= domain(A - B)" by blast -lemma domain_converse [simp]: "domain(converse(r)) = range(r)" -by blast - lemma domain_UN: "domain(UN x:A. B(x)) = (UN x:A. domain(B(x)))" by blast @@ -592,6 +622,20 @@ (** Range **) +lemma rangeI [intro]: ": r ==> b : range(r)" +apply (unfold range_def) +apply (erule converseI [THEN domainI]) +done + +lemma rangeE [elim!]: "[| b : range(r); !!x. : r ==> P |] ==> P" +by (unfold range_def, blast) + +lemma range_subset: "range(A*B) <= B" +apply (unfold range_def) +apply (subst converse_prod) +apply (rule domain_subset) +done + lemma range_of_prod: "a:A ==> range(A*B) = B" by blast @@ -610,12 +654,54 @@ lemma range_Diff_subset: "range(A) - range(B) <= range(A - B)" by blast +lemma domain_converse [simp]: "domain(converse(r)) = range(r)" +by blast + lemma range_converse [simp]: "range(converse(r)) = domain(r)" by blast (** Field **) +lemma fieldI1: ": r ==> a : field(r)" +by (unfold field_def, blast) + +lemma fieldI2: ": r ==> b : field(r)" +by (unfold field_def, blast) + +lemma fieldCI [intro]: + "(~ :r ==> : r) ==> a : field(r)" +apply (unfold field_def, blast) +done + +lemma fieldE [elim!]: + "[| a : field(r); + !!x. : r ==> P; + !!x. : r ==> P |] ==> P" +by (unfold field_def, blast) + +lemma field_subset: "field(A*B) <= A Un B" +by blast + +lemma domain_subset_field: "domain(r) <= field(r)" +apply (unfold field_def) +apply (rule Un_upper1) +done + +lemma range_subset_field: "range(r) <= field(r)" +apply (unfold field_def) +apply (rule Un_upper2) +done + +lemma domain_times_range: "r <= Sigma(A,B) ==> r <= domain(r)*range(r)" +by blast + +lemma field_times_field: "r <= Sigma(A,B) ==> r <= field(r)*field(r)" +by blast + +lemma relation_field_times_field: "relation(r) ==> r <= field(r)*field(r)" +by (simp add: relation_def, blast) + lemma field_of_prod: "field(A*A) = A" by blast @@ -637,8 +723,39 @@ lemma field_converse [simp]: "field(converse(r)) = field(r)" by blast +(** The Union of a set of relations is a relation -- Lemma for fun_Union **) +lemma rel_Union: "(ALL x:S. EX A B. x <= A*B) ==> + Union(S) <= domain(Union(S)) * range(Union(S))" +by blast -(** Image **) +(** The Union of 2 relations is a relation (Lemma for fun_Un) **) +lemma rel_Un: "[| r <= A*B; s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)" +by blast + +lemma domain_Diff_eq: "[| : r; c~=b |] ==> domain(r-{}) = domain(r)" +by blast + +lemma range_Diff_eq: "[| : r; c~=a |] ==> range(r-{}) = range(r)" +by blast + + +(*** Image of a set under a function/relation ***) + +lemma image_iff: "b : r``A <-> (EX x:A. :r)" +by (unfold image_def, blast) + +lemma image_singleton_iff: "b : r``{a} <-> :r" +by (rule image_iff [THEN iff_trans], blast) + +lemma imageI [intro]: "[| : r; a:A |] ==> b : r``A" +by (unfold image_def, blast) + +lemma imageE [elim!]: + "[| b: r``A; !!x.[| : r; x:A |] ==> P |] ==> P" +by (unfold image_def, blast) + +lemma image_subset: "r <= A*B ==> r``C <= B" +by blast lemma image_0 [simp]: "r``0 = 0" by blast @@ -667,7 +784,27 @@ by blast -(** Inverse Image **) +(*** Inverse image of a set under a function/relation ***) + +lemma vimage_iff: + "a : r-``B <-> (EX y:B. :r)" +by (unfold vimage_def image_def converse_def, blast) + +lemma vimage_singleton_iff: "a : r-``{b} <-> :r" +by (rule vimage_iff [THEN iff_trans], blast) + +lemma vimageI [intro]: "[| : r; b:B |] ==> a : r-``B" +by (unfold vimage_def, blast) + +lemma vimageE [elim!]: + "[| a: r-``B; !!x.[| : r; x:B |] ==> P |] ==> P" +apply (unfold vimage_def, blast) +done + +lemma vimage_subset: "r <= A*B ==> r-``C <= A" +apply (unfold vimage_def) +apply (erule converse_type [THEN image_subset]) +done lemma vimage_0 [simp]: "r-``0 = 0" by blast @@ -760,7 +897,10 @@ lemma Pow_INT_eq: "x:A ==> Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))" by blast -(** RepFun **) +(*** RepFun ***) + +lemma RepFun_subset: "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B" +by blast lemma RepFun_eq_0_iff [simp]: "{f(x).x:A}=0 <-> A=0" by blast @@ -770,7 +910,10 @@ apply blast done -(** Collect **) +(*** Collect ***) + +lemma Collect_subset: "Collect(A,P) <= A" +by blast lemma Collect_Un: "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)" by blast @@ -800,10 +943,74 @@ "Collect(\x\A. B(x), P) = (\x\A. Collect(B(x), P))" by blast +lemmas subset_SIs = subset_refl cons_subsetI subset_consI + Union_least UN_least Un_least + Inter_greatest Int_greatest RepFun_subset + Un_upper1 Un_upper2 Int_lower1 Int_lower2 + +(*First, ML bindings from the old file subset.ML*) +ML +{* +val cons_subsetI = thm "cons_subsetI"; +val subset_consI = thm "subset_consI"; +val cons_subset_iff = thm "cons_subset_iff"; +val cons_subsetE = thm "cons_subsetE"; +val subset_empty_iff = thm "subset_empty_iff"; +val subset_cons_iff = thm "subset_cons_iff"; +val subset_succI = thm "subset_succI"; +val succ_subsetI = thm "succ_subsetI"; +val succ_subsetE = thm "succ_subsetE"; +val succ_subset_iff = thm "succ_subset_iff"; +val singleton_subsetI = thm "singleton_subsetI"; +val singleton_subsetD = thm "singleton_subsetD"; +val Union_subset_iff = thm "Union_subset_iff"; +val Union_upper = thm "Union_upper"; +val Union_least = thm "Union_least"; +val subset_UN_iff_eq = thm "subset_UN_iff_eq"; +val UN_subset_iff = thm "UN_subset_iff"; +val UN_upper = thm "UN_upper"; +val UN_least = thm "UN_least"; +val Inter_subset_iff = thm "Inter_subset_iff"; +val Inter_lower = thm "Inter_lower"; +val Inter_greatest = thm "Inter_greatest"; +val INT_lower = thm "INT_lower"; +val INT_greatest = thm "INT_greatest"; +val Un_subset_iff = thm "Un_subset_iff"; +val Un_upper1 = thm "Un_upper1"; +val Un_upper2 = thm "Un_upper2"; +val Un_least = thm "Un_least"; +val Int_subset_iff = thm "Int_subset_iff"; +val Int_lower1 = thm "Int_lower1"; +val Int_lower2 = thm "Int_lower2"; +val Int_greatest = thm "Int_greatest"; +val Diff_subset = thm "Diff_subset"; +val Diff_contains = thm "Diff_contains"; +val subset_Diff_cons_iff = thm "subset_Diff_cons_iff"; +val Collect_subset = thm "Collect_subset"; +val RepFun_subset = thm "RepFun_subset"; + +val subset_SIs = thms "subset_SIs"; + +val subset_cs = claset() + delrules [subsetI, subsetCE] + addSIs subset_SIs + addIs [Union_upper, Inter_lower] + addSEs [cons_subsetE]; +*} +(*subset_cs is a claset for subset reasoning*) + ML {* val ZF_cs = claset() delrules [equalityI]; +val in_mono = thm "in_mono"; +val conj_mono = thm "conj_mono"; +val disj_mono = thm "disj_mono"; +val imp_mono = thm "imp_mono"; +val imp_refl = thm "imp_refl"; +val ex_mono = thm "ex_mono"; +val all_mono = thm "all_mono"; + val converse_iff = thm "converse_iff"; val converseI = thm "converseI"; val converseD = thm "converseD"; diff -r 8f394f266025 -r 01fa0c8dbc92 src/ZF/ex/Primes.thy --- a/src/ZF/ex/Primes.thy Fri Jun 28 20:01:09 2002 +0200 +++ b/src/ZF/ex/Primes.thy Sat Jun 29 21:33:06 2002 +0200 @@ -137,14 +137,15 @@ lemma dvd_mod_imp_dvd_raw: "[| a \ nat; b \ nat; k dvd b; k dvd (a mod b) |] ==> k dvd a" -apply (tactic "div_undefined_case_tac \"b=0\" 1") +apply (case_tac "b=0") + apply (simp add: DIVISION_BY_ZERO_MOD) apply (blast intro: mod_div_equality [THEN subst] elim: dvdE intro!: dvd_add dvd_mult mult_type mod_type div_type) done lemma dvd_mod_imp_dvd: "[| k dvd (a mod b); k dvd b; a \ nat |] ==> k dvd a" -apply (cut_tac b = "natify (b) " in dvd_mod_imp_dvd_raw) +apply (cut_tac b = "natify (b)" in dvd_mod_imp_dvd_raw) apply auto apply (simp add: divides_def) done @@ -176,7 +177,7 @@ lemma gcd_type [simp,TC]: "gcd(m, n) \ nat" apply (subgoal_tac "gcd (natify (m) , natify (n)) \ nat") apply simp -apply (rule_tac m = "natify (m) " and n = "natify (n) " in gcd_induct) +apply (rule_tac m = "natify (m)" and n = "natify (n)" in gcd_induct) apply auto apply (simp add: gcd_non_0) done @@ -192,12 +193,12 @@ done lemma gcd_dvd1 [simp]: "m \ nat ==> gcd(m,n) dvd m" -apply (cut_tac m = "natify (m) " and n = "natify (n) " in gcd_dvd_both) +apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_dvd_both) apply auto done lemma gcd_dvd2 [simp]: "n \ nat ==> gcd(m,n) dvd n" -apply (cut_tac m = "natify (m) " and n = "natify (n) " in gcd_dvd_both) +apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_dvd_both) apply auto done @@ -205,7 +206,8 @@ lemma dvd_mod: "[| f dvd a; f dvd b |] ==> f dvd (a mod b)" apply (unfold divides_def) -apply (tactic "div_undefined_case_tac \"b=0\" 1") +apply (case_tac "b=0") + apply (simp add: DIVISION_BY_ZERO_MOD) apply auto apply (blast intro: mod_mult_distrib2 [symmetric]) done @@ -254,7 +256,7 @@ done lemma gcd_commute: "gcd(m,n) = gcd(n,m)" -apply (cut_tac m = "natify (m) " and n = "natify (n) " in gcd_commute_raw) +apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_commute_raw) apply auto done @@ -267,7 +269,7 @@ done lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))" -apply (cut_tac k = "natify (k) " and m = "natify (m) " and n = "natify (n) " +apply (cut_tac k = "natify (k)" and m = "natify (m)" and n = "natify (n) " in gcd_assoc_raw) apply auto done @@ -293,7 +295,7 @@ done lemma gcd_mult_distrib2: "k #* gcd (m, n) = gcd (k #* m, k #* n)" -apply (cut_tac k = "natify (k) " and m = "natify (m) " and n = "natify (n) " +apply (cut_tac k = "natify (k)" and m = "natify (m)" and n = "natify (n) " in gcd_mult_distrib2_raw) apply auto done @@ -324,7 +326,7 @@ "[| p \ prime; ~ (p dvd n); n \ nat |] ==> gcd (p, n) = 1" apply (unfold prime_def) apply clarify -apply (drule_tac x = "gcd (p,n) " in bspec) +apply (drule_tac x = "gcd (p,n)" in bspec) apply auto apply (cut_tac m = "p" and n = "n" in gcd_dvd2) apply auto @@ -371,7 +373,7 @@ done lemma gcd_add_mult: "gcd (m, k #* m #+ n) = gcd (m, n)" -apply (cut_tac k = "natify (k) " in gcd_add_mult_raw) +apply (cut_tac k = "natify (k)" in gcd_add_mult_raw) apply auto done @@ -390,7 +392,7 @@ done lemma gcd_mult_cancel: "gcd (k,n) = 1 ==> gcd (k #* m, n) = gcd (m, n)" -apply (cut_tac m = "natify (m) " and n = "natify (n) " in gcd_mult_cancel_raw) +apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_mult_cancel_raw) apply auto done diff -r 8f394f266025 -r 01fa0c8dbc92 src/ZF/mono.ML --- a/src/ZF/mono.ML Fri Jun 28 20:01:09 2002 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,191 +0,0 @@ -(* Title: ZF/mono - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Monotonicity of various operations (for lattice properties see subset.ML) -*) - -(** Replacement, in its various formulations **) - -(*Not easy to express monotonicity in P, since any "bigger" predicate - would have to be single-valued*) -Goal "A<=B ==> Replace(A,P) <= Replace(B,P)"; -by (blast_tac (claset() addSEs [ReplaceE]) 1); -qed "Replace_mono"; - -Goal "A<=B ==> {f(x). x:A} <= {f(x). x:B}"; -by (Blast_tac 1); -qed "RepFun_mono"; - -Goal "A<=B ==> Pow(A) <= Pow(B)"; -by (Blast_tac 1); -qed "Pow_mono"; - -Goal "A<=B ==> Union(A) <= Union(B)"; -by (Blast_tac 1); -qed "Union_mono"; - -val prems = Goal - "[| A<=C; !!x. x:A ==> B(x)<=D(x) \ -\ |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))"; -by (blast_tac (claset() addIs (prems RL [subsetD])) 1); -qed "UN_mono"; - -(*Intersection is ANTI-monotonic. There are TWO premises! *) -Goal "[| A<=B; a:A |] ==> Inter(B) <= Inter(A)"; -by (Blast_tac 1); -qed "Inter_anti_mono"; - -Goal "C<=D ==> cons(a,C) <= cons(a,D)"; -by (Blast_tac 1); -qed "cons_mono"; - -Goal "[| A<=C; B<=D |] ==> A Un B <= C Un D"; -by (Blast_tac 1); -qed "Un_mono"; - -Goal "[| A<=C; B<=D |] ==> A Int B <= C Int D"; -by (Blast_tac 1); -qed "Int_mono"; - -Goal "[| A<=C; D<=B |] ==> A-B <= C-D"; -by (Blast_tac 1); -qed "Diff_mono"; - -(** Standard products, sums and function spaces **) - -Goal "[| A<=C; ALL x:A. B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)"; -by (Blast_tac 1); -qed "Sigma_mono_lemma"; -bind_thm ("Sigma_mono", ballI RSN (2,Sigma_mono_lemma)); - -Goalw sum_defs "[| A<=C; B<=D |] ==> A+B <= C+D"; -by (REPEAT (ares_tac [subset_refl,Un_mono,Sigma_mono] 1)); -qed "sum_mono"; - -(*Note that B->A and C->A are typically disjoint!*) -Goal "B<=C ==> A->B <= A->C"; -by (blast_tac (claset() addIs [lam_type] addEs [Pi_lamE]) 1); -qed "Pi_mono"; - -Goalw [lam_def] "A<=B ==> Lambda(A,c) <= Lambda(B,c)"; -by (etac RepFun_mono 1); -qed "lam_mono"; - -(** Quine-inspired ordered pairs, products, injections and sums **) - -Goalw [QPair_def] "[| a<=c; b<=d |] ==> <= "; -by (REPEAT (ares_tac [sum_mono] 1)); -qed "QPair_mono"; - -Goal "[| A<=C; ALL x:A. B(x) <= D(x) |] ==> \ -\ QSigma(A,B) <= QSigma(C,D)"; -by (Blast_tac 1); -qed "QSigma_mono_lemma"; -bind_thm ("QSigma_mono", ballI RSN (2,QSigma_mono_lemma)); - -Goalw [QInl_def] "a<=b ==> QInl(a) <= QInl(b)"; -by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1)); -qed "QInl_mono"; - -Goalw [QInr_def] "a<=b ==> QInr(a) <= QInr(b)"; -by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1)); -qed "QInr_mono"; - -Goal "[| A<=C; B<=D |] ==> A <+> B <= C <+> D"; -by (Blast_tac 1); -qed "qsum_mono"; - - -(** Converse, domain, range, field **) - -Goal "r<=s ==> converse(r) <= converse(s)"; -by (Blast_tac 1); -qed "converse_mono"; - -Goal "r<=s ==> domain(r)<=domain(s)"; -by (Blast_tac 1); -qed "domain_mono"; - -bind_thm ("domain_rel_subset", [domain_mono, domain_subset] MRS subset_trans); - -Goal "r<=s ==> range(r)<=range(s)"; -by (Blast_tac 1); -qed "range_mono"; - -bind_thm ("range_rel_subset", [range_mono, range_subset] MRS subset_trans); - -Goal "r<=s ==> field(r)<=field(s)"; -by (Blast_tac 1); -qed "field_mono"; - -Goal "r <= A*A ==> field(r) <= A"; -by (etac (field_mono RS subset_trans) 1); -by (Blast_tac 1); -qed "field_rel_subset"; - - -(** Images **) - -val [prem1,prem2] = Goal - "[| !! x y. :r ==> :s; A<=B |] ==> r``A <= s``B"; -by (blast_tac (claset() addIs [prem1, prem2 RS subsetD]) 1); -qed "image_pair_mono"; - -val [prem1,prem2] = Goal - "[| !! x y. :r ==> :s; A<=B |] ==> r-``A <= s-``B"; -by (blast_tac (claset() addIs [prem1, prem2 RS subsetD]) 1); -qed "vimage_pair_mono"; - -Goal "[| r<=s; A<=B |] ==> r``A <= s``B"; -by (Blast_tac 1); -qed "image_mono"; - -Goal "[| r<=s; A<=B |] ==> r-``A <= s-``B"; -by (Blast_tac 1); -qed "vimage_mono"; - -val [sub,PQimp] = Goal - "[| A<=B; !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)"; -by (blast_tac (claset() addIs [sub RS subsetD, PQimp RS mp]) 1); -qed "Collect_mono"; - -(** Monotonicity of implications -- some could go to FOL **) - -Goal "A<=B ==> x:A --> x:B"; -by (Blast_tac 1); -qed "in_mono"; - -goal IFOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"; -by (IntPr.fast_tac 1); -qed "conj_mono"; - -goal IFOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"; -by (IntPr.fast_tac 1); -qed "disj_mono"; - -goal IFOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"; -by (IntPr.fast_tac 1); -qed "imp_mono"; - -goal IFOL.thy "P-->P"; -by (rtac impI 1); -by (assume_tac 1); -qed "imp_refl"; - -val [PQimp] = goal IFOL.thy - "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))"; -by IntPr.safe_tac; -by (etac (PQimp RS mp RS exI) 1); -qed "ex_mono"; - -val [PQimp] = goal IFOL.thy - "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))"; -by IntPr.safe_tac; -by (etac (spec RS (PQimp RS mp)) 1); -qed "all_mono"; - -(*Used in intr_elim.ML and in individual datatype definitions*) -bind_thms ("basic_monos", - [subset_refl, imp_refl, disj_mono, conj_mono, ex_mono, Collect_mono, Part_mono, in_mono]); diff -r 8f394f266025 -r 01fa0c8dbc92 src/ZF/mono.thy --- a/src/ZF/mono.thy Fri Jun 28 20:01:09 2002 +0200 +++ b/src/ZF/mono.thy Sat Jun 29 21:33:06 2002 +0200 @@ -1,2 +1,143 @@ -mono = QPair + Sum + func +(* Title: ZF/mono + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Monotonicity of various operations +*) + +theory mono = Sum + func: + +(** Replacement, in its various formulations **) + +(*Not easy to express monotonicity in P, since any "bigger" predicate + would have to be single-valued*) +lemma Replace_mono: "A<=B ==> Replace(A,P) <= Replace(B,P)" +by (blast elim!: ReplaceE) + +lemma RepFun_mono: "A<=B ==> {f(x). x:A} <= {f(x). x:B}" +by blast + +lemma Pow_mono: "A<=B ==> Pow(A) <= Pow(B)" +by blast + +lemma Union_mono: "A<=B ==> Union(A) <= Union(B)" +by blast + +lemma UN_mono: + "[| A<=C; !!x. x:A ==> B(x)<=D(x) |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))" +by blast + +(*Intersection is ANTI-monotonic. There are TWO premises! *) +lemma Inter_anti_mono: "[| A<=B; a:A |] ==> Inter(B) <= Inter(A)" +by blast + +lemma cons_mono: "C<=D ==> cons(a,C) <= cons(a,D)" +by blast + +lemma Un_mono: "[| A<=C; B<=D |] ==> A Un B <= C Un D" +by blast + +lemma Int_mono: "[| A<=C; B<=D |] ==> A Int B <= C Int D" +by blast + +lemma Diff_mono: "[| A<=C; D<=B |] ==> A-B <= C-D" +by blast + +(** Standard products, sums and function spaces **) + +lemma Sigma_mono [rule_format]: + "[| A<=C; !!x. x:A --> B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)" +by blast + +lemma sum_mono: "[| A<=C; B<=D |] ==> A+B <= C+D" +by (unfold sum_def, blast) + +(*Note that B->A and C->A are typically disjoint!*) +lemma Pi_mono: "B<=C ==> A->B <= A->C" +by (blast intro: lam_type elim: Pi_lamE) + +lemma lam_mono: "A<=B ==> Lambda(A,c) <= Lambda(B,c)" +apply (unfold lam_def) +apply (erule RepFun_mono) +done + +(** Converse, domain, range, field **) + +lemma converse_mono: "r<=s ==> converse(r) <= converse(s)" +by blast + +lemma domain_mono: "r<=s ==> domain(r)<=domain(s)" +by blast +lemmas domain_rel_subset = subset_trans [OF domain_mono domain_subset] + +lemma range_mono: "r<=s ==> range(r)<=range(s)" +by blast + +lemmas range_rel_subset = subset_trans [OF range_mono range_subset] + +lemma field_mono: "r<=s ==> field(r)<=field(s)" +by blast + +lemma field_rel_subset: "r <= A*A ==> field(r) <= A" +by (erule field_mono [THEN subset_trans], blast) + + +(** Images **) + +lemma image_pair_mono: + "[| !! x y. :r ==> :s; A<=B |] ==> r``A <= s``B" +by blast + +lemma vimage_pair_mono: + "[| !! x y. :r ==> :s; A<=B |] ==> r-``A <= s-``B" +by blast + +lemma image_mono: "[| r<=s; A<=B |] ==> r``A <= s``B" +by blast + +lemma vimage_mono: "[| r<=s; A<=B |] ==> r-``A <= s-``B" +by blast + +lemma Collect_mono: + "[| A<=B; !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)" +by blast + +(*Used in intr_elim.ML and in individual datatype definitions*) +lemmas basic_monos = subset_refl imp_refl disj_mono conj_mono ex_mono + Collect_mono Part_mono in_mono + +ML +{* +val Replace_mono = thm "Replace_mono"; +val RepFun_mono = thm "RepFun_mono"; +val Pow_mono = thm "Pow_mono"; +val Union_mono = thm "Union_mono"; +val UN_mono = thm "UN_mono"; +val Inter_anti_mono = thm "Inter_anti_mono"; +val cons_mono = thm "cons_mono"; +val Un_mono = thm "Un_mono"; +val Int_mono = thm "Int_mono"; +val Diff_mono = thm "Diff_mono"; +val Sigma_mono = thm "Sigma_mono"; +val sum_mono = thm "sum_mono"; +val Pi_mono = thm "Pi_mono"; +val lam_mono = thm "lam_mono"; +val converse_mono = thm "converse_mono"; +val domain_mono = thm "domain_mono"; +val domain_rel_subset = thm "domain_rel_subset"; +val range_mono = thm "range_mono"; +val range_rel_subset = thm "range_rel_subset"; +val field_mono = thm "field_mono"; +val field_rel_subset = thm "field_rel_subset"; +val image_pair_mono = thm "image_pair_mono"; +val vimage_pair_mono = thm "vimage_pair_mono"; +val image_mono = thm "image_mono"; +val vimage_mono = thm "vimage_mono"; +val Collect_mono = thm "Collect_mono"; + +val basic_monos = thms "basic_monos"; +*} + +end diff -r 8f394f266025 -r 01fa0c8dbc92 src/ZF/subset.ML --- a/src/ZF/subset.ML Fri Jun 28 20:01:09 2002 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,216 +0,0 @@ -(* Title: ZF/subset - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge - -Derived rules involving subsets -Union and Intersection as lattice operations -*) - -(*** cons ***) - -Goal "[| a:C; B<=C |] ==> cons(a,B) <= C"; -by (Blast_tac 1); -qed "cons_subsetI"; - -Goal "B <= cons(a,B)"; -by (Blast_tac 1); -qed "subset_consI"; - -Goal "cons(a,B)<=C <-> a:C & B<=C"; -by (Blast_tac 1); -qed "cons_subset_iff"; -AddIffs [cons_subset_iff]; - -(*A safe special case of subset elimination, adding no new variables - [| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *) -bind_thm ("cons_subsetE", cons_subset_iff RS iffD1 RS conjE); - -Goal "A<=0 <-> A=0"; -by (Blast_tac 1) ; -qed "subset_empty_iff"; - -Goal "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"; -by (Blast_tac 1) ; -qed "subset_cons_iff"; - -(*** succ ***) - -Goal "i <= succ(i)"; -by (Blast_tac 1) ; -qed "subset_succI"; - -(*But if j is an ordinal or is transitive, then i:j implies i<=j! - See ordinal/Ord_succ_subsetI*) -Goalw [succ_def] "[| i:j; i<=j |] ==> succ(i)<=j"; -by (Blast_tac 1) ; -qed "succ_subsetI"; - -val major::prems= Goalw [succ_def] - "[| succ(i) <= j; [| i:j; i<=j |] ==> P \ -\ |] ==> P"; -by (rtac (major RS cons_subsetE) 1); -by (REPEAT (ares_tac prems 1)) ; -qed "succ_subsetE"; - -Goalw [succ_def] "succ(a) <= B <-> (a <= B & a : B)"; -by (Blast_tac 1) ; -qed "succ_subset_iff"; - -(*** singletons ***) - -Goal "a:C ==> {a} <= C"; -by (Blast_tac 1) ; -qed "singleton_subsetI"; - -Goal "{a} <= C ==> a:C"; -by (Blast_tac 1) ; -qed "singleton_subsetD"; - -(*** Big Union -- least upper bound of a set ***) - -Goal "Union(A) <= C <-> (ALL x:A. x <= C)"; -by (Blast_tac 1); -qed "Union_subset_iff"; - -Goal "B:A ==> B <= Union(A)"; -by (Blast_tac 1); -qed "Union_upper"; - -val [prem]= Goal - "[| !!x. x:A ==> x<=C |] ==> Union(A) <= C"; -by (rtac (ballI RS (Union_subset_iff RS iffD2)) 1); -by (etac prem 1) ; -qed "Union_least"; - -(*** Union of a family of sets ***) - -Goal "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))"; -by (blast_tac (claset() addSEs [equalityE]) 1); -qed "subset_UN_iff_eq"; - -Goal "(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)"; -by (Blast_tac 1); -qed "UN_subset_iff"; - -Goal "x:A ==> B(x) <= (UN x:A. B(x))"; -by (etac (RepFunI RS Union_upper) 1); -qed "UN_upper"; - -val [prem]= Goal - "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C"; -by (rtac (ballI RS (UN_subset_iff RS iffD2)) 1); -by (etac prem 1) ; -qed "UN_least"; - - -(*** Big Intersection -- greatest lower bound of a nonempty set ***) - -Goal "a: A ==> C <= Inter(A) <-> (ALL x:A. C <= x)"; -by (Blast_tac 1); -qed "Inter_subset_iff"; - -Goal "B:A ==> Inter(A) <= B"; -by (Blast_tac 1); -qed "Inter_lower"; - -val [prem1,prem2]= Goal - "[| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A)"; -by (rtac ([prem1, ballI] MRS (Inter_subset_iff RS iffD2)) 1); -by (etac prem2 1) ; -qed "Inter_greatest"; - -(*** Intersection of a family of sets ***) - -Goal "x:A ==> (INT x:A. B(x)) <= B(x)"; -by (Blast_tac 1); -qed "INT_lower"; - -val [nonempty,prem] = Goal - "[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))"; -by (rtac (nonempty RS RepFunI RS Inter_greatest) 1); -by (REPEAT (eresolve_tac [RepFunE, prem, ssubst] 1)); -qed "INT_greatest"; - - -(*** Finite Union -- the least upper bound of 2 sets ***) - -Goal "A Un B <= C <-> A <= C & B <= C"; -by (Blast_tac 1); -qed "Un_subset_iff"; - -Goal "A <= A Un B"; -by (Blast_tac 1); -qed "Un_upper1"; - -Goal "B <= A Un B"; -by (Blast_tac 1); -qed "Un_upper2"; - -Goal "[| A<=C; B<=C |] ==> A Un B <= C"; -by (Blast_tac 1); -qed "Un_least"; - - -(*** Finite Intersection -- the greatest lower bound of 2 sets *) - -Goal "C <= A Int B <-> C <= A & C <= B"; -by (Blast_tac 1); -qed "Int_subset_iff"; - -Goal "A Int B <= A"; -by (Blast_tac 1); -qed "Int_lower1"; - -Goal "A Int B <= B"; -by (Blast_tac 1); -qed "Int_lower2"; - -Goal "[| C<=A; C<=B |] ==> C <= A Int B"; -by (Blast_tac 1); -qed "Int_greatest"; - - -(*** Set difference *) - -Goal "A-B <= A"; -by (Blast_tac 1); -qed "Diff_subset"; - -Goal "[| C<=A; C Int B = 0 |] ==> C <= A-B"; -by (Blast_tac 1); -qed "Diff_contains"; - -Goal "B <= A - cons(c,C) <-> B<=A-C & c ~: B"; -by (Blast_tac 1); -qed "subset_Diff_cons_iff"; - - - -(** Collect **) - -Goal "Collect(A,P) <= A"; -by (Blast_tac 1); -qed "Collect_subset"; - - -(** RepFun **) - -val prems = Goal "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B"; -by (blast_tac (claset() addIs prems) 1); -qed "RepFun_subset"; - -bind_thms ("subset_SIs", - [subset_refl, cons_subsetI, subset_consI, - Union_least, UN_least, Un_least, - Inter_greatest, Int_greatest, RepFun_subset, - Un_upper1, Un_upper2, Int_lower1, Int_lower2]); - - -(*A claset for subset reasoning*) -val subset_cs = claset() - delrules [subsetI, subsetCE] - addSIs subset_SIs - addIs [Union_upper, Inter_lower] - addSEs [cons_subsetE]; - diff -r 8f394f266025 -r 01fa0c8dbc92 src/ZF/subset.thy --- a/src/ZF/subset.thy Fri Jun 28 20:01:09 2002 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -(*Dummy theory to document dependencies *) - -subset = pair diff -r 8f394f266025 -r 01fa0c8dbc92 src/ZF/upair.ML --- a/src/ZF/upair.ML Fri Jun 28 20:01:09 2002 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,404 +0,0 @@ -(* Title: ZF/upair - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge - -UNORDERED pairs in Zermelo-Fraenkel Set Theory - -Observe the order of dependence: - Upair is defined in terms of Replace - Un is defined in terms of Upair and Union (similarly for Int) - cons is defined in terms of Upair and Un - Ordered pairs and descriptions are defined using cons ("set notation") -*) - -(*** Lemmas about power sets ***) - -bind_thm ("Pow_bottom", empty_subsetI RS PowI); (* 0 : Pow(B) *) -bind_thm ("Pow_top", subset_refl RS PowI); (* A : Pow(A) *) - - -(*** Unordered pairs - Upair ***) - -Goalw [Upair_def] "c : Upair(a,b) <-> (c=a | c=b)"; -by (Blast_tac 1) ; -qed "Upair_iff"; - -Addsimps [Upair_iff]; - -Goal "a : Upair(a,b)"; -by (Simp_tac 1); -qed "UpairI1"; - -Goal "b : Upair(a,b)"; -by (Simp_tac 1); -qed "UpairI2"; - -val major::prems= Goal - "[| a : Upair(b,c); a=b ==> P; a=c ==> P |] ==> P"; -by (rtac (major RS (Upair_iff RS iffD1 RS disjE)) 1); -by (REPEAT (eresolve_tac prems 1)) ; -qed "UpairE"; - -AddSIs [UpairI1,UpairI2]; -AddSEs [UpairE]; - -(*** Rules for binary union -- Un -- defined via Upair ***) - -Goalw [Un_def] "c : A Un B <-> (c:A | c:B)"; -by (Blast_tac 1); -qed "Un_iff"; - -Addsimps [Un_iff]; - -Goal "c : A ==> c : A Un B"; -by (Asm_simp_tac 1); -qed "UnI1"; - -Goal "c : B ==> c : A Un B"; -by (Asm_simp_tac 1); -qed "UnI2"; - -val major::prems= Goal - "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"; -by (rtac (major RS (Un_iff RS iffD1 RS disjE)) 1); -by (REPEAT (eresolve_tac prems 1)) ; -qed "UnE"; - -(*Stronger version of the rule above*) -val major::prems = Goal - "[| c : A Un B; c:A ==> P; [| c:B; c~:A |] ==> P |] ==> P"; -by (rtac (major RS UnE) 1); -by (eresolve_tac prems 1); -by (rtac classical 1); -by (eresolve_tac prems 1); -by (swap_res_tac prems 1); -by (etac notnotD 1); -qed "UnE'"; - -(*Classical introduction rule: no commitment to A vs B*) -val prems = Goal "(c ~: B ==> c : A) ==> c : A Un B"; -by (Simp_tac 1); -by (blast_tac (claset() addSIs prems) 1); -qed "UnCI"; - -AddSIs [UnCI]; -AddSEs [UnE]; - - -(*** Rules for small intersection -- Int -- defined via Upair ***) - -Goalw [Int_def] "c : A Int B <-> (c:A & c:B)"; -by (Blast_tac 1); -qed "Int_iff"; - -Addsimps [Int_iff]; - -Goal "[| c : A; c : B |] ==> c : A Int B"; -by (Asm_simp_tac 1); -qed "IntI"; - -Goal "c : A Int B ==> c : A"; -by (Asm_full_simp_tac 1); -qed "IntD1"; - -Goal "c : A Int B ==> c : B"; -by (Asm_full_simp_tac 1); -qed "IntD2"; - -val prems = Goal "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P"; -by (resolve_tac prems 1); -by (REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ; -qed "IntE"; - -AddSIs [IntI]; -AddSEs [IntE]; - -(*** Rules for set difference -- defined via Upair ***) - -Goalw [Diff_def] "c : A-B <-> (c:A & c~:B)"; -by (Blast_tac 1); -qed "Diff_iff"; - -Addsimps [Diff_iff]; - -Goal "[| c : A; c ~: B |] ==> c : A - B"; -by (Asm_simp_tac 1); -qed "DiffI"; - -Goal "c : A - B ==> c : A"; -by (Asm_full_simp_tac 1); -qed "DiffD1"; - -Goal "c : A - B ==> c ~: B"; -by (Asm_full_simp_tac 1); -qed "DiffD2"; - -val prems = Goal "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P"; -by (resolve_tac prems 1); -by (REPEAT (ares_tac (prems RL [DiffD1, DiffD2]) 1)) ; -qed "DiffE"; - -AddSIs [DiffI]; -AddSEs [DiffE]; - -(*** Rules for cons -- defined via Un and Upair ***) - -Goalw [cons_def] "a : cons(b,A) <-> (a=b | a:A)"; -by (Blast_tac 1); -qed "cons_iff"; - -Addsimps [cons_iff]; - -Goal "a : cons(a,B)"; -by (Simp_tac 1); -qed "consI1"; - -Addsimps [consI1]; -AddTCs [consI1]; (*risky as a typechecking rule, but solves otherwise - unconstrained goals of the form x : ?A*) - -Goal "a : B ==> a : cons(b,B)"; -by (Asm_simp_tac 1); -qed "consI2"; - -val major::prems= Goal - "[| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P"; -by (rtac (major RS (cons_iff RS iffD1 RS disjE)) 1); -by (REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ; -qed "consE"; - -(*Stronger version of the rule above*) -val major::prems = Goal - "[| a : cons(b,A); a=b ==> P; [| a:A; a~=b |] ==> P |] ==> P"; -by (rtac (major RS consE) 1); -by (eresolve_tac prems 1); -by (rtac classical 1); -by (eresolve_tac prems 1); -by (swap_res_tac prems 1); -by (etac notnotD 1); -qed "consE'"; - -(*Classical introduction rule*) -val prems = Goal "(a~:B ==> a=b) ==> a: cons(b,B)"; -by (Simp_tac 1); -by (blast_tac (claset() addSIs prems) 1); -qed "consCI"; - -AddSIs [consCI]; -AddSEs [consE]; - -Goal "cons(a,B) ~= 0"; -by (blast_tac (claset() addEs [equalityE]) 1) ; -qed "cons_not_0"; - -bind_thm ("cons_neq_0", cons_not_0 RS notE); - -Addsimps [cons_not_0, cons_not_0 RS not_sym]; - - -(*** Singletons - using cons ***) - -Goal "a : {b} <-> a=b"; -by (Simp_tac 1); -qed "singleton_iff"; - -Goal "a : {a}"; -by (rtac consI1 1) ; -qed "singletonI"; - -bind_thm ("singletonE", make_elim (singleton_iff RS iffD1)); - -AddSIs [singletonI]; -AddSEs [singletonE]; - -(*** Rules for Descriptions ***) - -val [pa,eq] = Goalw [the_def] - "[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"; -by (fast_tac (claset() addSIs [pa] addEs [eq RS subst]) 1) ; -qed "the_equality"; - -AddIs [the_equality]; - -(* Only use this if you already know EX!x. P(x) *) -Goal "[| EX! x. P(x); P(a) |] ==> (THE x. P(x)) = a"; -by (Blast_tac 1); -qed "the_equality2"; - -Goal "EX! x. P(x) ==> P(THE x. P(x))"; -by (etac ex1E 1); -by (stac the_equality 1); -by (REPEAT (Blast_tac 1)); -qed "theI"; - -(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then - (THE x.P(x)) rewrites to (THE x. Q(x)) *) - -(*If it's "undefined", it's zero!*) -Goalw [the_def] "~ (EX! x. P(x)) ==> (THE x. P(x))=0"; -by (blast_tac (claset() addSEs [ReplaceE]) 1); -qed "the_0"; - -(*Easier to apply than theI: conclusion has only one occurrence of P*) -val prems = -Goal "[| ~ Q(0) ==> EX! x. P(x); !!x. P(x) ==> Q(x) |] ==> Q(THE x. P(x))"; -by (rtac classical 1); -by (resolve_tac prems 1); -by (rtac theI 1); -by (rtac classical 1); -by (resolve_tac prems 1); -by (etac (the_0 RS subst) 1); -by (assume_tac 1); -qed "theI2"; - -(*** if -- a conditional expression for formulae ***) - -Goalw [if_def] "(if True then a else b) = a"; -by (Blast_tac 1); -qed "if_true"; - -Goalw [if_def] "(if False then a else b) = b"; -by (Blast_tac 1); -qed "if_false"; - -(*Never use with case splitting, or if P is known to be true or false*) -val prems = Goalw [if_def] - "[| P<->Q; Q ==> a=c; ~Q ==> b=d |] \ -\ ==> (if P then a else b) = (if Q then c else d)"; -by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1); -qed "if_cong"; - -(*Prevents simplification of x and y: faster and allows the execution - of functional programs. NOW THE DEFAULT.*) -Goal "P<->Q ==> (if P then x else y) = (if Q then x else y)"; -by (Asm_simp_tac 1); -qed "if_weak_cong"; - -(*Not needed for rewriting, since P would rewrite to True anyway*) -Goalw [if_def] "P ==> (if P then a else b) = a"; -by (Blast_tac 1); -qed "if_P"; - -(*Not needed for rewriting, since P would rewrite to False anyway*) -Goalw [if_def] "~P ==> (if P then a else b) = b"; -by (Blast_tac 1); -qed "if_not_P"; - -Addsimps [if_true, if_false]; - -Goal "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"; -by (case_tac "Q" 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1) ; -qed "split_if"; - -(** Rewrite rules for boolean case-splitting: faster than - addsplits[split_if] -**) - -bind_thm ("split_if_eq1", inst "P" "%x. x = ?b" split_if); -bind_thm ("split_if_eq2", inst "P" "%x. ?a = x" split_if); - -bind_thm ("split_if_mem1", inst "P" "%x. x : ?b" split_if); -bind_thm ("split_if_mem2", inst "P" "%x. ?a : x" split_if); - -bind_thms ("split_ifs", [split_if_eq1, split_if_eq2, split_if_mem1, split_if_mem2]); - -(*Logically equivalent to split_if_mem2*) -Goal "a: (if P then x else y) <-> P & a:x | ~P & a:y"; -by (simp_tac (simpset() addsplits [split_if]) 1) ; -qed "if_iff"; - -val prems = Goal - "[| P ==> a: A; ~P ==> b: A |] ==> (if P then a else b): A"; -by (simp_tac (simpset() addsimps prems addsplits [split_if]) 1) ; -qed "if_type"; - -AddTCs [if_type]; - -(*** Foundation lemmas ***) - -(*was called mem_anti_sym*) -val prems = Goal "[| a:b; ~P ==> b:a |] ==> P"; -by (rtac classical 1); -by (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1); -by (REPEAT (blast_tac (claset() addIs prems addSEs [equalityE]) 1)); -qed "mem_asym"; - -(*was called mem_anti_refl*) -Goal "a:a ==> P"; -by (blast_tac (claset() addIs [mem_asym]) 1); -qed "mem_irrefl"; - -(*mem_irrefl should NOT be added to default databases: - it would be tried on most goals, making proofs slower!*) - -Goal "a ~: a"; -by (rtac notI 1); -by (etac mem_irrefl 1); -qed "mem_not_refl"; - -(*Good for proving inequalities by rewriting*) -Goal "a:A ==> a ~= A"; -by (blast_tac (claset() addSEs [mem_irrefl]) 1); -qed "mem_imp_not_eq"; - -(*** Rules for succ ***) - -Goalw [succ_def] "i : succ(j) <-> i=j | i:j"; -by (Blast_tac 1); -qed "succ_iff"; - -Goalw [succ_def] "i : succ(i)"; -by (rtac consI1 1) ; -qed "succI1"; - -Addsimps [succI1]; - -Goalw [succ_def] "i : j ==> i : succ(j)"; -by (etac consI2 1) ; -qed "succI2"; - -val major::prems= Goalw [succ_def] - "[| i : succ(j); i=j ==> P; i:j ==> P |] ==> P"; -by (rtac (major RS consE) 1); -by (REPEAT (eresolve_tac prems 1)) ; -qed "succE"; - -(*Classical introduction rule*) -val [prem]= Goal "(i~:j ==> i=j) ==> i: succ(j)"; -by (rtac (disjCI RS (succ_iff RS iffD2)) 1); -by (etac prem 1) ; -qed "succCI"; - -AddSIs [succCI]; -AddSEs [succE]; - -Goal "succ(n) ~= 0"; -by (blast_tac (claset() addSEs [equalityE]) 1) ; -qed "succ_not_0"; - -bind_thm ("succ_neq_0", succ_not_0 RS notE); - -Addsimps [succ_not_0, succ_not_0 RS not_sym]; -AddSEs [succ_neq_0, sym RS succ_neq_0]; - - -(* succ(c) <= B ==> c : B *) -bind_thm ("succ_subsetD", succI1 RSN (2,subsetD)); - -(* succ(b) ~= b *) -bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym); - -Goal "succ(m) = succ(n) <-> m=n"; -by (blast_tac (claset() addEs [mem_asym] addSEs [equalityE]) 1) ; -qed "succ_inject_iff"; - -bind_thm ("succ_inject", succ_inject_iff RS iffD1); - -Addsimps [succ_inject_iff]; -AddSDs [succ_inject]; - -(*Not needed now that cons is available. Deletion reduces the search space.*) -Delrules [UpairI1,UpairI2,UpairE]; diff -r 8f394f266025 -r 01fa0c8dbc92 src/ZF/upair.thy --- a/src/ZF/upair.thy Fri Jun 28 20:01:09 2002 +0200 +++ b/src/ZF/upair.thy Sat Jun 29 21:33:06 2002 +0200 @@ -2,6 +2,14 @@ ID: $Id$ Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory Copyright 1993 University of Cambridge + +UNORDERED pairs in Zermelo-Fraenkel Set Theory + +Observe the order of dependence: + Upair is defined in terms of Replace + Un is defined in terms of Upair and Union (similarly for Int) + cons is defined in terms of Upair and Un + Ordered pairs and descriptions are defined using cons ("set notation") *) theory upair = ZF @@ -10,4 +18,379 @@ setup TypeCheck.setup declare atomize_ball [symmetric, rulify] +(*** Lemmas about power sets ***) + +lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 : Pow(B) *) +lemmas Pow_top = subset_refl [THEN PowI] (* A : Pow(A) *) + + +(*** Unordered pairs - Upair ***) + +lemma Upair_iff [simp]: "c : Upair(a,b) <-> (c=a | c=b)" +by (unfold Upair_def, blast) + +lemma UpairI1: "a : Upair(a,b)" +by simp + +lemma UpairI2: "b : Upair(a,b)" +by simp + +lemma UpairE: + "[| a : Upair(b,c); a=b ==> P; a=c ==> P |] ==> P" +apply simp +apply blast +done + +(*** Rules for binary union -- Un -- defined via Upair ***) + +lemma Un_iff [simp]: "c : A Un B <-> (c:A | c:B)" +apply (simp add: Un_def) +apply (blast intro: UpairI1 UpairI2 elim: UpairE) +done + +lemma UnI1: "c : A ==> c : A Un B" +by simp + +lemma UnI2: "c : B ==> c : A Un B" +by simp + +lemma UnE [elim!]: "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P" +apply simp +apply blast +done + +(*Stronger version of the rule above*) +lemma UnE': "[| c : A Un B; c:A ==> P; [| c:B; c~:A |] ==> P |] ==> P" +apply simp +apply blast +done + +(*Classical introduction rule: no commitment to A vs B*) +lemma UnCI [intro!]: "(c ~: B ==> c : A) ==> c : A Un B" +apply simp +apply blast +done + + +(*** Rules for small intersection -- Int -- defined via Upair ***) + +lemma Int_iff [simp]: "c : A Int B <-> (c:A & c:B)" +apply (unfold Int_def) +apply (blast intro: UpairI1 UpairI2 elim: UpairE) +done + +lemma IntI [intro!]: "[| c : A; c : B |] ==> c : A Int B" +by simp + +lemma IntD1: "c : A Int B ==> c : A" +by simp + +lemma IntD2: "c : A Int B ==> c : B" +by simp + +lemma IntE [elim!]: "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P" +by simp + + +(*** Rules for set difference -- defined via Upair ***) + +lemma Diff_iff [simp]: "c : A-B <-> (c:A & c~:B)" +by (unfold Diff_def, blast) + +lemma DiffI [intro!]: "[| c : A; c ~: B |] ==> c : A - B" +by simp + +lemma DiffD1: "c : A - B ==> c : A" +by simp + +lemma DiffD2: "c : A - B ==> c ~: B" +by simp + +lemma DiffE [elim!]: "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P" +by simp + + +(*** Rules for cons -- defined via Un and Upair ***) + +lemma cons_iff [simp]: "a : cons(b,A) <-> (a=b | a:A)" +apply (unfold cons_def) +apply (blast intro: UpairI1 UpairI2 elim: UpairE) +done + +(*risky as a typechecking rule, but solves otherwise unconstrained goals of +the form x : ?A*) +lemma consI1 [simp,TC]: "a : cons(a,B)" +by simp + + +lemma consI2: "a : B ==> a : cons(b,B)" +by simp + +lemma consE [elim!]: + "[| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P" +apply simp +apply blast +done + +(*Stronger version of the rule above*) +lemma consE': + "[| a : cons(b,A); a=b ==> P; [| a:A; a~=b |] ==> P |] ==> P" +apply simp +apply blast +done + +(*Classical introduction rule*) +lemma consCI [intro!]: "(a~:B ==> a=b) ==> a: cons(b,B)" +apply simp +apply blast +done + +lemma cons_not_0 [simp]: "cons(a,B) ~= 0" +by (blast elim: equalityE) + +lemmas cons_neq_0 = cons_not_0 [THEN notE, standard] + +declare cons_not_0 [THEN not_sym, simp] + + +(*** Singletons - using cons ***) + +lemma singleton_iff: "a : {b} <-> a=b" +by simp + +lemma singletonI [intro!]: "a : {a}" +by (rule consI1) + +lemmas singletonE = singleton_iff [THEN iffD1, elim_format, standard, elim!] + + +(*** Rules for Descriptions ***) + +lemma the_equality [intro]: + "[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a" +apply (unfold the_def) +apply (fast dest: subst) +done + +(* Only use this if you already know EX!x. P(x) *) +lemma the_equality2: "[| EX! x. P(x); P(a) |] ==> (THE x. P(x)) = a" +by blast + +lemma theI: "EX! x. P(x) ==> P(THE x. P(x))" +apply (erule ex1E) +apply (subst the_equality) +apply (blast+) +done + +(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then + (THE x.P(x)) rewrites to (THE x. Q(x)) *) + +(*If it's "undefined", it's zero!*) +lemma the_0: "~ (EX! x. P(x)) ==> (THE x. P(x))=0" +apply (unfold the_def) +apply (blast elim!: ReplaceE) +done + +(*Easier to apply than theI: conclusion has only one occurrence of P*) +lemma theI2: + assumes p1: "~ Q(0) ==> EX! x. P(x)" + and p2: "!!x. P(x) ==> Q(x)" + shows "Q(THE x. P(x))" +apply (rule classical) +apply (rule p2) +apply (rule theI) +apply (rule classical) +apply (rule p1) +apply (erule the_0 [THEN subst], assumption) +done + +(*** if -- a conditional expression for formulae ***) + +lemma if_true [simp]: "(if True then a else b) = a" +by (unfold if_def, blast) + +lemma if_false [simp]: "(if False then a else b) = b" +by (unfold if_def, blast) + +(*Never use with case splitting, or if P is known to be true or false*) +lemma if_cong: + "[| P<->Q; Q ==> a=c; ~Q ==> b=d |] + ==> (if P then a else b) = (if Q then c else d)" +by (simp add: if_def cong add: conj_cong) + +(*Prevents simplification of x and y: faster and allows the execution + of functional programs. NOW THE DEFAULT.*) +lemma if_weak_cong: "P<->Q ==> (if P then x else y) = (if Q then x else y)" +by simp + +(*Not needed for rewriting, since P would rewrite to True anyway*) +lemma if_P: "P ==> (if P then a else b) = a" +by (unfold if_def, blast) + +(*Not needed for rewriting, since P would rewrite to False anyway*) +lemma if_not_P: "~P ==> (if P then a else b) = b" +by (unfold if_def, blast) + +lemma split_if: "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))" +(*no case_tac yet!*) +apply (rule_tac P=Q in case_split_thm, simp_all) +done + +(** Rewrite rules for boolean case-splitting: faster than + addsplits[split_if] +**) + +lemmas split_if_eq1 = split_if [of "%x. x = b", standard] +lemmas split_if_eq2 = split_if [of "%x. a = x", standard] + +lemmas split_if_mem1 = split_if [of "%x. x : b", standard] +lemmas split_if_mem2 = split_if [of "%x. a : x", standard] + +lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2 + +(*Logically equivalent to split_if_mem2*) +lemma if_iff: "a: (if P then x else y) <-> P & a:x | ~P & a:y" +by (simp split add: split_if) + +lemma if_type [TC]: + "[| P ==> a: A; ~P ==> b: A |] ==> (if P then a else b): A" +by (simp split add: split_if) + + +(*** Foundation lemmas ***) + +(*was called mem_anti_sym*) +lemma mem_asym: "[| a:b; ~P ==> b:a |] ==> P" +apply (rule classical) +apply (rule_tac A1 = "{a,b}" in foundation [THEN disjE]) +apply (blast elim!: equalityE)+ +done + +(*was called mem_anti_refl*) +lemma mem_irrefl: "a:a ==> P" +by (blast intro: mem_asym) + +(*mem_irrefl should NOT be added to default databases: + it would be tried on most goals, making proofs slower!*) + +lemma mem_not_refl: "a ~: a" +apply (rule notI) +apply (erule mem_irrefl) +done + +(*Good for proving inequalities by rewriting*) +lemma mem_imp_not_eq: "a:A ==> a ~= A" +by (blast elim!: mem_irrefl) + +(*** Rules for succ ***) + +lemma succ_iff: "i : succ(j) <-> i=j | i:j" +by (unfold succ_def, blast) + +lemma succI1 [simp]: "i : succ(i)" +by (simp add: succ_iff) + +lemma succI2: "i : j ==> i : succ(j)" +by (simp add: succ_iff) + +lemma succE [elim!]: + "[| i : succ(j); i=j ==> P; i:j ==> P |] ==> P" +apply (simp add: succ_iff, blast) +done + +(*Classical introduction rule*) +lemma succCI [intro!]: "(i~:j ==> i=j) ==> i: succ(j)" +by (simp add: succ_iff, blast) + +lemma succ_not_0 [simp]: "succ(n) ~= 0" +by (blast elim!: equalityE) + +lemmas succ_neq_0 = succ_not_0 [THEN notE, standard, elim!] + +declare succ_not_0 [THEN not_sym, simp] +declare sym [THEN succ_neq_0, elim!] + +(* succ(c) <= B ==> c : B *) +lemmas succ_subsetD = succI1 [THEN [2] subsetD] + +(* succ(b) ~= b *) +lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym, standard] + +lemma succ_inject_iff [simp]: "succ(m) = succ(n) <-> m=n" +by (blast elim: mem_asym elim!: equalityE) + +lemmas succ_inject = succ_inject_iff [THEN iffD1, standard, dest!] + +ML +{* +val Pow_bottom = thm "Pow_bottom"; +val Pow_top = thm "Pow_top"; +val Upair_iff = thm "Upair_iff"; +val UpairI1 = thm "UpairI1"; +val UpairI2 = thm "UpairI2"; +val UpairE = thm "UpairE"; +val Un_iff = thm "Un_iff"; +val UnI1 = thm "UnI1"; +val UnI2 = thm "UnI2"; +val UnE = thm "UnE"; +val UnE' = thm "UnE'"; +val UnCI = thm "UnCI"; +val Int_iff = thm "Int_iff"; +val IntI = thm "IntI"; +val IntD1 = thm "IntD1"; +val IntD2 = thm "IntD2"; +val IntE = thm "IntE"; +val Diff_iff = thm "Diff_iff"; +val DiffI = thm "DiffI"; +val DiffD1 = thm "DiffD1"; +val DiffD2 = thm "DiffD2"; +val DiffE = thm "DiffE"; +val cons_iff = thm "cons_iff"; +val consI1 = thm "consI1"; +val consI2 = thm "consI2"; +val consE = thm "consE"; +val consE' = thm "consE'"; +val consCI = thm "consCI"; +val cons_not_0 = thm "cons_not_0"; +val cons_neq_0 = thm "cons_neq_0"; +val singleton_iff = thm "singleton_iff"; +val singletonI = thm "singletonI"; +val singletonE = thm "singletonE"; +val the_equality = thm "the_equality"; +val the_equality2 = thm "the_equality2"; +val theI = thm "theI"; +val the_0 = thm "the_0"; +val theI2 = thm "theI2"; +val if_true = thm "if_true"; +val if_false = thm "if_false"; +val if_cong = thm "if_cong"; +val if_weak_cong = thm "if_weak_cong"; +val if_P = thm "if_P"; +val if_not_P = thm "if_not_P"; +val split_if = thm "split_if"; +val split_if_eq1 = thm "split_if_eq1"; +val split_if_eq2 = thm "split_if_eq2"; +val split_if_mem1 = thm "split_if_mem1"; +val split_if_mem2 = thm "split_if_mem2"; +val if_iff = thm "if_iff"; +val if_type = thm "if_type"; +val mem_asym = thm "mem_asym"; +val mem_irrefl = thm "mem_irrefl"; +val mem_not_refl = thm "mem_not_refl"; +val mem_imp_not_eq = thm "mem_imp_not_eq"; +val succ_iff = thm "succ_iff"; +val succI1 = thm "succI1"; +val succI2 = thm "succI2"; +val succE = thm "succE"; +val succCI = thm "succCI"; +val succ_not_0 = thm "succ_not_0"; +val succ_neq_0 = thm "succ_neq_0"; +val succ_subsetD = thm "succ_subsetD"; +val succ_neq_self = thm "succ_neq_self"; +val succ_inject_iff = thm "succ_inject_iff"; +val succ_inject = thm "succ_inject"; + +val split_ifs = thms "split_ifs"; +*} + end