nominal2: comparison Nominal/Nominal2.thy

equal deleted inserted replaced

-:d6fe94028a5d
+:ca6b4bc7a871
 end
 *}
 ML {*
-fun define_raw_dts dts bn_funs bn_eqs binds lthy =
+fun define_raw_dts dts bn_funs bn_eqs bclauses lthy =
 let
 val thy = Local_Theory.exit_global lthy
 val thy_name = Context.theory_name thy
 val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts
 val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name))
 (bn_fun_strs ~~ bn_fun_strs')
 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs
-val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds
+val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses
 val (raw_dt_full_names, thy1) =
 Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy
 val lthy1 = Named_Target.theory_init thy1
 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) =
 if get_STEPS lthy > 0
 then define_raw_dts dts bn_funs bn_eqs bclauses lthy
 else raise TEST lthy
+val _ = tracing ("raw_bclauses\n" ^ cat_lines (map @{make_string} raw_bclauses))
 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
 val {descr, sorts, ...} = dtinfo
 val raw_tys = all_dtyps descr sorts
 val raw_full_ty_names = map (fst o dest_Type) raw_tys
 |> map dest_TFree
 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names
 val raw_cns_info = all_dtyp_constrs_types descr sorts
-val raw_constrs = flat (map (map (fn (c, _, _, _) => c)) raw_cns_info)
+val raw_constrs = map (map (fn (c, _, _, _) => c)) raw_cns_info
 val raw_inject_thms = flat (map #inject dtinfos)
 val raw_distinct_thms = flat (map #distinct dtinfos)
 val raw_induct_thm = #induct dtinfo
 val raw_induct_thms = #inducts dtinfo
 (* definitions of raw permutations by primitive recursion *)
 val _ = warning "Definition of raw permutations";
 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) =
 if get_STEPS lthy0 > 0
-then define_raw_perms raw_full_ty_names raw_tys tvs raw_constrs raw_induct_thm lthy0
+then define_raw_perms raw_full_ty_names raw_tys tvs (flat raw_constrs) raw_induct_thm lthy0
 else raise TEST lthy0
 (* noting the raw permutations as eqvt theorems *)
 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a
 |> map mk_funs_rsp
 else raise TEST lthy6
 val raw_constrs_rsp =
 if get_STEPS lthy > 18
-then raw_constrs_rsp raw_constrs alpha_trms alpha_intros
+then raw_constrs_rsp (flat raw_constrs) alpha_trms alpha_intros
 (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6
 else raise TEST lthy6
 val alpha_permute_rsp =
 if get_STEPS lthy > 19
 val qty_full_names = map (fst o dest_Type) qtys
 val qty_names = map Long_Name.base_name qty_full_names
 (* defining of quotient term-constructors, binding functions, free vars functions *)
 val _ = warning "Defining the quotient constants"
-val qconstrs_descr =
+val qconstrs_descrs =
-flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts)
+map2 (map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx))) (get_cnstrs dts) raw_constrs
-|> map2 (fn t => fn (b, mx) => (b, t, mx)) raw_constrs
 val qbns_descr =
 map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns
 val qfvs_descr =
 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms
 val qperm_bn_descr =
 map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns
+val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info),
-val ((((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), lthy8)=
+lthy8) =
 if get_STEPS lthy > 24
 then
 lthy7
-|> define_qconsts qtys qconstrs_descr
+|> fold_map (define_qconsts qtys) qconstrs_descrs
 ||>> define_qconsts qtys qbns_descr
 ||>> define_qconsts qtys qfvs_descr
 ||>> define_qconsts qtys qfv_bns_descr
 ||>> define_qconsts qtys qalpha_bns_descr
 ||>> define_qconsts qtys qperm_bn_descr
 val lthy9a =
 if get_STEPS lthy > 26
 then define_qsizes qtys qty_full_names tvs qsize_descr lthy9
 else raise TEST lthy9
-val qtrms = map #qconst qconstrs_info
+val qtrms = map (map #qconst) qconstrs_infos
 val qbns = map #qconst qbns_info
 val qfvs = map #qconst qfvs_info
 val qfv_bns = map #qconst qfv_bns_info
 val qalpha_bns = map #qconst qalpha_bns_info
 val qperm_bns = map #qconst qperm_bns_info
 (* supports lemmas *)
 val _ = warning "Proving Supports Lemmas and fs-Instances"
 val qsupports_thms =
 if get_STEPS lthy > 29
-then prove_supports lthyB qperm_simps qtrms
+then prove_supports lthyB qperm_simps (flat qtrms)
 else raise TEST lthyB
 (* finite supp lemmas *)
 val qfsupp_thms =
 if get_STEPS lthy > 30
 (* fv - supp equality *)
 val _ = warning "Proving Equality between fv and supp"
 val qfv_supp_thms =
 if get_STEPS lthy > 32
-then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs
+then prove_fv_supp qtys (flat qtrms) qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs
 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
 else []
 (* postprocessing of eq and fv theorems *)

changeset 2600	ca6b4bc7a871
parent 2598	b136721eedb2
child 2601	89c55d36980f