implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
authorhuffman
Mon Jun 10 06:08:12 2013 -0700 (2013-06-10)
changeset 52358f4c4bcb0d564
parent 52357 a5d3730043c2
child 52359 0eafa146b399
implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
src/HOL/Tools/transfer.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Tools/transfer.ML	Mon Jun 10 08:39:48 2013 -0400
     1.2 +++ b/src/HOL/Tools/transfer.ML	Mon Jun 10 06:08:12 2013 -0700
     1.3 @@ -16,6 +16,7 @@
     1.4    val transfer_add: attribute
     1.5    val transfer_del: attribute
     1.6    val transferred_attribute: thm list -> attribute
     1.7 +  val untransferred_attribute: thm list -> attribute
     1.8    val transfer_domain_add: attribute
     1.9    val transfer_domain_del: attribute
    1.10    val transfer_rule_of_term: Proof.context -> bool -> term -> thm
    1.11 @@ -606,6 +607,39 @@
    1.12      handle THM _ => thm
    1.13  *)
    1.14  
    1.15 +fun untransferred ctxt extra_rules thm =
    1.16 +  let
    1.17 +    val start_rule = @{thm untransfer_start}
    1.18 +    val rules = extra_rules @ get_transfer_raw ctxt
    1.19 +    val eq_rules = get_relator_eq_raw ctxt
    1.20 +    val err_msg = "Transfer failed to convert goal to an object-logic formula"
    1.21 +    val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
    1.22 +    val thm1 = Drule.forall_intr_vars thm
    1.23 +    val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
    1.24 +                |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
    1.25 +    val thm2 = thm1
    1.26 +      |> Thm.certify_instantiate (instT, [])
    1.27 +      |> Raw_Simplifier.rewrite_rule pre_simps
    1.28 +    val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
    1.29 +    val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
    1.30 +    val rule = transfer_rule_of_term ctxt' true t
    1.31 +    val tac =
    1.32 +      rtac (thm2 RS start_rule) 1 THEN
    1.33 +      (rtac rule
    1.34 +        THEN_ALL_NEW
    1.35 +          (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
    1.36 +            THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
    1.37 +        handle TERM (_, ts) => raise TERM (err_msg, ts)
    1.38 +    val thm3 = Goal.prove_internal [] @{cpat "Trueprop ?P"} (K tac)
    1.39 +    val tnames = map (fst o dest_TFree o snd) instT
    1.40 +  in
    1.41 +    thm3
    1.42 +      |> Raw_Simplifier.rewrite_rule post_simps
    1.43 +      |> Raw_Simplifier.norm_hhf
    1.44 +      |> Drule.generalize (tnames, [])
    1.45 +      |> Drule.zero_var_indexes
    1.46 +  end
    1.47 +
    1.48  (** Methods and attributes **)
    1.49  
    1.50  val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
    1.51 @@ -648,9 +682,15 @@
    1.52  fun transferred_attribute thms = Thm.rule_attribute
    1.53    (fn context => transferred (Context.proof_of context) thms)
    1.54  
    1.55 +fun untransferred_attribute thms = Thm.rule_attribute
    1.56 +  (fn context => untransferred (Context.proof_of context) thms)
    1.57 +
    1.58  val transferred_attribute_parser =
    1.59    Attrib.thms >> transferred_attribute
    1.60  
    1.61 +val untransferred_attribute_parser =
    1.62 +  Attrib.thms >> untransferred_attribute
    1.63 +
    1.64  (* Theory setup *)
    1.65  
    1.66  val relator_eq_setup =
    1.67 @@ -697,6 +737,8 @@
    1.68       "transfer domain rule for transfer method"
    1.69    #> Attrib.setup @{binding transferred} transferred_attribute_parser
    1.70       "raw theorem transferred to abstract theorem using transfer rules"
    1.71 +  #> Attrib.setup @{binding untransferred} untransferred_attribute_parser
    1.72 +     "abstract theorem transferred to raw theorem using transfer rules"
    1.73    #> Global_Theory.add_thms_dynamic
    1.74       (@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get)
    1.75    #> Method.setup @{binding transfer} (transfer_method true)
     2.1 --- a/src/HOL/Transfer.thy	Mon Jun 10 08:39:48 2013 -0400
     2.2 +++ b/src/HOL/Transfer.thy	Mon Jun 10 06:08:12 2013 -0700
     2.3 @@ -96,6 +96,9 @@
     2.4  lemma transfer_prover_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
     2.5    by simp
     2.6  
     2.7 +lemma untransfer_start: "\<lbrakk>Q; Rel (op =) P Q\<rbrakk> \<Longrightarrow> P"
     2.8 +  unfolding Rel_def by simp
     2.9 +
    2.10  lemma Rel_eq_refl: "Rel (op =) x x"
    2.11    unfolding Rel_def ..
    2.12