73 val llist_quniv = result(); |
73 val llist_quniv = result(); |
74 |
74 |
75 val llist_subset_quniv = standard |
75 val llist_subset_quniv = standard |
76 (llist_mono RS (llist_quniv RSN (2,subset_trans))); |
76 (llist_mono RS (llist_quniv RSN (2,subset_trans))); |
77 |
77 |
78 (*** Equality for llist(A) as a greatest fixed point ***) |
78 (* Definition and use of LList_Eq has been moved to llist_eq.ML to allow |
79 |
79 automatic association between theory name and filename. *) |
80 structure LList_Eq = Co_Inductive_Fun |
|
81 (val thy = LList.thy addconsts [(["lleq"],"i=>i")]; |
|
82 val rec_doms = [("lleq","llist(A) <*> llist(A)")]; |
|
83 val sintrs = |
|
84 ["<LNil; LNil> : lleq(A)", |
|
85 "[| a:A; <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"]; |
|
86 val monos = []; |
|
87 val con_defs = []; |
|
88 val type_intrs = LList.intrs@[QSigmaI]; |
|
89 val type_elims = [QSigmaE2]); |
|
90 |
|
91 (** Alternatives for above: |
|
92 val con_defs = LList.con_defs |
|
93 val type_intrs = co_data_typechecks |
|
94 val type_elims = [quniv_QPair_E] |
|
95 **) |
|
96 |
|
97 val lleq_cs = subset_cs |
|
98 addSIs [succI1, Int_Vset_0_subset, |
|
99 QPair_Int_Vset_succ_subset_trans, |
|
100 QPair_Int_Vset_subset_trans]; |
|
101 |
|
102 (*Keep unfolding the lazy list until the induction hypothesis applies*) |
|
103 goal LList_Eq.thy |
|
104 "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'"; |
|
105 by (etac trans_induct 1); |
|
106 by (safe_tac subset_cs); |
|
107 by (etac LList_Eq.elim 1); |
|
108 by (safe_tac (subset_cs addSEs [QPair_inject])); |
|
109 by (rewrite_goals_tac LList.con_defs); |
|
110 by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac); |
|
111 (*0 case*) |
|
112 by (fast_tac lleq_cs 1); |
|
113 (*succ(j) case*) |
|
114 by (rewtac QInr_def); |
|
115 by (fast_tac lleq_cs 1); |
|
116 (*Limit(i) case*) |
|
117 by (etac (Limit_Vfrom_eq RS ssubst) 1); |
|
118 by (rtac (Int_UN_distrib RS ssubst) 1); |
|
119 by (fast_tac lleq_cs 1); |
|
120 val lleq_Int_Vset_subset_lemma = result(); |
|
121 |
|
122 val lleq_Int_Vset_subset = standard |
|
123 (lleq_Int_Vset_subset_lemma RS spec RS spec RS mp); |
|
124 |
|
125 |
|
126 (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*) |
|
127 val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)"; |
|
128 by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1); |
|
129 by (rtac (LList_Eq.dom_subset RS qconverse_type) 1); |
|
130 by (safe_tac qconverse_cs); |
|
131 by (etac LList_Eq.elim 1); |
|
132 by (ALLGOALS (fast_tac qconverse_cs)); |
|
133 val lleq_symmetric = result(); |
|
134 |
|
135 goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'"; |
|
136 by (rtac equalityI 1); |
|
137 by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1 |
|
138 ORELSE etac lleq_symmetric 1)); |
|
139 val lleq_implies_equal = result(); |
|
140 |
|
141 val [eqprem,lprem] = goal LList_Eq.thy |
|
142 "[| l=l'; l: llist(A) |] ==> <l;l'> : lleq(A)"; |
|
143 by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1); |
|
144 by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1); |
|
145 by (safe_tac qpair_cs); |
|
146 by (etac LList.elim 1); |
|
147 by (ALLGOALS (fast_tac qpair_cs)); |
|
148 val equal_llist_implies_leq = result(); |
|
149 |
|
150 |
|