src/ZF/Epsilon.ML
author paulson
Wed, 15 May 2002 10:42:32 +0200
changeset 13149 773657d466cb
parent 12814 2f5edb146f7e
permissions -rw-r--r--
better simplification of trivial existential equalities
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 782
diff changeset
     1
(*  Title:      ZF/epsilon.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 782
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
5809
bacf85370ce0 removed obsolete comment and "open" declaration
paulson
parents: 5505
diff changeset
     6
Epsilon induction and recursion
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
(*** Basic closure properties ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
    11
Goalw [eclose_def] "A <= eclose(A)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
by (rtac (nat_rec_0 RS equalityD2 RS subset_trans) 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    13
by (rtac (nat_0I RS UN_upper) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
    14
qed "arg_subset_eclose";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9211
diff changeset
    16
bind_thm ("arg_into_eclose", arg_subset_eclose RS subsetD);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
    18
Goalw [eclose_def,Transset_def] "Transset(eclose(A))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
by (rtac (subsetI RS ballI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
by (etac UN_E 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
by (rtac (nat_succI RS UN_I) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
by (etac (nat_rec_succ RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
by (etac UnionI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
by (assume_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
    26
qed "Transset_eclose";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
(* x : eclose(A) ==> x <= eclose(A) *)
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
    29
bind_thm ("eclose_subset",
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
    30
    rewrite_rule [Transset_def] Transset_eclose RS bspec);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
(* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
    33
bind_thm ("ecloseD", eclose_subset RS subsetD);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9211
diff changeset
    35
bind_thm ("arg_in_eclose_sing", arg_subset_eclose RS singleton_subsetD);
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9211
diff changeset
    36
bind_thm ("arg_into_eclose_sing", arg_in_eclose_sing RS ecloseD);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
(* This is epsilon-induction for eclose(A); see also eclose_induct_down...
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
   [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
   |] ==> P(a) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
*)
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
    42
bind_thm ("eclose_induct", Transset_eclose RSN (2, Transset_induct));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
(*Epsilon induction*)
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 8201
diff changeset
    45
val prems = Goal
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
    "[| !!x. ALL y:x. P(y) ==> P(x) |]  ==>  P(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
by (rtac (arg_in_eclose_sing RS eclose_induct) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
by (eresolve_tac prems 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
    49
qed "eps_induct";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
(*Perform epsilon-induction on i. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
fun eps_ind_tac a = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
    EVERY' [res_inst_tac [("a",a)] eps_induct,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 782
diff changeset
    54
            rename_last_tac a ["1"]];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
(*** Leastness of eclose ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
(** eclose(A) is the least transitive set including A as a subset. **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
    61
Goalw [Transset_def]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
    62
    "[| Transset(X);  A<=X;  n: nat |] ==> \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
\             nat_rec(n, A, %m r. Union(r)) <= X";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
by (etac nat_induct 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3889
diff changeset
    65
by (asm_simp_tac (simpset() addsimps [nat_rec_0]) 1);
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3889
diff changeset
    66
by (asm_simp_tac (simpset() addsimps [nat_rec_succ]) 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
    67
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
    68
qed "eclose_least_lemma";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
    70
Goalw [eclose_def]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
    71
     "[| Transset(X);  A<=X |] ==> eclose(A) <= X";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    72
by (rtac (eclose_least_lemma RS UN_least) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
by (REPEAT (assume_tac 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
    74
qed "eclose_least";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 8201
diff changeset
    77
val [major,base,step] = Goal
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 782
diff changeset
    78
    "[| a: eclose(b);                                           \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 782
diff changeset
    79
\       !!y.   [| y: b |] ==> P(y);                             \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 782
diff changeset
    80
\       !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)        \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
\    |] ==> P(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
by (rtac (major RSN (3, eclose_least RS subsetD RS CollectD2)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
by (rtac (CollectI RS subsetI) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
by (etac (arg_subset_eclose RS subsetD) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
by (etac base 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
by (rewtac Transset_def);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3889
diff changeset
    87
by (blast_tac (claset() addIs [step,ecloseD]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
    88
qed "eclose_induct_down";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5116
diff changeset
    90
Goal "Transset(X) ==> eclose(X) = X";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    91
by (etac ([eclose_least, arg_subset_eclose] MRS equalityI) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    92
by (rtac subset_refl 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
    93
qed "Transset_eclose_eq_arg";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
(*** Epsilon recursion ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
(*Unused...*)
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5116
diff changeset
    99
Goal "[| A: eclose(B);  B: eclose(C) |] ==> A: eclose(C)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
by (rtac ([Transset_eclose, eclose_subset] MRS eclose_least RS subsetD) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
by (REPEAT (assume_tac 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   102
qed "mem_eclose_trans";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
(*Variant of the previous lemma in a useable form for the sequel*)
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   105
Goal "[| A: eclose({B});  B: eclose({C}) |] ==> A: eclose({C})";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
by (rtac ([Transset_eclose, singleton_subsetI] MRS eclose_least RS subsetD) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
by (REPEAT (assume_tac 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   108
qed "mem_eclose_sing_trans";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
8201
a81d18b0a9b1 tidied some proofs
paulson
parents: 8127
diff changeset
   110
Goalw [Transset_def] "[| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j";
a81d18b0a9b1 tidied some proofs
paulson
parents: 8127
diff changeset
   111
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   112
qed "under_Memrel";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9211
diff changeset
   115
bind_thm ("under_Memrel_eclose", Transset_eclose RS under_Memrel);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9211
diff changeset
   117
bind_thm ("wfrec_ssubst", standard (wf_Memrel RS wfrec RS ssubst));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9211
diff changeset
   119
val [kmemj,jmemi] = goal (the_context ())
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
    "[| k:eclose({j});  j:eclose({i}) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
\    wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
by (rtac (kmemj RS eclose_induct) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
by (rtac wfrec_ssubst 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
by (rtac wfrec_ssubst 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3889
diff changeset
   125
by (asm_simp_tac (simpset() addsimps [under_Memrel_eclose,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 782
diff changeset
   126
                                  jmemi RSN (2,mem_eclose_sing_trans)]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   127
qed "wfrec_eclose_eq";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 8201
diff changeset
   129
Goal
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
    "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
by (rtac (arg_in_eclose_sing RS wfrec_eclose_eq) 1);
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 8201
diff changeset
   132
by (etac arg_into_eclose_sing 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   133
qed "wfrec_eclose_eq2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   135
Goalw [transrec_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
    "transrec(a,H) = H(a, lam x:a. transrec(x,H))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
by (rtac wfrec_ssubst 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3889
diff changeset
   138
by (simp_tac (simpset() addsimps [wfrec_eclose_eq2, arg_in_eclose_sing,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 782
diff changeset
   139
                              under_Memrel_eclose]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   140
qed "transrec";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
(*Avoids explosions in proofs; resolve it with a meta-level definition.*)
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 8201
diff changeset
   143
val rew::prems = Goal
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
    "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
by (REPEAT (resolve_tac (prems@[transrec]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   147
qed "def_transrec";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 8201
diff changeset
   149
val prems = Goal
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
    "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
\    |]  ==> transrec(a,H) : B(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1);
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1461
diff changeset
   153
by (stac transrec 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
by (REPEAT (ares_tac (prems @ [lam_type]) 1 ORELSE etac bspec 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   155
qed "transrec_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5116
diff changeset
   157
Goal "Ord(i) ==> eclose({i}) <= succ(i)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
by (etac (Ord_is_Transset RS Transset_succ RS eclose_least) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
by (rtac (succI1 RS singleton_subsetI) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   160
qed "eclose_sing_Ord";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 8201
diff changeset
   162
val prems = Goal
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
    "[| j: i;  Ord(i);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
\       !!x u. [| x: i;  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
\    |]  ==> transrec(j,H) : B(j)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
by (rtac transrec_type 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
by (rtac (Ord_in_Ord RS eclose_sing_Ord RS subsetD RS succE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   170
qed "Ord_transrec_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
(*** Rank ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   175
Goal "rank(a) = (UN y:a. succ(rank(y)))";
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1461
diff changeset
   176
by (stac (rank_def RS def_transrec) 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   177
by (Simp_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   178
qed "rank";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   180
Goal "Ord(rank(a))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
by (eps_ind_tac "a" 1);
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1461
diff changeset
   182
by (stac rank 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
by (rtac (Ord_succ RS Ord_UN) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
by (etac bspec 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
by (assume_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   186
qed "Ord_rank";
6071
1b2392ac5752 removal of DO_GOAL
paulson
parents: 6070
diff changeset
   187
Addsimps [Ord_rank];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 8201
diff changeset
   189
Goal "Ord(i) ==> rank(i) = i";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 8201
diff changeset
   190
by (etac trans_induct 1);
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1461
diff changeset
   191
by (stac rank 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3889
diff changeset
   192
by (asm_simp_tac (simpset() addsimps [Ord_equality]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   193
qed "rank_of_Ord";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5116
diff changeset
   195
Goal "a:b ==> rank(a) < rank(b)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
129
dc50a4b96d7b expandshort and other trivial changes
lcp
parents: 25
diff changeset
   197
by (etac (UN_I RS ltI) 1);
6071
1b2392ac5752 removal of DO_GOAL
paulson
parents: 6070
diff changeset
   198
by (rtac Ord_UN 2);
1b2392ac5752 removal of DO_GOAL
paulson
parents: 6070
diff changeset
   199
by Auto_tac;
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   200
qed "rank_lt";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 8201
diff changeset
   202
Goal "a: eclose(b) ==> rank(a) < rank(b)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 8201
diff changeset
   203
by (etac eclose_induct_down 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
by (etac rank_lt 1);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   205
by (etac (rank_lt RS lt_trans) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
by (assume_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   207
qed "eclose_rank_lt";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5116
diff changeset
   209
Goal "a<=b ==> rank(a) le rank(b)";
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   210
by (rtac subset_imp_le 1);
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1461
diff changeset
   211
by (stac rank 1);
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1461
diff changeset
   212
by (stac rank 1);
6071
1b2392ac5752 removal of DO_GOAL
paulson
parents: 6070
diff changeset
   213
by Auto_tac;
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   214
qed "rank_mono";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   216
Goal "rank(Pow(a)) = succ(rank(a))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
by (rtac (rank RS trans) 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 129
diff changeset
   218
by (rtac le_anti_sym 1);
6163
be8234f37e48 expandshort
paulson
parents: 6071
diff changeset
   219
by (rtac UN_upper_le 2);
be8234f37e48 expandshort
paulson
parents: 6071
diff changeset
   220
by (rtac UN_least_le 1);
12485
3df60299a6d0 Relaxed the precondition of UN_upper_le
paulson
parents: 9907
diff changeset
   221
by (auto_tac (claset() addIs [rank_mono], simpset() addsimps [Ord_UN]));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   222
qed "rank_Pow";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   224
Goal "rank(0) = 0";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
by (rtac (rank RS trans) 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   226
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   227
qed "rank_0";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   229
Goal "rank(succ(x)) = succ(rank(x))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
by (rtac (rank RS trans) 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   231
by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   232
by (etac succE 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   233
by (Blast_tac 1);
129
dc50a4b96d7b expandshort and other trivial changes
lcp
parents: 25
diff changeset
   234
by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   235
qed "rank_succ";
8127
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   236
Addsimps [rank_0, rank_succ];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   238
Goal "rank(Union(A)) = (UN x:A. rank(x))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
by (rtac equalityI 1);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   240
by (rtac (rank_mono RS le_imp_subset RS UN_least) 2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
by (etac Union_upper 2);
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1461
diff changeset
   242
by (stac rank 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
by (rtac UN_least 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
by (etac UnionE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
by (rtac subset_trans 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
by (etac (RepFunI RS Union_upper) 2);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   247
by (etac (rank_lt RS succ_leI RS le_imp_subset) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   248
qed "rank_Union";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   250
Goal "rank(eclose(a)) = rank(a)";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 129
diff changeset
   251
by (rtac le_anti_sym 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
by (rtac (arg_subset_eclose RS rank_mono) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   254
by (rtac (Ord_rank RS UN_least_le) 1);
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   255
by (etac (eclose_rank_lt RS succ_leI) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   256
qed "rank_eclose";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   258
Goalw [Pair_def] "rank(a) < rank(<a,b>)";
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   259
by (rtac (consI1 RS rank_lt RS lt_trans) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
by (rtac (consI1 RS consI2 RS rank_lt) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   261
qed "rank_pair1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   263
Goalw [Pair_def] "rank(b) < rank(<a,b>)";
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   264
by (rtac (consI1 RS consI2 RS rank_lt RS lt_trans) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
by (rtac (consI1 RS consI2 RS rank_lt) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   266
qed "rank_pair2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
8127
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   268
(*Not clear how to remove the P(a) condition, since the "then" part
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   269
  must refer to "a"*)
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   270
Goal "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)";
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   271
by (asm_simp_tac (simpset() addsimps [the_0, the_equality2]) 1);
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   272
qed "the_equality_if";
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   273
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   274
(*The premise is needed not just to fix i but to ensure f~=0*)
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   275
Goalw [apply_def] "i : domain(f) ==> rank(f`i) < rank(f)";
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   276
by (Clarify_tac 1);
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   277
by (subgoal_tac "rank(y) < rank(f)" 1);
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   278
by (blast_tac (claset() addIs [lt_trans, rank_lt, rank_pair2]) 2);
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   279
by (subgoal_tac "0 < rank(f)" 1);
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   280
by (etac (Ord_rank RS Ord_0_le RS lt_trans1) 2);
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   281
by (asm_simp_tac (simpset() addsimps [the_equality_if]) 1);
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   282
qed "rank_apply";
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   283
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   284
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
(*** Corollaries of leastness ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5116
diff changeset
   287
Goal "A:B ==> eclose(A)<=eclose(B)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
by (rtac (Transset_eclose RS eclose_least) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
by (etac (arg_into_eclose RS eclose_subset) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   290
qed "mem_eclose_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5116
diff changeset
   292
Goal "A<=B ==> eclose(A) <= eclose(B)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
by (rtac (Transset_eclose RS eclose_least) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
by (etac subset_trans 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
by (rtac arg_subset_eclose 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   296
qed "eclose_mono";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
(** Idempotence of eclose **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   300
Goal "eclose(eclose(A)) = eclose(A)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
by (rtac ([Transset_eclose, subset_refl] MRS eclose_least) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
by (rtac arg_subset_eclose 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 437
diff changeset
   304
qed "eclose_idem";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   305
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   306
(** Transfinite recursion for definitions based on the 
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   307
    three cases of ordinals **)
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   308
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   309
Goal "transrec2(0,a,b) = a";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   310
by (rtac (transrec2_def RS def_transrec RS trans) 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   311
by (Simp_tac 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   312
qed "transrec2_0";
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   313
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   314
Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   315
by (rtac (transrec2_def RS def_transrec RS trans) 1);
12814
paulson
parents: 12485
diff changeset
   316
by (simp_tac (simpset() addsimps [the_equality, if_P]) 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   317
qed "transrec2_succ";
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   318
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5116
diff changeset
   319
Goal "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   320
by (rtac (transrec2_def RS def_transrec RS trans) 1);
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5116
diff changeset
   321
by (Simp_tac 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3889
diff changeset
   322
by (blast_tac (claset() addSDs [Limit_has_0] addSEs [succ_LimitE]) 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   323
qed "transrec2_Limit";
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   324
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2033
diff changeset
   325
Addsimps [transrec2_0, transrec2_succ];
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2637
diff changeset
   326
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   327
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   328
(** recursor -- better than nat_rec; the succ case has no type requirement! **)
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   329
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   330
(*NOT suitable for rewriting*)
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   331
val lemma = recursor_def RS def_transrec RS trans;
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   332
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   333
Goal "recursor(a,b,0) = a";
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   334
by (rtac (nat_case_0 RS lemma) 1);
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   335
qed "recursor_0";
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   336
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   337
Goal "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))";
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   338
by (rtac lemma 1);
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   339
by (Simp_tac 1);
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   340
qed "recursor_succ";
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   341
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   342
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   343
(** rec: old version for compatibility **)
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   344
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   345
Goalw [rec_def] "rec(0,a,b) = a";
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   346
by (rtac recursor_0 1);
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   347
qed "rec_0";
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   348
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   349
Goalw [rec_def] "rec(succ(m),a,b) = b(m, rec(m,a,b))";
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   350
by (rtac recursor_succ 1);
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   351
qed "rec_succ";
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   352
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   353
Addsimps [rec_0, rec_succ];
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   354
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   355
val major::prems = Goal
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   356
    "[| n: nat;  \
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   357
\       a: C(0);  \
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   358
\       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   359
\    |] ==> rec(n,a,b) : C(n)";
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   360
by (rtac (major RS nat_induct) 1);
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   361
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   362
qed "rec_type";
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 5809
diff changeset
   363