tuned; store pred_simps
authorkuncar
Tue Nov 18 16:19:57 2014 +0100 (2014-11-18)
changeset 60220530112e8c6ba
parent 60219 2bce9a690b1e
child 60221 45545e6c0984
tuned; store pred_simps
src/HOL/Tools/Transfer/transfer.ML
src/HOL/Tools/Transfer/transfer_bnf.ML
     1.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Tue Nov 18 16:19:57 2014 +0100
     1.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Tue Nov 18 16:19:57 2014 +0100
     1.3 @@ -8,9 +8,12 @@
     1.4  signature TRANSFER =
     1.5  sig
     1.6    type pred_data
     1.7 +  val mk_pred_data: thm -> thm -> thm list -> pred_data
     1.8    val rel_eq_onp: pred_data -> thm
     1.9    val rel_eq_onp_with_tops: pred_data -> thm
    1.10    val pred_def: pred_data -> thm
    1.11 +  val pred_simps: pred_data -> thm list
    1.12 +  val update_pred_simps: thm list -> pred_data -> pred_data
    1.13  
    1.14    val bottom_rewr_conv: thm list -> conv
    1.15    val top_rewr_conv: thm list -> conv
    1.16 @@ -59,13 +62,23 @@
    1.17  val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq
    1.18    o HOLogic.dest_Trueprop o Thm.concl_of);
    1.19  
    1.20 -type pred_data = {pred_def:thm, rel_eq_onp: thm}
    1.21 +datatype pred_data = PRED_DATA of {pred_def:thm, rel_eq_onp: thm, pred_simps: thm list}
    1.22 +
    1.23 +fun mk_pred_data pred_def rel_eq_onp pred_simps = PRED_DATA {pred_def = pred_def, 
    1.24 +  rel_eq_onp = rel_eq_onp, pred_simps = pred_simps}
    1.25 +
    1.26 +fun map_pred_data' f1 f2 f3 (PRED_DATA {pred_def, rel_eq_onp, pred_simps}) =
    1.27 +  PRED_DATA {pred_def = f1 pred_def, rel_eq_onp = f2 rel_eq_onp, pred_simps = f3 pred_simps}
    1.28  
    1.29 -val rel_eq_onp: pred_data -> thm = #rel_eq_onp
    1.30 -val rel_eq_onp_with_tops: pred_data -> thm = (Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
    1.31 +fun rep_pred_data (PRED_DATA p) = p
    1.32 +val rel_eq_onp = #rel_eq_onp o rep_pred_data
    1.33 +val rel_eq_onp_with_tops = (Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
    1.34    (top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))))
    1.35 -  o #rel_eq_onp
    1.36 -val pred_def: pred_data -> thm = #pred_def
    1.37 +  o #rel_eq_onp o rep_pred_data
    1.38 +val pred_def = #pred_def o rep_pred_data
    1.39 +val pred_simps = #pred_simps o rep_pred_data
    1.40 +fun update_pred_simps new_pred_data = map_pred_data' I I (K new_pred_data)
    1.41 +
    1.42  
    1.43  structure Data = Generic_Data
    1.44  (
    1.45 @@ -796,9 +809,12 @@
    1.46  val untransferred_attribute_parser =
    1.47    Attrib.thms >> untransferred_attribute
    1.48  
    1.49 -fun morph_pred_data phi {pred_def, rel_eq_onp} = 
    1.50 -  {pred_def =  Morphism.thm phi pred_def,
    1.51 -  rel_eq_onp = Morphism.thm phi rel_eq_onp}
    1.52 +fun morph_pred_data phi = 
    1.53 +  let
    1.54 +    val morph_thm = Morphism.thm phi
    1.55 +  in
    1.56 +    map_pred_data' morph_thm morph_thm (map morph_thm)
    1.57 +  end
    1.58  
    1.59  fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name
    1.60    |> Option.map (morph_pred_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
     2.1 --- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Nov 18 16:19:57 2014 +0100
     2.2 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Nov 18 16:19:57 2014 +0100
     2.3 @@ -283,7 +283,7 @@
     2.4      fun qualify defname suffix = Binding.qualified true suffix defname
     2.5      val Domainp_rel_thm_name = qualify (base_name_of_bnf bnf) "Domainp_rel"
     2.6      val rel_eq_onp_thm_name = qualify (base_name_of_bnf bnf) "rel_eq_onp"
     2.7 -    val pred_data = {pred_def = pred_def, rel_eq_onp = rel_eq_onp}
     2.8 +    val pred_data = Transfer.mk_pred_data pred_def rel_eq_onp []
     2.9      val type_name = type_name_of_bnf bnf
    2.10      val relator_domain_attr = @{attributes [relator_domain]}
    2.11      val notes = [((Domainp_rel_thm_name, []), [([Domainp_rel], relator_domain_attr)]),
    2.12 @@ -398,18 +398,26 @@
    2.13      fun qualify defname suffix = Binding.qualified true suffix defname
    2.14      val pred_inject_thm_name = qualify (base_name_of_bnf (bnf_of_fp_sugar fp_sugar)) "pred_inject"
    2.15      val simp_attrs = @{attributes [simp]}
    2.16 +    val type_name = type_name_of_bnf (#fp_bnf fp_sugar)
    2.17 +    val pred_data = lookup_defined_pred_data lthy type_name 
    2.18 +      |> Transfer.update_pred_simps pred_injects
    2.19    in
    2.20 -    [((pred_inject_thm_name, []), [(pred_injects, simp_attrs)])]
    2.21 +    lthy 
    2.22 +    |> Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) 
    2.23 +    |> snd
    2.24 +    |> Local_Theory.declaration {syntax = false, pervasive = true}
    2.25 +      (fn phi => Transfer.update_pred_data type_name  (Transfer.morph_pred_data phi pred_data))
    2.26 +    |> Local_Theory.restore
    2.27    end
    2.28  
    2.29  
    2.30  fun transfer_fp_sugars_interpretation fp_sugar lthy =
    2.31    let
    2.32 -    val pred_injects_notes = pred_injects fp_sugar lthy
    2.33 +    val lthy = pred_injects fp_sugar lthy
    2.34      val transfer_rules_notes = fp_sugar_transfer_rules fp_sugar
    2.35    in
    2.36      lthy
    2.37 -    |> Local_Theory.notes (pred_injects_notes @ transfer_rules_notes)
    2.38 +    |> Local_Theory.notes transfer_rules_notes
    2.39      |> snd
    2.40    end
    2.41