add theory data for relator identity rules;
authorhuffman
Tue Apr 17 11:03:08 2012 +0200 (2012-04-17)
changeset 47503cb44d09d9d22
parent 47502 4c949049cd78
child 47504 aa1b8a59017f
child 47505 e33d957ae2bf
add theory data for relator identity rules;
preprocess transfer rules generated by lift_definition using relator rules
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/transfer.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Apr 17 09:12:15 2012 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Apr 17 11:03:08 2012 +0200
     1.3 @@ -183,6 +183,7 @@
     1.4        Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
     1.5  
     1.6      val transfer_thm = [quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}
     1.7 +        |> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy')
     1.8  
     1.9      fun qualify defname suffix = Binding.name suffix
    1.10        |> Binding.qualify true defname
     2.1 --- a/src/HOL/Tools/transfer.ML	Tue Apr 17 09:12:15 2012 +0200
     2.2 +++ b/src/HOL/Tools/transfer.ML	Tue Apr 17 11:03:08 2012 +0200
     2.3 @@ -8,6 +8,7 @@
     2.4  sig
     2.5    val fo_conv: Proof.context -> conv
     2.6    val prep_conv: conv
     2.7 +  val get_relator_eq: Proof.context -> thm list
     2.8    val transfer_add: attribute
     2.9    val transfer_del: attribute
    2.10    val transfer_tac: Proof.context -> int -> tactic
    2.11 @@ -24,6 +25,15 @@
    2.12    val description = "raw correspondence rule for transfer method"
    2.13  )
    2.14  
    2.15 +structure Relator_Eq = Named_Thms
    2.16 +(
    2.17 +  val name = @{binding relator_eq}
    2.18 +  val description = "relator equality rule (used by transfer method)"
    2.19 +)
    2.20 +
    2.21 +fun get_relator_eq ctxt =
    2.22 +  map (Thm.symmetric o mk_meta_eq) (Relator_Eq.get ctxt)
    2.23 +
    2.24  (** Conversions **)
    2.25  
    2.26  val App_rule = Thm.symmetric @{thm App_def}
    2.27 @@ -106,7 +116,7 @@
    2.28    let
    2.29      val T = RelT (HOLogic.dest_Trueprop (Logic.strip_assums_concl t))
    2.30      val cT = ctyp_of (Proof_Context.theory_of ctxt) T
    2.31 -    val rews = [@{thm fun_rel_eq [symmetric, THEN eq_reflection]}]
    2.32 +    val rews = get_relator_eq ctxt
    2.33      val thm1 = Drule.instantiate' [SOME cT] [] @{thm Rel_eq_refl}
    2.34      val thm2 = Raw_Simplifier.rewrite_rule rews thm1
    2.35    in
    2.36 @@ -177,6 +187,7 @@
    2.37  
    2.38  val setup =
    2.39    Data.setup
    2.40 +  #> Relator_Eq.setup
    2.41    #> Attrib.setup @{binding transfer_rule} transfer_attribute
    2.42       "correspondence rule for transfer method"
    2.43    #> Method.setup @{binding transfer} transfer_method
     3.1 --- a/src/HOL/Transfer.thy	Tue Apr 17 09:12:15 2012 +0200
     3.2 +++ b/src/HOL/Transfer.thy	Tue Apr 17 11:03:08 2012 +0200
     3.3 @@ -88,6 +88,8 @@
     3.4  
     3.5  setup Transfer.setup
     3.6  
     3.7 +declare fun_rel_eq [relator_eq]
     3.8 +
     3.9  lemma Rel_App [transfer_raw]:
    3.10    assumes "Rel (A ===> B) f g" and "Rel A x y"
    3.11    shows "Rel B (App f x) (App g y)"