65 val dnam = Long_Name.base_name dname; |
67 val dnam = Long_Name.base_name dname; |
66 |
68 |
67 val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); |
69 val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); |
68 val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); |
70 val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); |
69 |
71 |
70 val copy_def = |
|
71 let fun r i = proj (Bound 0) eqs i; |
|
72 in |
|
73 ("copy_def", %%:(dname^"_copy") == /\ "f" |
|
74 (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep)) |
|
75 end; |
|
76 |
|
77 (* ----- axiom and definitions concerning induction ------------------------- *) |
72 (* ----- axiom and definitions concerning induction ------------------------- *) |
78 |
73 |
79 val reach_ax = ("reach", mk_trp(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n |
|
80 `%x_name === %:x_name)); |
|
81 val take_def = |
|
82 ("take_def", |
|
83 %%:(dname^"_take") == |
|
84 mk_lam("n",proj |
|
85 (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n)); |
|
86 val finite_def = |
74 val finite_def = |
87 ("finite_def", |
75 ("finite_def", |
88 %%:(dname^"_finite") == |
76 %%:(dname^"_finite") == |
89 mk_lam(x_name, |
77 mk_lam(x_name, |
90 mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); |
78 mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); |
91 |
79 |
92 in (dnam, |
80 in (dnam, |
93 (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]), |
81 (if definitional then [] else [abs_iso_ax, rep_iso_ax]), |
94 (if definitional then [] else [copy_def]) @ |
82 [finite_def]) |
95 [take_def, finite_def]) |
|
96 end; (* let (calc_axioms) *) |
83 end; (* let (calc_axioms) *) |
97 |
84 |
98 |
85 |
99 (* legacy type inference *) |
86 (* legacy type inference *) |
100 |
87 |
110 fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy; |
97 fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy; |
111 |
98 |
112 fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x); |
99 fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x); |
113 fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; |
100 fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; |
114 |
101 |
115 fun add_axioms definitional comp_dnam (eqs : eq list) thy' = |
102 fun add_axioms definitional eqs' comp_dnam (eqs : eq list) thy' = |
116 let |
103 let |
117 val comp_dname = Sign.full_bname thy' comp_dnam; |
104 val comp_dname = Sign.full_bname thy' comp_dnam; |
118 val dnames = map (fst o fst) eqs; |
105 val dnames = map (fst o fst) eqs; |
119 val x_name = idx_name dnames "x"; |
106 val x_name = idx_name dnames "x"; |
120 fun copy_app dname = %%:(dname^"_copy")`Bound 0; |
|
121 val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == |
|
122 /\ "f"(mk_ctuple (map copy_app dnames))); |
|
123 |
107 |
124 fun one_con (con, _, args) = |
108 fun one_con (con, _, args) = |
125 let |
109 let |
126 val nonrec_args = filter_out is_rec args; |
110 val nonrec_args = filter_out is_rec args; |
127 val rec_args = filter is_rec args; |
111 val rec_args = filter is_rec args; |
163 mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs))); |
147 mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs))); |
164 TEMPORARILY DISABLED *) |
148 TEMPORARILY DISABLED *) |
165 |
149 |
166 fun add_one (dnam, axs, dfs) = |
150 fun add_one (dnam, axs, dfs) = |
167 Sign.add_path dnam |
151 Sign.add_path dnam |
168 #> add_defs_infer dfs |
|
169 #> add_axioms_infer axs |
152 #> add_axioms_infer axs |
170 #> Sign.parent_path; |
153 #> Sign.parent_path; |
171 |
154 |
172 val map_tab = Domain_Isomorphism.get_map_tab thy'; |
155 val map_tab = Domain_Isomorphism.get_map_tab thy'; |
173 |
156 val axs = mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs; |
174 val thy = thy' |
157 val thy = thy' |> fold add_one axs; |
175 |> fold add_one (mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs); |
158 |
|
159 fun get_iso_info ((dname, tyvars), cons') = |
|
160 let |
|
161 fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t |
|
162 fun prod (_,args,_) = |
|
163 case args of [] => oneT |
|
164 | _ => foldr1 mk_sprodT (map opt_lazy args); |
|
165 val ax_abs_iso = PureThy.get_thm thy (dname ^ ".abs_iso"); |
|
166 val ax_rep_iso = PureThy.get_thm thy (dname ^ ".rep_iso"); |
|
167 val lhsT = Type(dname,tyvars); |
|
168 val rhsT = foldr1 mk_ssumT (map prod cons'); |
|
169 val rep_const = Const(dname^"_rep", lhsT ->> rhsT); |
|
170 val abs_const = Const(dname^"_abs", rhsT ->> lhsT); |
|
171 in |
|
172 { |
|
173 absT = lhsT, |
|
174 repT = rhsT, |
|
175 abs_const = abs_const, |
|
176 rep_const = rep_const, |
|
177 abs_inverse = ax_abs_iso, |
|
178 rep_inverse = ax_rep_iso |
|
179 } |
|
180 end; |
|
181 val dom_binds = map (Binding.name o Long_Name.base_name) dnames; |
|
182 val thy = |
|
183 if definitional then thy |
|
184 else snd (Domain_Isomorphism.define_take_functions |
|
185 (dom_binds ~~ map get_iso_info eqs') thy); |
|
186 |
|
187 fun add_one' (dnam, axs, dfs) = |
|
188 Sign.add_path dnam |
|
189 #> add_defs_infer dfs |
|
190 #> Sign.parent_path; |
|
191 val thy = fold add_one' axs thy; |
|
192 |
|
193 (* declare lub_take axioms *) |
|
194 local |
|
195 fun ax_lub_take dname = |
|
196 let |
|
197 val dnam : string = Long_Name.base_name dname; |
|
198 val take_const = %%:(dname^"_take"); |
|
199 val lub = %%: @{const_name lub}; |
|
200 val image = %%: @{const_name image}; |
|
201 val UNIV = %%: @{const_name UNIV}; |
|
202 val lhs = lub $ (image $ take_const $ UNIV); |
|
203 val ax = mk_trp (lhs === ID); |
|
204 in |
|
205 add_one (dnam, [("lub_take", ax)], []) |
|
206 end |
|
207 in |
|
208 val thy = |
|
209 if definitional then thy |
|
210 else fold ax_lub_take dnames thy |
|
211 end; |
176 |
212 |
177 val use_copy_def = length eqs>1 andalso not definitional; |
213 val use_copy_def = length eqs>1 andalso not definitional; |
178 in |
214 in |
179 thy |
215 thy |
180 |> Sign.add_path comp_dnam |
216 |> Sign.add_path comp_dnam |
181 |> add_defs_infer ((*bisim_def::*)(if use_copy_def then [copy_def] else [])) |
217 (* |
|
218 |> add_defs_infer [bisim_def] |
|
219 *) |
182 |> Sign.parent_path |
220 |> Sign.parent_path |
183 end; (* let (add_axioms) *) |
221 end; (* let (add_axioms) *) |
184 |
222 |
185 end; (* struct *) |
223 end; (* struct *) |