# HG changeset patch # User nipkow # Date 1370873074 -7200 # Node ID 6b80ba92c4fe95d29579e6c3f89a173a56f9a77c # Parent ac7ac2b242a2dfdcdac1f75224af91778649fc72# Parent 7d5ad23b8245162922f3c9f9283d3be72453c9c5 merged diff -r 7d5ad23b8245 -r 6b80ba92c4fe src/HOL/Library/Quotient_Set.thy --- a/src/HOL/Library/Quotient_Set.thy Mon Jun 10 16:04:18 2013 +0200 +++ b/src/HOL/Library/Quotient_Set.thy Mon Jun 10 16:04:34 2013 +0200 @@ -217,32 +217,48 @@ shows "((A ===> op=) ===> set_rel A ===> set_rel A) Set.filter Set.filter" unfolding Set.filter_def[abs_def] fun_rel_def set_rel_def by blast +lemma bi_unique_set_rel_lemma: + assumes "bi_unique R" and "set_rel R X Y" + obtains f where "Y = image f X" and "inj_on f X" and "\x\X. R x (f x)" +proof + let ?f = "\x. THE y. R x y" + from assms show f: "\x\X. R x (?f x)" + apply (clarsimp simp add: set_rel_def) + apply (drule (1) bspec, clarify) + apply (rule theI2, assumption) + apply (simp add: bi_unique_def) + apply assumption + done + from assms show "Y = image ?f X" + apply safe + apply (clarsimp simp add: set_rel_def) + apply (drule (1) bspec, clarify) + apply (rule image_eqI) + apply (rule the_equality [symmetric], assumption) + apply (simp add: bi_unique_def) + apply assumption + apply (clarsimp simp add: set_rel_def) + apply (frule (1) bspec, clarify) + apply (rule theI2, assumption) + apply (clarsimp simp add: bi_unique_def) + apply (simp add: bi_unique_def, metis) + done + show "inj_on ?f X" + apply (rule inj_onI) + apply (drule f [rule_format]) + apply (drule f [rule_format]) + apply (simp add: assms(1) [unfolded bi_unique_def]) + done +qed + lemma finite_transfer [transfer_rule]: - assumes "bi_unique A" - shows "(set_rel A ===> op =) finite finite" - apply (rule fun_relI, rename_tac X Y) - apply (rule iffI) - apply (subgoal_tac "Y \ (\x. THE y. A x y) ` X") - apply (erule finite_subset, erule finite_imageI) - apply (rule subsetI, rename_tac y) - apply (clarsimp simp add: set_rel_def) - apply (drule (1) bspec, clarify) - apply (rule image_eqI) - apply (rule the_equality [symmetric]) - apply assumption - apply (simp add: assms [unfolded bi_unique_def]) - apply assumption - apply (subgoal_tac "X \ (\y. THE x. A x y) ` Y") - apply (erule finite_subset, erule finite_imageI) - apply (rule subsetI, rename_tac x) - apply (clarsimp simp add: set_rel_def) - apply (drule (1) bspec, clarify) - apply (rule image_eqI) - apply (rule the_equality [symmetric]) - apply assumption - apply (simp add: assms [unfolded bi_unique_def]) - apply assumption - done + "bi_unique A \ (set_rel A ===> op =) finite finite" + by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, + auto dest: finite_imageD) + +lemma card_transfer [transfer_rule]: + "bi_unique A \ (set_rel A ===> op =) card card" + by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, simp add: card_image) subsection {* Setup for lifting package *} diff -r 7d5ad23b8245 -r 6b80ba92c4fe src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Mon Jun 10 16:04:18 2013 +0200 +++ b/src/HOL/Tools/transfer.ML Mon Jun 10 16:04:34 2013 +0200 @@ -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 7d5ad23b8245 -r 6b80ba92c4fe src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Mon Jun 10 16:04:18 2013 +0200 +++ b/src/HOL/Transfer.thy Mon Jun 10 16:04:34 2013 +0200 @@ -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 .. diff -r 7d5ad23b8245 -r 6b80ba92c4fe src/HOL/ex/Transfer_Ex.thy --- a/src/HOL/ex/Transfer_Ex.thy Mon Jun 10 16:04:18 2013 +0200 +++ b/src/HOL/ex/Transfer_Ex.thy Mon Jun 10 16:04:34 2013 +0200 @@ -2,7 +2,7 @@ header {* Various examples for transfer procedure *} theory Transfer_Ex -imports Main +imports Main Transfer_Int_Nat begin lemma ex1: "(x::nat) + y = y + x" @@ -11,31 +11,55 @@ lemma "0 \ (y\int) \ 0 \ (x\int) \ x + y = y + x" by (fact ex1 [transferred]) +(* Using new transfer package *) +lemma "0 \ (x\int) \ 0 \ (y\int) \ x + y = y + x" + by (fact ex1 [untransferred]) + lemma ex2: "(a::nat) div b * b + a mod b = a" by (rule mod_div_equality) lemma "0 \ (b\int) \ 0 \ (a\int) \ a div b * b + a mod b = a" by (fact ex2 [transferred]) +(* Using new transfer package *) +lemma "0 \ (a\int) \ 0 \ (b\int) \ a div b * b + a mod b = a" + by (fact ex2 [untransferred]) + lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y" by auto lemma "\x\0\int. \y\0. \z\0. x + y \ z" by (fact ex3 [transferred nat_int]) +(* Using new transfer package *) +lemma "\x\int\{0..}. \y\{0..}. \z\{0..}. x + y \ z" + by (fact ex3 [untransferred]) + lemma ex4: "(x::nat) >= y \ (x - y) + y = x" by auto lemma "0 \ (x\int) \ 0 \ (y\int) \ y \ x \ tsub x y + y = x" by (fact ex4 [transferred]) +(* Using new transfer package *) +lemma "0 \ (y\int) \ 0 \ (x\int) \ y \ x \ tsub x y + y = x" + by (fact ex4 [untransferred]) + lemma ex5: "(2::nat) * \{..n} = n * (n + 1)" by (induct n rule: nat_induct, auto) lemma "0 \ (n\int) \ 2 * \{0..n} = n * (n + 1)" by (fact ex5 [transferred]) +(* Using new transfer package *) +lemma "0 \ (n\int) \ 2 * \{0..n} = n * (n + 1)" + by (fact ex5 [untransferred]) + lemma "0 \ (n\nat) \ 2 * \{0..n} = n * (n + 1)" by (fact ex5 [transferred, transferred]) -end \ No newline at end of file +(* Using new transfer package *) +lemma "0 \ (n\nat) \ 2 * \{..n} = n * (n + 1)" + by (fact ex5 [untransferred, Transfer.transferred]) + +end diff -r 7d5ad23b8245 -r 6b80ba92c4fe src/HOL/ex/Transfer_Int_Nat.thy --- a/src/HOL/ex/Transfer_Int_Nat.thy Mon Jun 10 16:04:18 2013 +0200 +++ b/src/HOL/ex/Transfer_Int_Nat.thy Mon Jun 10 16:04:34 2013 +0200 @@ -91,6 +91,24 @@ lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd" unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd) +lemma ZN_atMost [transfer_rule]: + "(ZN ===> set_rel ZN) (atLeastAtMost 0) atMost" + unfolding fun_rel_def ZN_def set_rel_def + by (clarsimp simp add: Bex_def, arith) + +lemma ZN_atLeastAtMost [transfer_rule]: + "(ZN ===> ZN ===> set_rel ZN) atLeastAtMost atLeastAtMost" + unfolding fun_rel_def ZN_def set_rel_def + by (clarsimp simp add: Bex_def, arith) + +lemma ZN_setsum [transfer_rule]: + "bi_unique A \ ((A ===> ZN) ===> set_rel A ===> ZN) setsum setsum" + apply (intro fun_relI) + apply (erule (1) bi_unique_set_rel_lemma) + apply (simp add: setsum.reindex int_setsum ZN_def fun_rel_def) + apply (rule setsum_cong2, simp) + done + text {* For derived operations, we can use the @{text "transfer_prover"} method to help generate transfer rules. *}