src/ZF/WF.ML
author lcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 435 ca5356bd315a
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
clasohm@0
     1
(*  Title: 	ZF/wf.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Tobias Nipkow and Lawrence C Paulson
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
clasohm@0
     6
For wf.thy.  Well-founded Recursion
clasohm@0
     7
clasohm@0
     8
Derived first for transitive relations, and finally for arbitrary WF relations
clasohm@0
     9
via wf_trancl and trans_trancl.
clasohm@0
    10
clasohm@0
    11
It is difficult to derive this general case directly, using r^+ instead of
clasohm@0
    12
r.  In is_recfun, the two occurrences of the relation must have the same
clasohm@0
    13
form.  Inserting r^+ in the_recfun or wftrec yields a recursion rule with
clasohm@0
    14
r^+ -`` {a} instead of r-``{a}.  This recursion rule is stronger in
clasohm@0
    15
principle, but harder to use, especially to prove wfrec_eclose_eq in
clasohm@0
    16
epsilon.ML.  Expanding out the definition of wftrec in wfrec would yield
clasohm@0
    17
a mess.
clasohm@0
    18
*)
clasohm@0
    19
clasohm@0
    20
open WF;
clasohm@0
    21
clasohm@0
    22
clasohm@0
    23
(*** Well-founded relations ***)
clasohm@0
    24
clasohm@0
    25
(*Are these two theorems at all useful??*)
clasohm@0
    26
clasohm@0
    27
(*If every subset of field(r) possesses an r-minimal element then wf(r).
clasohm@0
    28
  Seems impossible to prove this for domain(r) or range(r) instead...
clasohm@0
    29
  Consider in particular finite wf relations!*)
clasohm@0
    30
val [prem1,prem2] = goalw WF.thy [wf_def]
clasohm@0
    31
    "[| field(r)<=A;  \
clasohm@0
    32
\       !!Z u. [| Z<=A;  u:Z;  ALL x:Z. EX y:Z. <y,x>:r |] ==> False |] \
clasohm@0
    33
\    ==>  wf(r)";
clasohm@0
    34
by (rtac (equals0I RS disjCI RS allI) 1);
clasohm@0
    35
by (rtac prem2 1);
clasohm@0
    36
by (res_inst_tac [ ("B1", "Z") ] (prem1 RS (Int_lower1 RS subset_trans)) 1);
clasohm@0
    37
by (fast_tac ZF_cs 1);
clasohm@0
    38
by (fast_tac ZF_cs 1);
clasohm@0
    39
val wfI = result();
clasohm@0
    40
clasohm@0
    41
(*If r allows well-founded induction then wf(r)*)
clasohm@0
    42
val [prem1,prem2] = goal WF.thy
clasohm@0
    43
    "[| field(r)<=A;  \
clasohm@0
    44
\       !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B |]  \
clasohm@0
    45
\    ==>  wf(r)";
clasohm@0
    46
by (rtac (prem1 RS wfI) 1);
clasohm@0
    47
by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1);
clasohm@0
    48
by (fast_tac ZF_cs 3);
clasohm@0
    49
by (fast_tac ZF_cs 2);
clasohm@0
    50
by (fast_tac ZF_cs 1);
clasohm@0
    51
val wfI2 = result();
clasohm@0
    52
clasohm@0
    53
clasohm@0
    54
(** Well-founded Induction **)
clasohm@0
    55
clasohm@0
    56
(*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*)
clasohm@0
    57
val major::prems = goalw WF.thy [wf_def]
clasohm@0
    58
    "[| wf(r);          \
clasohm@0
    59
\       !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) \
clasohm@0
    60
\    |]  ==>  P(a)";
clasohm@0
    61
by (res_inst_tac [ ("x", "{z:domain(r) Un {a}. ~P(z)}") ]  (major RS allE) 1);
clasohm@0
    62
by (etac disjE 1);
clasohm@0
    63
by (rtac classical 1);
clasohm@0
    64
by (etac equals0D 1);
clasohm@0
    65
by (etac (singletonI RS UnI2 RS CollectI) 1);
clasohm@0
    66
by (etac bexE 1);
clasohm@0
    67
by (etac CollectE 1);
clasohm@0
    68
by (etac swap 1);
clasohm@0
    69
by (resolve_tac prems 1);
clasohm@0
    70
by (fast_tac ZF_cs 1);
clasohm@0
    71
val wf_induct = result();
clasohm@0
    72
clasohm@0
    73
(*Perform induction on i, then prove the wf(r) subgoal using prems. *)
clasohm@0
    74
fun wf_ind_tac a prems i = 
clasohm@0
    75
    EVERY [res_inst_tac [("a",a)] wf_induct i,
clasohm@0
    76
	   rename_last_tac a ["1"] (i+1),
clasohm@0
    77
	   ares_tac prems i];
clasohm@0
    78
clasohm@0
    79
(*The form of this rule is designed to match wfI2*)
clasohm@0
    80
val wfr::amem::prems = goal WF.thy
clasohm@0
    81
    "[| wf(r);  a:A;  field(r)<=A;  \
clasohm@0
    82
\       !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) \
clasohm@0
    83
\    |]  ==>  P(a)";
clasohm@0
    84
by (rtac (amem RS rev_mp) 1);
clasohm@0
    85
by (wf_ind_tac "a" [wfr] 1);
clasohm@0
    86
by (rtac impI 1);
clasohm@0
    87
by (eresolve_tac prems 1);
clasohm@0
    88
by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1);
clasohm@0
    89
val wf_induct2 = result();
clasohm@0
    90
clasohm@0
    91
val prems = goal WF.thy "[| wf(r);  <a,x>:r;  <x,a>:r |] ==> False";
clasohm@0
    92
by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> False" 1);
clasohm@0
    93
by (wf_ind_tac "a" prems 2);
clasohm@0
    94
by (fast_tac ZF_cs 2);
clasohm@0
    95
by (fast_tac (FOL_cs addIs prems) 1);
clasohm@0
    96
val wf_anti_sym = result();
clasohm@0
    97
clasohm@0
    98
(*transitive closure of a WF relation is WF!*)
clasohm@0
    99
val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
clasohm@0
   100
by (rtac (trancl_type RS field_rel_subset RS wfI2) 1);
clasohm@0
   101
by (rtac subsetI 1);
clasohm@0
   102
(*must retain the universal formula for later use!*)
clasohm@0
   103
by (rtac (bspec RS mp) 1 THEN assume_tac 1 THEN assume_tac 1);
clasohm@0
   104
by (eres_inst_tac [("a","x")] (prem RS wf_induct2) 1);
clasohm@0
   105
by (rtac subset_refl 1);
clasohm@0
   106
by (rtac (impI RS allI) 1);
clasohm@0
   107
by (etac tranclE 1);
clasohm@0
   108
by (etac (bspec RS mp) 1);
clasohm@0
   109
by (etac fieldI1 1);
clasohm@0
   110
by (fast_tac ZF_cs 1);
clasohm@0
   111
by (fast_tac ZF_cs 1);
clasohm@0
   112
val wf_trancl = result();
clasohm@0
   113
clasohm@0
   114
(** r-``{a} is the set of everything under a in r **)
clasohm@0
   115
clasohm@0
   116
val underI = standard (vimage_singleton_iff RS iffD2);
clasohm@0
   117
val underD = standard (vimage_singleton_iff RS iffD1);
clasohm@0
   118
clasohm@0
   119
(** is_recfun **)
clasohm@0
   120
clasohm@0
   121
val [major] = goalw WF.thy [is_recfun_def]
clasohm@0
   122
    "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)";
clasohm@0
   123
by (rtac (major RS ssubst) 1);
clasohm@0
   124
by (rtac (lamI RS rangeI RS lam_type) 1);
clasohm@0
   125
by (assume_tac 1);
clasohm@0
   126
val is_recfun_type = result();
clasohm@0
   127
clasohm@0
   128
val [isrec,rel] = goalw WF.thy [is_recfun_def]
clasohm@0
   129
    "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))";
clasohm@0
   130
by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (isrec RS ssubst) 1);
clasohm@0
   131
by (rtac (rel RS underI RS beta) 1);
clasohm@0
   132
val apply_recfun = result();
clasohm@0
   133
clasohm@0
   134
(*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
clasohm@0
   135
  spec RS mp  instantiates induction hypotheses*)
clasohm@0
   136
fun indhyp_tac hyps =
lcp@6
   137
    resolve_tac (TrueI::refl::hyps) ORELSE' 
clasohm@0
   138
    (cut_facts_tac hyps THEN'
clasohm@0
   139
       DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
clasohm@0
   140
		        eresolve_tac [underD, transD, spec RS mp]));
clasohm@0
   141
lcp@6
   142
(*** NOTE! some simplifications need a different solver!! ***)
lcp@6
   143
val wf_super_ss = ZF_ss setsolver indhyp_tac;
clasohm@0
   144
clasohm@0
   145
val prems = goalw WF.thy [is_recfun_def]
clasohm@0
   146
    "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \
clasohm@0
   147
\    <x,a>:r --> <x,b>:r --> f`x=g`x";
clasohm@0
   148
by (cut_facts_tac prems 1);
clasohm@0
   149
by (wf_ind_tac "x" prems 1);
clasohm@0
   150
by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
clasohm@0
   151
by (rewtac restrict_def);
lcp@6
   152
by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
clasohm@0
   153
val is_recfun_equal_lemma = result();
clasohm@0
   154
val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
clasohm@0
   155
clasohm@0
   156
val prems as [wfr,transr,recf,recg,_] = goal WF.thy
clasohm@0
   157
    "[| wf(r);  trans(r);       \
clasohm@0
   158
\       is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |] ==> \
clasohm@0
   159
\    restrict(f, r-``{b}) = g";
clasohm@0
   160
by (cut_facts_tac prems 1);
clasohm@0
   161
by (rtac (consI1 RS restrict_type RS fun_extension) 1);
clasohm@0
   162
by (etac is_recfun_type 1);
clasohm@0
   163
by (ALLGOALS
lcp@6
   164
    (asm_simp_tac (wf_super_ss addsimps
clasohm@0
   165
		   [ [wfr,transr,recf,recg] MRS is_recfun_equal ])));
clasohm@0
   166
val is_recfun_cut = result();
clasohm@0
   167
clasohm@0
   168
(*** Main Existence Lemma ***)
clasohm@0
   169
clasohm@0
   170
val prems = goal WF.thy
clasohm@0
   171
    "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g";
clasohm@0
   172
by (cut_facts_tac prems 1);
clasohm@0
   173
by (rtac fun_extension 1);
clasohm@0
   174
by (REPEAT (ares_tac [is_recfun_equal] 1
clasohm@0
   175
     ORELSE eresolve_tac [is_recfun_type,underD] 1));
clasohm@0
   176
val is_recfun_functional = result();
clasohm@0
   177
clasohm@0
   178
(*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
clasohm@0
   179
val prems = goalw WF.thy [the_recfun_def]
clasohm@0
   180
    "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |]  \
clasohm@0
   181
\    ==> is_recfun(r, a, H, the_recfun(r,a,H))";
clasohm@0
   182
by (rtac (ex1I RS theI) 1);
clasohm@0
   183
by (REPEAT (ares_tac (prems@[is_recfun_functional]) 1));
clasohm@0
   184
val is_the_recfun = result();
clasohm@0
   185
clasohm@0
   186
val prems = goal WF.thy
clasohm@0
   187
    "[| wf(r);  trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))";
clasohm@0
   188
by (cut_facts_tac prems 1);
clasohm@0
   189
by (wf_ind_tac "a" prems 1);
clasohm@0
   190
by (res_inst_tac [("f", "lam y: r-``{a1}. wftrec(r,y,H)")] is_the_recfun 1);
clasohm@0
   191
by (REPEAT (assume_tac 2));
clasohm@0
   192
by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
clasohm@0
   193
(*Applying the substitution: must keep the quantified assumption!!*)
lcp@6
   194
by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1));
clasohm@0
   195
by (fold_tac [is_recfun_def]);
lcp@6
   196
by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1);
clasohm@0
   197
by (rtac is_recfun_type 1);
clasohm@0
   198
by (ALLGOALS
lcp@6
   199
    (asm_simp_tac
lcp@6
   200
     (wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut])));
clasohm@0
   201
val unfold_the_recfun = result();
clasohm@0
   202
clasohm@0
   203
clasohm@0
   204
(*** Unfolding wftrec ***)
clasohm@0
   205
clasohm@0
   206
val prems = goal WF.thy
clasohm@0
   207
    "[| wf(r);  trans(r);  <b,a>:r |] ==> \
clasohm@0
   208
\    restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)";
clasohm@0
   209
by (REPEAT (ares_tac (prems @ [is_recfun_cut, unfold_the_recfun]) 1));
clasohm@0
   210
val the_recfun_cut = result();
clasohm@0
   211
clasohm@0
   212
(*NOT SUITABLE FOR REWRITING since it is recursive!*)
lcp@6
   213
goalw WF.thy [wftrec_def]
lcp@6
   214
    "!!r. [| wf(r);  trans(r) |] ==> \
lcp@6
   215
\         wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
clasohm@0
   216
by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);
lcp@6
   217
by (ALLGOALS (asm_simp_tac
lcp@6
   218
	(ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut])));
clasohm@0
   219
val wftrec = result();
clasohm@0
   220
clasohm@0
   221
(** Removal of the premise trans(r) **)
clasohm@0
   222
clasohm@0
   223
(*NOT SUITABLE FOR REWRITING since it is recursive!*)
clasohm@0
   224
val [wfr] = goalw WF.thy [wfrec_def]
clasohm@0
   225
    "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
clasohm@0
   226
by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1);
clasohm@0
   227
by (rtac trans_trancl 1);
lcp@6
   228
by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1);
clasohm@0
   229
by (etac r_into_trancl 1);
clasohm@0
   230
by (rtac subset_refl 1);
clasohm@0
   231
val wfrec = result();
clasohm@0
   232
clasohm@0
   233
(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
clasohm@0
   234
val rew::prems = goal WF.thy
clasohm@0
   235
    "[| !!x. h(x)==wfrec(r,x,H);  wf(r) |] ==> \
clasohm@0
   236
\    h(a) = H(a, lam x: r-``{a}. h(x))";
clasohm@0
   237
by (rewtac rew);
clasohm@0
   238
by (REPEAT (resolve_tac (prems@[wfrec]) 1));
clasohm@0
   239
val def_wfrec = result();
clasohm@0
   240
clasohm@0
   241
val prems = goal WF.thy
clasohm@0
   242
    "[| wf(r);  a:A;  field(r)<=A;  \
clasohm@0
   243
\       !!x u. [| x: A;  u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x)   \
clasohm@0
   244
\    |] ==> wfrec(r,a,H) : B(a)";
clasohm@0
   245
by (res_inst_tac [("a","a")] wf_induct2 1);
clasohm@0
   246
by (rtac (wfrec RS ssubst) 4);
clasohm@0
   247
by (REPEAT (ares_tac (prems@[lam_type]) 1
clasohm@0
   248
     ORELSE eresolve_tac [spec RS mp, underD] 1));
clasohm@0
   249
val wfrec_type = result();