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
     1 (*  Title: 	ZF/ex/Brouwer.ML
     2     ID:         $ $
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Infinite branching datatype definitions
     7   (1) the Brouwer ordinals
     8   (2) the Martin-Löf wellordering type
     9 *)
    10 
    11 open Brouwer;
    12 
    13 (** The Brouwer ordinals **)
    14 
    15 goal Brouwer.thy "brouwer = {0} + brouwer + (nat -> brouwer)";
    16 let open brouwer;  val rew = rewrite_rule con_defs in  
    17 by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
    18                      addEs [rew elim]) 1)
    19 end;
    20 val brouwer_unfold = result();
    21 
    22 (*A nicer induction rule than the standard one*)
    23 val major::prems = goal Brouwer.thy
    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))				\
    29 \    |] ==> P(b)";
    30 by (rtac (major RS brouwer.induct) 1);
    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);
    34 val brouwer_induct2 = result();
    35 
    36 
    37 (** The Martin-Löf wellordering type **)
    38 
    39 goal Brouwer.thy "Well(A,B) = (SUM x:A. B(x) -> Well(A,B))";
    40 let open Well;  val rew = rewrite_rule con_defs in  
    41 by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
    42                      addEs [rew elim]) 1)
    43 end;
    44 val Well_unfold = result();
    45 
    46 (*A nicer induction rule than the standard one*)
    47 val major::prems = goal Brouwer.thy
    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))						\
    51 \    |] ==> P(w)";
    52 by (rtac (major RS Well.induct) 1);
    53 by (REPEAT_SOME (ares_tac prems));
    54 by (fast_tac (ZF_cs addEs [fun_weaken_type]) 1);
    55 by (fast_tac (ZF_cs addDs [apply_type]) 1);
    56 val Well_induct2 = result();
    57 
    58 
    59 (*In fact it's isomorphic to nat, but we need a recursion operator for
    60   Well to prove this.*)
    61 goal Brouwer.thy "Well(bool, %x.x) = 1 + (1 -> Well(bool, %x.x))";
    62 by (resolve_tac [Well_unfold RS trans] 1);
    63 by (simp_tac (ZF_ss addsimps [Sigma_bool, Pi_empty1, succ_def]) 1);
    64 val Well_bool_unfold = result();