diff -r 4049a2651dd9 -r 01ff621599bc Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Wed Jul 06 15:59:11 2011 +0200 +++ b/Nominal/Nominal2.thy Thu Jul 07 16:16:42 2011 +0200 @@ -145,7 +145,7 @@ ML {* (* definition of the raw datatype *) -fun define_raw_dts dts bn_funs bn_eqs bclauses lthy = +fun define_raw_dts dts cnstr_names cnstr_tys bn_funs bn_eqs bclauses lthy = let val thy = Local_Theory.exit_global lthy val thy_name = Context.theory_name thy @@ -155,8 +155,6 @@ val dt_full_names' = add_raws dt_full_names val dts_env = dt_full_names ~~ dt_full_names' - val cnstr_names = get_cnstr_strs dts - val cnstr_tys = get_typed_cnstrs dts val cnstr_full_names = map (Long_Name.qualify thy_name) cnstr_names val cnstr_full_names' = map (fn (x, y) => Long_Name.qualify thy_name (Long_Name.qualify (add_raw x) (add_raw y))) cnstr_tys @@ -168,16 +166,52 @@ 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_full_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 bclauses - val (raw_dt_full_names, thy1) = - Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy + val (raw_full_dt_names', thy1) = + Datatype.add_datatype Datatype.default_config raw_full_dt_names raw_dts thy val lthy1 = Named_Target.theory_init thy1 + + val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) raw_full_dt_names' + val {descr, sorts, ...} = hd dtinfos + + val raw_tys = Datatype_Aux.get_rec_types descr sorts + val raw_ty_args = hd raw_tys + |> snd o dest_Type + |> map dest_TFree + + val raw_cns_info = all_dtyp_constrs_types descr sorts + val raw_all_cns = (map o 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 (hd dtinfos) + val raw_induct_thms = #inducts (hd dtinfos) + val raw_exhaust_thms = map #exhaust dtinfos + val raw_size_trms = map HOLogic.size_const raw_tys + val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy1) (hd raw_full_dt_names') + |> `(fn thms => (length thms) div 2) + |> uncurry drop + + val raw_result = RawDtInfo + {raw_dt_names = raw_full_dt_names', + raw_dts = raw_dts, + raw_tys = raw_tys, + raw_ty_args = raw_ty_args, + raw_cns_info = raw_cns_info, + raw_all_cns = raw_all_cns, + raw_inject_thms = raw_inject_thms, + raw_distinct_thms = raw_distinct_thms, + raw_induct_thm = raw_induct_thm, + raw_induct_thms = raw_induct_thms, + raw_exhaust_thms = raw_exhaust_thms, + raw_size_trms = raw_size_trms, + raw_size_thms = raw_size_thms} in - (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy1) + (raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_result, lthy1) end *} @@ -185,62 +219,52 @@ ML {* fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy = let - val _ = trace_msg (K "Defining raw datatypes...") - val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy0) = - define_raw_dts dts bn_funs bn_eqs bclauses lthy + val cnstr_names = get_cnstr_strs dts + val cnstr_tys = get_typed_cnstrs dts - val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_dt_names - val {descr, sorts, ...} = hd dtinfos - - val raw_tys = Datatype_Aux.get_rec_types descr sorts - val tvs = hd raw_tys - |> snd o dest_Type - |> map dest_TFree + val _ = trace_msg (K "Defining raw datatypes...") + val (raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_dt_info, lthy0) = + define_raw_dts dts cnstr_names cnstr_tys bn_funs bn_eqs bclauses lthy - val raw_cns_info = all_dtyp_constrs_types descr sorts - val raw_constrs = (map o 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 (hd dtinfos) - val raw_induct_thms = #inducts (hd dtinfos) - val raw_exhaust_thms = map #exhaust dtinfos - val raw_size_trms = map HOLogic.size_const raw_tys - val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names) - |> `(fn thms => (length thms) div 2) - |> uncurry drop + val RawDtInfo + {raw_dt_names, + raw_tys, + raw_ty_args, + raw_all_cns, + raw_inject_thms, + raw_distinct_thms, + raw_induct_thm, + raw_induct_thms, + raw_exhaust_thms, + raw_size_trms, + raw_size_thms, ...} = raw_dt_info val _ = trace_msg (K "Defining raw permutations...") - val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = - define_raw_perms raw_dt_names raw_tys tvs (flat raw_constrs) raw_induct_thm lthy0 + val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = define_raw_perms raw_dt_info lthy0 (* noting the raw permutations as eqvt theorems *) val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a val _ = trace_msg (K "Defining raw fv- and bn-functions...") val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_inducts, lthy3a) = - define_raw_bns raw_dt_names raw_dts raw_bn_funs raw_bn_eqs - (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 + define_raw_bns raw_dt_info raw_bn_funs raw_bn_eqs lthy3 (* defining the permute_bn functions *) val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = - define_raw_bn_perms raw_tys raw_bn_info raw_cns_info - (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a + define_raw_bn_perms raw_dt_info raw_bn_info lthy3a val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) = - define_raw_fvs raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses - (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b + define_raw_fvs raw_dt_info raw_bn_info raw_bclauses lthy3b val _ = trace_msg (K "Defining alpha relations...") val (alpha_result, lthy4) = - define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c + define_raw_alpha raw_dt_info raw_bn_info raw_bclauses raw_fvs lthy3c val _ = trace_msg (K "Proving distinct theorems...") - val alpha_distincts = - raw_prove_alpha_distincts lthy4 alpha_result raw_distinct_thms raw_dt_names + val alpha_distincts = raw_prove_alpha_distincts lthy4 alpha_result raw_dt_info val _ = trace_msg (K "Proving eq-iff theorems...") - val alpha_eq_iff = raw_prove_alpha_eq_iff lthy4 alpha_result raw_distinct_thms raw_inject_thms + val alpha_eq_iff = raw_prove_alpha_eq_iff lthy4 alpha_result raw_dt_info val _ = trace_msg (K "Proving equivariance of bns, fvs, size and alpha...") val raw_bn_eqvt = @@ -253,11 +277,15 @@ raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) (Local_Theory.restore lthy_tmp) - val raw_size_eqvt = - raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) - (Local_Theory.restore lthy_tmp) - |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]}) - |> map (fn thm => thm RS @{thm sym}) + val raw_size_eqvt = + let + val RawDtInfo {raw_size_trms, raw_size_thms, raw_induct_thms, ...} = raw_dt_info + in + raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) + (Local_Theory.restore lthy_tmp) + |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]}) + |> map (fn thm => thm RS @{thm sym}) + end val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) @@ -293,7 +321,7 @@ |> map mk_funs_rsp val raw_constrs_rsp = - raw_constrs_rsp lthy5 alpha_result (flat raw_constrs) (alpha_bn_imp_thms @ raw_funs_rsp_aux) + raw_constrs_rsp lthy5 alpha_result (flat raw_all_cns) (alpha_bn_imp_thms @ raw_funs_rsp_aux) val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt @@ -324,7 +352,7 @@ val _ = trace_msg (K "Defining the quotient constants...") val qconstrs_descrs = - (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) (get_cnstrs dts) raw_constrs + (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) (get_cnstrs dts) raw_all_cns val qbns_descr = map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) bn_funs raw_bns @@ -362,10 +390,10 @@ ||>> define_qconsts qtys qperm_bn_descr val lthy9 = - define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8 + define_qperms qtys qty_full_names raw_ty_args qperm_descr raw_perm_laws lthy8 val lthy9a = - define_qsizes qtys qty_full_names tvs qsize_descr lthy9 + define_qsizes qtys qty_full_names raw_ty_args qsize_descr lthy9 val qtrms = (map o map) #qconst qconstrs_infos val qbns = map #qconst qbns_info @@ -408,7 +436,7 @@ val qfsupp_thms = prove_fsupp lthyB qtys qinduct qsupports_thms (* fs instances *) - val lthyC = fs_instance qtys qty_full_names tvs qfsupp_thms lthyB + val lthyC = fs_instance qtys qty_full_names raw_ty_args qfsupp_thms lthyB val _ = trace_msg (K "Proving equality between fv and supp...") val qfv_supp_thms =