author | clasohm |
Tue, 30 Jan 1996 13:42:57 +0100 | |
changeset 1461 | 6bcb44e4d6e5 |
parent 782 | 200a16083201 |
child 2469 | b50b8c0eec01 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/ex/Brouwer.ML |
489 | 2 |
ID: $ $ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
489 | 4 |
Copyright 1994 University of Cambridge |
5 |
||
525
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
6 |
Infinite branching datatype definitions |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
7 |
(1) the Brouwer ordinals |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
8 |
(2) the Martin-Löf wellordering type |
489 | 9 |
*) |
10 |
||
515 | 11 |
open Brouwer; |
489 | 12 |
|
525
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
13 |
(** The Brouwer ordinals **) |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
14 |
|
489 | 15 |
goal Brouwer.thy "brouwer = {0} + brouwer + (nat -> brouwer)"; |
525
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
16 |
let open brouwer; val rew = rewrite_rule con_defs in |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
17 |
by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs) |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
18 |
addEs [rew elim]) 1) |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
19 |
end; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
525
diff
changeset
|
20 |
qed "brouwer_unfold"; |
489 | 21 |
|
22 |
(*A nicer induction rule than the standard one*) |
|
23 |
val major::prems = goal Brouwer.thy |
|
1461 | 24 |
"[| b: brouwer; \ |
25 |
\ P(Zero); \ |
|
26 |
\ !!b. [| b: brouwer; P(b) |] ==> P(Suc(b)); \ |
|
27 |
\ !!h. [| h: nat -> brouwer; ALL i:nat. P(h`i) \ |
|
28 |
\ |] ==> P(Lim(h)) \ |
|
489 | 29 |
\ |] ==> P(b)"; |
515 | 30 |
by (rtac (major RS brouwer.induct) 1); |
489 | 31 |
by (REPEAT_SOME (ares_tac prems)); |
32 |
by (fast_tac (ZF_cs addEs [fun_weaken_type]) 1); |
|
33 |
by (fast_tac (ZF_cs addDs [apply_type]) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
525
diff
changeset
|
34 |
qed "brouwer_induct2"; |
525
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
35 |
|
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
36 |
|
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
37 |
(** The Martin-Löf wellordering type **) |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
38 |
|
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
39 |
goal Brouwer.thy "Well(A,B) = (SUM x:A. B(x) -> Well(A,B))"; |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
40 |
let open Well; val rew = rewrite_rule con_defs in |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
41 |
by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs) |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
42 |
addEs [rew elim]) 1) |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
43 |
end; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
525
diff
changeset
|
44 |
qed "Well_unfold"; |
525
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
45 |
|
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
46 |
(*A nicer induction rule than the standard one*) |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
47 |
val major::prems = goal Brouwer.thy |
1461 | 48 |
"[| w: Well(A,B); \ |
49 |
\ !!a f. [| a: A; f: B(a) -> Well(A,B); ALL y: B(a). P(f`y) \ |
|
50 |
\ |] ==> P(Sup(a,f)) \ |
|
525
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
51 |
\ |] ==> P(w)"; |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
52 |
by (rtac (major RS Well.induct) 1); |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
53 |
by (REPEAT_SOME (ares_tac prems)); |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
54 |
by (fast_tac (ZF_cs addEs [fun_weaken_type]) 1); |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
55 |
by (fast_tac (ZF_cs addDs [apply_type]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
525
diff
changeset
|
56 |
qed "Well_induct2"; |
525
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
57 |
|
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
58 |
|
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
59 |
(*In fact it's isomorphic to nat, but we need a recursion operator for |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
60 |
Well to prove this.*) |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
61 |
goal Brouwer.thy "Well(bool, %x.x) = 1 + (1 -> Well(bool, %x.x))"; |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
62 |
by (resolve_tac [Well_unfold RS trans] 1); |
e62519a8497d
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
63 |
by (simp_tac (ZF_ss addsimps [Sigma_bool, Pi_empty1, succ_def]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
525
diff
changeset
|
64 |
qed "Well_bool_unfold"; |