--- 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 "\<forall>x\<in>X. R x (f x)"
+proof
+ let ?f = "\<lambda>x. THE y. R x y"
+ from assms show f: "\<forall>x\<in>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 \<subseteq> (\<lambda>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 \<subseteq> (\<lambda>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 \<Longrightarrow> (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 \<Longrightarrow> (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 *}
--- 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)
--- 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: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
by simp
+lemma untransfer_start: "\<lbrakk>Q; Rel (op =) P Q\<rbrakk> \<Longrightarrow> P"
+ unfolding Rel_def by simp
+
lemma Rel_eq_refl: "Rel (op =) x x"
unfolding Rel_def ..
--- 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 \<le> (y\<Colon>int) \<Longrightarrow> 0 \<le> (x\<Colon>int) \<Longrightarrow> x + y = y + x"
by (fact ex1 [transferred])
+(* Using new transfer package *)
+lemma "0 \<le> (x\<Colon>int) \<Longrightarrow> 0 \<le> (y\<Colon>int) \<Longrightarrow> 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 \<le> (b\<Colon>int) \<Longrightarrow> 0 \<le> (a\<Colon>int) \<Longrightarrow> a div b * b + a mod b = a"
by (fact ex2 [transferred])
+(* Using new transfer package *)
+lemma "0 \<le> (a\<Colon>int) \<Longrightarrow> 0 \<le> (b\<Colon>int) \<Longrightarrow> 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 "\<forall>x\<ge>0\<Colon>int. \<forall>y\<ge>0. \<exists>z\<ge>0. x + y \<le> z"
by (fact ex3 [transferred nat_int])
+(* Using new transfer package *)
+lemma "\<forall>x\<Colon>int\<in>{0..}. \<forall>y\<in>{0..}. \<exists>z\<in>{0..}. x + y \<le> z"
+ by (fact ex3 [untransferred])
+
lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
by auto
lemma "0 \<le> (x\<Colon>int) \<Longrightarrow> 0 \<le> (y\<Colon>int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
by (fact ex4 [transferred])
+(* Using new transfer package *)
+lemma "0 \<le> (y\<Colon>int) \<Longrightarrow> 0 \<le> (x\<Colon>int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
+ by (fact ex4 [untransferred])
+
lemma ex5: "(2::nat) * \<Sum>{..n} = n * (n + 1)"
by (induct n rule: nat_induct, auto)
lemma "0 \<le> (n\<Colon>int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
by (fact ex5 [transferred])
+(* Using new transfer package *)
+lemma "0 \<le> (n\<Colon>int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
+ by (fact ex5 [untransferred])
+
lemma "0 \<le> (n\<Colon>nat) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
by (fact ex5 [transferred, transferred])
-end
\ No newline at end of file
+(* Using new transfer package *)
+lemma "0 \<le> (n\<Colon>nat) \<Longrightarrow> 2 * \<Sum>{..n} = n * (n + 1)"
+ by (fact ex5 [untransferred, Transfer.transferred])
+
+end
--- 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 \<Longrightarrow> ((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. *}