src/ZF/AC/WO6_WO1.ML
author lcp
Fri, 14 Apr 1995 11:25:23 +0200
changeset 1057 5097aa914449
parent 1041 6664d0b54d0f
child 1071 96dfc9977bf5
permissions -rw-r--r--
Renamed diff_sing_lepoll to Diff_sing_lepoll.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
     1
(*  Title: 	ZF/AC/WO6_WO1.ML
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
     2
    ID:         $Id$
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
     3
    Author: 	Krzysztof Gr`abczewski
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
     4
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
     5
The proof of "WO6 ==> WO1".  Simplified by L C Paulson.
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
     6
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
     7
From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin,
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
     8
pages 2-5
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
     9
*)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    10
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    11
open WO6_WO1;
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    12
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    13
goal OrderType.thy 
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    14
      "!!i j k. [| k < i++j;  Ord(i);  Ord(j) |] ==>  \
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    15
\                  k < i  |  (~ k<i & k = i ++ (k--i) & (k--i)<j)";
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    16
by (res_inst_tac [("i","k"),("j","i")] Ord_linear2 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    17
by (dtac odiff_lt_mono2 4 THEN assume_tac 4);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    18
by (asm_full_simp_tac
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    19
    (ZF_ss addsimps [oadd_odiff_inverse, odiff_oadd_inverse]) 4);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    20
by (safe_tac (ZF_cs addSEs [lt_Ord]));
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    21
val lt_oadd_odiff_disj = result();
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    22
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    23
(*The corresponding elimination rule*)
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    24
val lt_oadd_odiff_cases = rule_by_tactic (safe_tac ZF_cs)
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    25
                                         (lt_oadd_odiff_disj RS disjE);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    26
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    27
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    28
(* The most complicated part of the proof - lemma ii - p. 2-4		  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    29
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    30
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    31
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    32
(* some properties of relation uu(beta, gamma, delta) - p. 2		  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    33
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    34
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    35
goalw thy [uu_def] "domain(uu(f,b,g,d)) <= f`b";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    36
by (fast_tac ZF_cs 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    37
val domain_uu_subset = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    38
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    39
goal thy "!! a. ALL b<a. f`b lepoll m ==> \
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    40
\               ALL b<a. ALL g<a. ALL d<a. domain(uu(f,b,g,d)) lepoll m";
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    41
by (fast_tac (AC_cs addSEs
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    42
	[domain_uu_subset RS subset_imp_lepoll RS lepoll_trans]) 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    43
val quant_domain_uu_lepoll_m = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    44
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    45
goalw thy [uu_def] "uu(f,b,g,d) <= f`b * f`g";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    46
by (fast_tac ZF_cs 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    47
val uu_subset1 = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    48
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    49
goalw thy [uu_def] "uu(f,b,g,d) <= f`d";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    50
by (fast_tac ZF_cs 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    51
val uu_subset2 = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    52
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    53
goal thy "!! a. [| ALL b<a. f`b lepoll m;  d<a |] ==> uu(f,b,g,d) lepoll m";
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    54
by (fast_tac (AC_cs
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    55
	addSEs [uu_subset2 RS subset_imp_lepoll RS lepoll_trans]) 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    56
val uu_lepoll_m = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    57
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    58
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    59
(* Two cases for lemma ii 						  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    60
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    61
goalw thy [lesspoll_def] 
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    62
  "!! a f u. ALL b<a. ALL g<a. ALL d<a. u(f,b,g,d) lepoll m ==>  \
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    63
\            (ALL b<a. f`b ~= 0 --> (EX g<a. EX d<a. u(f,b,g,d) ~= 0 &  \
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    64
\		           		u(f,b,g,d) lesspoll m)) |  \
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    65
\            (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 -->  \
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    66
\		           		u(f,b,g,d) eqpoll m))";
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    67
by (asm_simp_tac OrdQuant_ss 1);
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    68
by (fast_tac AC_cs 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    69
val cases = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    70
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    71
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    72
(* Lemmas used in both cases						  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    73
(* ********************************************************************** *)
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    74
goal thy "!!a C. Ord(a) ==> (UN b<a++a. C(b)) = (UN b<a. C(b) Un C(a++b))";
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    75
by (fast_tac (AC_cs addSIs [equalityI] addIs [ltI] 
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    76
                    addSDs [lt_oadd_disj]
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    77
                    addSEs [lt_oadd1, oadd_lt_mono2]) 1);
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    78
val UN_oadd = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    79
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    80
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    81
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    82
(* Case 1 : lemmas							  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    83
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    84
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    85
goalw thy [vv1_def] "vv1(f,m,b) <= f`b";
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    86
by (rtac (letI RS letI) 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    87
by (split_tac [expand_if] 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    88
by (simp_tac (ZF_ss addsimps [domain_uu_subset]) 1);
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    89
val vv1_subset = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    90
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    91
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    92
(* Case 1 : Union of images is the whole "y"				  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    93
(* ********************************************************************** *)
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    94
goalw thy [gg1_def]
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    95
  "!! a f y. [| Ord(a);  m:nat |] ==>  	\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    96
\	     (UN b<a++a. gg1(f,a,m)`b) = (UN b<a. f`b)";
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    97
by (asm_simp_tac
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    98
    (OrdQuant_ss addsimps [UN_oadd, lt_oadd1,
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
    99
			   oadd_le_self RS le_imp_not_lt, lt_Ord,
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   100
			   odiff_oadd_inverse, ltD,
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   101
			   vv1_subset RS Diff_partition, ww1_def]) 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   102
val UN_gg1_eq = result();
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   103
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   104
goal thy "domain(gg1(f,a,m)) = a++a";
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   105
by (simp_tac (ZF_ss addsimps [lam_funtype RS domain_of_fun, gg1_def]) 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   106
val domain_gg1 = result();
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   107
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   108
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   109
(* every value of defined function is less than or equipollent to m	  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   110
(* ********************************************************************** *)
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   111
goal thy "!!a b. [| P(a, b);  Ord(a);  Ord(b);  \
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   112
\		Least_a = (LEAST a. EX x. Ord(x) & P(a, x)) |]  \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   113
\		==> P(Least_a, LEAST b. P(Least_a, b))";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   114
by (eresolve_tac [ssubst] 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   115
by (res_inst_tac [("Q","%z. P(z, LEAST b. P(z, b))")] LeastI2 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   116
by (REPEAT (fast_tac (ZF_cs addSEs [LeastI]) 1));
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   117
val nested_LeastI = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   118
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   119
val nested_Least_instance = 
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   120
   standard
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   121
     (read_instantiate 
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   122
	[("P","%g d. domain(uu(f,b,g,d)) ~= 0 &  \
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   123
\		domain(uu(f,b,g,d)) lepoll m")] nested_LeastI);
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   124
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   125
goalw thy [gg1_def]
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   126
    "!!a. [| Ord(a);  m:nat;  \
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   127
\	     ALL b<a. f`b ~=0 -->  					\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   128
\	     (EX g<a. EX d<a. domain(uu(f,b,g,d)) ~= 0  &  		\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   129
\	                      domain(uu(f,b,g,d)) lepoll m);    	\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   130
\            ALL b<a. f`b lepoll succ(m);  b<a++a			\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   131
\	  |] ==> gg1(f,a,m)`b lepoll m";
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   132
by (asm_simp_tac OrdQuant_ss 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   133
by (safe_tac (OrdQuant_cs addSEs [lt_oadd_odiff_cases]));
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   134
(*Case b<a   : show vv1(f,m,b) lepoll m *)
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   135
by (asm_simp_tac (ZF_ss addsimps [vv1_def, Let_def] 
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   136
                        setloop split_tac [expand_if]) 1);
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   137
by (fast_tac (AC_cs addIs [nested_Least_instance RS conjunct2]
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   138
		addSEs [lt_Ord]
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   139
		addSIs [empty_lepollI]) 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   140
(*Case a le b: show ww1(f,m,b--a) lepoll m *)
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   141
by (asm_simp_tac (ZF_ss addsimps [ww1_def]) 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   142
by (excluded_middle_tac "f`(b--a) = 0" 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   143
by (asm_simp_tac (OrdQuant_ss addsimps [empty_lepollI]) 2);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   144
by (resolve_tac [Diff_lepoll] 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   145
by (fast_tac AC_cs 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   146
by (rtac vv1_subset 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   147
by (dtac (ospec RS mp) 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   148
by (REPEAT (eresolve_tac [asm_rl, oexE] 1));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   149
by (asm_simp_tac (ZF_ss
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   150
	addsimps [vv1_def, Let_def, lt_Ord, 
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   151
		  nested_Least_instance RS conjunct1]) 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   152
val gg1_lepoll_m = result();
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   153
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   154
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   155
(* Case 2 : lemmas							  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   156
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   157
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   158
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   159
(* Case 2 : vv2_subset							  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   160
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   161
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   162
goalw thy [uu_def] "!!f. [| b<a;  g<a;  f`b~=0;  f`g~=0;  \
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   163
\			    y*y <= y;  (UN b<a. f`b)=y  \
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   164
\			 |] ==> EX d<a. uu(f,b,g,d) ~= 0";
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   165
by (fast_tac (AC_cs addSIs [not_emptyI] 
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   166
		addSDs [SigmaI RSN (2, subsetD)]
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   167
		addSEs [not_emptyE]) 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   168
val ex_d_uu_not_empty = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   169
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   170
goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0;  \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   171
\			y*y<=y;	(UN b<a. f`b)=y |]  \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   172
\		==> uu(f,b,g,LEAST d. (uu(f,b,g,d) ~= 0)) ~= 0";
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   173
by (dresolve_tac [ex_d_uu_not_empty] 1 THEN REPEAT (assume_tac 1));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   174
by (fast_tac (AC_cs addSEs [LeastI, lt_Ord]) 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   175
val uu_not_empty = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   176
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   177
goal ZF.thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0";
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   178
by (REPEAT (eresolve_tac [asm_rl, not_emptyE, subsetD RS SigmaE, 
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   179
		sym RSN (2, subst_elem) RS domainI RS not_emptyI] 1));
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   180
val not_empty_rel_imp_domain = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   181
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   182
goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0;  \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   183
\			y*y <= y; (UN b<a. f`b)=y |]  \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   184
\		==> (LEAST d. uu(f,b,g,d) ~= 0) < a";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   185
by (eresolve_tac [ex_d_uu_not_empty RS oexE] 1
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   186
	THEN REPEAT (assume_tac 1));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   187
by (resolve_tac [Least_le RS lt_trans1] 1
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   188
	THEN (REPEAT (ares_tac [lt_Ord] 1)));
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   189
val Least_uu_not_empty_lt_a = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   190
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   191
goal ZF.thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}";
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   192
by (fast_tac ZF_cs 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   193
val subset_Diff_sing = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   194
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   195
(*Could this be proved more directly?*)
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   196
goal thy "!!A B. [| A lepoll m; m lepoll B; B <= A; m:nat |] ==> A=B";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   197
by (eresolve_tac [natE] 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   198
by (fast_tac (AC_cs addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   199
by (hyp_subst_tac 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   200
by (resolve_tac [equalityI] 1);
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   201
by (assume_tac 2);
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   202
by (resolve_tac [subsetI] 1);
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   203
by (excluded_middle_tac "?P" 1 THEN (assume_tac 2));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   204
by (eresolve_tac [subset_Diff_sing RS subset_imp_lepoll RSN (2, 
1057
5097aa914449 Renamed diff_sing_lepoll to Diff_sing_lepoll.
lcp
parents: 1041
diff changeset
   205
		Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS 
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   206
		succ_lepoll_natE] 1
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   207
	THEN REPEAT (assume_tac 1));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   208
val supset_lepoll_imp_eq = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   209
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   210
goal thy
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   211
	"!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 -->  \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   212
\	domain(uu(f, b, g, d)) eqpoll succ(m);  \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   213
\	ALL b<a. f`b lepoll succ(m); y*y <= y;  \
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   214
\	(UN b<a. f`b)=y; b<a; g<a; d<a; f`b~=0; f`g~=0; m:nat; s:f`b |]  \
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   215
\	 ==> uu(f,b,g,LEAST d. uu(f,b,g,d)~=0) : f`b -> f`g";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   216
by (eres_inst_tac [("x","g")] oallE 1 THEN (contr_tac 2));
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   217
by (eres_inst_tac [("P","%z. ?QQ(z) ~= 0 --> ?RR(z)")] oallE 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   218
by (eresolve_tac [impE] 1);
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   219
by (eresolve_tac [uu_not_empty RS (uu_subset1 RS not_empty_rel_imp_domain)] 1
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   220
	THEN REPEAT (assume_tac 1));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   221
by (eresolve_tac [Least_uu_not_empty_lt_a RSN (2, notE)] 2
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   222
	THEN (TRYALL assume_tac));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   223
by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS 
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   224
	(Least_uu_not_empty_lt_a RSN (2, uu_lepoll_m) RSN (2, 
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   225
	uu_subset1 RSN (4, rel_is_fun)))] 1
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   226
	THEN (TRYALL assume_tac));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   227
by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RSN (2, 
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   228
		supset_lepoll_imp_eq)] 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   229
by (REPEAT (fast_tac (AC_cs addSIs [domain_uu_subset, nat_succI]) 1));
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   230
val uu_Least_is_fun = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   231
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   232
goalw thy [vv2_def]
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   233
    "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 -->		\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   234
\	     domain(uu(f, b, g, d)) eqpoll succ(m);			\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   235
\	     ALL b<a. f`b lepoll succ(m); y*y <= y;			\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   236
\	     (UN b<a. f`b)=y;  b<a;  g<a;  m:nat;  s:f`b		\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   237
\	   |] ==> vv2(f,b,g,s) <= f`g";
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   238
by (split_tac [expand_if] 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   239
by (fast_tac (FOL_cs addSEs [uu_Least_is_fun]
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   240
	             addSIs [empty_subsetI, not_emptyI, 
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   241
			     singleton_subsetI, apply_type]) 1);
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   242
val vv2_subset = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   243
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   244
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   245
(* Case 2 : Union of images is the whole "y"				  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   246
(* ********************************************************************** *)
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   247
goalw thy [gg2_def]
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   248
    "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 -->  		\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   249
\	     domain(uu(f,b,g,d)) eqpoll succ(m);  			\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   250
\	     ALL b<a. f`b lepoll succ(m); y*y<=y;  			\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   251
\	     (UN b<a.f`b)=y;  Ord(a);  m:nat;  s:f`b;  b<a		\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   252
\	  |] ==> (UN g<a++a. gg2(f,a,b,s) ` g) = y";
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   253
bd sym 1;
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   254
by (asm_simp_tac
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   255
    (OrdQuant_ss addsimps [UN_oadd, lt_oadd1,
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   256
			   oadd_le_self RS le_imp_not_lt, lt_Ord,
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   257
			   odiff_oadd_inverse, ww2_def,
1057
5097aa914449 Renamed diff_sing_lepoll to Diff_sing_lepoll.
lcp
parents: 1041
diff changeset
   258
			   vv2_subset RS Diff_partition]) 1);
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   259
val UN_gg2_eq = result();
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   260
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   261
goal thy "domain(gg2(f,a,b,s)) = a++a";
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   262
by (simp_tac (ZF_ss addsimps [lam_funtype RS domain_of_fun, gg2_def]) 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   263
val domain_gg2 = result();
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   264
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   265
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   266
(* every value of defined function is less than or equipollent to m	  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   267
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   268
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   269
goalw thy [vv2_def]
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   270
    "!!m. [| m:nat; m~=0 |] ==> vv2(f,b,g,s) lepoll m";
1057
5097aa914449 Renamed diff_sing_lepoll to Diff_sing_lepoll.
lcp
parents: 1041
diff changeset
   271
by (asm_simp_tac (OrdQuant_ss addsimps [empty_lepollI]
5097aa914449 Renamed diff_sing_lepoll to Diff_sing_lepoll.
lcp
parents: 1041
diff changeset
   272
                              setloop split_tac [expand_if]) 1);
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   273
by (fast_tac (AC_cs
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   274
	addSDs [le_imp_subset RS subset_imp_lepoll RS lepoll_0_is_0]
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   275
	addSIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans,
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   276
		not_lt_imp_le RS le_imp_subset RS subset_imp_lepoll,
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   277
		nat_into_Ord, nat_1I]) 1);
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   278
val vv2_lepoll = result();
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   279
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   280
goalw thy [ww2_def]
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   281
    "!!m. [| ALL b<a. f`b lepoll succ(m);  g<a;  m:nat;  vv2(f,b,g,d) <= f`g  \
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   282
\	  |] ==> ww2(f,b,g,d) lepoll m";
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   283
by (excluded_middle_tac "f`g = 0" 1);
1057
5097aa914449 Renamed diff_sing_lepoll to Diff_sing_lepoll.
lcp
parents: 1041
diff changeset
   284
by (asm_simp_tac (OrdQuant_ss addsimps [empty_lepollI]) 2);
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   285
by (dresolve_tac [ospec] 1 THEN (assume_tac 1));
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   286
by (resolve_tac [Diff_lepoll] 1
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   287
	THEN (TRYALL assume_tac));
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   288
by (asm_simp_tac (OrdQuant_ss addsimps [vv2_def, expand_if, not_emptyI]) 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   289
val ww2_lepoll = result();
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   290
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   291
goalw thy [gg2_def]
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   292
    "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 -->		\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   293
\	     domain(uu(f,b,g,d)) eqpoll succ(m);			\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   294
\	     ALL b<a. f`b lepoll succ(m);  y*y <= y;			\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   295
\	     (UN b<a. f`b)=y;  b<a;  s:f`b;  m:nat;  m~= 0;  g<a++a	\
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   296
\         |] ==> gg2(f,a,b,s) ` g lepoll m";
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   297
by (asm_simp_tac OrdQuant_ss 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   298
by (safe_tac (OrdQuant_cs addSEs [lt_oadd_odiff_cases, lt_Ord2]));
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   299
by (asm_simp_tac (OrdQuant_ss addsimps [vv2_lepoll]) 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   300
by (asm_simp_tac (ZF_ss addsimps [ww2_lepoll, vv2_subset]) 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   301
val gg2_lepoll_m = result();
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   302
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   303
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   304
(* lemma ii	 							  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   305
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   306
goalw thy [NN_def]
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   307
	"!!y. [| succ(m) : NN(y); y*y <= y; m:nat; m~=0 |] ==> m : NN(y)";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   308
by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1));
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   309
by (resolve_tac [quant_domain_uu_lepoll_m RS cases RS disjE] 1
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   310
    THEN (assume_tac 1));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   311
(* case 1 *)
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   312
by (asm_full_simp_tac (ZF_ss addsimps [lesspoll_succ_iff]) 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   313
by (res_inst_tac [("x","a++a")] exI 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   314
by (fast_tac (OrdQuant_cs addSIs [Ord_oadd, domain_gg1, UN_gg1_eq, 
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   315
				  gg1_lepoll_m]) 1);
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   316
(* case 2 *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   317
by (REPEAT (eresolve_tac [oexE, conjE] 1));
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   318
by (res_inst_tac [("A","f`?B")] not_emptyE 1 THEN (assume_tac 1));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   319
by (resolve_tac [CollectI] 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   320
by (eresolve_tac [succ_natD] 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   321
by (res_inst_tac [("x","a++a")] exI 1);
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   322
by (res_inst_tac [("x","gg2(f,a,b,x)")] exI 1);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   323
(*Calling fast_tac might get rid of the res_inst_tac calls, but it
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   324
  is just too slow.*)
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   325
by (asm_simp_tac (OrdQuant_ss addsimps 
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   326
		  [Ord_oadd, domain_gg2, UN_gg2_eq, gg2_lepoll_m]) 1);
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   327
val lemma_ii = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   328
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   329
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   330
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   331
(* lemma iv - p. 4 :                                                      *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   332
(* For every set x there is a set y such that   x Un (y * y) <= y         *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   333
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   334
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   335
(* the quantifier ALL looks inelegant but makes the proofs shorter  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   336
(* (used only in the following two lemmas)                          *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   337
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   338
goal thy "ALL n:nat. rec(n, x, %k r. r Un r*r) <=  \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   339
\                    rec(succ(n), x, %k r. r Un r*r)";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   340
by (fast_tac (ZF_cs addIs [rec_succ RS ssubst]) 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   341
val z_n_subset_z_succ_n = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   342
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   343
goal thy "!!n. [| ALL n:nat. f(n)<=f(succ(n)); n le m; n : nat; m: nat |]  \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   344
\              ==> f(n)<=f(m)";
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   345
by (res_inst_tac [("P","n le m")] impE 1 THEN (REPEAT (assume_tac 2)));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   346
by (res_inst_tac [("P","%z. n le z --> f(n) <= f(z)")] nat_induct 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   347
by (REPEAT (fast_tac lt_cs 1));
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   348
val le_subsets = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   349
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   350
goal thy "!!n m. [| n le m; m:nat |] ==>  \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   351
\	rec(n, x, %k r. r Un r*r) <= rec(m, x, %k r. r Un r*r)";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   352
by (resolve_tac [z_n_subset_z_succ_n RS le_subsets] 1 
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   353
    THEN (TRYALL assume_tac));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   354
by (eresolve_tac [Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD] 1
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   355
    THEN (assume_tac 1));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   356
val le_imp_rec_subset = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   357
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   358
goal thy "EX y. x Un y*y <= y";
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   359
by (res_inst_tac [("x","UN n:nat. rec(n, x, %k r. r Un r*r)")] exI 1);
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   360
by (safe_tac ZF_cs);
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   361
by (fast_tac (ZF_cs addSIs [nat_0I] addss nat_ss) 1);
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   362
by (res_inst_tac [("a","succ(n Un na)")] UN_I 1);
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   363
by (eresolve_tac [Un_nat_type RS nat_succI] 1 THEN (assume_tac 1));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   364
by (fast_tac (ZF_cs addIs [le_imp_rec_subset RS subsetD]
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   365
		addSIs [Un_upper1_le, Un_upper2_le, Un_nat_type]
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   366
		addSEs [nat_into_Ord] addss nat_ss) 1);
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   367
val lemma_iv = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   368
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   369
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   370
(* Rubin & Rubin wrote :						  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   371
(* "It follows from (ii) and mathematical induction that if y*y <= y then *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   372
(* y can be well-ordered"						  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   373
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   374
(* In fact we have to prove :						  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   375
(*	* WO6 ==> NN(y) ~= 0						  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   376
(*	* reverse induction which lets us infer that 1 : NN(y)		  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   377
(*	* 1 : NN(y) ==> y can be well-ordered				  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   378
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   379
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   380
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   381
(*	WO6 ==> NN(y) ~= 0						  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   382
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   383
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   384
goalw thy [WO6_def, NN_def] "!!y. WO6 ==> NN(y) ~= 0";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   385
by (eresolve_tac [allE] 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   386
by (fast_tac (ZF_cs addSIs [not_emptyI]) 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   387
val WO6_imp_NN_not_empty = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   388
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   389
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   390
(*	1 : NN(y) ==> y can be well-ordered				  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   391
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   392
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   393
goal thy "!!f. [| (UN b<a. f`b)=y; x:y; ALL b<a. f`b lepoll 1; Ord(a) |]  \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   394
\		==> EX c<a. f`c = {x}";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   395
by (fast_tac (AC_cs addSEs [lepoll_1_is_sing]) 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   396
val lemma1 = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   397
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   398
goal thy "!!f. [| (UN b<a. f`b)=y; x:y; ALL b<a. f`b lepoll 1; Ord(a) |]  \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   399
\		==> f` (LEAST i. f`i = {x}) = {x}";
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   400
by (dresolve_tac [lemma1] 1 THEN REPEAT (assume_tac 1));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   401
by (fast_tac (AC_cs addSEs [lt_Ord] addIs [LeastI]) 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   402
val lemma2 = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   403
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   404
goalw thy [NN_def] "!!y. 1 : NN(y) ==> EX a f. Ord(a) & f:inj(y, a)";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   405
by (eresolve_tac [CollectE] 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   406
by (REPEAT (eresolve_tac [exE, conjE] 1));
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   407
by (res_inst_tac [("x","a")] exI 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   408
by (res_inst_tac [("x","lam x:y. LEAST i. f`i = {x}")] exI 1);
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   409
by (resolve_tac [conjI] 1 THEN (assume_tac 1));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   410
by (res_inst_tac [("d","%i. THE x. x:f`i")] lam_injective 1);
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   411
by (dresolve_tac [lemma1] 1 THEN REPEAT (assume_tac 1));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   412
by (fast_tac (AC_cs addSEs [Least_le RS lt_trans1 RS ltD, lt_Ord]) 1);
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   413
by (resolve_tac [lemma2 RS ssubst] 1 THEN REPEAT (assume_tac 1));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   414
by (fast_tac (ZF_cs addSIs [the_equality]) 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   415
val NN_imp_ex_inj = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   416
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   417
goal thy "!!y. [| y*y <= y; 1 : NN(y) |] ==> EX r. well_ord(y, r)";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   418
by (dresolve_tac [NN_imp_ex_inj] 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   419
by (fast_tac (ZF_cs addSEs [well_ord_Memrel RSN (2,  well_ord_rvimage)]) 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   420
val y_well_ord = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   421
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   422
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   423
(*	reverse induction which lets us infer that 1 : NN(y)		  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   424
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   425
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   426
val [prem1, prem2] = goal thy
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   427
	"[| n:nat; !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |]  \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   428
\	==> n~=0 --> P(n) --> P(1)";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   429
by (res_inst_tac [("n","n")] nat_induct 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   430
by (resolve_tac [prem1] 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   431
by (fast_tac ZF_cs 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   432
by (excluded_middle_tac "x=0" 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   433
by (fast_tac ZF_cs 2);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   434
by (fast_tac (ZF_cs addSIs [prem2]) 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   435
val rev_induct_lemma = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   436
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   437
val prems = goal thy
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   438
	"[| P(n); n:nat; n~=0;  \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   439
\	!!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |]  \
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   440
\	==> P(1)";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   441
by (resolve_tac [rev_induct_lemma RS impE] 1);
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   442
by (eresolve_tac [impE] 4 THEN (assume_tac 5));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   443
by (REPEAT (ares_tac prems 1));
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   444
val rev_induct = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   445
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   446
goalw thy [NN_def] "!!n. n:NN(y) ==> n:nat";
1057
5097aa914449 Renamed diff_sing_lepoll to Diff_sing_lepoll.
lcp
parents: 1041
diff changeset
   447
by (etac CollectD1 1);
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   448
val NN_into_nat = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   449
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   450
goal thy "!!n. [| n:NN(y); y*y <= y; n~=0 |] ==> 1:NN(y)";
1057
5097aa914449 Renamed diff_sing_lepoll to Diff_sing_lepoll.
lcp
parents: 1041
diff changeset
   451
by (resolve_tac [rev_induct] 1 THEN REPEAT (ares_tac [NN_into_nat] 1));
1041
6664d0b54d0f Deleted subset_imp_Un_Diff_eq, as it is identical to
lcp
parents: 992
diff changeset
   452
by (resolve_tac [lemma_ii] 1 THEN REPEAT (assume_tac 1));
992
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   453
val lemma3 = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   454
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   455
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   456
(* Main theorem "WO6 ==> WO1"						  *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   457
(* ********************************************************************** *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   458
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   459
(* another helpful lemma *)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   460
goalw thy [NN_def] "!!y. 0:NN(y) ==> y=0";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   461
by (fast_tac (AC_cs addSIs [equalityI] 
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   462
                    addSDs [lepoll_0_is_0] addEs [subst]) 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   463
val NN_y_0 = result();
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   464
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   465
goalw thy [WO1_def] "!!Z. WO6 ==> WO1";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   466
by (resolve_tac [allI] 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   467
by (excluded_middle_tac "A=0" 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   468
by (fast_tac (ZF_cs addSIs [well_ord_Memrel, nat_0I RS nat_into_Ord]) 2);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   469
by (res_inst_tac [("x1","A")] (lemma_iv RS revcut_rl) 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   470
by (eresolve_tac [exE] 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   471
by (dresolve_tac [WO6_imp_NN_not_empty] 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   472
by (eresolve_tac [Un_subset_iff RS iffD1 RS conjE] 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   473
by (eres_inst_tac [("A","NN(y)")] not_emptyE 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   474
by (forward_tac [y_well_ord] 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   475
by (fast_tac (ZF_cs addEs [well_ord_subset]) 2);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   476
by (fast_tac (ZF_cs addSIs [lemma3] addSDs [NN_y_0] addSEs [not_emptyE]) 1);
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   477
qed "WO6_imp_WO1";
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
   478