--- a/src/HOL/IsaMakefile Tue Apr 03 22:04:50 2012 +0200
+++ b/src/HOL/IsaMakefile Tue Apr 03 22:31:00 2012 +0200
@@ -306,6 +306,7 @@
Sledgehammer.thy \
SMT.thy \
String.thy \
+ Transfer.thy \
Typerep.thy \
$(SRC)/Provers/Arith/assoc_fold.ML \
$(SRC)/Provers/Arith/cancel_numeral_factor.ML \
@@ -394,6 +395,7 @@
Tools/SMT/z3_proof_tools.ML \
Tools/string_code.ML \
Tools/string_syntax.ML \
+ Tools/transfer.ML \
$(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
--- a/src/HOL/Lifting.thy Tue Apr 03 22:04:50 2012 +0200
+++ b/src/HOL/Lifting.thy Tue Apr 03 22:31:00 2012 +0200
@@ -6,7 +6,7 @@
header {* Lifting package *}
theory Lifting
-imports Plain Equiv_Relations
+imports Plain Equiv_Relations Transfer
keywords
"print_quotmaps" "print_quotients" :: diag and
"lift_definition" :: thy_goal and
@@ -18,7 +18,7 @@
("Tools/Lifting/lifting_setup.ML")
begin
-subsection {* Function map and function relation *}
+subsection {* Function map *}
notation map_fun (infixr "--->" 55)
@@ -26,29 +26,6 @@
"(id ---> id) = id"
by (simp add: fun_eq_iff)
-definition
- fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" (infixr "===>" 55)
-where
- "fun_rel R1 R2 = (\<lambda>f g. \<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
-
-lemma fun_relI [intro]:
- assumes "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
- shows "(R1 ===> R2) f g"
- using assms by (simp add: fun_rel_def)
-
-lemma fun_relE:
- assumes "(R1 ===> R2) f g" and "R1 x y"
- obtains "R2 (f x) (g y)"
- using assms by (simp add: fun_rel_def)
-
-lemma fun_rel_eq:
- shows "((op =) ===> (op =)) = (op =)"
- by (auto simp add: fun_eq_iff elim: fun_relE)
-
-lemma fun_rel_eq_rel:
- shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"
- by (simp add: fun_rel_def)
-
subsection {* Quotient Predicate *}
definition
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/transfer.ML Tue Apr 03 22:31:00 2012 +0200
@@ -0,0 +1,176 @@
+(* Title: HOL/Tools/transfer.ML
+ Author: Brian Huffman, TU Muenchen
+
+Generic theorem transfer method.
+*)
+
+signature TRANSFER =
+sig
+ val fo_conv: Proof.context -> conv
+ val prep_conv: conv
+ val transfer_add: attribute
+ val transfer_del: attribute
+ val transfer_tac: Proof.context -> int -> tactic
+ val correspondence_tac: Proof.context -> int -> tactic
+ val setup: theory -> theory
+end
+
+structure Transfer : TRANSFER =
+struct
+
+structure Data = Named_Thms
+(
+ val name = @{binding transfer_raw}
+ val description = "raw correspondence rule for transfer method"
+)
+
+(** Conversions **)
+
+val App_rule = Thm.symmetric @{thm App_def}
+val Abs_rule = Thm.symmetric @{thm Abs_def}
+val Rel_rule = Thm.symmetric @{thm Rel_def}
+
+fun dest_funcT cT =
+ (case Thm.dest_ctyp cT of [T, U] => (T, U)
+ | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))
+
+fun App_conv ct =
+ let val (cT, cU) = dest_funcT (Thm.ctyp_of_term ct)
+ in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] App_rule end
+
+fun Abs_conv ct =
+ let val (cT, cU) = dest_funcT (Thm.ctyp_of_term ct)
+ in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Abs_rule end
+
+fun Rel_conv ct =
+ let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)
+ val (cU, _) = dest_funcT cT'
+ in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
+
+fun Trueprop_conv cv ct =
+ (case Thm.term_of ct of
+ Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
+ | _ => raise CTERM ("Trueprop_conv", [ct]))
+
+(* Conversion to insert tags on every application and abstraction. *)
+fun fo_conv ctxt ct = (
+ Conv.combination_conv (fo_conv ctxt then_conv App_conv) (fo_conv ctxt)
+ else_conv
+ Conv.abs_conv (fo_conv o snd) ctxt then_conv Abs_conv
+ else_conv
+ Conv.all_conv) ct
+
+(* Conversion to preprocess a correspondence rule *)
+fun prep_conv ct = (
+ Conv.implies_conv Conv.all_conv prep_conv
+ else_conv
+ Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))
+ else_conv
+ Conv.all_conv) ct
+
+(* Conversion to prep a proof goal containing a correspondence rule *)
+fun correspond_conv ctxt ct = (
+ Conv.forall_conv (correspond_conv o snd) ctxt
+ else_conv
+ Conv.implies_conv Conv.all_conv (correspond_conv ctxt)
+ else_conv
+ Trueprop_conv
+ (Conv.combination_conv
+ (Conv.combination_conv Rel_conv (fo_conv ctxt)) (fo_conv ctxt))
+ else_conv
+ Conv.all_conv) ct
+
+
+(** Transfer proof method **)
+
+fun bnames (t $ u) = bnames t @ bnames u
+ | bnames (Abs (x,_,t)) = x :: bnames t
+ | bnames _ = []
+
+fun rename [] t = (t, [])
+ | rename (x::xs) ((c as Const (@{const_name Abs}, _)) $ Abs (_, T, t)) =
+ let val (t', xs') = rename xs t
+ in (c $ Abs (x, T, t'), xs') end
+ | rename xs0 (t $ u) =
+ let val (t', xs1) = rename xs0 t
+ val (u', xs2) = rename xs1 u
+ in (t' $ u', xs2) end
+ | rename xs t = (t, xs)
+
+fun cert ctxt t = cterm_of (Proof_Context.theory_of ctxt) t
+
+fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y
+
+(* Tactic to correspond a value to itself *)
+fun eq_tac ctxt = SUBGOAL (fn (t, i) =>
+ let
+ val T = RelT (HOLogic.dest_Trueprop (Logic.strip_assums_concl t))
+ val cT = ctyp_of (Proof_Context.theory_of ctxt) T
+ val rews = [@{thm fun_rel_eq [symmetric, THEN eq_reflection]}]
+ val thm1 = Drule.instantiate' [SOME cT] [] @{thm Rel_eq_refl}
+ val thm2 = Raw_Simplifier.rewrite_rule rews thm1
+ in
+ rtac thm2 i
+ end handle Match => no_tac | TERM _ => no_tac)
+
+fun transfer_tac ctxt = SUBGOAL (fn (t, i) =>
+ let
+ val bs = bnames t
+ val rules = Data.get ctxt
+ in
+ EVERY
+ [rewrite_goal_tac @{thms transfer_forall_eq transfer_implies_eq} i,
+ CONVERSION (Trueprop_conv (fo_conv ctxt)) i,
+ rtac @{thm transfer_start [rotated]} i,
+ REPEAT_ALL_NEW (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) (i + 1),
+ (* Alpha-rename bound variables in goal *)
+ SUBGOAL (fn (u, i) =>
+ rtac @{thm equal_elim_rule1} i THEN
+ rtac (Thm.reflexive (cert ctxt (fst (rename bs u)))) i) i,
+ (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
+ rewrite_goal_tac @{thms App_def Abs_def} i,
+ rewrite_goal_tac @{thms transfer_forall_eq [symmetric] transfer_implies_eq [symmetric]} i,
+ rtac @{thm _} i]
+ end)
+
+fun correspondence_tac ctxt i =
+ let
+ val rules = Data.get ctxt
+ in
+ EVERY
+ [CONVERSION (correspond_conv ctxt) i,
+ REPEAT_ALL_NEW
+ (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) i]
+ end
+
+val transfer_method =
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_tac ctxt))
+
+val correspondence_method =
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (correspondence_tac ctxt))
+
+(* Attribute for correspondence rules *)
+
+val prep_rule = Conv.fconv_rule prep_conv
+
+val transfer_add =
+ Thm.declaration_attribute (Data.add_thm o prep_rule)
+
+val transfer_del =
+ Thm.declaration_attribute (Data.del_thm o prep_rule)
+
+val transfer_attribute =
+ Attrib.add_del transfer_add transfer_del
+
+(* Theory setup *)
+
+val setup =
+ Data.setup
+ #> Attrib.setup @{binding transfer_rule} transfer_attribute
+ "correspondence rule for transfer method"
+ #> Method.setup @{binding transfer} transfer_method
+ "generic theorem transfer method"
+ #> Method.setup @{binding correspondence} correspondence_method
+ "for proving correspondence rules"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Transfer.thy Tue Apr 03 22:31:00 2012 +0200
@@ -0,0 +1,240 @@
+(* Title: HOL/Transfer.thy
+ Author: Brian Huffman, TU Muenchen
+*)
+
+header {* Generic theorem transfer using relations *}
+
+theory Transfer
+imports Plain Hilbert_Choice
+uses ("Tools/transfer.ML")
+begin
+
+subsection {* Relator for function space *}
+
+definition
+ fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" (infixr "===>" 55)
+where
+ "fun_rel A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
+
+lemma fun_relI [intro]:
+ assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
+ shows "(A ===> B) f g"
+ using assms by (simp add: fun_rel_def)
+
+lemma fun_relD:
+ assumes "(A ===> B) f g" and "A x y"
+ shows "B (f x) (g y)"
+ using assms by (simp add: fun_rel_def)
+
+lemma fun_relE:
+ assumes "(A ===> B) f g" and "A x y"
+ obtains "B (f x) (g y)"
+ using assms by (simp add: fun_rel_def)
+
+lemma fun_rel_eq:
+ shows "((op =) ===> (op =)) = (op =)"
+ by (auto simp add: fun_eq_iff elim: fun_relE)
+
+lemma fun_rel_eq_rel:
+ shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"
+ by (simp add: fun_rel_def)
+
+
+subsection {* Transfer method *}
+
+text {* Explicit tags for application, abstraction, and relation
+membership allow for backward proof methods. *}
+
+definition App :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+ where "App f \<equiv> f"
+
+definition Abs :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+ where "Abs f \<equiv> f"
+
+definition Rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
+ where "Rel r \<equiv> r"
+
+text {* Handling of meta-logic connectives *}
+
+definition transfer_forall where
+ "transfer_forall \<equiv> All"
+
+definition transfer_implies where
+ "transfer_implies \<equiv> op \<longrightarrow>"
+
+lemma transfer_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (transfer_forall (\<lambda>x. P x))"
+ unfolding atomize_all transfer_forall_def ..
+
+lemma transfer_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (transfer_implies A B)"
+ unfolding atomize_imp transfer_implies_def ..
+
+lemma transfer_start: "\<lbrakk>Rel (op =) P Q; P\<rbrakk> \<Longrightarrow> Q"
+ unfolding Rel_def by simp
+
+lemma transfer_start': "\<lbrakk>Rel (op \<longrightarrow>) P Q; P\<rbrakk> \<Longrightarrow> Q"
+ unfolding Rel_def by simp
+
+lemma Rel_eq_refl: "Rel (op =) x x"
+ unfolding Rel_def ..
+
+use "Tools/transfer.ML"
+
+setup Transfer.setup
+
+lemma Rel_App [transfer_raw]:
+ assumes "Rel (A ===> B) f g" and "Rel A x y"
+ shows "Rel B (App f x) (App g y)"
+ using assms unfolding Rel_def App_def fun_rel_def by fast
+
+lemma Rel_Abs [transfer_raw]:
+ assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
+ shows "Rel (A ===> B) (Abs (\<lambda>x. f x)) (Abs (\<lambda>y. g y))"
+ using assms unfolding Rel_def Abs_def fun_rel_def by fast
+
+hide_const (open) App Abs Rel
+
+
+subsection {* Predicates on relations, i.e. ``class constraints'' *}
+
+definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+ where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)"
+
+definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+ where "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)"
+
+definition bi_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+ where "bi_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y) \<and> (\<forall>y. \<exists>x. R x y)"
+
+definition bi_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+ where "bi_unique R \<longleftrightarrow>
+ (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
+ (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
+
+lemma right_total_alt_def:
+ "right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
+ unfolding right_total_def fun_rel_def
+ apply (rule iffI, fast)
+ apply (rule allI)
+ apply (drule_tac x="\<lambda>x. True" in spec)
+ apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec)
+ apply fast
+ done
+
+lemma right_unique_alt_def:
+ "right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)"
+ unfolding right_unique_def fun_rel_def by auto
+
+lemma bi_total_alt_def:
+ "bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All"
+ unfolding bi_total_def fun_rel_def
+ apply (rule iffI, fast)
+ apply safe
+ apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec)
+ apply (drule_tac x="\<lambda>y. True" in spec)
+ apply fast
+ apply (drule_tac x="\<lambda>x. True" in spec)
+ apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec)
+ apply fast
+ done
+
+lemma bi_unique_alt_def:
+ "bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
+ unfolding bi_unique_def fun_rel_def by auto
+
+
+subsection {* Properties of relators *}
+
+lemma right_total_eq [transfer_rule]: "right_total (op =)"
+ unfolding right_total_def by simp
+
+lemma right_unique_eq [transfer_rule]: "right_unique (op =)"
+ unfolding right_unique_def by simp
+
+lemma bi_total_eq [transfer_rule]: "bi_total (op =)"
+ unfolding bi_total_def by simp
+
+lemma bi_unique_eq [transfer_rule]: "bi_unique (op =)"
+ unfolding bi_unique_def by simp
+
+lemma right_total_fun [transfer_rule]:
+ "\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)"
+ unfolding right_total_def fun_rel_def
+ apply (rule allI, rename_tac g)
+ apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI)
+ apply clarify
+ apply (subgoal_tac "(THE y. A x y) = y", simp)
+ apply (rule someI_ex)
+ apply (simp)
+ apply (rule the_equality)
+ apply assumption
+ apply (simp add: right_unique_def)
+ done
+
+lemma right_unique_fun [transfer_rule]:
+ "\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)"
+ unfolding right_total_def right_unique_def fun_rel_def
+ by (clarify, rule ext, fast)
+
+lemma bi_total_fun [transfer_rule]:
+ "\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)"
+ unfolding bi_total_def fun_rel_def
+ apply safe
+ apply (rename_tac f)
+ apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
+ apply clarify
+ apply (subgoal_tac "(THE x. A x y) = x", simp)
+ apply (rule someI_ex)
+ apply (simp)
+ apply (rule the_equality)
+ apply assumption
+ apply (simp add: bi_unique_def)
+ apply (rename_tac g)
+ apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI)
+ apply clarify
+ apply (subgoal_tac "(THE y. A x y) = y", simp)
+ apply (rule someI_ex)
+ apply (simp)
+ apply (rule the_equality)
+ apply assumption
+ apply (simp add: bi_unique_def)
+ done
+
+lemma bi_unique_fun [transfer_rule]:
+ "\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)"
+ unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff
+ by (safe, metis, fast)
+
+
+subsection {* Correspondence rules *}
+
+lemma eq_parametric [transfer_rule]:
+ assumes "bi_unique A"
+ shows "(A ===> A ===> op =) (op =) (op =)"
+ using assms unfolding bi_unique_def fun_rel_def by auto
+
+lemma All_parametric [transfer_rule]:
+ assumes "bi_total A"
+ shows "((A ===> op =) ===> op =) All All"
+ using assms unfolding bi_total_def fun_rel_def by fast
+
+lemma Ex_parametric [transfer_rule]:
+ assumes "bi_total A"
+ shows "((A ===> op =) ===> op =) Ex Ex"
+ using assms unfolding bi_total_def fun_rel_def by fast
+
+lemma If_parametric [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
+ unfolding fun_rel_def by simp
+
+lemma comp_parametric [transfer_rule]:
+ "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)"
+ unfolding fun_rel_def by simp
+
+lemma fun_upd_parametric [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
+ unfolding fun_upd_def [abs_def] by correspondence
+
+lemmas transfer_forall_parametric [transfer_rule]
+ = All_parametric [folded transfer_forall_def]
+
+end