--- a/src/HOL/IsaMakefile Tue Apr 03 21:39:28 2012 +0200
+++ b/src/HOL/IsaMakefile Tue Apr 03 23:49:24 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 \
@@ -316,6 +317,7 @@
Tools/code_evaluation.ML \
Tools/groebner.ML \
Tools/int_arith.ML \
+ Tools/legacy_transfer.ML \
Tools/Lifting/lifting_def.ML \
Tools/Lifting/lifting_info.ML \
Tools/Lifting/lifting_term.ML \
--- a/src/HOL/Lifting.thy Tue Apr 03 21:39:28 2012 +0200
+++ b/src/HOL/Lifting.thy Tue Apr 03 23:49:24 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
--- a/src/HOL/Nat_Transfer.thy Tue Apr 03 21:39:28 2012 +0200
+++ b/src/HOL/Nat_Transfer.thy Tue Apr 03 23:49:24 2012 +0200
@@ -5,7 +5,7 @@
theory Nat_Transfer
imports Int
-uses ("Tools/transfer.ML")
+uses ("Tools/legacy_transfer.ML")
begin
subsection {* Generic transfer machinery *}
@@ -16,9 +16,9 @@
lemma transfer_morphismI[intro]: "transfer_morphism f A"
by (simp add: transfer_morphism_def)
-use "Tools/transfer.ML"
+use "Tools/legacy_transfer.ML"
-setup Transfer.setup
+setup Legacy_Transfer.setup
subsection {* Set up transfer from nat to int *}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/legacy_transfer.ML Tue Apr 03 23:49:24 2012 +0200
@@ -0,0 +1,270 @@
+(* Title: HOL/Tools/transfer.ML
+ Author: Amine Chaieb, University of Cambridge, 2009
+ Jeremy Avigad, Carnegie Mellon University
+ Florian Haftmann, TU Muenchen
+
+Simple transfer principle on theorems.
+*)
+
+signature LEGACY_TRANSFER =
+sig
+ datatype selection = Direction of term * term | Hints of string list | Prop
+ val transfer: Context.generic -> selection -> string list -> thm -> thm list
+ type entry
+ val add: thm -> bool -> entry -> Context.generic -> Context.generic
+ val del: thm -> entry -> Context.generic -> Context.generic
+ val drop: thm -> Context.generic -> Context.generic
+ val setup: theory -> theory
+end;
+
+structure Legacy_Transfer : LEGACY_TRANSFER =
+struct
+
+(* data administration *)
+
+val direction_of = Thm.dest_binop o Thm.dest_arg o cprop_of;
+
+val transfer_morphism_key = Drule.strip_imp_concl (Thm.cprop_of @{thm transfer_morphismI});
+
+fun check_morphism_key ctxt key =
+ let
+ val _ = Thm.match (transfer_morphism_key, Thm.cprop_of key)
+ handle Pattern.MATCH => error ("Transfer: expected theorem of the form "
+ ^ quote (Syntax.string_of_term ctxt (Thm.term_of transfer_morphism_key)));
+ in direction_of key end;
+
+type entry = { inj : thm list, embed : thm list, return : thm list, cong : thm list,
+ hints : string list };
+
+val empty_entry = { inj = [], embed = [], return = [], cong = [], hints = [] };
+fun merge_entry ({ inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 } : entry,
+ { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } : entry) =
+ { inj = merge Thm.eq_thm (inj1, inj2), embed = merge Thm.eq_thm (embed1, embed2),
+ return = merge Thm.eq_thm (return1, return2), cong = merge Thm.eq_thm (cong1, cong2),
+ hints = merge (op =) (hints1, hints2) };
+
+structure Data = Generic_Data
+(
+ type T = (thm * entry) list;
+ val empty = [];
+ val extend = I;
+ val merge = AList.join Thm.eq_thm (K merge_entry);
+);
+
+
+(* data lookup *)
+
+fun transfer_rules_of ({ inj, embed, return, cong, ... } : entry) =
+ (inj, embed, return, cong);
+
+fun get_by_direction context (a, D) =
+ let
+ val ctxt = Context.proof_of context;
+ val certify = Thm.cterm_of (Context.theory_of context);
+ val a0 = certify a;
+ val D0 = certify D;
+ fun eq_direction ((a, D), thm') =
+ let
+ val (a', D') = direction_of thm';
+ in a aconvc a' andalso D aconvc D' end;
+ in case AList.lookup eq_direction (Data.get context) (a0, D0) of
+ SOME e => ((a0, D0), transfer_rules_of e)
+ | NONE => error ("Transfer: no such instance: ("
+ ^ Syntax.string_of_term ctxt a ^ ", " ^ Syntax.string_of_term ctxt D ^ ")")
+ end;
+
+fun get_by_hints context hints =
+ let
+ val insts = map_filter (fn (k, e) => if exists (member (op =) (#hints e)) hints
+ then SOME (direction_of k, transfer_rules_of e) else NONE) (Data.get context);
+ val _ = if null insts then error ("Transfer: no such labels: " ^ commas_quote hints) else ();
+ in insts end;
+
+fun splits P [] = []
+ | splits P (xs as (x :: _)) =
+ let
+ val (pss, qss) = List.partition (P x) xs;
+ in if null pss then [qss] else if null qss then [pss] else pss :: splits P qss end;
+
+fun get_by_prop context t =
+ let
+ val tys = map snd (Term.add_vars t []);
+ val _ = if null tys then error "Transfer: unable to guess instance" else ();
+ val tyss = splits (curry Type.could_unify) tys;
+ val get_ty = typ_of o ctyp_of_term o fst o direction_of;
+ val insts = map_filter (fn tys => get_first (fn (k, e) =>
+ if Type.could_unify (hd tys, range_type (get_ty k))
+ then SOME (direction_of k, transfer_rules_of e)
+ else NONE) (Data.get context)) tyss;
+ val _ = if null insts then
+ error "Transfer: no instances, provide direction or hints explicitly" else ();
+ in insts end;
+
+
+(* applying transfer data *)
+
+fun transfer_thm ((raw_a, raw_D), (inj, embed, return, cong)) leave ctxt1 thm =
+ let
+ (* identify morphism function *)
+ val ([a, D], ctxt2) = ctxt1
+ |> Variable.import true (map Drule.mk_term [raw_a, raw_D])
+ |>> map Drule.dest_term o snd;
+ val transform = Thm.apply @{cterm "Trueprop"} o Thm.apply D;
+ val T = Thm.typ_of (Thm.ctyp_of_term a);
+ val (aT, bT) = (Term.range_type T, Term.domain_type T);
+
+ (* determine variables to transfer *)
+ val ctxt3 = ctxt2
+ |> Variable.declare_thm thm
+ |> Variable.declare_term (term_of a)
+ |> Variable.declare_term (term_of D);
+ val certify = Thm.cterm_of (Proof_Context.theory_of ctxt3);
+ val vars = filter (fn ((v, _), T) => Type.could_unify (T, aT) andalso
+ not (member (op =) leave v)) (Term.add_vars (Thm.prop_of thm) []);
+ val c_vars = map (certify o Var) vars;
+ val (vs', ctxt4) = Variable.variant_fixes (map (fst o fst) vars) ctxt3;
+ val c_vars' = map (certify o (fn v => Free (v, bT))) vs';
+ val c_exprs' = map (Thm.apply a) c_vars';
+
+ (* transfer *)
+ val (hyps, ctxt5) = ctxt4
+ |> Assumption.add_assumes (map transform c_vars');
+ val simpset =
+ Simplifier.context ctxt5 HOL_ss addsimps (inj @ embed @ return)
+ |> fold Simplifier.add_cong cong;
+ val thm' = thm
+ |> Drule.cterm_instantiate (c_vars ~~ c_exprs')
+ |> fold_rev Thm.implies_intr (map cprop_of hyps)
+ |> Simplifier.asm_full_simplify simpset
+ in singleton (Variable.export ctxt5 ctxt1) thm' end;
+
+fun transfer_thm_multiple insts leave ctxt thm =
+ map (fn inst => transfer_thm inst leave ctxt thm) insts;
+
+datatype selection = Direction of term * term | Hints of string list | Prop;
+
+fun insts_for context thm (Direction direction) = [get_by_direction context direction]
+ | insts_for context thm (Hints hints) = get_by_hints context hints
+ | insts_for context thm Prop = get_by_prop context (Thm.prop_of thm);
+
+fun transfer context selection leave thm =
+ transfer_thm_multiple (insts_for context thm selection) leave (Context.proof_of context) thm;
+
+
+(* maintaining transfer data *)
+
+fun extend_entry ctxt (a, D) guess
+ { inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 }
+ { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } =
+ let
+ fun add_del eq del add = union eq add #> subtract eq del;
+ val guessed = if guess
+ then map (fn thm => transfer_thm
+ ((a, D), (if null inj1 then inj2 else inj1, [], [], cong1)) [] ctxt thm RS sym) embed1
+ else [];
+ in
+ { inj = union Thm.eq_thm inj1 inj2, embed = union Thm.eq_thm embed1 embed2,
+ return = union Thm.eq_thm guessed (union Thm.eq_thm return1 return2),
+ cong = union Thm.eq_thm cong1 cong2, hints = union (op =) hints1 hints2 }
+ end;
+
+fun diminish_entry
+ { inj = inj0, embed = embed0, return = return0, cong = cong0, hints = hints0 }
+ { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } =
+ { inj = subtract Thm.eq_thm inj0 inj2, embed = subtract Thm.eq_thm embed0 embed2,
+ return = subtract Thm.eq_thm return0 return2, cong = subtract Thm.eq_thm cong0 cong2,
+ hints = subtract (op =) hints0 hints2 };
+
+fun add key guess entry context =
+ let
+ val ctxt = Context.proof_of context;
+ val a_D = check_morphism_key ctxt key;
+ in
+ context
+ |> Data.map (AList.map_default Thm.eq_thm
+ (key, empty_entry) (extend_entry ctxt a_D guess entry))
+ end;
+
+fun del key entry = Data.map (AList.map_entry Thm.eq_thm key (diminish_entry entry));
+
+fun drop key = Data.map (AList.delete Thm.eq_thm key);
+
+
+(* syntax *)
+
+local
+
+fun these scan = Scan.optional scan [];
+fun these_pair scan = Scan.optional scan ([], []);
+
+fun keyword k = Scan.lift (Args.$$$ k) >> K ();
+fun keyword_colon k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
+
+val addN = "add";
+val delN = "del";
+val keyN = "key";
+val modeN = "mode";
+val automaticN = "automatic";
+val manualN = "manual";
+val injN = "inj";
+val embedN = "embed";
+val returnN = "return";
+val congN = "cong";
+val labelsN = "labels";
+
+val leavingN = "leaving";
+val directionN = "direction";
+
+val any_keyword = keyword_colon addN || keyword_colon delN || keyword_colon keyN
+ || keyword_colon modeN || keyword_colon injN || keyword_colon embedN || keyword_colon returnN
+ || keyword_colon congN || keyword_colon labelsN
+ || keyword_colon leavingN || keyword_colon directionN;
+
+val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+val names = Scan.repeat (Scan.unless any_keyword (Scan.lift Args.name))
+
+val mode = keyword_colon modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false)
+ || (Scan.lift (Args.$$$ automaticN) >> K true));
+val inj = (keyword_colon injN |-- thms) -- these (keyword_colon delN |-- thms);
+val embed = (keyword_colon embedN |-- thms) -- these (keyword_colon delN |-- thms);
+val return = (keyword_colon returnN |-- thms) -- these (keyword_colon delN |-- thms);
+val cong = (keyword_colon congN |-- thms) -- these (keyword_colon delN |-- thms);
+val labels = (keyword_colon labelsN |-- names) -- these (keyword_colon delN |-- names);
+
+val entry_pair = these_pair inj -- these_pair embed
+ -- these_pair return -- these_pair cong -- these_pair labels
+ >> (fn (((((inja, injd), (embeda, embedd)), (returna, returnd)), (conga, congd)),
+ (hintsa, hintsd)) =>
+ ({ inj = inja, embed = embeda, return = returna, cong = conga, hints = hintsa },
+ { inj = injd, embed = embedd, return = returnd, cong = congd, hints = hintsd }));
+
+val selection = (keyword_colon directionN |-- (Args.term -- Args.term) >> Direction)
+ || these names >> (fn hints => if null hints then Prop else Hints hints);
+
+in
+
+val transfer_attribute = keyword delN >> K (Thm.declaration_attribute drop)
+ || keyword addN |-- Scan.optional mode true -- entry_pair
+ >> (fn (guess, (entry_add, entry_del)) => Thm.declaration_attribute
+ (fn thm => add thm guess entry_add #> del thm entry_del))
+ || keyword_colon keyN |-- Attrib.thm
+ >> (fn key => Thm.declaration_attribute
+ (fn thm => add key false
+ { inj = [], embed = [], return = [thm], cong = [], hints = [] }));
+
+val transferred_attribute = selection -- these (keyword_colon leavingN |-- names)
+ >> (fn (selection, leave) => Thm.rule_attribute (fn context =>
+ Conjunction.intr_balanced o transfer context selection leave));
+
+end;
+
+
+(* theory setup *)
+
+val setup =
+ Attrib.setup @{binding transfer} transfer_attribute
+ "Installs transfer data" #>
+ Attrib.setup @{binding transferred} transferred_attribute
+ "Transfers theorems";
+
+end;
--- a/src/HOL/Tools/transfer.ML Tue Apr 03 21:39:28 2012 +0200
+++ b/src/HOL/Tools/transfer.ML Tue Apr 03 23:49:24 2012 +0200
@@ -1,270 +1,176 @@
(* Title: HOL/Tools/transfer.ML
- Author: Amine Chaieb, University of Cambridge, 2009
- Jeremy Avigad, Carnegie Mellon University
- Florian Haftmann, TU Muenchen
+ Author: Brian Huffman, TU Muenchen
-Simple transfer principle on theorems.
+Generic theorem transfer method.
*)
signature TRANSFER =
sig
- datatype selection = Direction of term * term | Hints of string list | Prop
- val transfer: Context.generic -> selection -> string list -> thm -> thm list
- type entry
- val add: thm -> bool -> entry -> Context.generic -> Context.generic
- val del: thm -> entry -> Context.generic -> Context.generic
- val drop: thm -> Context.generic -> Context.generic
+ 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;
+end
structure Transfer : TRANSFER =
struct
-(* data administration *)
-
-val direction_of = Thm.dest_binop o Thm.dest_arg o cprop_of;
-
-val transfer_morphism_key = Drule.strip_imp_concl (Thm.cprop_of @{thm transfer_morphismI});
+structure Data = Named_Thms
+(
+ val name = @{binding transfer_raw}
+ val description = "raw correspondence rule for transfer method"
+)
-fun check_morphism_key ctxt key =
- let
- val _ = Thm.match (transfer_morphism_key, Thm.cprop_of key)
- handle Pattern.MATCH => error ("Transfer: expected theorem of the form "
- ^ quote (Syntax.string_of_term ctxt (Thm.term_of transfer_morphism_key)));
- in direction_of key end;
+(** Conversions **)
-type entry = { inj : thm list, embed : thm list, return : thm list, cong : thm list,
- hints : string list };
+val App_rule = Thm.symmetric @{thm App_def}
+val Abs_rule = Thm.symmetric @{thm Abs_def}
+val Rel_rule = Thm.symmetric @{thm Rel_def}
-val empty_entry = { inj = [], embed = [], return = [], cong = [], hints = [] };
-fun merge_entry ({ inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 } : entry,
- { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } : entry) =
- { inj = merge Thm.eq_thm (inj1, inj2), embed = merge Thm.eq_thm (embed1, embed2),
- return = merge Thm.eq_thm (return1, return2), cong = merge Thm.eq_thm (cong1, cong2),
- hints = merge (op =) (hints1, hints2) };
+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
-structure Data = Generic_Data
-(
- type T = (thm * entry) list;
- val empty = [];
- val extend = I;
- val merge = AList.join Thm.eq_thm (K merge_entry);
-);
+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
-
-(* data lookup *)
-
-fun transfer_rules_of ({ inj, embed, return, cong, ... } : entry) =
- (inj, embed, return, cong);
+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 get_by_direction context (a, D) =
- let
- val ctxt = Context.proof_of context;
- val certify = Thm.cterm_of (Context.theory_of context);
- val a0 = certify a;
- val D0 = certify D;
- fun eq_direction ((a, D), thm') =
- let
- val (a', D') = direction_of thm';
- in a aconvc a' andalso D aconvc D' end;
- in case AList.lookup eq_direction (Data.get context) (a0, D0) of
- SOME e => ((a0, D0), transfer_rules_of e)
- | NONE => error ("Transfer: no such instance: ("
- ^ Syntax.string_of_term ctxt a ^ ", " ^ Syntax.string_of_term ctxt D ^ ")")
- 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
-fun get_by_hints context hints =
- let
- val insts = map_filter (fn (k, e) => if exists (member (op =) (#hints e)) hints
- then SOME (direction_of k, transfer_rules_of e) else NONE) (Data.get context);
- val _ = if null insts then error ("Transfer: no such labels: " ^ commas_quote hints) else ();
- in insts end;
-
-fun splits P [] = []
- | splits P (xs as (x :: _)) =
- let
- val (pss, qss) = List.partition (P x) xs;
- in if null pss then [qss] else if null qss then [pss] else pss :: splits P qss end;
+(* 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
-fun get_by_prop context t =
- let
- val tys = map snd (Term.add_vars t []);
- val _ = if null tys then error "Transfer: unable to guess instance" else ();
- val tyss = splits (curry Type.could_unify) tys;
- val get_ty = typ_of o ctyp_of_term o fst o direction_of;
- val insts = map_filter (fn tys => get_first (fn (k, e) =>
- if Type.could_unify (hd tys, range_type (get_ty k))
- then SOME (direction_of k, transfer_rules_of e)
- else NONE) (Data.get context)) tyss;
- val _ = if null insts then
- error "Transfer: no instances, provide direction or hints explicitly" else ();
- in insts end;
+(* 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
-(* applying transfer data *)
+(** Transfer proof method **)
+
+fun bnames (t $ u) = bnames t @ bnames u
+ | bnames (Abs (x,_,t)) = x :: bnames t
+ | bnames _ = []
-fun transfer_thm ((raw_a, raw_D), (inj, embed, return, cong)) leave ctxt1 thm =
- let
- (* identify morphism function *)
- val ([a, D], ctxt2) = ctxt1
- |> Variable.import true (map Drule.mk_term [raw_a, raw_D])
- |>> map Drule.dest_term o snd;
- val transform = Thm.apply @{cterm "Trueprop"} o Thm.apply D;
- val T = Thm.typ_of (Thm.ctyp_of_term a);
- val (aT, bT) = (Term.range_type T, Term.domain_type T);
-
- (* determine variables to transfer *)
- val ctxt3 = ctxt2
- |> Variable.declare_thm thm
- |> Variable.declare_term (term_of a)
- |> Variable.declare_term (term_of D);
- val certify = Thm.cterm_of (Proof_Context.theory_of ctxt3);
- val vars = filter (fn ((v, _), T) => Type.could_unify (T, aT) andalso
- not (member (op =) leave v)) (Term.add_vars (Thm.prop_of thm) []);
- val c_vars = map (certify o Var) vars;
- val (vs', ctxt4) = Variable.variant_fixes (map (fst o fst) vars) ctxt3;
- val c_vars' = map (certify o (fn v => Free (v, bT))) vs';
- val c_exprs' = map (Thm.apply a) c_vars';
+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)
- (* transfer *)
- val (hyps, ctxt5) = ctxt4
- |> Assumption.add_assumes (map transform c_vars');
- val simpset =
- Simplifier.context ctxt5 HOL_ss addsimps (inj @ embed @ return)
- |> fold Simplifier.add_cong cong;
- val thm' = thm
- |> Drule.cterm_instantiate (c_vars ~~ c_exprs')
- |> fold_rev Thm.implies_intr (map cprop_of hyps)
- |> Simplifier.asm_full_simplify simpset
- in singleton (Variable.export ctxt5 ctxt1) thm' end;
+fun cert ctxt t = cterm_of (Proof_Context.theory_of ctxt) t
-fun transfer_thm_multiple insts leave ctxt thm =
- map (fn inst => transfer_thm inst leave ctxt thm) insts;
-
-datatype selection = Direction of term * term | Hints of string list | Prop;
-
-fun insts_for context thm (Direction direction) = [get_by_direction context direction]
- | insts_for context thm (Hints hints) = get_by_hints context hints
- | insts_for context thm Prop = get_by_prop context (Thm.prop_of thm);
+fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y
-fun transfer context selection leave thm =
- transfer_thm_multiple (insts_for context thm selection) leave (Context.proof_of context) thm;
-
-
-(* maintaining transfer data *)
-
-fun extend_entry ctxt (a, D) guess
- { inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 }
- { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } =
+(* Tactic to correspond a value to itself *)
+fun eq_tac ctxt = SUBGOAL (fn (t, i) =>
let
- fun add_del eq del add = union eq add #> subtract eq del;
- val guessed = if guess
- then map (fn thm => transfer_thm
- ((a, D), (if null inj1 then inj2 else inj1, [], [], cong1)) [] ctxt thm RS sym) embed1
- else [];
+ 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
- { inj = union Thm.eq_thm inj1 inj2, embed = union Thm.eq_thm embed1 embed2,
- return = union Thm.eq_thm guessed (union Thm.eq_thm return1 return2),
- cong = union Thm.eq_thm cong1 cong2, hints = union (op =) hints1 hints2 }
- end;
+ rtac thm2 i
+ end handle Match => no_tac | TERM _ => no_tac)
-fun diminish_entry
- { inj = inj0, embed = embed0, return = return0, cong = cong0, hints = hints0 }
- { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } =
- { inj = subtract Thm.eq_thm inj0 inj2, embed = subtract Thm.eq_thm embed0 embed2,
- return = subtract Thm.eq_thm return0 return2, cong = subtract Thm.eq_thm cong0 cong2,
- hints = subtract (op =) hints0 hints2 };
-
-fun add key guess entry context =
+fun transfer_tac ctxt = SUBGOAL (fn (t, i) =>
let
- val ctxt = Context.proof_of context;
- val a_D = check_morphism_key ctxt key;
+ val bs = bnames t
+ val rules = Data.get ctxt
in
- context
- |> Data.map (AList.map_default Thm.eq_thm
- (key, empty_entry) (extend_entry ctxt a_D guess entry))
- end;
-
-fun del key entry = Data.map (AList.map_entry Thm.eq_thm key (diminish_entry entry));
-
-fun drop key = Data.map (AList.delete Thm.eq_thm key);
-
-
-(* syntax *)
-
-local
-
-fun these scan = Scan.optional scan [];
-fun these_pair scan = Scan.optional scan ([], []);
-
-fun keyword k = Scan.lift (Args.$$$ k) >> K ();
-fun keyword_colon k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
-
-val addN = "add";
-val delN = "del";
-val keyN = "key";
-val modeN = "mode";
-val automaticN = "automatic";
-val manualN = "manual";
-val injN = "inj";
-val embedN = "embed";
-val returnN = "return";
-val congN = "cong";
-val labelsN = "labels";
-
-val leavingN = "leaving";
-val directionN = "direction";
-
-val any_keyword = keyword_colon addN || keyword_colon delN || keyword_colon keyN
- || keyword_colon modeN || keyword_colon injN || keyword_colon embedN || keyword_colon returnN
- || keyword_colon congN || keyword_colon labelsN
- || keyword_colon leavingN || keyword_colon directionN;
+ 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)
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
-val names = Scan.repeat (Scan.unless any_keyword (Scan.lift Args.name))
+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 mode = keyword_colon modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false)
- || (Scan.lift (Args.$$$ automaticN) >> K true));
-val inj = (keyword_colon injN |-- thms) -- these (keyword_colon delN |-- thms);
-val embed = (keyword_colon embedN |-- thms) -- these (keyword_colon delN |-- thms);
-val return = (keyword_colon returnN |-- thms) -- these (keyword_colon delN |-- thms);
-val cong = (keyword_colon congN |-- thms) -- these (keyword_colon delN |-- thms);
-val labels = (keyword_colon labelsN |-- names) -- these (keyword_colon delN |-- names);
-
-val entry_pair = these_pair inj -- these_pair embed
- -- these_pair return -- these_pair cong -- these_pair labels
- >> (fn (((((inja, injd), (embeda, embedd)), (returna, returnd)), (conga, congd)),
- (hintsa, hintsd)) =>
- ({ inj = inja, embed = embeda, return = returna, cong = conga, hints = hintsa },
- { inj = injd, embed = embedd, return = returnd, cong = congd, hints = hintsd }));
+val transfer_method =
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_tac ctxt))
-val selection = (keyword_colon directionN |-- (Args.term -- Args.term) >> Direction)
- || these names >> (fn hints => if null hints then Prop else Hints hints);
+val correspondence_method =
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (correspondence_tac ctxt))
-in
+(* Attribute for correspondence rules *)
+
+val prep_rule = Conv.fconv_rule prep_conv
-val transfer_attribute = keyword delN >> K (Thm.declaration_attribute drop)
- || keyword addN |-- Scan.optional mode true -- entry_pair
- >> (fn (guess, (entry_add, entry_del)) => Thm.declaration_attribute
- (fn thm => add thm guess entry_add #> del thm entry_del))
- || keyword_colon keyN |-- Attrib.thm
- >> (fn key => Thm.declaration_attribute
- (fn thm => add key false
- { inj = [], embed = [], return = [thm], cong = [], hints = [] }));
+val transfer_add =
+ Thm.declaration_attribute (Data.add_thm o prep_rule)
-val transferred_attribute = selection -- these (keyword_colon leavingN |-- names)
- >> (fn (selection, leave) => Thm.rule_attribute (fn context =>
- Conjunction.intr_balanced o transfer context selection leave));
+val transfer_del =
+ Thm.declaration_attribute (Data.del_thm o prep_rule)
-end;
+val transfer_attribute =
+ Attrib.add_del transfer_add transfer_del
-
-(* theory setup *)
+(* Theory setup *)
val setup =
- Attrib.setup @{binding transfer} transfer_attribute
- "Installs transfer data" #>
- Attrib.setup @{binding transferred} transferred_attribute
- "Transfers theorems";
+ 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;
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Transfer.thy Tue Apr 03 23:49:24 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