nominal2: comparison Nominal/NewParser.thy

equal deleted inserted replaced

-:c670a849af65
+:1e6160690546
 we need to also export a cases-rule for nominal datatypes
 size function
 *)
 section{* Interface for nominal_datatype *}
+ML {*
+(* attributes *)
+val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
+val rsp_attrib = Attrib.internal (K Quotient_Info.rsp_rules_add)
+*}
 ML {*
 (* nominal datatype parser *)
 local
 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
 else raise TEST lthy
 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
 val {descr, sorts, ...} = dtinfo
-val all_raw_tys = all_dtyps descr sorts
-val all_raw_ty_names = map (fn (_, (n, _, _)) => n) descr
 val all_raw_constrs =
 flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts))
+val all_raw_tys = all_dtyps descr sorts
+val all_raw_ty_names = map (fst o dest_Type) all_raw_tys
 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_ty_names
 val inject_thms = flat (map #inject dtinfos);
 val distinct_thms = flat (map #distinct dtinfos);
 val constr_thms = inject_thms @ distinct_thms
 val rel_dtinfos = List.take (dtinfos, (length dts));
 (* definitions of raw permutations *)
 val _ = warning "Definition of raw permutations";
 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) =
 if get_STEPS lthy0 > 1
-then Local_Theory.theory_result (define_raw_perms descr sorts raw_induct_thm (length dts)) lthy0
+then Local_Theory.theory_result
+(define_raw_perms all_raw_ty_names all_raw_tys all_raw_constrs raw_induct_thm) lthy0
 else raise TEST lthy0
+val lthy2a = Named_Target.reinit lthy2 lthy2
 (* noting the raw permutations as eqvt theorems *)
-val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
+val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a
-val (_, lthy2a) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2
-val thy = Local_Theory.exit_global lthy2a;
-val thy_name = Context.theory_name thy
 (* definition of raw fv_functions *)
 val _ = warning "Definition of raw fv-functions";
-val lthy3 = Named_Target.init NONE thy;
 val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
 if get_STEPS lthy3 > 2
 then raw_bn_decls all_raw_ty_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
 else raise TEST lthy3
 if get_STEPS lthy > 6
 then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_simps) lthy4
 else raise TEST lthy4
 (* noting the bn_eqvt lemmas in a temprorary theory *)
-val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
+val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), bn_eqvt) lthy4)
-val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4)
 val fv_eqvt =
 if get_STEPS lthy > 7
 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps)
 (Local_Theory.restore lthy_tmp)
 (Local_Theory.restore lthy_tmp)
 |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]})
 |> map (fn thm => thm RS @{thm sym})
 else raise TEST lthy4
-val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp)
+val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), fv_eqvt) lthy_tmp)
 val (alpha_eqvt, lthy6) =
 if get_STEPS lthy > 9
 then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
 else raise TEST lthy4
 val raw_constrs_rsp = raw_constrs_rsp all_raw_constrs alpha_trms alpha_intros
 (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6
 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
+(* noting the quot_respects lemmas *)
+val (_, lthy6a) =
+if get_STEPS lthy > 15
+then Local_Theory.note ((Binding.empty, [rsp_attrib]),
+raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp) lthy6
+else raise TEST lthy6
 (* defining the quotient type *)
 val _ = warning "Declaring the quotient types"
 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
 val qty_binds = map (fn (_, bind, _, _) => bind) dts
 val qty_names = map Name.of_binding qty_binds;
-val qty_full_names = map (Long_Name.qualify thy_name) qty_names (* not used *)
 val (qty_infos, lthy7) =
-if get_STEPS lthy > 15
+if get_STEPS lthy > 16
-then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
+then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a
-else raise TEST lthy6
+else raise TEST lthy6a
 val qtys = map #qtyp qty_infos
 (* defining of quotient term-constructors, binding functions, free vars functions *)
 val _ = warning "Defining the quotient constants"
 val qfvs_descr =
 map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs
 val qfv_bns_descr =
-map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs  raw_fv_bns
+map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns
 val qalpha_bns_descr =
 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs  alpha_bn_trms
+val qperm_descr =
+map2 (fn n => fn t => ("permute_" ^ n, t, NoSyn)) qty_names raw_perm_funs
 val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) =
-if get_STEPS lthy > 16
+if get_STEPS lthy > 17
 then
 lthy7
 |> qconst_defs qtys qconstrs_descr
 ||>> qconst_defs qtys qbns_descr
 ||>> qconst_defs qtys qfvs_descr
 ||>> qconst_defs qtys qfv_bns_descr
 ||>> qconst_defs qtys qalpha_bns_descr
 else raise TEST lthy7
+(*val _ = Local_Theory.theory_result
+(qperm_defs qtys qty_full_names qperm_descr raw_perm_laws) lthy8*)
 val qconstrs = map #qconst qconstrs_info
 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
 (* temporary theorem bindings *)
 val (_, lthy8') = lthy8
 |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts)
 ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff)
 ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps)
 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs)
 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps)
 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws)
 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
-||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp)
-||>> Local_Theory.note ((@{binding "size_rsp"}, []), raw_size_rsp)
-||>> Local_Theory.note ((@{binding "constrs_rsp"}, []), raw_constrs_rsp)
-||>> Local_Theory.note ((@{binding "permute_rsp"}, []), alpha_permute_rsp)
 val _ =
-if get_STEPS lthy > 17
+if get_STEPS lthy > 18
 then true else raise TEST lthy8'
 (* old stuff *)
+val thy = ProofContext.theory_of lthy8'
+val thy_name = Context.theory_name thy
+val qty_full_names = map (Long_Name.qualify thy_name) qty_names
 val _ = warning "Proving respects";
 val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
 val bns = raw_bns ~~ bn_nos;
 val thy = Local_Theory.exit_global lthy12c;
 val perm_names = map (fn x => "permute_" ^ x) qty_names
 val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs
 (* use Local_Theory.theory_result *)
 val thy' = qperm_defs qtys qty_full_names dd raw_perm_laws thy;
-val lthy13 = Named_Target.init NONE thy';
+val lthy13 = Named_Target.init "" thy';
 val q_name = space_implode "_" qty_names;
 fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
 val _ = warning "Lifting induction";
 val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs;

changeset 2398	1e6160690546
parent 2397	c670a849af65
child 2399	107c06267f33