added pred_def, rel_eq_onp tuned
authorkuncar
Tue Nov 18 16:19:51 2014 +0100 (2014-11-18)
changeset 60216ef4f0b5b925e
parent 60215 5fb4990dfc73
child 60217 40c63ffce97f
added pred_def, rel_eq_onp tuned
src/HOL/Tools/Lifting/lifting_bnf.ML
src/HOL/Tools/Transfer/transfer.ML
src/HOL/Tools/Transfer/transfer_bnf.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Sun May 03 00:01:10 2015 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Tue Nov 18 16:19:51 2014 +0100
     1.3 @@ -87,9 +87,8 @@
     1.4  
     1.5  fun relator_eq_onp bnf ctxt =
     1.6    let
     1.7 -    val relator_eq_onp_thm = lookup_defined_pred_data ctxt (type_name_of_bnf bnf)
     1.8 -      |> Transfer.rel_eq_onp |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv 
     1.9 -          (Raw_Simplifier.rewrite ctxt false @{thms eq_onp_top_eq_eq[THEN eq_reflection]})))
    1.10 +    val relator_eq_onp_thm = lookup_defined_pred_data ctxt (type_name_of_bnf bnf) 
    1.11 +      |> Transfer.rel_eq_onp
    1.12    in
    1.13      [((Binding.empty, []), [([relator_eq_onp_thm], @{attributes [relator_eq_onp]})])]    
    1.14    end
     2.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Sun May 03 00:01:10 2015 +0200
     2.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Tue Nov 18 16:19:51 2014 +0100
     2.3 @@ -9,9 +9,12 @@
     2.4  sig
     2.5    type pred_data
     2.6    val rel_eq_onp: pred_data -> thm
     2.7 +  val rel_eq_onp_with_tops: pred_data -> thm
     2.8 +  val pred_def: pred_data -> thm
     2.9  
    2.10    val bottom_rewr_conv: thm list -> conv
    2.11    val top_rewr_conv: thm list -> conv
    2.12 +  val top_sweep_rewr_conv: thm list -> conv
    2.13  
    2.14    val prep_conv: conv
    2.15    val get_transfer_raw: Proof.context -> thm list
    2.16 @@ -46,15 +49,23 @@
    2.17  structure Transfer : TRANSFER =
    2.18  struct
    2.19  
    2.20 +fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
    2.21 +fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
    2.22 +fun top_sweep_rewr_conv rewrs = Conv.top_sweep_conv (K (Conv.rewrs_conv rewrs)) @{context}
    2.23 +
    2.24  (** Theory Data **)
    2.25  
    2.26  val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o apply2 snd) (single o fst);
    2.27  val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq
    2.28    o HOLogic.dest_Trueprop o Thm.concl_of);
    2.29  
    2.30 -type pred_data = {rel_eq_onp: thm}
    2.31 +type pred_data = {pred_def:thm, rel_eq_onp: thm}
    2.32  
    2.33  val rel_eq_onp: pred_data -> thm = #rel_eq_onp
    2.34 +val rel_eq_onp_with_tops: pred_data -> thm = (Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
    2.35 +  (top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))))
    2.36 +  o #rel_eq_onp
    2.37 +val pred_def: pred_data -> thm = #pred_def
    2.38  
    2.39  structure Data = Generic_Data
    2.40  (
    2.41 @@ -182,9 +193,6 @@
    2.42  
    2.43  (** Conversions **)
    2.44  
    2.45 -fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
    2.46 -fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
    2.47 -
    2.48  fun transfer_rel_conv conv =
    2.49    Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv)))
    2.50  
    2.51 @@ -788,7 +796,9 @@
    2.52  val untransferred_attribute_parser =
    2.53    Attrib.thms >> untransferred_attribute
    2.54  
    2.55 -fun morph_pred_data phi {rel_eq_onp} = {rel_eq_onp = Morphism.thm phi rel_eq_onp}
    2.56 +fun morph_pred_data phi {pred_def, rel_eq_onp} = 
    2.57 +  {pred_def =  Morphism.thm phi pred_def,
    2.58 +  rel_eq_onp = Morphism.thm phi rel_eq_onp}
    2.59  
    2.60  fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name
    2.61    |> Option.map (morph_pred_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
     3.1 --- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Sun May 03 00:01:10 2015 +0200
     3.2 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Nov 18 16:19:51 2014 +0100
     3.3 @@ -283,10 +283,7 @@
     3.4      fun qualify defname suffix = Binding.qualified true suffix defname
     3.5      val Domainp_rel_thm_name = qualify (base_name_of_bnf bnf) "Domainp_rel"
     3.6      val rel_eq_onp_thm_name = qualify (base_name_of_bnf bnf) "rel_eq_onp"
     3.7 -    val rel_eq_onp_internal = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
     3.8 -      (Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
     3.9 -        rel_eq_onp
    3.10 -    val pred_data = {rel_eq_onp = rel_eq_onp_internal}
    3.11 +    val pred_data = {pred_def = pred_def, rel_eq_onp = rel_eq_onp}
    3.12      val type_name = type_name_of_bnf bnf
    3.13      val relator_domain_attr = @{attributes [relator_domain]}
    3.14      val notes = [((Domainp_rel_thm_name, []), [([Domainp_rel], relator_domain_attr)]),
    3.15 @@ -340,7 +337,7 @@
    3.16          map type_name_of_bnf (#fp_nesting_bnfs fp_sugar)
    3.17        @ map type_name_of_bnf (#live_nesting_bnfs fp_sugar)
    3.18        @ map type_name_of_bnf (#bnfs (#fp_res fp_sugar)))
    3.19 -    val eq_onps = map (Transfer.rel_eq_onp o lookup_defined_pred_data lthy) involved_types
    3.20 +    val eq_onps = map (Transfer.rel_eq_onp_with_tops o lookup_defined_pred_data lthy) involved_types
    3.21      val old_lthy = lthy
    3.22      val (As, lthy) = mk_TFrees' (map Type.sort_of_atyp (lives_of_fp fp_sugar)) lthy
    3.23      val predTs = map mk_pred1T As