# HG changeset patch # User huffman # Date 1370869692 25200 # Node ID f4c4bcb0d5646196538434b4aaad91cd884b8008 # Parent a5d3730043c26feec537eb15aade0a1433d00e85 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction diff -r a5d3730043c2 -r f4c4bcb0d564 src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Mon Jun 10 08:39:48 2013 -0400 +++ b/src/HOL/Tools/transfer.ML Mon Jun 10 06:08:12 2013 -0700 @@ -16,6 +16,7 @@ val transfer_add: attribute val transfer_del: attribute val transferred_attribute: thm list -> attribute + val untransferred_attribute: thm list -> attribute val transfer_domain_add: attribute val transfer_domain_del: attribute val transfer_rule_of_term: Proof.context -> bool -> term -> thm @@ -606,6 +607,39 @@ handle THM _ => thm *) +fun untransferred ctxt extra_rules thm = + let + val start_rule = @{thm untransfer_start} + val rules = extra_rules @ get_transfer_raw ctxt + val eq_rules = get_relator_eq_raw ctxt + val err_msg = "Transfer failed to convert goal to an object-logic formula" + val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} + val thm1 = Drule.forall_intr_vars thm + val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) []) + |> map (fn v as ((a, _), S) => (v, TFree (a, S))) + val thm2 = thm1 + |> Thm.certify_instantiate (instT, []) + |> Raw_Simplifier.rewrite_rule pre_simps + val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt + val t = HOLogic.dest_Trueprop (Thm.concl_of thm2) + val rule = transfer_rule_of_term ctxt' true t + val tac = + rtac (thm2 RS start_rule) 1 THEN + (rtac rule + THEN_ALL_NEW + (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) + THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1 + handle TERM (_, ts) => raise TERM (err_msg, ts) + val thm3 = Goal.prove_internal [] @{cpat "Trueprop ?P"} (K tac) + val tnames = map (fst o dest_TFree o snd) instT + in + thm3 + |> Raw_Simplifier.rewrite_rule post_simps + |> Raw_Simplifier.norm_hhf + |> Drule.generalize (tnames, []) + |> Drule.zero_var_indexes + end + (** Methods and attributes **) val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => @@ -648,9 +682,15 @@ fun transferred_attribute thms = Thm.rule_attribute (fn context => transferred (Context.proof_of context) thms) +fun untransferred_attribute thms = Thm.rule_attribute + (fn context => untransferred (Context.proof_of context) thms) + val transferred_attribute_parser = Attrib.thms >> transferred_attribute +val untransferred_attribute_parser = + Attrib.thms >> untransferred_attribute + (* Theory setup *) val relator_eq_setup = @@ -697,6 +737,8 @@ "transfer domain rule for transfer method" #> Attrib.setup @{binding transferred} transferred_attribute_parser "raw theorem transferred to abstract theorem using transfer rules" + #> Attrib.setup @{binding untransferred} untransferred_attribute_parser + "abstract theorem transferred to raw theorem using transfer rules" #> Global_Theory.add_thms_dynamic (@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get) #> Method.setup @{binding transfer} (transfer_method true) diff -r a5d3730043c2 -r f4c4bcb0d564 src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Mon Jun 10 08:39:48 2013 -0400 +++ b/src/HOL/Transfer.thy Mon Jun 10 06:08:12 2013 -0700 @@ -96,6 +96,9 @@ lemma transfer_prover_start: "\x = x'; Rel R x' y\ \ Rel R x y" by simp +lemma untransfer_start: "\Q; Rel (op =) P Q\ \ P" + unfolding Rel_def by simp + lemma Rel_eq_refl: "Rel (op =) x x" unfolding Rel_def ..