src/bool/boolScript.sml

135                       ���TYPE_DEFINITION = \P:'a->bool. \rep:'b->'a.
136                               (!x' x''. (rep x' = rep x'') ==> (x' = x'')) /\
137                               (!x. P x = (?x'. x = rep x'))���);
2535       val rep = ���rep :'b -> 'a���
2537     GEN P (GEN rep
2539           (RIGHT_BETA (AP_THM TYPE_DEFINITION P)) rep)))
2558  *  |- !P. (?rep. TYPE_DEFINITION P rep) ==>                                 *
2559  *         ?rep abs. (!a. abs (rep a) = a) /\ !r. P r = (rep (abs r) = r)    *
2563    let val th1 = ASSUME ���?rep:'b->'a. TYPE_DEFINITION P rep���
2570                          (AP_TERM ���rep:'b->'a��� (ASSUME ���a:'b=a'���))
2573        val ABS = ���\r:'a. @a:'b. r = rep a���
2574        val absd =  RIGHT_BETA (AP_THM (REFL ABS) ���rep (a:'b):'a���)
2584        (* val rep = fst(strip_comb t1r) *)
2585        val rep = rator t1r
2586        val template = mk_eq(t1l, mk_comb(rep,v))
2589        val t2 = EXISTS (���?a:'b. r:'a = rep a���, ���^ABS r���)
2590                        (SYM(ASSUME ���rep(^ABS (r:'a):'b) = r���))
2591        val imp2 = DISCH ���rep(^ABS (r:'a):'b) = r���
2597        val eth2 = EXISTS (���?rep:'b->'a. ^(concl eth1)���,
2598                           ���rep:'b->'a���) eth1
2599        val result = DISCH (concl th1) (CHOOSE (���rep:'b->'a���,def) eth2)
4096   val typedef_eq = AP_THM typedef_eq0 ���rep:'a itself -> 'a���
4099   val onto' = INST [���x:'a��� |-> ���(rep:'a itself -> 'a) i���]
4102     val ex' = EXISTS (���?x':'a itself. rep i = rep x':'a���, ���i:'a itself���)
4103                      (REFL ���(rep:'a itself -> 'a) i���)
4115            CHOOSE (���rep:'a itself -> 'a���, ITSELF_TYPE_DEF) all_eq_thevalue)