66 val iTs = OldTerm.term_tvars (prop_of (hd intrs)); |
66 val iTs = OldTerm.term_tvars (prop_of (hd intrs)); |
67 val Tvs = map TVar iTs; |
67 val Tvs = map TVar iTs; |
68 val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop |
68 val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop |
69 (Logic.strip_imp_concl (prop_of (hd intrs)))); |
69 (Logic.strip_imp_concl (prop_of (hd intrs)))); |
70 val params = map dest_Var (Library.take (nparms, ts)); |
70 val params = map dest_Var (Library.take (nparms, ts)); |
71 val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs); |
71 val tname = space_implode "_" (NameSpace.base_name s ^ "T" :: vs); |
72 fun constr_of_intr intr = (Sign.base_name (name_of_thm intr), |
72 fun constr_of_intr intr = (NameSpace.base_name (name_of_thm intr), |
73 map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @ |
73 map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @ |
74 filter_out (equal Extraction.nullT) (map |
74 filter_out (equal Extraction.nullT) (map |
75 (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)), |
75 (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)), |
76 NoSyn); |
76 NoSyn); |
77 in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn, |
77 in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn, |
110 val xs = map (Var o apfst (rpair 0)) |
110 val xs = map (Var o apfst (rpair 0)) |
111 (Name.variant_list used (replicate (length elTs) "x") ~~ elTs); |
111 (Name.variant_list used (replicate (length elTs) "x") ~~ elTs); |
112 val rT = if n then Extraction.nullT |
112 val rT = if n then Extraction.nullT |
113 else Type (space_implode "_" (s ^ "T" :: vs), |
113 else Type (space_implode "_" (s ^ "T" :: vs), |
114 map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs); |
114 map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs); |
115 val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT); |
115 val r = if n then Extraction.nullt else Var ((NameSpace.base_name s, 0), rT); |
116 val S = list_comb (h, params @ xs); |
116 val S = list_comb (h, params @ xs); |
117 val rvs = relevant_vars S; |
117 val rvs = relevant_vars S; |
118 val vs' = map fst rvs \\ vs; |
118 val vs' = map fst rvs \\ vs; |
119 val rname = space_implode "_" (s ^ "R" :: vs); |
119 val rname = space_implode "_" (s ^ "R" :: vs); |
120 |
120 |
193 | fun_of ts rts args used [] = |
193 | fun_of ts rts args used [] = |
194 let val xs = rev (rts @ ts) |
194 let val xs = rev (rts @ ts) |
195 in if conclT = Extraction.nullT |
195 in if conclT = Extraction.nullT |
196 then list_abs_free (map dest_Free xs, HOLogic.unit) |
196 then list_abs_free (map dest_Free xs, HOLogic.unit) |
197 else list_abs_free (map dest_Free xs, list_comb |
197 else list_abs_free (map dest_Free xs, list_comb |
198 (Free ("r" ^ Sign.base_name (name_of_thm intr), |
198 (Free ("r" ^ NameSpace.base_name (name_of_thm intr), |
199 map fastype_of (rev args) ---> conclT), rev args)) |
199 map fastype_of (rev args) ---> conclT), rev args)) |
200 end |
200 end |
201 |
201 |
202 in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end; |
202 in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end; |
203 |
203 |
215 HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs |
215 HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs |
216 else fs |
216 else fs |
217 end) (premss ~~ dummies); |
217 end) (premss ~~ dummies); |
218 val frees = fold Term.add_frees fs []; |
218 val frees = fold Term.add_frees fs []; |
219 val Ts = map fastype_of fs; |
219 val Ts = map fastype_of fs; |
220 fun name_of_fn intr = "r" ^ Sign.base_name (name_of_thm intr) |
220 fun name_of_fn intr = "r" ^ NameSpace.base_name (name_of_thm intr) |
221 in |
221 in |
222 fst (fold_map (fn concl => fn names => |
222 fst (fold_map (fn concl => fn names => |
223 let val T = Extraction.etype_of thy vs [] concl |
223 let val T = Extraction.etype_of thy vs [] concl |
224 in if T = Extraction.nullT then (Extraction.nullt, names) else |
224 in if T = Extraction.nullT then (Extraction.nullt, names) else |
225 let |
225 let |
243 thy |
243 thy |
244 |> f (map snd dts) |
244 |> f (map snd dts) |
245 |-> (fn dtinfo => pair ((map fst dts), SOME dtinfo)) |
245 |-> (fn dtinfo => pair ((map fst dts), SOME dtinfo)) |
246 handle DatatypeAux.Datatype_Empty name' => |
246 handle DatatypeAux.Datatype_Empty name' => |
247 let |
247 let |
248 val name = Sign.base_name name'; |
248 val name = NameSpace.base_name name'; |
249 val dname = Name.variant used "Dummy" |
249 val dname = Name.variant used "Dummy" |
250 in |
250 in |
251 thy |
251 thy |
252 |> add_dummies f (map (add_dummy name dname) dts) (dname :: used) |
252 |> add_dummies f (map (add_dummy name dname) dts) (dname :: used) |
253 end; |
253 end; |
294 val (ty_eqs, rlz_eqs) = split_list |
294 val (ty_eqs, rlz_eqs) = split_list |
295 (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss); |
295 (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss); |
296 |
296 |
297 val thy1' = thy1 |> |
297 val thy1' = thy1 |> |
298 Theory.copy |> |
298 Theory.copy |> |
299 Sign.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |> |
299 Sign.add_types (map (fn s => (NameSpace.base_name s, ar, NoSyn)) tnames) |> |
300 fold (fn s => AxClass.axiomatize_arity |
300 fold (fn s => AxClass.axiomatize_arity |
301 (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |> |
301 (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |> |
302 Extraction.add_typeof_eqns_i ty_eqs; |
302 Extraction.add_typeof_eqns_i ty_eqs; |
303 val dts = List.mapPartial (fn (s, rs) => if s mem rsets then |
303 val dts = List.mapPartial (fn (s, rs) => if s mem rsets then |
304 SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss; |
304 SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss; |
333 val (rlzpreds, rlzpreds') = split_list |
333 val (rlzpreds, rlzpreds') = split_list |
334 (distinct (op = o pairself (#1 o #1)) (map (fn rintr => |
334 (distinct (op = o pairself (#1 o #1)) (map (fn rintr => |
335 let |
335 let |
336 val Const (s, T) = head_of (HOLogic.dest_Trueprop |
336 val Const (s, T) = head_of (HOLogic.dest_Trueprop |
337 (Logic.strip_assums_concl rintr)); |
337 (Logic.strip_assums_concl rintr)); |
338 val s' = Sign.base_name s; |
338 val s' = NameSpace.base_name s; |
339 val T' = Logic.unvarifyT T |
339 val T' = Logic.unvarifyT T |
340 in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs)); |
340 in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs)); |
341 val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T)) |
341 val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T)) |
342 (List.take (snd (strip_comb |
342 (List.take (snd (strip_comb |
343 (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms)); |
343 (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms)); |
347 val (ind_info, thy3') = thy2 |> |
347 val (ind_info, thy3') = thy2 |> |
348 InductivePackage.add_inductive_global (serial_string ()) |
348 InductivePackage.add_inductive_global (serial_string ()) |
349 {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty, |
349 {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty, |
350 coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} |
350 coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} |
351 rlzpreds rlzparams (map (fn (rintr, intr) => |
351 rlzpreds rlzparams (map (fn (rintr, intr) => |
352 ((Binding.name (Sign.base_name (name_of_thm intr)), []), |
352 ((Binding.name (NameSpace.base_name (name_of_thm intr)), []), |
353 subst_atomic rlzpreds' (Logic.unvarify rintr))) |
353 subst_atomic rlzpreds' (Logic.unvarify rintr))) |
354 (rintrs ~~ maps snd rss)) [] ||> |
354 (rintrs ~~ maps snd rss)) [] ||> |
355 Sign.absolute_path; |
355 Sign.absolute_path; |
356 val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3'; |
356 val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3'; |
357 |
357 |