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