--- a/Nominal/Nominal2.thy Mon Apr 30 15:45:23 2012 +0100
+++ b/Nominal/Nominal2.thy Tue May 01 12:16:04 2012 +0100
@@ -53,7 +53,6 @@
ML {*
val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
-val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)
val simp_attr = Attrib.internal (K Simplifier.simp_add)
val induct_attr = Attrib.internal (K Induct.induct_simp_add)
*}
@@ -313,15 +312,24 @@
val _ = trace_msg (K "Proving respectfulness...")
val raw_funs_rsp_aux =
raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs)
-
- val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux
+
+ val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp) raw_funs_rsp_aux
+
+ fun match_const cnst th =
+ (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o prop_of) th =
+ fst (dest_Const cnst);
+ fun find_matching_rsp cnst =
+ hd (filter (fn th => match_const cnst th) raw_funs_rsp);
+ val raw_fv_rsp = map find_matching_rsp raw_fvs;
+ val raw_bn_rsp = map find_matching_rsp raw_bns;
+ val raw_fv_bn_rsp = map find_matching_rsp raw_fv_bns;
val raw_size_rsp =
raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt)
|> map mk_funs_rsp
val raw_constrs_rsp =
- raw_constrs_rsp lthy5 alpha_result (flat raw_all_cns) (alpha_bn_imp_thms @ raw_funs_rsp_aux)
+ raw_constrs_rsp lthy5 alpha_result raw_all_cns (alpha_bn_imp_thms @ raw_funs_rsp_aux)
val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
@@ -330,59 +338,54 @@
val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps
- (* noting the quot_respects lemmas *)
- val (_, lthy6) =
- Local_Theory.note ((Binding.empty, [rsp_attr]),
- raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @
- alpha_bn_rsp @ raw_perm_bn_rsp) lthy5
-
val _ = trace_msg (K "Defining the quotient types...")
val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts
-
- val (qty_infos, lthy7) =
+
+ val (qty_infos, lthy7) =
let
val AlphaResult {alpha_trms, alpha_tys, ...} = alpha_result
in
- define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
+ define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy5
end
val qtys = map #qtyp qty_infos
val qty_full_names = map (fst o dest_Type) qtys
- val qty_names = map Long_Name.base_name qty_full_names
+ val qty_names = map Long_Name.base_name qty_full_names
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, @{thm TrueI}))
- (get_cnstrs dts) raw_all_cns
+ (map2 o map2) (fn (b, _, mx) => fn (t, th) => (Variable.check_name b, t, mx, th))
+ (get_cnstrs dts) (map (op ~~) (raw_all_cns ~~ raw_constrs_rsp))
val qbns_descr =
- map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) bn_funs raw_bns
+ map2 (fn (b, _, mx) => fn (t, th) => (Variable.check_name b, t, mx, th)) bn_funs (raw_bns ~~ raw_bn_rsp)
- val qfvs_descr =
- map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_fvs
+ val qfvs_descr =
+ map2 (fn n => fn (t, th) => ("fv_" ^ n, t, NoSyn, th)) qty_names (raw_fvs ~~ raw_fv_rsp)
- val qfv_bns_descr =
- map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI}))
- bn_funs raw_fv_bns
+ val qfv_bns_descr =
+ map2 (fn (b, _, _) => fn (t, th) => ("fv_" ^ Variable.check_name b, t, NoSyn, th))
+ bn_funs (raw_fv_bns ~~ raw_fv_bn_rsp)
val qalpha_bns_descr =
let
val AlphaResult {alpha_bn_trms, ...} = alpha_result
in
- map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI}))
- bn_funs alpha_bn_trms
+ map2 (fn (b, _, _) => fn (t, th) => ("alpha_" ^ Variable.check_name b, t, NoSyn, th))
+ bn_funs (alpha_bn_trms ~~ alpha_bn_rsp)
end
val qperm_descr =
- map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, @{thm TrueI}))
- qty_names raw_perm_funs
+ map2 (fn n => fn (t, th) => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, th))
+ qty_names (raw_perm_funs ~~ (take (length raw_perm_funs) alpha_permute_rsp))
val qsize_descr =
- map2 (fn n => fn t => ("size_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_size_trms
+ map2 (fn n => fn (t, th) => ("size_" ^ n, t, NoSyn, th)) qty_names
+ (raw_size_trms ~~ (take (length raw_size_trms) raw_size_rsp))
val qperm_bn_descr =
- map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI}))
- bn_funs raw_perm_bns
+ map2 (fn (b, _, _) => fn (t, th) => ("permute_" ^ Variable.check_name b, t, NoSyn, th))
+ bn_funs (raw_perm_bns ~~ raw_perm_bn_rsp)
val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info),
lthy8) =