src/ZF/AC/AC2_AC6.ML
author paulson
Tue, 04 Mar 1997 10:42:28 +0100
changeset 2717 b29c45ef3d86
parent 2496 40efb87985b5
child 4091 771b1f6422a8
permissions -rw-r--r--
best_tac avoids looping with change to RepFun_eqI in claset
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
     1
(*  Title:      ZF/AC/AC2_AC6.ML
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
     3
    Author:     Krzysztof Grabczewski
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     4
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
     5
The proofs needed to show that each of AC2, AC3, ..., AC6 is equivalent
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
     6
to AC0 and AC1:
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     7
AC1 ==> AC2 ==> AC1
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     8
AC1 ==> AC4 ==> AC3 ==> AC1
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     9
AC4 ==> AC5 ==> AC4
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    10
AC1 <-> AC6
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    11
*)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    12
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    13
(* ********************************************************************** *)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
    14
(* AC1 ==> AC2                                                            *)
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    15
(* ********************************************************************** *)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    16
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    17
goal thy "!!B. [| B:A; f:(PROD X:A. X); 0~:A |]  \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
    18
\               ==> {f`B} <= B Int {f`C. C:A}";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
    19
by (fast_tac (!claset addSEs [apply_type]) 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    20
val lemma1 = result();
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    21
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    22
goalw thy [pairwise_disjoint_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
    23
        "!!A. [| pairwise_disjoint(A); B:A; C:A; D:B; D:C |] ==> f`B = f`C";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
    24
by (fast_tac (!claset addSEs [equals0D]) 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    25
val lemma2 = result();
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    26
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    27
goalw thy AC_defs "!!Z. AC1 ==> AC2"; 
1206
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
    28
by (rtac allI 1);
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
    29
by (rtac impI 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    30
by (REPEAT (eresolve_tac [asm_rl,conjE,allE,exE,impE] 1));
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    31
by (REPEAT (resolve_tac [exI,ballI,equalityI] 1));
1206
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
    32
by (rtac lemma1 2 THEN (REPEAT (assume_tac 2)));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
    33
by (fast_tac (!claset addSEs [RepFunE, lemma2] addEs [apply_type]) 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
    34
qed "AC1_AC2";
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    35
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    36
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    37
(* ********************************************************************** *)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
    38
(* AC2 ==> AC1                                                            *)
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    39
(* ********************************************************************** *)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    40
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    41
goal thy "!!A. 0~:A ==> 0 ~: {B*{B}. B:A}";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
    42
by (fast_tac (!claset addSDs [sym RS (Sigma_empty_iff RS iffD1)]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
    43
        addSEs [RepFunE, equals0D]) 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    44
val lemma1 = result();
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    45
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    46
goal thy "!!A. [| X*{X} Int C = {y}; X:A |]  \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
    47
\               ==> (THE y. X*{X} Int C = {y}): X*A";
1206
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
    48
by (rtac subst_elem 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
    49
by (fast_tac (!claset addSIs [the_equality]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
    50
                addSEs [sym RS trans RS (singleton_eq_iff RS iffD1)]) 2);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
    51
by (fast_tac (!claset addSEs [equalityE, make_elim singleton_subsetD]) 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    52
val lemma2 = result();
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    53
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    54
goal thy "!!A. ALL D:{E*{E}. E:A}. EX y. D Int C = {y}  \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
    55
\       ==> (lam x:A. fst(THE z. (x*{x} Int C = {z}))) :  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
    56
\               (PROD X:A. X) ";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
    57
by (fast_tac (!claset addSEs [lemma2]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
    58
                addSIs [lam_type, RepFunI, fst_type]
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
    59
                addSDs [bspec]) 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    60
val lemma3 = result();
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    61
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    62
goalw thy (AC_defs@AC_aux_defs) "!!Z. AC2 ==> AC1";
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    63
by (REPEAT (resolve_tac [allI, impI] 1));
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    64
by (REPEAT (eresolve_tac [allE, impE] 1));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
    65
by (fast_tac (!claset addSEs [lemma3]) 2);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
    66
by (fast_tac (!claset addSIs [lemma1, equals0I]) 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
    67
qed "AC2_AC1";
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    68
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    69
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    70
(* ********************************************************************** *)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
    71
(* AC1 ==> AC4                                                            *)
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    72
(* ********************************************************************** *)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    73
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    74
goal thy "!!R. 0 ~: {R``{x}. x:domain(R)}";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
    75
by (fast_tac (!claset addEs [sym RS equals0D]) 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    76
val lemma = result();
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    77
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    78
goalw thy AC_defs "!!Z. AC1 ==> AC4";
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    79
by (REPEAT (resolve_tac [allI, impI] 1));
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    80
by (REPEAT (eresolve_tac [allE, lemma RSN (2, impE), exE] 1));
2717
b29c45ef3d86 best_tac avoids looping with change to RepFun_eqI in claset
paulson
parents: 2496
diff changeset
    81
by (best_tac (!claset addSIs [lam_type] addSEs [apply_type]) 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
    82
qed "AC1_AC4";
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    83
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    84
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    85
(* ********************************************************************** *)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
    86
(* AC4 ==> AC3                                                            *)
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    87
(* ********************************************************************** *)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    88
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    89
goal thy "!!f. f:A->B ==> (UN z:A. {z}*f`z) <= A*Union(B)";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
    90
by (fast_tac (!claset addSDs [apply_type]) 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    91
val lemma1 = result();
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    92
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    93
goal thy "!!f. domain(UN z:A. {z}*f(z)) = {a:A. f(a)~=0}";
2496
40efb87985b5 Removal of needless "addIs [equality]", etc.
paulson
parents: 2469
diff changeset
    94
by (fast_tac (!claset addSIs [not_emptyI] addDs [range_type]) 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    95
val lemma2 = result();
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    96
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    97
goal thy "!!f. x:A ==> (UN z:A. {z}*f(z))``{x} = f(x)";
2496
40efb87985b5 Removal of needless "addIs [equality]", etc.
paulson
parents: 2469
diff changeset
    98
by (Fast_tac 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    99
val lemma3 = result();
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   100
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   101
goalw thy AC_defs "!!Z. AC4 ==> AC3";
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   102
by (REPEAT (resolve_tac [allI,ballI] 1));
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   103
by (REPEAT (eresolve_tac [allE,impE] 1));
1206
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   104
by (etac lemma1 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   105
by (asm_full_simp_tac (!simpset addsimps [lemma2, lemma3]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
   106
                        addcongs [Pi_cong]) 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   107
qed "AC4_AC3";
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   108
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   109
(* ********************************************************************** *)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
   110
(* AC3 ==> AC1                                                            *)
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   111
(* ********************************************************************** *)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   112
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   113
goal thy "!!A. b~:A ==> (PROD x:{a:A. id(A)`a~=b}. id(A)`x) = (PROD x:A. x)";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   114
by (asm_full_simp_tac (!simpset addsimps [id_def] addcongs [Pi_cong]) 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   115
by (res_inst_tac [("b","A")] subst_context 1);
2496
40efb87985b5 Removal of needless "addIs [equality]", etc.
paulson
parents: 2469
diff changeset
   116
by (Fast_tac 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   117
val lemma = result();
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   118
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   119
goalw thy AC_defs "!!Z. AC3 ==> AC1";
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   120
by (REPEAT (resolve_tac [allI, impI] 1));
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   121
by (REPEAT (eresolve_tac [allE, ballE] 1));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   122
by (fast_tac (!claset addSIs [id_type]) 2);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   123
by (fast_tac (!claset addEs [lemma RS subst]) 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   124
qed "AC3_AC1";
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   125
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   126
(* ********************************************************************** *)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
   127
(* AC4 ==> AC5                                                            *)
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   128
(* ********************************************************************** *)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   129
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   130
goalw thy (range_def::AC_defs) "!!Z. AC4 ==> AC5";
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   131
by (REPEAT (resolve_tac [allI,ballI] 1));
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   132
by (REPEAT (eresolve_tac [allE,impE] 1));
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   133
by (eresolve_tac [fun_is_rel RS converse_type] 1);
1206
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   134
by (etac exE 1);
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   135
by (rtac bexI 1);
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   136
by (rtac Pi_type 2 THEN (assume_tac 2));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   137
by (fast_tac (!claset addSDs [apply_type]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
   138
        addSEs [fun_is_rel RS converse_type RS subsetD RS SigmaD2]) 2);
1206
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   139
by (rtac ballI 1);
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   140
by (rtac apply_equality 1 THEN (assume_tac 2));
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   141
by (etac domainE 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   142
by (forward_tac [range_type] 1 THEN (assume_tac 1));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   143
by (fast_tac (!claset addDs [apply_equality]) 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   144
qed "AC4_AC5";
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   145
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   146
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   147
(* ********************************************************************** *)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
   148
(* AC5 ==> AC4, Rubin & Rubin, p. 11                                      *)
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   149
(* ********************************************************************** *)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   150
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   151
goal thy "!!A. R <= A*B ==> (lam x:R. fst(x)) : R -> A";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   152
by (fast_tac (!claset addSIs [lam_type, fst_type]) 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   153
val lemma1 = result();
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   154
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   155
goalw thy [range_def] "!!A. R <= A*B ==> range(lam x:R. fst(x)) = domain(R)";
1206
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   156
by (rtac equalityI 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   157
by (fast_tac (!claset addSEs [lamE]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
   158
                addEs [subst_elem]
1932
cc9f1ba8f29a Tidying: removing redundant args in classical reasoner calls
paulson
parents: 1924
diff changeset
   159
                addSDs [Pair_fst_snd_eq]) 1);
1206
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   160
by (rtac subsetI 1);
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   161
by (etac domainE 1);
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   162
by (rtac domainI 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   163
by (fast_tac (!claset addSEs [lamI RS subst_elem] addIs [fst_conv RS ssubst]) 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   164
val lemma2 = result();
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   165
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   166
goal thy "!!A. [| EX f: A->C. P(f,domain(f)); A=B |] ==>  EX f: B->C. P(f,B)";
1206
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   167
by (etac bexE 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   168
by (forward_tac [domain_of_fun] 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   169
by (Fast_tac 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   170
val lemma3 = result();
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   171
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   172
goal thy "!!g. [| R <= A*B; g: C->R; ALL x:C. (lam z:R. fst(z))` (g`x) = x |] \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
   173
\               ==> (lam x:C. snd(g`x)): (PROD x:C. R``{x})";
1206
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   174
by (rtac lam_type 1);
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   175
by (dtac apply_type 1 THEN (assume_tac 1));
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   176
by (dtac bspec 1 THEN (assume_tac 1));
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
   177
by (rtac imageI 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   178
by (resolve_tac [subsetD RS Pair_fst_snd_eq RSN (2, subst_elem)] 1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
   179
        THEN (REPEAT (assume_tac 1)));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   180
by (Asm_full_simp_tac 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   181
val lemma4 = result();
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   182
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   183
goalw thy AC_defs "!!Z. AC5 ==> AC4";
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   184
by (REPEAT (resolve_tac [allI,impI] 1));
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   185
by (REPEAT (eresolve_tac [allE,ballE] 1));
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   186
by (eresolve_tac [lemma1 RSN (2, notE)] 2 THEN (assume_tac 2));
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   187
by (dresolve_tac [lemma2 RSN (2, lemma3)] 1 THEN (assume_tac 1));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   188
by (fast_tac (!claset addSEs [lemma4]) 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   189
qed "AC5_AC4";
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   190
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   191
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   192
(* ********************************************************************** *)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
   193
(* AC1 <-> AC6                                                            *)
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   194
(* ********************************************************************** *)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   195
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   196
goalw thy AC_defs "AC1 <-> AC6";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   197
by (fast_tac (!claset addDs [equals0D] addSEs [not_emptyE]) 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   198
qed "AC1_iff_AC6";
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   199