--- 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<n";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "zero_less_diff";
-Addsimps [zero_less_diff];
-
-
-(** Difference 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 [("m","natify(m)"),("n","natify(n)")] diff_induct 2);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [diff_cancel])));
-qed "diff_mult_distrib" ;
-
-Goal "k #* (m #- n) = (k #* m) #- (k #* n)";
-by (simp_tac
- (simpset() addsimps [inst "m" "k" mult_commute, diff_mult_distrib]) 1);
-qed "diff_mult_distrib2";
-
-
-(*** Remainder ***)
-
-(*We need m:nat even with natify*)
-Goal "[| 0<n; n le m; m:nat |] ==> 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<n ==> 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<n; n : nat |] ==> 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<n; n le m; m:nat |] ==> 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<n ==> 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<n; n : nat |] ==> 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<n; n le m; m:nat |] ==> 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<n; n le m; m:nat |] ==> 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<n" 1);
-(*case n le x*)
-by (asm_full_simp_tac
- (simpset() addsimps [not_lt_iff_le, add_assoc, mod_geq,
- div_termination RS ltD, add_diff_inverse]) 2);
-(*case x<n*)
-by (Asm_simp_tac 1);
-val lemma = result();
-
-Goal "(m div n)#*n #+ m mod n = natify(m)";
-by (subgoal_tac
- "(natify(m) div natify(n))#*natify(n) #+ natify(m) mod natify(n) = \
-\ natify(m)" 1);
-by (stac lemma 2);
-by Auto_tac;
-qed "mod_div_equality_natify";
-
-Goal "m: nat ==> (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<n; m:nat; n:nat |] \
-\ ==> 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)<n" 1);
-(* case succ(x) < n *)
-by (asm_simp_tac (simpset() addsimps [nat_le_refl RS lt_trans,
- succ_neq_self]) 2);
-by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq]) 2);
-(* case n le succ(x) *)
-by (asm_full_simp_tac (simpset() addsimps [mod_geq, not_lt_iff_le]) 1);
-by (etac leE 1);
-(*equality case*)
-by (asm_full_simp_tac (simpset() addsimps [diff_self_eq_0]) 2);
-by (asm_simp_tac (simpset() addsimps [mod_geq, div_termination RS ltD,
- diff_succ]) 1);
-val lemma = result();
-
-Goal "n:nat ==> \
-\ 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<n; n:nat |] ==> 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<n" 3);
-(*case x<n*)
-by (Asm_simp_tac 3);
-(*case n le x*)
-by (asm_full_simp_tac
- (simpset() addsimps [mod_geq, not_lt_iff_le, div_termination RS ltD]) 3);
-by Auto_tac;
-qed "mod_less_divisor";
-
-Goal "m mod 1 = 0";
-by (cut_inst_tac [("n","1")] mod_less_divisor 1);
-by Auto_tac;
-qed "mod_1_eq";
-Addsimps [mod_1_eq];
-
-Goal "b<2 ==> 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<j; 0<k; j:nat; k:nat |] ==> 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<j; 0<k; j:nat; k:nat |] ==> 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<k & m<n)";
-by (safe_tac (claset() addSIs [mult_lt_mono1]));
-by (etac natE 1);
-by Auto_tac;
-by (rtac (not_le_iff_lt RS iffD1) 1);
-by (dtac (not_le_iff_lt RSN (2,rev_iffD2)) 3);
-by (blast_tac (claset() addIs [mult_le_mono1]) 5);
-by Auto_tac;
-val lemma = result();
-
-Goal "(m#*k < n#*k) <-> (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 \\<longleftrightarrow> (0 < k \\<longrightarrow> 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<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n";
-by (eres_inst_tac [("i","m")] complete_induct 1);
-by (excluded_middle_tac "x<n" 1);
-by (asm_simp_tac (simpset() addsimps [div_less, zero_lt_mult_iff,
- mult_lt_mono2]) 2);
-by (asm_full_simp_tac
- (simpset() addsimps [not_lt_iff_le,
- zero_lt_mult_iff, le_refl RS mult_le_mono, div_geq,
- diff_mult_distrib2 RS sym,
- div_termination RS ltD]) 1);
-qed "div_cancel_raw";
-
-Goal "[| 0 < natify(n); 0 < natify(k) |] ==> (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<n" 1);
- by (asm_simp_tac
- (simpset() addsimps [mod_less, zero_lt_mult_iff, mult_lt_mono2]) 1);
-by (asm_full_simp_tac
- (simpset() addsimps [not_lt_iff_le,
- zero_lt_mult_iff, le_refl RS mult_le_mono, mod_geq,
- diff_mult_distrib2 RS sym,
- div_termination RS ltD]) 1);
-qed "mult_mod_distrib_raw";
-
-Goal "k #* (m mod n) = (k#*m) mod (k#*n)";
-by (cut_inst_tac [("k","natify(k)"),("m","natify(m)"),("n","natify(n)")]
- mult_mod_distrib_raw 1);
-by Auto_tac;
-qed "mod_mult_distrib2";
-
-Goal "(m mod n) #* k = (m#*k) mod (n#*k)";
-by (simp_tac (simpset() addsimps [mult_commute, mod_mult_distrib2]) 1);
-qed "mult_mod_distrib";
-
-Goal "n \\<in> 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 \\<in> 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<n; n: nat |] ==> 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<n) <-> (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";
-
-
-
--- 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<n"
+apply (rule_tac m = "m" and n = "n" in diff_induct)
+apply (simp_all (no_asm_simp))
+done
+
+
+(** Difference distributes over multiplication **)
+
+lemma diff_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] m = "natify (m) " and n = "natify (n) " in diff_induct)
+apply (simp_all add: diff_cancel)
+done
+
+lemma diff_mult_distrib2: "k #* (m #- n) = (k #* m) #- (k #* n)"
+apply (simp (no_asm) add: mult_commute [of k] diff_mult_distrib)
+done
+
+
+(*** Remainder ***)
+
+(*We need m:nat even with natify*)
+lemma div_termination: "[| 0<n; n le m; m:nat |] ==> 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<n ==> 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<n; n : nat |] ==> 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<n; n le m; m:nat |] ==> 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<n ==> 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<n; n : nat |] ==> 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<n; n le m; m:nat |] ==> 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<n; n le m; m:nat |] ==> 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<n")
+txt{*case x<n*}
+apply (simp (no_asm_simp))
+txt{*case n le x*}
+apply (simp add: not_lt_iff_le add_assoc mod_geq div_termination [THEN ltD] add_diff_inverse)
+done
+
+lemma mod_div_equality_natify: "(m div n)#*n #+ m mod n = natify(m)"
+apply (subgoal_tac " (natify (m) div natify (n))#*natify (n) #+ natify (m) mod natify (n) = natify (m) ")
+apply force
+apply (subst mod_div_lemma, auto)
+done
+
+lemma mod_div_equality: "m: nat ==> (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<n; m:nat; n:nat |]
+ ==> 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) <n")
+txt{* case succ(x) < n *}
+ apply (simp (no_asm_simp) add: nat_le_refl [THEN lt_trans] succ_neq_self)
+ apply (simp add: ltD [THEN mem_imp_not_eq])
+txt{* case n le succ(x) *}
+apply (simp add: mod_geq not_lt_iff_le)
+apply (erule leE)
+ apply (simp (no_asm_simp) add: mod_geq div_termination [THEN ltD] diff_succ)
+txt{*equality case*}
+apply (simp add: diff_self_eq_0)
+done
+
+lemma mod_succ:
+ "n:nat ==> 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<n; n:nat |] ==> 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<n", auto)
+txt{* case n le x*}
+apply (simp add: mod_geq not_lt_iff_le div_termination [THEN ltD])
+done
+
+lemma mod_1_eq [simp]: "m mod 1 = 0"
+by (cut_tac n = "1" in mod_less_divisor, auto)
+
+lemma mod2_cases: "b<2 ==> 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<j; 0<k; j:nat; k:nat |] ==> 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<j; 0<k; j:nat; k:nat |] ==> 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<k & m<n)"
+apply (safe intro!: mult_lt_mono1)
+apply (erule natE, auto)
+apply (rule not_le_iff_lt [THEN iffD1])
+apply (drule_tac [3] not_le_iff_lt [THEN [2] rev_iffD2])
+prefer 5 apply (blast intro: mult_le_mono1, auto)
+done
+
+lemma mult_less_cancel2 [simp]:
+ "(m#*k < n#*k) <-> (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 \<longleftrightarrow> (0 < k \<longrightarrow> 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<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n"
+apply (erule_tac i = "m" in complete_induct)
+apply (case_tac "x<n")
+ apply (simp add: div_less zero_lt_mult_iff mult_lt_mono2)
+apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono]
+ div_geq diff_mult_distrib2 [symmetric] div_termination [THEN ltD])
+done
+
+lemma div_cancel:
+ "[| 0 < natify(n); 0 < natify(k) |] ==> (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<n")
+ apply (simp (no_asm_simp) add: mod_less zero_lt_mult_iff mult_lt_mono2)
+apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono]
+ mod_geq diff_mult_distrib2 [symmetric] div_termination [THEN ltD])
+done
+
+lemma mod_mult_distrib2: "k #* (m mod n) = (k#*m) mod (k#*n)"
+apply (cut_tac k = "natify (k) " and m = "natify (m)" and n = "natify (n)"
+ in mult_mod_distrib_raw)
+apply auto
+done
+
+lemma mult_mod_distrib: "(m mod n) #* k = (m#*k) mod (n#*k)"
+apply (simp (no_asm) add: mult_commute mod_mult_distrib2)
+done
+
+lemma mod_add_self2_raw: "n \<in> 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 \<in> 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<n; n: nat |] ==> 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<n) <-> (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<b |] ==> 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
--- 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"
--- 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
--- 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 |] ==> <a;b> <= <c;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";
+
+
--- 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" ("<(_;/ _)>")
--- 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;
--- 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. <a,y>: r)"
-by (unfold domain_def, blast)
+(** cons; Finite Sets **)
-lemma domainI [intro]: "<a,b>: r ==> a: domain(r)"
-by (unfold domain_def, blast)
-
-lemma domainE [elim!]:
- "[| a : domain(r); !!y. <a,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]: "<a,b>: r ==> b : range(r)"
-apply (unfold range_def)
-apply (erule converseI [THEN domainI])
-done
-
-lemma rangeE [elim!]: "[| b : range(r); !!x. <x,b>: 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: "<a,b>: r ==> a : field(r)"
-by (unfold field_def, blast)
-
-lemma fieldI2: "<a,b>: r ==> b : field(r)"
-by (unfold field_def, blast)
-
-lemma fieldCI [intro]:
- "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
-apply (unfold field_def, blast)
-done
-
-lemma fieldE [elim!]:
- "[| a : field(r);
- !!x. <a,x>: r ==> P;
- !!x. <x,a>: 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. <x,b>:r)"
-by (unfold image_def, blast)
-
-lemma image_singleton_iff: "b : r``{a} <-> <a,b>:r"
-by (rule image_iff [THEN iff_trans], blast)
-
-lemma imageI [intro]: "[| <a,b>: r; a:A |] ==> b : r``A"
-by (unfold image_def, blast)
-
-lemma imageE [elim!]:
- "[| b: r``A; !!x.[| <x,b>: 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. <a,y>:r)"
-apply (unfold vimage_def image_def converse_def, blast)
-done
-
-lemma vimage_singleton_iff: "a : r-``{b} <-> <a,b>:r"
-by (rule vimage_iff [THEN iff_trans], blast)
-
-lemma vimageI [intro]: "[| <a,b>: 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.[| <a,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: "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"
+lemma subset_cons_iff: "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"
by blast
-lemma range_Diff_eq: "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = 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. <a,y>: r)"
+by (unfold domain_def, blast)
+
+lemma domainI [intro]: "<a,b>: r ==> a: domain(r)"
+by (unfold domain_def, blast)
+
+lemma domainE [elim!]:
+ "[| a : domain(r); !!y. <a,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]: "<a,b>: r ==> b : range(r)"
+apply (unfold range_def)
+apply (erule converseI [THEN domainI])
+done
+
+lemma rangeE [elim!]: "[| b : range(r); !!x. <x,b>: 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: "<a,b>: r ==> a : field(r)"
+by (unfold field_def, blast)
+
+lemma fieldI2: "<a,b>: r ==> b : field(r)"
+by (unfold field_def, blast)
+
+lemma fieldCI [intro]:
+ "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
+apply (unfold field_def, blast)
+done
+
+lemma fieldE [elim!]:
+ "[| a : field(r);
+ !!x. <a,x>: r ==> P;
+ !!x. <x,a>: 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: "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"
+by blast
+
+lemma range_Diff_eq: "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)"
+by blast
+
+
+(*** Image of a set under a function/relation ***)
+
+lemma image_iff: "b : r``A <-> (EX x:A. <x,b>:r)"
+by (unfold image_def, blast)
+
+lemma image_singleton_iff: "b : r``{a} <-> <a,b>:r"
+by (rule image_iff [THEN iff_trans], blast)
+
+lemma imageI [intro]: "[| <a,b>: r; a:A |] ==> b : r``A"
+by (unfold image_def, blast)
+
+lemma imageE [elim!]:
+ "[| b: r``A; !!x.[| <x,b>: 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. <a,y>:r)"
+by (unfold vimage_def image_def converse_def, blast)
+
+lemma vimage_singleton_iff: "a : r-``{b} <-> <a,b>:r"
+by (rule vimage_iff [THEN iff_trans], blast)
+
+lemma vimageI [intro]: "[| <a,b>: r; b:B |] ==> a : r-``B"
+by (unfold vimage_def, blast)
+
+lemma vimageE [elim!]:
+ "[| a: r-``B; !!x.[| <a,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(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>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";
--- 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 \<in> nat; b \<in> 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 \<in> 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) \<in> nat"
apply (subgoal_tac "gcd (natify (m) , natify (n)) \<in> 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 \<in> 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 \<in> 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 \<in> prime; ~ (p dvd n); n \<in> 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
--- 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 |] ==> <a;b> <= <c;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. <x,y>:r ==> <x,y>: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. <x,y>:r ==> <x,y>: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]);
--- 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. <x,y>:r ==> <x,y>:s; A<=B |] ==> r``A <= s``B"
+by blast
+
+lemma vimage_pair_mono:
+ "[| !! x y. <x,y>:r ==> <x,y>: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
--- 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];
-
--- 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
--- 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];
--- 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