40 |
40 |
41 (*** flip --- equations merely assumed; certain consequences proved ***) |
41 (*** flip --- equations merely assumed; certain consequences proved ***) |
42 |
42 |
43 val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type]; |
43 val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type]; |
44 |
44 |
45 goal QUniv.thy "!!b. b:bool ==> b Int X : quniv(A)"; |
45 goal QUniv.thy "!!b. b:bool ==> b Int X <= univ(eclose(A))"; |
46 by (etac boolE 1); |
46 by (fast_tac (quniv_cs addSEs [boolE]) 1); |
47 by (REPEAT (resolve_tac [one_Int_in_quniv, zero_Int_in_quniv] 1 |
47 val bool_Int_subset_univ = result(); |
48 ORELSE etac ssubst 1)); |
|
49 val bool_Int_into_quniv = result(); |
|
50 |
48 |
51 (* (!!x. x : A ==> B(x) : quniv(C)) ==> (UN x:A. B(x)) : quniv(C) *) |
49 val flip_cs = quniv_cs addSIs [not_type] |
52 val UN_in_quniv = standard (qunivD RS UN_least RS qunivI); |
50 addIs [bool_Int_subset_univ]; |
53 |
|
54 val Int_Vset_in_quniv = qunivD RS Int_Vset_subset RS qunivI; |
|
55 |
|
56 val flip_cs = |
|
57 ZF_cs addSIs [not_type, |
|
58 QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, |
|
59 zero_in_quniv, Int_Vset_0_subset RS qunivI, |
|
60 Transset_0, |
|
61 zero_Int_in_quniv, one_Int_in_quniv, |
|
62 QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv] |
|
63 addIs [bool_Int_into_quniv, Int_quniv_in_quniv]; |
|
64 |
51 |
65 (*Reasoning borrowed from llist_eq.ML; a similar proof works for all |
52 (*Reasoning borrowed from llist_eq.ML; a similar proof works for all |
66 "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*) |
53 "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*) |
67 goal LListFn.thy |
54 goal LListFn.thy |
68 "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) : quniv(bool)"; |
55 "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \ |
|
56 \ univ(eclose(bool))"; |
69 by (etac trans_induct 1); |
57 by (etac trans_induct 1); |
70 by (safe_tac ZF_cs); |
58 by (rtac ballI 1); |
71 by (etac LList.elim 1); |
59 by (etac LList.elim 1); |
72 by (asm_simp_tac flip_ss 1); |
60 by (asm_simp_tac flip_ss 1); |
73 by (asm_simp_tac flip_ss 2); |
61 by (asm_simp_tac flip_ss 2); |
74 by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs)); |
62 by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs)); |
|
63 (*LNil case*) |
75 by (fast_tac flip_cs 1); |
64 by (fast_tac flip_cs 1); |
76 by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac); |
65 (*LCons case*) |
77 (*0 case*) |
66 by (safe_tac flip_cs); |
78 by (fast_tac flip_cs 1); |
67 by (ALLGOALS (fast_tac (flip_cs addSEs [Ord_trans, make_elim bspec]))); |
79 (*succ(j) case*) |
|
80 by (fast_tac flip_cs 1); |
|
81 (*Limit(i) case*) |
|
82 by (etac (Limit_Vfrom_eq RS ssubst) 1); |
|
83 by (rtac (Int_UN_distrib RS ssubst) 1); |
|
84 by (rtac UN_in_quniv 1); |
|
85 by (fast_tac flip_cs 1); |
|
86 val flip_llist_quniv_lemma = result(); |
68 val flip_llist_quniv_lemma = result(); |
87 |
69 |
88 goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)"; |
70 goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)"; |
89 by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1); |
71 by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1); |
90 by (REPEAT (assume_tac 1)); |
72 by (REPEAT (assume_tac 1)); |
91 val flip_in_quniv = result(); |
73 val flip_in_quniv = result(); |
92 |
74 |
93 val [prem] = goal LListFn.thy "l : llist(bool) ==> flip(l): llist(bool)"; |
75 val [prem] = goal LListFn.thy "l : llist(bool) ==> flip(l): llist(bool)"; |
94 by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")] |
76 by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")] |