src/ZF/WF.ML
author clasohm
Wed, 29 Jun 1994 12:13:03 +0200
changeset 443 10884e64c241
parent 437 435875e4b21d
child 485 5e00a676a211
permissions -rw-r--r--
added parentheses made necessary by new constrain precedence
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/wf.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Tobias Nipkow and Lawrence C Paulson
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
For wf.thy.  Well-founded Recursion
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
Derived first for transitive relations, and finally for arbitrary WF relations
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
via wf_trancl and trans_trancl.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
It is difficult to derive this general case directly, using r^+ instead of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
r.  In is_recfun, the two occurrences of the relation must have the same
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
form.  Inserting r^+ in the_recfun or wftrec yields a recursion rule with
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
r^+ -`` {a} instead of r-``{a}.  This recursion rule is stronger in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
principle, but harder to use, especially to prove wfrec_eclose_eq in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
epsilon.ML.  Expanding out the definition of wftrec in wfrec would yield
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a mess.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
open WF;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
(*** Well-founded relations ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    25
(** Equivalences between wf and wf_on **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    26
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    27
goalw WF.thy [wf_def, wf_on_def] "!!A r. wf(r) ==> wf[A](r)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    28
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    29
val wf_imp_wf_on = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    30
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    31
goalw WF.thy [wf_def, wf_on_def] "!!r. wf[field(r)](r) ==> wf(r)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    32
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    33
val wf_on_field_imp_wf = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    34
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    35
goal WF.thy "wf(r) <-> wf[field(r)](r)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    36
by (fast_tac (ZF_cs addSEs [wf_imp_wf_on, wf_on_field_imp_wf]) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    37
val wf_iff_wf_on_field = result();
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    39
goalw WF.thy [wf_on_def, wf_def] "!!A B r. [| wf[A](r);  B<=A |] ==> wf[B](r)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    40
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    41
val wf_on_subset_A = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    42
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    43
goalw WF.thy [wf_on_def, wf_def] "!!A r s. [| wf[A](r);  s<=r |] ==> wf[A](s)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    44
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    45
val wf_on_subset_r = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    46
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    47
(** Introduction rules for wf_on **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    48
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    49
(*If every non-empty subset of A has an r-minimal element then wf[A](r).*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    50
val [prem] = goalw WF.thy [wf_on_def, wf_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    51
    "[| !!Z u. [| Z<=A;  u:Z;  ALL x:Z. EX y:Z. <y,x>:r |] ==> False |] \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    52
\    ==>  wf[A](r)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
by (rtac (equals0I RS disjCI RS allI) 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    54
by (res_inst_tac [ ("Z", "Z") ] prem 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    55
by (ALLGOALS (fast_tac ZF_cs));
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    56
val wf_onI = result();
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    58
(*If r allows well-founded induction over A then wf[A](r)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    59
  Premise is equivalent to 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    60
  !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B  *)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    61
val [prem] = goal WF.thy
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    62
    "[| !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A  \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    63
\              |] ==> y:B |] \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    64
\    ==>  wf[A](r)";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    65
by (rtac wf_onI 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    66
by (res_inst_tac [ ("c", "u") ] (prem RS DiffE) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    67
by (contr_tac 3);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
by (fast_tac ZF_cs 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
by (fast_tac ZF_cs 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
    70
val wf_onI2 = result();
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
(** Well-founded Induction **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
(*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
val major::prems = goalw WF.thy [wf_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
    "[| wf(r);          \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
\       !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
\    |]  ==>  P(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
by (res_inst_tac [ ("x", "{z:domain(r) Un {a}. ~P(z)}") ]  (major RS allE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
by (etac disjE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
by (rtac classical 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
by (etac equals0D 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
by (etac (singletonI RS UnI2 RS CollectI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
by (etac bexE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
by (etac CollectE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
by (etac swap 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
val wf_induct = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
(*Perform induction on i, then prove the wf(r) subgoal using prems. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
fun wf_ind_tac a prems i = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
    EVERY [res_inst_tac [("a",a)] wf_induct i,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
	   rename_last_tac a ["1"] (i+1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
	   ares_tac prems i];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
(*The form of this rule is designed to match wfI2*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
val wfr::amem::prems = goal WF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
    "[| wf(r);  a:A;  field(r)<=A;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
\       !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
\    |]  ==>  P(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
by (rtac (amem RS rev_mp) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
by (wf_ind_tac "a" [wfr] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
by (rtac impI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
by (eresolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
val wf_induct2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   110
goal ZF.thy "!!r A. field(r Int A*A) <= A";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   111
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   112
val field_Int_square = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   113
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   114
val wfr::amem::prems = goalw WF.thy [wf_on_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   115
    "[| wf[A](r);  a:A;  					\
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   116
\       !!x.[| x: A;  ALL y:A. <y,x>: r --> P(y) |] ==> P(x) 	\
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   117
\    |]  ==>  P(a)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   118
by (rtac ([wfr, amem, field_Int_square] MRS wf_induct2) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   119
by (REPEAT (ares_tac prems 1));
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   120
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   121
val wf_on_induct = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   122
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   123
fun wf_on_ind_tac a prems i = 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   124
    EVERY [res_inst_tac [("a",a)] wf_on_induct i,
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   125
	   rename_last_tac a ["1"] (i+2),
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   126
	   REPEAT (ares_tac prems i)];
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   127
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   128
(*If r allows well-founded induction then wf(r)*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   129
val [subs,indhyp] = goal WF.thy
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   130
    "[| field(r)<=A;  \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   131
\       !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A  \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   132
\              |] ==> y:B |] \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   133
\    ==>  wf(r)";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   134
by (rtac ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   135
by (REPEAT (ares_tac [indhyp] 1));
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   136
val wfI2 = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   137
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   138
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   139
(*** Properties of well-founded relations ***)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   140
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   141
goal WF.thy "!!r. wf(r) ==> <a,a> ~: r";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   142
by (wf_ind_tac "a" [] 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   143
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   144
val wf_not_refl = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   145
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   146
goal WF.thy "!!r. [| wf(r);  <a,x>:r;  <x,a>:r |] ==> P";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   147
by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P" 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   148
by (wf_ind_tac "a" [] 2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
by (fast_tac ZF_cs 2);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   150
by (fast_tac FOL_cs 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   151
val wf_asym = result();
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   153
goal WF.thy "!!r. [| wf[A](r); a: A |] ==> <a,a> ~: r";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   154
by (wf_on_ind_tac "a" [] 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   155
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   156
val wf_on_not_refl = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   157
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   158
goal WF.thy "!!r. [| wf[A](r);  <a,b>:r;  <b,a>:r;  a:A;  b:A |] ==> P";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   159
by (subgoal_tac "ALL y:A. <a,y>:r --> <y,a>:r --> P" 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   160
by (wf_on_ind_tac "a" [] 2);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   161
by (fast_tac ZF_cs 2);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   162
by (fast_tac ZF_cs 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   163
val wf_on_asym = result();
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   164
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   165
(*Needed to prove well_ordI.  Could also reason that wf[A](r) means
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   166
  wf(r Int A*A);  thus wf( (r Int A*A)^+ ) and use wf_not_refl *)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   167
goal WF.thy
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   168
    "!!r. [| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   169
by (subgoal_tac
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   170
    "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P" 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   171
by (wf_on_ind_tac "a" [] 2);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   172
by (fast_tac ZF_cs 2);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   173
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   174
val wf_on_chain3 = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   175
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   176
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   177
(*retains the universal formula for later use!*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   178
val bchain_tac = EVERY' [rtac (bspec RS mp), assume_tac, assume_tac ];
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   179
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   180
(*transitive closure of a WF relation is WF provided A is downwards closed*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   181
val [wfr,subs] = goal WF.thy
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   182
    "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   183
by (rtac wf_onI2 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   184
by (bchain_tac 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   185
by (eres_inst_tac [("a","y")] (wfr RS wf_on_induct) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   186
by (rtac (impI RS ballI) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
by (etac tranclE 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   188
by (etac (bspec RS mp) 1 THEN assume_tac 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
by (fast_tac ZF_cs 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   190
by (cut_facts_tac [subs] 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   191
(*astar_tac is slightly faster*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   192
by (best_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   193
val wf_on_trancl = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   194
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   195
goal WF.thy "!!r. wf(r) ==> wf(r^+)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   196
by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   197
by (rtac (trancl_type RS field_rel_subset RSN (2, wf_on_subset_A)) 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   198
by (etac wf_on_trancl 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
val wf_trancl = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   202
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   203
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
(** r-``{a} is the set of everything under a in r **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
val underI = standard (vimage_singleton_iff RS iffD2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
val underD = standard (vimage_singleton_iff RS iffD1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
(** is_recfun **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
val [major] = goalw WF.thy [is_recfun_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
    "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
by (rtac (major RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
by (rtac (lamI RS rangeI RS lam_type) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
val is_recfun_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
val [isrec,rel] = goalw WF.thy [is_recfun_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
    "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))";
443
10884e64c241 added parentheses made necessary by new constrain precedence
clasohm
parents: 437
diff changeset
   220
by (res_inst_tac [("P", "%x.?t(x) = (?u::i)")] (isrec RS ssubst) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
by (rtac (rel RS underI RS beta) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
val apply_recfun = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
(*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
  spec RS mp  instantiates induction hypotheses*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
fun indhyp_tac hyps =
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   227
    resolve_tac (TrueI::refl::hyps) ORELSE' 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
    (cut_facts_tac hyps THEN'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
       DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
		        eresolve_tac [underD, transD, spec RS mp]));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   232
(*** NOTE! some simplifications need a different solver!! ***)
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   233
val wf_super_ss = ZF_ss setsolver indhyp_tac;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
val prems = goalw WF.thy [is_recfun_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
    "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
\    <x,a>:r --> <x,b>:r --> f`x=g`x";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
by (wf_ind_tac "x" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
by (rewtac restrict_def);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   242
by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
val is_recfun_equal_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
val prems as [wfr,transr,recf,recg,_] = goal WF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
    "[| wf(r);  trans(r);       \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
\       is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
\    restrict(f, r-``{b}) = g";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
by (rtac (consI1 RS restrict_type RS fun_extension) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
by (etac is_recfun_type 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
by (ALLGOALS
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   254
    (asm_simp_tac (wf_super_ss addsimps
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
		   [ [wfr,transr,recf,recg] MRS is_recfun_equal ])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
val is_recfun_cut = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
(*** Main Existence Lemma ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
val prems = goal WF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
    "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
by (rtac fun_extension 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
by (REPEAT (ares_tac [is_recfun_equal] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
     ORELSE eresolve_tac [is_recfun_type,underD] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
val is_recfun_functional = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
(*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
val prems = goalw WF.thy [the_recfun_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
    "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |]  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
\    ==> is_recfun(r, a, H, the_recfun(r,a,H))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
by (rtac (ex1I RS theI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
by (REPEAT (ares_tac (prems@[is_recfun_functional]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
val is_the_recfun = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
val prems = goal WF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
    "[| wf(r);  trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
by (wf_ind_tac "a" prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
by (res_inst_tac [("f", "lam y: r-``{a1}. wftrec(r,y,H)")] is_the_recfun 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
by (REPEAT (assume_tac 2));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
(*Applying the substitution: must keep the quantified assumption!!*)
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   284
by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
by (fold_tac [is_recfun_def]);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   286
by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
by (rtac is_recfun_type 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
by (ALLGOALS
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   289
    (asm_simp_tac
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   290
     (wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
val unfold_the_recfun = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
(*** Unfolding wftrec ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
val prems = goal WF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
    "[| wf(r);  trans(r);  <b,a>:r |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
\    restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
by (REPEAT (ares_tac (prems @ [is_recfun_cut, unfold_the_recfun]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
val the_recfun_cut = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
(*NOT SUITABLE FOR REWRITING since it is recursive!*)
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   303
goalw WF.thy [wftrec_def]
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   304
    "!!r. [| wf(r);  trans(r) |] ==> \
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   305
\         wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   307
by (ALLGOALS (asm_simp_tac
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   308
	(ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
val wftrec = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
(** Removal of the premise trans(r) **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
(*NOT SUITABLE FOR REWRITING since it is recursive!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
val [wfr] = goalw WF.thy [wfrec_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
    "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
by (rtac trans_trancl 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   318
by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
by (etac r_into_trancl 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
by (rtac subset_refl 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
val wfrec = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
val rew::prems = goal WF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
    "[| !!x. h(x)==wfrec(r,x,H);  wf(r) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
\    h(a) = H(a, lam x: r-``{a}. h(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
by (REPEAT (resolve_tac (prems@[wfrec]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
val def_wfrec = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
val prems = goal WF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
    "[| wf(r);  a:A;  field(r)<=A;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
\       !!x u. [| x: A;  u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x)   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
\    |] ==> wfrec(r,a,H) : B(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
by (res_inst_tac [("a","a")] wf_induct2 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
by (rtac (wfrec RS ssubst) 4);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
by (REPEAT (ares_tac (prems@[lam_type]) 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
     ORELSE eresolve_tac [spec RS mp, underD] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
val wfrec_type = result();
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   340
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   341
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   342
goalw WF.thy [wf_on_def, wfrec_on_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   343
 "!!A r. [| wf[A](r);  a: A |] ==> \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   344
\        wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   345
by (etac (wfrec RS trans) 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   346
by (asm_simp_tac (ZF_ss addsimps [vimage_Int_square, cons_subset_iff]) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   347
val wfrec_on = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 6
diff changeset
   348