147 val cnstrs_env = cnstr_full_names ~~ cnstr_full_names' |
147 val cnstrs_env = cnstr_full_names ~~ cnstr_full_names' |
148 |
148 |
149 val bn_fun_strs = get_bn_fun_strs bn_funs |
149 val bn_fun_strs = get_bn_fun_strs bn_funs |
150 val bn_fun_strs' = add_raws bn_fun_strs |
150 val bn_fun_strs' = add_raws bn_fun_strs |
151 val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' |
151 val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' |
152 val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) |
152 val bn_fun_full_env = map (apply2 (Long_Name.qualify thy_name)) |
153 (bn_fun_strs ~~ bn_fun_strs') |
153 (bn_fun_strs ~~ bn_fun_strs') |
154 |
154 |
155 val raw_dts = rawify_dts dts dts_env |
155 val raw_dts = rawify_dts dts dts_env |
156 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
156 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
157 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses |
157 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses |
158 |
158 |
159 val (raw_full_dt_names', thy1) = |
159 val (raw_full_dt_names', thy1) = |
160 Datatype.add_datatype Datatype.default_config raw_dts thy |
160 Old_Datatype.add_datatype Old_Datatype_Aux.default_config raw_dts thy |
161 |
161 |
162 val lthy1 = Named_Target.theory_init thy1 |
162 val lthy1 = Named_Target.theory_init thy1 |
163 |
163 |
164 val dtinfos = map (Datatype.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names' |
164 val dtinfos = map (Old_Datatype_Data.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names' |
165 val {descr, ...} = hd dtinfos |
165 val {descr, ...} = hd dtinfos |
166 |
166 |
167 val raw_tys = Datatype_Aux.get_rec_types descr |
167 val raw_tys = Old_Datatype_Aux.get_rec_types descr |
168 val raw_ty_args = hd raw_tys |
168 val raw_ty_args = hd raw_tys |
169 |> snd o dest_Type |
169 |> snd o dest_Type |
170 |> map dest_TFree |
170 |> map dest_TFree |
171 |
171 |
172 val raw_cns_info = all_dtyp_constrs_types descr |
172 val raw_cns_info = all_dtyp_constrs_types descr |
177 val raw_induct_thm = #induct (hd dtinfos) |
177 val raw_induct_thm = #induct (hd dtinfos) |
178 val raw_induct_thms = #inducts (hd dtinfos) |
178 val raw_induct_thms = #inducts (hd dtinfos) |
179 val raw_exhaust_thms = map #exhaust dtinfos |
179 val raw_exhaust_thms = map #exhaust dtinfos |
180 val raw_size_trms = map HOLogic.size_const raw_tys |
180 val raw_size_trms = map HOLogic.size_const raw_tys |
181 val raw_size_thms = these (Option.map ((fn ths => drop (length ths div 2) ths) o fst o snd) |
181 val raw_size_thms = these (Option.map ((fn ths => drop (length ths div 2) ths) o fst o snd) |
182 (BNF_LFP_Size.lookup_size lthy1 (hd raw_full_dt_names'))) |
182 (BNF_LFP_Size.size_of lthy1 (hd raw_full_dt_names'))) |
183 |
183 |
184 val raw_result = RawDtInfo |
184 val raw_result = RawDtInfo |
185 {raw_dt_names = raw_full_dt_names', |
185 {raw_dt_names = raw_full_dt_names', |
186 raw_dts = raw_dts, |
186 raw_dts = raw_dts, |
187 raw_tys = raw_tys, |
187 raw_tys = raw_tys, |
301 raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) |
301 raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) |
302 |
302 |
303 val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp lthy5) raw_funs_rsp_aux |
303 val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp lthy5) raw_funs_rsp_aux |
304 |
304 |
305 fun match_const cnst th = |
305 fun match_const cnst th = |
306 (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o prop_of) th = |
306 (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o Thm.prop_of) th = |
307 fst (dest_Const cnst); |
307 fst (dest_Const cnst); |
308 fun find_matching_rsp cnst = |
308 fun find_matching_rsp cnst = |
309 hd (filter (fn th => match_const cnst th) raw_funs_rsp); |
309 hd (filter (fn th => match_const cnst th) raw_funs_rsp); |
310 val raw_fv_rsp = map find_matching_rsp raw_fvs; |
310 val raw_fv_rsp = map find_matching_rsp raw_fvs; |
311 val raw_bn_rsp = map find_matching_rsp raw_bns; |
311 val raw_bn_rsp = map find_matching_rsp raw_bns; |
396 val qfv_bns = map #qconst qfv_bns_info |
396 val qfv_bns = map #qconst qfv_bns_info |
397 val qalpha_bns = map #qconst qalpha_bns_info |
397 val qalpha_bns = map #qconst qalpha_bns_info |
398 val qperm_bns = map #qconst qperm_bns_info |
398 val qperm_bns = map #qconst qperm_bns_info |
399 |
399 |
400 val _ = trace_msg (K "Lifting of theorems...") |
400 val _ = trace_msg (K "Lifting of theorems...") |
401 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def rel_prod_def |
401 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def rel_prod_sel |
402 prod.case} |
402 prod.case} |
403 |
403 |
404 val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, |
404 val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, |
405 qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps, |
405 qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps, |
406 qalpha_refl_thms, qalpha_sym_thms, qalpha_trans_thms ], lthyB) = |
406 qalpha_refl_thms, qalpha_sym_thms, qalpha_trans_thms ], lthyB) = |
450 member (op=) qfv_names lhs |
450 member (op=) qfv_names lhs |
451 | is_qfv_thm _ = false |
451 | is_qfv_thm _ = false |
452 |
452 |
453 val qsupp_constrs = qfv_defs |
453 val qsupp_constrs = qfv_defs |
454 |> map (simplify (put_simpset HOL_basic_ss lthyC |
454 |> map (simplify (put_simpset HOL_basic_ss lthyC |
455 addsimps (filter (is_qfv_thm o prop_of) qfv_supp_thms))) |
455 addsimps (filter (is_qfv_thm o Thm.prop_of) qfv_supp_thms))) |
456 |
456 |
457 val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp} |
457 val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp} |
458 val transform_thms = |
458 val transform_thms = |
459 [ @{lemma "a \<notin> (S \<union> T) \<longleftrightarrow> a \<notin> S \<and> a \<notin> T" by simp}, |
459 [ @{lemma "a \<notin> (S \<union> T) \<longleftrightarrow> a \<notin> S \<and> a \<notin> T" by simp}, |
460 @{lemma "a \<notin> (S - T) \<longleftrightarrow> a \<notin> S \<or> a \<in> T" by simp}, |
460 @{lemma "a \<notin> (S - T) \<longleftrightarrow> a \<notin> S \<or> a \<in> T" by simp}, |
546 let |
546 let |
547 fun prep_spec ((tname, tvs, mx), constrs) = |
547 fun prep_spec ((tname, tvs, mx), constrs) = |
548 ((tname, tvs, mx), constrs |> map (fn (c, atys, mx', _) => (c, map snd atys, mx'))) |
548 ((tname, tvs, mx), constrs |> map (fn (c, atys, mx', _) => (c, map snd atys, mx'))) |
549 |
549 |
550 val (dts, spec_ctxt) = |
550 val (dts, spec_ctxt) = |
551 Datatype.read_specs (map prep_spec dt_strs) thy |
551 Old_Datatype.read_specs (map prep_spec dt_strs) thy |
552 |
552 |
553 fun augment ((tname, tvs, mx), constrs) = |
553 fun augment ((tname, tvs, mx), constrs) = |
554 ((tname, map (apsnd (augment_sort thy)) tvs, mx), |
554 ((tname, map (apsnd (augment_sort thy)) tvs, mx), |
555 constrs |> map (fn (c, tys, mx') => (c, map (augment_sort_typ thy) tys, mx'))) |
555 constrs |> map (fn (c, tys, mx') => (c, map (augment_sort_typ thy) tys, mx'))) |
556 |
556 |
734 opt_name -- Parse.and_list1 dt_parser -- bnfun_parser >> tuple3 |
734 opt_name -- Parse.and_list1 dt_parser -- bnfun_parser >> tuple3 |
735 |
735 |
736 end |
736 end |
737 |
737 |
738 (* Command Keyword *) |
738 (* Command Keyword *) |
739 val _ = Outer_Syntax.local_theory @{command_spec "nominal_datatype"} |
739 val _ = Outer_Syntax.local_theory @{command_keyword nominal_datatype} |
740 "declaration of nominal datatypes" |
740 "declaration of nominal datatypes" |
741 (main_parser >> nominal_datatype2_cmd) |
741 (main_parser >> nominal_datatype2_cmd) |
742 *} |
742 *} |
743 |
743 |
744 |
744 end |
745 end |
|