--- a/src/HOL/Library/FSet.thy Thu Apr 10 17:48:17 2014 +0200
+++ b/src/HOL/Library/FSet.thy Thu Apr 10 17:48:18 2014 +0200
@@ -846,10 +846,10 @@
thm right_unique_rel_fset left_unique_rel_fset
lemma bi_unique_rel_fset[transfer_rule]: "bi_unique A \<Longrightarrow> bi_unique (rel_fset A)"
-by (auto intro: right_unique_rel_fset left_unique_rel_fset iff: bi_unique_iff)
+by (auto intro: right_unique_rel_fset left_unique_rel_fset iff: bi_unique_alt_def)
lemma bi_total_rel_fset[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_fset A)"
-by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_iff)
+by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_alt_def)
lemmas fset_relator_eq_onp [relator_eq_onp] = set_relator_eq_onp[Transfer.transferred]
--- a/src/HOL/Lifting.thy Thu Apr 10 17:48:17 2014 +0200
+++ b/src/HOL/Lifting.thy Thu Apr 10 17:48:18 2014 +0200
@@ -161,6 +161,11 @@
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"
unfolding Quotient_alt_def3 fun_eq_iff by auto
+lemma Quotient_alt_def5:
+ "Quotient R Abs Rep T \<longleftrightarrow>
+ T \<le> BNF_Util.Grp UNIV Abs \<and> BNF_Util.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"
+ unfolding Quotient_alt_def4 Grp_def by blast
+
lemma fun_quotient:
assumes 1: "Quotient R1 abs1 rep1 T1"
assumes 2: "Quotient R2 abs2 rep2 T2"
@@ -210,32 +215,6 @@
lemma in_respects: "x \<in> Respects R \<longleftrightarrow> R x x"
unfolding Respects_def by simp
-subsection {* Invariant *}
-
-definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
- where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
-
-lemma eq_onp_to_eq:
- assumes "eq_onp P x y"
- shows "x = y"
-using assms by (simp add: eq_onp_def)
-
-lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
-unfolding eq_onp_def rel_fun_def by auto
-
-lemma rel_fun_eq_onp_rel:
- shows "((eq_onp R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
-by (auto simp add: eq_onp_def rel_fun_def)
-
-lemma eq_onp_same_args:
- shows "eq_onp P x x \<equiv> P x"
-using assms by (auto simp add: eq_onp_def)
-
-lemma eq_onp_transfer [transfer_rule]:
- assumes [transfer_rule]: "bi_unique A"
- shows "((A ===> op=) ===> A ===> A ===> op=) eq_onp eq_onp"
-unfolding eq_onp_def[abs_def] by transfer_prover
-
lemma UNIV_typedef_to_Quotient:
assumes "type_definition Rep Abs UNIV"
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
@@ -574,6 +553,8 @@
declare fun_mono[relator_mono]
lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2
+ML_file "Tools/Lifting/lifting_bnf.ML"
+
ML_file "Tools/Lifting/lifting_term.ML"
ML_file "Tools/Lifting/lifting_def.ML"
--- a/src/HOL/Lifting_Set.thy Thu Apr 10 17:48:17 2014 +0200
+++ b/src/HOL/Lifting_Set.thy Thu Apr 10 17:48:18 2014 +0200
@@ -75,7 +75,7 @@
lemma bi_total_rel_set [transfer_rule]:
"bi_total A \<Longrightarrow> bi_total (rel_set A)"
-by(simp add: bi_total_conv_left_right left_total_rel_set right_total_rel_set)
+by(simp add: bi_total_alt_def left_total_rel_set right_total_rel_set)
lemma bi_unique_rel_set [transfer_rule]:
"bi_unique A \<Longrightarrow> bi_unique (rel_set A)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Thu Apr 10 17:48:18 2014 +0200
@@ -0,0 +1,118 @@
+(* Title: HOL/Tools/Transfer/transfer_bnf.ML
+ Author: Ondrej Kuncar, TU Muenchen
+
+Setup for Lifting for types that are BNF.
+*)
+
+signature LIFTING_BNF =
+sig
+end
+
+structure Lifting_BNF : LIFTING_BNF =
+struct
+
+open BNF_Util
+open BNF_Def
+open Transfer_BNF
+
+(* Quotient map theorem *)
+
+fun Quotient_tac bnf ctxt i =
+ let
+ val rel_Grp = rel_Grp_of_bnf bnf
+ fun get_lhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst
+ val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd))
+ val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars
+ val inst = map2 (curry(pairself (certify ctxt))) vars UNIVs
+ val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst)
+ |> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)}
+ |> (fn thm => thm RS sym)
+ val rel_mono = rel_mono_of_bnf bnf
+ val rel_conversep_sym = rel_conversep_of_bnf bnf RS sym
+ in
+ EVERY' [SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Quotient_alt_def5}]),
+ REPEAT_DETERM o (etac conjE), rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_Grp_UNIV_sym]),
+ rtac rel_mono THEN_ALL_NEW atac, rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt
+ [rel_conversep_sym, rel_Grp_UNIV_sym]), rtac rel_mono THEN_ALL_NEW atac,
+ SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_conversep_sym, rel_OO_of_bnf bnf RS sym]),
+ hyp_subst_tac ctxt, rtac refl] i
+ end
+
+fun mk_Quotient args =
+ let
+ val argTs = map fastype_of args
+ in
+ list_comb (Const (@{const_name Quotient}, argTs ---> HOLogic.boolT), args)
+ end
+
+fun prove_Quotient_map bnf ctxt =
+ let
+ val live = live_of_bnf bnf
+ val old_ctxt = ctxt
+ val (((As, Bs), Ds), ctxt) = ctxt
+ |> mk_TFrees live
+ ||>> mk_TFrees live
+ ||>> mk_TFrees (dead_of_bnf bnf)
+ val argTss = map2 (fn a => fn b => [mk_pred2T a a, a --> b, b --> a,mk_pred2T a b]) As Bs
+ val ((argss, argss'), ctxt) = fold_map2 mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss) ctxt
+ |>> `transpose
+
+ val assms = map (mk_Quotient #> HOLogic.mk_Trueprop) argss
+ val R_rel = list_comb (mk_rel_of_bnf Ds As As bnf, nth argss' 0)
+ val Abs_map = list_comb (mk_map_of_bnf Ds As Bs bnf, nth argss' 1)
+ val Rep_map = list_comb (mk_map_of_bnf Ds Bs As bnf, nth argss' 2)
+ val T_rel = list_comb (mk_rel_of_bnf Ds As Bs bnf, nth argss' 3)
+ val concl = mk_Quotient [R_rel, Abs_map, Rep_map, T_rel] |> HOLogic.mk_Trueprop
+ val goal = Logic.list_implies (assms, concl)
+ val thm = Goal.prove ctxt [] [] goal
+ (fn {context = ctxt, prems = _} => Quotient_tac bnf ctxt 1)
+ in
+ Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
+ end
+
+
+fun Quotient_map bnf ctxt =
+ let
+ val Quotient = prove_Quotient_map bnf ctxt
+ fun qualify defname suffix = Binding.qualified true suffix defname
+ val Quotient_thm_name = qualify (base_name_of_bnf bnf) "Quotient"
+ val notes = [((Quotient_thm_name, []), [([Quotient], @{attributes [quot_map]})])]
+ in
+ notes
+ end
+
+(* relator_eq_onp *)
+
+fun relator_eq_onp bnf ctxt =
+ let
+ val pred_data = lookup_defined_pred_data ctxt (type_name_of_bnf bnf)
+ in
+ [((Binding.empty, []), [([Transfer.rel_eq_onp pred_data], @{attributes [relator_eq_onp]})])]
+ end
+
+(* relator_mono *)
+
+fun relator_mono bnf =
+ [((Binding.empty, []), [([rel_mono_of_bnf bnf], @{attributes [relator_mono]})])]
+
+(* relator_distr *)
+
+fun relator_distr bnf =
+ [((Binding.empty, []), [([rel_OO_of_bnf bnf RS sym], @{attributes [relator_distr]})])]
+
+(* interpretation *)
+
+fun lifting_bnf_interpretation bnf lthy =
+ if dead_of_bnf bnf > 0 then lthy
+ else
+ let
+ val notes = relator_eq_onp bnf lthy @ Quotient_map bnf lthy @ relator_mono bnf
+ @ relator_distr bnf
+ in
+ snd (Local_Theory.notes notes lthy)
+ end
+
+val _ = Context.>> (Context.map_theory (bnf_interpretation
+ (bnf_only_type_ctr (fn bnf => map_local_theory (lifting_bnf_interpretation bnf)))))
+
+end
--- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Apr 10 17:48:17 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu Apr 10 17:48:18 2014 +0200
@@ -534,7 +534,7 @@
end
val unfold_ret_val_invs = Conv.bottom_conv
- (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args}))) lthy
+ (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
val cr_to_pcr_conv = Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)
val unfold_inv_conv =
Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) lthy
--- a/src/HOL/Tools/Quotient/quotient_def.ML Thu Apr 10 17:48:17 2014 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Thu Apr 10 17:48:18 2014 +0200
@@ -121,7 +121,7 @@
end
val unfold_ret_val_invs = Conv.bottom_conv
- (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args}))) lthy
+ (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Transfer/transfer.ML Thu Apr 10 17:48:18 2014 +0200
@@ -0,0 +1,868 @@
+(* Title: HOL/Tools/Transfer/transfer.ML
+ Author: Brian Huffman, TU Muenchen
+ Author: Ondrej Kuncar, TU Muenchen
+
+Generic theorem transfer method.
+*)
+
+signature TRANSFER =
+sig
+ type pred_data
+ val rel_eq_onp: pred_data -> thm
+
+ val bottom_rewr_conv: thm list -> conv
+ val top_rewr_conv: thm list -> conv
+
+ val prep_conv: conv
+ val get_transfer_raw: Proof.context -> thm list
+ val get_relator_eq_item_net: Proof.context -> thm Item_Net.T
+ val get_relator_eq: Proof.context -> thm list
+ val get_sym_relator_eq: Proof.context -> thm list
+ val get_relator_eq_raw: Proof.context -> thm list
+ val get_relator_domain: Proof.context -> thm list
+ val morph_pred_data: morphism -> pred_data -> pred_data
+ val lookup_pred_data: Proof.context -> string -> pred_data option
+ val update_pred_data: string -> pred_data -> Context.generic -> Context.generic
+ val get_compound_lhs: Proof.context -> (term * thm) Item_Net.T
+ val get_compound_rhs: Proof.context -> (term * thm) Item_Net.T
+ val transfer_add: attribute
+ val transfer_del: attribute
+ val transfer_raw_add: thm -> Context.generic -> Context.generic
+ val transfer_raw_del: thm -> Context.generic -> Context.generic
+ val transferred_attribute: thm list -> attribute
+ val untransferred_attribute: thm list -> attribute
+ val prep_transfer_domain_thm: Proof.context -> thm -> thm
+ val transfer_domain_add: attribute
+ val transfer_domain_del: attribute
+ val transfer_rule_of_term: Proof.context -> bool -> term -> thm
+ val transfer_rule_of_lhs: Proof.context -> term -> thm
+ val eq_tac: Proof.context -> int -> tactic
+ val transfer_step_tac: Proof.context -> int -> tactic
+ val transfer_tac: bool -> Proof.context -> int -> tactic
+ val transfer_prover_tac: Proof.context -> int -> tactic
+ val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic
+ val setup: theory -> theory
+end
+
+structure Transfer : TRANSFER =
+struct
+
+(** Theory Data **)
+
+val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o pairself snd) (single o fst);
+val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq
+ o HOLogic.dest_Trueprop o Thm.concl_of);
+
+type pred_data = {rel_eq_onp: thm}
+
+val rel_eq_onp = #rel_eq_onp
+
+structure Data = Generic_Data
+(
+ type T =
+ { transfer_raw : thm Item_Net.T,
+ known_frees : (string * typ) list,
+ compound_lhs : (term * thm) Item_Net.T,
+ compound_rhs : (term * thm) Item_Net.T,
+ relator_eq : thm Item_Net.T,
+ relator_eq_raw : thm Item_Net.T,
+ relator_domain : thm Item_Net.T,
+ pred_data : pred_data Symtab.table }
+ val empty =
+ { transfer_raw = Thm.intro_rules,
+ known_frees = [],
+ compound_lhs = compound_xhs_empty_net,
+ compound_rhs = compound_xhs_empty_net,
+ relator_eq = rewr_rules,
+ relator_eq_raw = Thm.full_rules,
+ relator_domain = Thm.full_rules,
+ pred_data = Symtab.empty }
+ val extend = I
+ fun merge
+ ( { transfer_raw = t1, known_frees = k1,
+ compound_lhs = l1,
+ compound_rhs = c1, relator_eq = r1,
+ relator_eq_raw = rw1, relator_domain = rd1,
+ pred_data = pd1 },
+ { transfer_raw = t2, known_frees = k2,
+ compound_lhs = l2,
+ compound_rhs = c2, relator_eq = r2,
+ relator_eq_raw = rw2, relator_domain = rd2,
+ pred_data = pd2 } ) =
+ { transfer_raw = Item_Net.merge (t1, t2),
+ known_frees = Library.merge (op =) (k1, k2),
+ compound_lhs = Item_Net.merge (l1, l2),
+ compound_rhs = Item_Net.merge (c1, c2),
+ relator_eq = Item_Net.merge (r1, r2),
+ relator_eq_raw = Item_Net.merge (rw1, rw2),
+ relator_domain = Item_Net.merge (rd1, rd2),
+ pred_data = Symtab.merge (K true) (pd1, pd2) }
+)
+
+fun get_transfer_raw ctxt = ctxt
+ |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
+
+fun get_known_frees ctxt = ctxt
+ |> (#known_frees o Data.get o Context.Proof)
+
+fun get_compound_lhs ctxt = ctxt
+ |> (#compound_lhs o Data.get o Context.Proof)
+
+fun get_compound_rhs ctxt = ctxt
+ |> (#compound_rhs o Data.get o Context.Proof)
+
+fun get_relator_eq_item_net ctxt = (#relator_eq o Data.get o Context.Proof) ctxt
+
+fun get_relator_eq ctxt = ctxt
+ |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
+ |> map safe_mk_meta_eq
+
+fun get_sym_relator_eq ctxt = ctxt
+ |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
+ |> map (Thm.symmetric o safe_mk_meta_eq)
+
+fun get_relator_eq_raw ctxt = ctxt
+ |> (Item_Net.content o #relator_eq_raw o Data.get o Context.Proof)
+
+fun get_relator_domain ctxt = ctxt
+ |> (Item_Net.content o #relator_domain o Data.get o Context.Proof)
+
+fun get_pred_data ctxt = ctxt
+ |> (#pred_data o Data.get o Context.Proof)
+
+fun map_data f1 f2 f3 f4 f5 f6 f7 f8
+ { transfer_raw, known_frees, compound_lhs, compound_rhs,
+ relator_eq, relator_eq_raw, relator_domain, pred_data } =
+ { transfer_raw = f1 transfer_raw,
+ known_frees = f2 known_frees,
+ compound_lhs = f3 compound_lhs,
+ compound_rhs = f4 compound_rhs,
+ relator_eq = f5 relator_eq,
+ relator_eq_raw = f6 relator_eq_raw,
+ relator_domain = f7 relator_domain,
+ pred_data = f8 pred_data }
+
+fun map_transfer_raw f = map_data f I I I I I I I
+fun map_known_frees f = map_data I f I I I I I I
+fun map_compound_lhs f = map_data I I f I I I I I
+fun map_compound_rhs f = map_data I I I f I I I I
+fun map_relator_eq f = map_data I I I I f I I I
+fun map_relator_eq_raw f = map_data I I I I I f I I
+fun map_relator_domain f = map_data I I I I I I f I
+fun map_pred_data f = map_data I I I I I I I f
+
+fun add_transfer_thm thm = Data.map
+ (map_transfer_raw (Item_Net.update thm) o
+ map_compound_lhs
+ (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
+ Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>
+ Item_Net.update (lhs, thm)
+ | _ => I) o
+ map_compound_rhs
+ (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
+ Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>
+ Item_Net.update (rhs, thm)
+ | _ => I) o
+ map_known_frees (Term.add_frees (Thm.concl_of thm)))
+
+fun del_transfer_thm thm = Data.map
+ (map_transfer_raw (Item_Net.remove thm) o
+ map_compound_lhs
+ (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
+ Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>
+ Item_Net.remove (lhs, thm)
+ | _ => I) o
+ map_compound_rhs
+ (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
+ Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>
+ Item_Net.remove (rhs, thm)
+ | _ => I))
+
+fun transfer_raw_add thm ctxt = add_transfer_thm thm ctxt
+fun transfer_raw_del thm ctxt = del_transfer_thm thm ctxt
+
+(** Conversions **)
+
+fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
+fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
+
+fun transfer_rel_conv conv =
+ Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv)))
+
+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 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
+
+(* Conversion to preprocess a transfer rule *)
+fun safe_Rel_conv ct =
+ Conv.try_conv (HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))) ct
+
+fun prep_conv ct = (
+ Conv.implies_conv safe_Rel_conv prep_conv
+ else_conv
+ safe_Rel_conv
+ else_conv
+ Conv.all_conv) ct
+
+(** Replacing explicit equalities with is_equality premises **)
+
+fun mk_is_equality t =
+ Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t
+
+val is_equality_lemma =
+ @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))"
+ by (unfold is_equality_def, rule, drule meta_spec,
+ erule meta_mp, rule refl, simp)}
+
+fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
+ let
+ val thy = Thm.theory_of_thm thm
+ val prop = Thm.prop_of thm
+ val (t, mk_prop') = dest prop
+ (* Only consider "op =" at non-base types *)
+ fun is_eq (Const (@{const_name HOL.eq}, Type ("fun", [T, _]))) =
+ (case T of Type (_, []) => false | _ => true)
+ | is_eq _ = false
+ val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)
+ val eq_consts = rev (add_eqs t [])
+ val eqTs = map (snd o dest_Const) eq_consts
+ val used = Term.add_free_names prop []
+ val names = map (K "") eqTs |> Name.variant_list used
+ val frees = map Free (names ~~ eqTs)
+ val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
+ val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
+ val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
+ val cprop = Thm.cterm_of thy prop2
+ val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
+ fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
+ in
+ forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
+ end
+ handle TERM _ => thm
+
+fun abstract_equalities_transfer ctxt thm =
+ let
+ fun dest prop =
+ let
+ val prems = Logic.strip_imp_prems prop
+ val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
+ val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
+ in
+ (rel, fn rel' =>
+ Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))
+ end
+ val contracted_eq_thm =
+ Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
+ handle CTERM _ => thm
+ in
+ gen_abstract_equalities ctxt dest contracted_eq_thm
+ end
+
+fun abstract_equalities_relator_eq ctxt rel_eq_thm =
+ gen_abstract_equalities ctxt (fn x => (x, I))
+ (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
+
+fun abstract_equalities_domain ctxt thm =
+ let
+ fun dest prop =
+ let
+ val prems = Logic.strip_imp_prems prop
+ val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
+ val ((eq, dom), y) = apfst Term.dest_comb (Term.dest_comb concl)
+ in
+ (dom, fn dom' => Logic.list_implies (prems, HOLogic.mk_Trueprop (eq $ dom' $ y)))
+ end
+ fun transfer_rel_conv conv =
+ Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.arg1_conv (Conv.arg_conv conv)))
+ val contracted_eq_thm =
+ Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
+ in
+ gen_abstract_equalities ctxt dest contracted_eq_thm
+ end
+
+
+(** Replacing explicit Domainp predicates with Domainp assumptions **)
+
+fun mk_Domainp_assm (T, R) =
+ HOLogic.mk_eq ((Const (@{const_name Domainp}, Term.fastype_of T --> Term.fastype_of R) $ T), R)
+
+val Domainp_lemma =
+ @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))"
+ by (rule, drule meta_spec,
+ erule meta_mp, rule refl, simp)}
+
+fun fold_Domainp f (t as Const (@{const_name Domainp},_) $ (Var (_,_))) = f t
+ | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u
+ | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t
+ | fold_Domainp _ _ = I
+
+fun subst_terms tab t =
+ let
+ val t' = Termtab.lookup tab t
+ in
+ case t' of
+ SOME t' => t'
+ | NONE =>
+ (case t of
+ u $ v => (subst_terms tab u) $ (subst_terms tab v)
+ | Abs (a, T, t) => Abs (a, T, subst_terms tab t)
+ | t => t)
+ end
+
+fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
+ let
+ val thy = Thm.theory_of_thm thm
+ val prop = Thm.prop_of thm
+ val (t, mk_prop') = dest prop
+ val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])
+ val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_tms
+ val used = Term.add_free_names t []
+ val rels = map (snd o dest_comb) Domainp_tms
+ val rel_names = map (fst o fst o dest_Var) rels
+ val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used
+ val frees = map Free (names ~~ Domainp_Ts)
+ val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees);
+ val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t
+ val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
+ val prop2 = Logic.list_rename_params (rev names) prop1
+ val cprop = Thm.cterm_of thy prop2
+ val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
+ fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
+ in
+ forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
+ end
+ handle TERM _ => thm
+
+fun abstract_domains_transfer ctxt thm =
+ let
+ fun dest prop =
+ let
+ val prems = Logic.strip_imp_prems prop
+ val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
+ val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
+ in
+ (x, fn x' =>
+ Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
+ end
+ in
+ gen_abstract_domains ctxt dest thm
+ end
+
+fun abstract_domains_relator_domain ctxt thm =
+ let
+ fun dest prop =
+ let
+ val prems = Logic.strip_imp_prems prop
+ val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
+ val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
+ in
+ (y, fn y' =>
+ Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x $ y')))
+ end
+ in
+ gen_abstract_domains ctxt dest thm
+ end
+
+fun detect_transfer_rules thm =
+ let
+ fun is_transfer_rule tm = case (HOLogic.dest_Trueprop tm) of
+ (Const (@{const_name HOL.eq}, _)) $ ((Const (@{const_name Domainp}, _)) $ _) $ _ => false
+ | _ $ _ $ _ => true
+ | _ => false
+ fun safe_transfer_rule_conv ctm =
+ if is_transfer_rule (term_of ctm) then safe_Rel_conv ctm else Conv.all_conv ctm
+ in
+ Conv.fconv_rule (Conv.prems_conv ~1 safe_transfer_rule_conv) thm
+ end
+
+(** Adding transfer domain rules **)
+
+fun prep_transfer_domain_thm ctxt thm =
+ (abstract_equalities_domain ctxt o detect_transfer_rules) thm
+
+fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o
+ prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
+
+fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o
+ prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
+
+(** Transfer proof method **)
+
+val post_simps =
+ @{thms transfer_forall_eq [symmetric]
+ transfer_implies_eq [symmetric] transfer_bforall_unfold}
+
+fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) =>
+ let
+ val keepers = keepers @ get_known_frees ctxt
+ val vs = rev (Term.add_frees t [])
+ val vs' = filter_out (member (op =) keepers) vs
+ in
+ Induct.arbitrary_tac ctxt 0 vs' i
+ end)
+
+fun mk_relT (T, U) = T --> U --> HOLogic.boolT
+
+fun mk_Rel t =
+ let val T = fastype_of t
+ in Const (@{const_name Transfer.Rel}, T --> T) $ t end
+
+fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ (* precondition: prj(T,U) must consist of only TFrees and type "fun" *)
+ fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
+ let
+ val r1 = rel T1 U1
+ val r2 = rel T2 U2
+ val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
+ in
+ Const (@{const_name rel_fun}, rT) $ r1 $ r2
+ end
+ | rel T U =
+ let
+ val (a, _) = dest_TFree (prj (T, U))
+ in
+ Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
+ end
+ fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
+ | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =
+ let
+ val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
+ val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
+ val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
+ val thm0 = Thm.assume cprop
+ val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
+ val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
+ val r2 = Thm.dest_fun2 (Thm.dest_arg (cprop_of thm1))
+ val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r1))
+ val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r2))
+ val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
+ val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
+ val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
+ val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
+ in
+ (thm2 COMP rule, hyps)
+ end
+ | zip ctxt thms (f $ t) (g $ u) =
+ let
+ val (thm1, hyps1) = zip ctxt thms f g
+ val (thm2, hyps2) = zip ctxt thms t u
+ in
+ (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
+ end
+ | zip _ _ t u =
+ let
+ val T = fastype_of t
+ val U = fastype_of u
+ val prop = mk_Rel (rel T U) $ t $ u
+ val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
+ in
+ (Thm.assume cprop, [cprop])
+ end
+ val r = mk_Rel (rel (fastype_of t) (fastype_of u))
+ val goal = HOLogic.mk_Trueprop (r $ t $ u)
+ val rename = Thm.trivial (cterm_of thy goal)
+ val (thm, hyps) = zip ctxt [] t u
+ in
+ Drule.implies_intr_list hyps (thm RS rename)
+ end
+
+(* create a lambda term of the same shape as the given term *)
+fun skeleton (is_atom : term -> bool) ctxt t =
+ let
+ fun dummy ctxt =
+ let
+ val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt
+ in
+ (Free (c, dummyT), ctxt)
+ end
+ fun go (Bound i) ctxt = (Bound i, ctxt)
+ | go (Abs (x, _, t)) ctxt =
+ let
+ val (t', ctxt) = go t ctxt
+ in
+ (Abs (x, dummyT, t'), ctxt)
+ end
+ | go (tu as (t $ u)) ctxt =
+ if is_atom tu andalso not (Term.is_open tu) then dummy ctxt else
+ let
+ val (t', ctxt) = go t ctxt
+ val (u', ctxt) = go u ctxt
+ in
+ (t' $ u', ctxt)
+ end
+ | go _ ctxt = dummy ctxt
+ in
+ go t ctxt |> fst |> Syntax.check_term ctxt |>
+ map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type})))
+ end
+
+(** Monotonicity analysis **)
+
+(* TODO: Put extensible table in theory data *)
+val monotab =
+ Symtab.make
+ [(@{const_name transfer_implies}, [~1, 1]),
+ (@{const_name transfer_forall}, [1])(*,
+ (@{const_name implies}, [~1, 1]),
+ (@{const_name All}, [1])*)]
+
+(*
+Function bool_insts determines the set of boolean-relation variables
+that can be instantiated to implies, rev_implies, or iff.
+
+Invariants: bool_insts p (t, u) requires that
+ u :: _ => _ => ... => bool, and
+ t is a skeleton of u
+*)
+fun bool_insts p (t, u) =
+ let
+ fun strip2 (t1 $ t2, u1 $ u2, tus) =
+ strip2 (t1, u1, (t2, u2) :: tus)
+ | strip2 x = x
+ fun or3 ((a, b, c), (x, y, z)) = (a orelse x, b orelse y, c orelse z)
+ fun go Ts p (Abs (_, T, t), Abs (_, _, u)) tab = go (T :: Ts) p (t, u) tab
+ | go Ts p (t, u) tab =
+ let
+ val (a, _) = dest_TFree (Term.body_type (Term.fastype_of1 (Ts, t)))
+ val (_, tf, tus) = strip2 (t, u, [])
+ val ps_opt = case tf of Const (c, _) => Symtab.lookup monotab c | _ => NONE
+ val tab1 =
+ case ps_opt of
+ SOME ps =>
+ let
+ val ps' = map (fn x => p * x) (take (length tus) ps)
+ in
+ fold I (map2 (go Ts) ps' tus) tab
+ end
+ | NONE => tab
+ val tab2 = Symtab.make [(a, (p >= 0, p <= 0, is_none ps_opt))]
+ in
+ Symtab.join (K or3) (tab1, tab2)
+ end
+ val tab = go [] p (t, u) Symtab.empty
+ fun f (a, (true, false, false)) = SOME (a, @{const implies})
+ | f (a, (false, true, false)) = SOME (a, @{const rev_implies})
+ | f (a, (true, true, _)) = SOME (a, HOLogic.eq_const HOLogic.boolT)
+ | f _ = NONE
+ in
+ map_filter f (Symtab.dest tab)
+ end
+
+fun retrieve_terms t net = map fst (Item_Net.retrieve net t)
+
+fun matches_list ctxt term =
+ is_some o find_first (fn pat => Pattern.matches (Proof_Context.theory_of ctxt) (pat, term))
+
+fun transfer_rule_of_term ctxt equiv t : thm =
+ let
+ val compound_rhs = get_compound_rhs ctxt
+ fun is_rhs t = compound_rhs |> retrieve_terms t |> matches_list ctxt t
+ val s = skeleton is_rhs ctxt t
+ val frees = map fst (Term.add_frees s [])
+ val tfrees = map fst (Term.add_tfrees s [])
+ fun prep a = "R" ^ Library.unprefix "'" a
+ val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
+ val tab = tfrees ~~ rnames
+ fun prep a = the (AList.lookup (op =) tab a)
+ val thm = transfer_rule_of_terms fst ctxt' tab s t
+ val binsts = bool_insts (if equiv then 0 else 1) (s, t)
+ val cbool = @{ctyp bool}
+ val relT = @{typ "bool => bool => bool"}
+ val idx = Thm.maxidx_of thm + 1
+ val thy = Proof_Context.theory_of ctxt
+ fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
+ fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
+ in
+ thm
+ |> Thm.generalize (tfrees, rnames @ frees) idx
+ |> Thm.instantiate (map tinst binsts, map inst binsts)
+ end
+
+fun transfer_rule_of_lhs ctxt t : thm =
+ let
+ val compound_lhs = get_compound_lhs ctxt
+ fun is_lhs t = compound_lhs |> retrieve_terms t |> matches_list ctxt t
+ val s = skeleton is_lhs ctxt t
+ val frees = map fst (Term.add_frees s [])
+ val tfrees = map fst (Term.add_tfrees s [])
+ fun prep a = "R" ^ Library.unprefix "'" a
+ val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
+ val tab = tfrees ~~ rnames
+ fun prep a = the (AList.lookup (op =) tab a)
+ val thm = transfer_rule_of_terms snd ctxt' tab t s
+ val binsts = bool_insts 1 (s, t)
+ val cbool = @{ctyp bool}
+ val relT = @{typ "bool => bool => bool"}
+ val idx = Thm.maxidx_of thm + 1
+ val thy = Proof_Context.theory_of ctxt
+ fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
+ fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
+ in
+ thm
+ |> Thm.generalize (tfrees, rnames @ frees) idx
+ |> Thm.instantiate (map tinst binsts, map inst binsts)
+ end
+
+fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules)
+ THEN_ALL_NEW rtac @{thm is_equality_eq}
+
+fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt)
+
+fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac (get_transfer_raw ctxt))
+ THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt)))
+
+fun transfer_tac equiv ctxt i =
+ let
+ val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
+ val start_rule =
+ if equiv then @{thm transfer_start} else @{thm transfer_start'}
+ val rules = get_transfer_raw ctxt
+ val eq_rules = get_relator_eq_raw ctxt
+ (* allow unsolved subgoals only for standard transfer method, not for transfer' *)
+ val end_tac = if equiv then K all_tac else K no_tac
+ val err_msg = "Transfer failed to convert goal to an object-logic formula"
+ fun main_tac (t, i) =
+ rtac start_rule i THEN
+ (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))
+ THEN_ALL_NEW
+ (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))
+ ORELSE' end_tac)) (i + 1)
+ handle TERM (_, ts) => raise TERM (err_msg, ts)
+ in
+ EVERY
+ [rewrite_goal_tac ctxt pre_simps i THEN
+ SUBGOAL main_tac i,
+ (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
+ rewrite_goal_tac ctxt post_simps i,
+ Goal.norm_hhf_tac ctxt i]
+ end
+
+fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
+ let
+ val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
+ val rule1 = transfer_rule_of_term ctxt false rhs
+ val rules = get_transfer_raw ctxt
+ val eq_rules = get_relator_eq_raw ctxt
+ val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm rel_fun_eq[symmetric,THEN eq_reflection]}])
+ in
+ EVERY
+ [CONVERSION prep_conv i,
+ rtac @{thm transfer_prover_start} i,
+ ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
+ THEN_ALL_NEW
+ (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))) (i+1),
+ rtac @{thm refl} i]
+ end)
+
+(** Transfer attribute **)
+
+fun transferred ctxt extra_rules thm =
+ let
+ val start_rule = @{thm transfer_start}
+ val start_rule' = @{thm transfer_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 ctxt 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_lhs ctxt' t
+ val tac =
+ resolve_tac [thm2 RS start_rule', thm2 RS start_rule] 1 THEN
+ (rtac rule
+ THEN_ALL_NEW
+ (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
+ THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
+ handle TERM (_, ts) => raise TERM (err_msg, ts)
+ val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
+ val tnames = map (fst o dest_TFree o snd) instT
+ in
+ thm3
+ |> Raw_Simplifier.rewrite_rule ctxt' post_simps
+ |> Simplifier.norm_hhf ctxt'
+ |> Drule.generalize (tnames, [])
+ |> Drule.zero_var_indexes
+ end
+(*
+ 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 ctxt 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_rules_tac eq_rules)))) 1
+ handle TERM (_, ts) => raise TERM (err_msg, ts)
+ val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
+ val tnames = map (fst o dest_TFree o snd) instT
+ in
+ thm3
+ |> Raw_Simplifier.rewrite_rule ctxt' post_simps
+ |> Simplifier.norm_hhf ctxt'
+ |> Drule.generalize (tnames, [])
+ |> Drule.zero_var_indexes
+ end
+
+(** Methods and attributes **)
+
+val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
+ error ("Bad free variable: " ^ Syntax.string_of_term ctxt t))
+
+val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon)
+ |-- Scan.repeat free) []
+
+fun transfer_method equiv : (Proof.context -> Proof.method) context_parser =
+ fixing >> (fn vs => fn ctxt =>
+ SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt))
+
+val transfer_prover_method : (Proof.context -> Proof.method) context_parser =
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
+
+(* Attribute for transfer rules *)
+
+fun prep_rule ctxt =
+ abstract_domains_transfer ctxt o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv
+
+val transfer_add =
+ Thm.declaration_attribute (fn thm => fn ctxt =>
+ (add_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
+
+val transfer_del =
+ Thm.declaration_attribute (fn thm => fn ctxt =>
+ (del_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
+
+val transfer_attribute =
+ Attrib.add_del transfer_add transfer_del
+
+(* Attributes for transfer domain rules *)
+
+val transfer_domain_add = Thm.declaration_attribute add_transfer_domain_thm
+
+val transfer_domain_del = Thm.declaration_attribute del_transfer_domain_thm
+
+val transfer_domain_attribute =
+ Attrib.add_del transfer_domain_add transfer_domain_del
+
+(* Attributes for transferred rules *)
+
+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
+
+fun morph_pred_data phi {rel_eq_onp} = {rel_eq_onp = Morphism.thm phi rel_eq_onp}
+
+fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name
+ |> Option.map (morph_pred_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
+
+fun update_pred_data type_name qinfo ctxt =
+ Data.map (map_pred_data (Symtab.update (type_name, qinfo))) ctxt
+
+(* Theory setup *)
+
+val relator_eq_setup =
+ let
+ val name = @{binding relator_eq}
+ fun add_thm thm context = context
+ |> Data.map (map_relator_eq (Item_Net.update thm))
+ |> Data.map (map_relator_eq_raw
+ (Item_Net.update (abstract_equalities_relator_eq (Context.proof_of context) thm)))
+ fun del_thm thm context = context
+ |> Data.map (map_relator_eq (Item_Net.remove thm))
+ |> Data.map (map_relator_eq_raw
+ (Item_Net.remove (abstract_equalities_relator_eq (Context.proof_of context) thm)))
+ val add = Thm.declaration_attribute add_thm
+ val del = Thm.declaration_attribute del_thm
+ val text = "declaration of relator equality rule (used by transfer method)"
+ val content = Item_Net.content o #relator_eq o Data.get
+ in
+ Attrib.setup name (Attrib.add_del add del) text
+ #> Global_Theory.add_thms_dynamic (name, content)
+ end
+
+val relator_domain_setup =
+ let
+ val name = @{binding relator_domain}
+ fun add_thm thm context =
+ let
+ val thm = abstract_domains_relator_domain (Context.proof_of context) thm
+ in
+ context |> Data.map (map_relator_domain (Item_Net.update thm)) |> add_transfer_domain_thm thm
+ end
+ fun del_thm thm context =
+ let
+ val thm = abstract_domains_relator_domain (Context.proof_of context) thm
+ in
+ context |> Data.map (map_relator_domain (Item_Net.remove thm)) |> del_transfer_domain_thm thm
+ end
+ val add = Thm.declaration_attribute add_thm
+ val del = Thm.declaration_attribute del_thm
+ val text = "declaration of relator domain rule (used by transfer method)"
+ val content = Item_Net.content o #relator_domain o Data.get
+ in
+ Attrib.setup name (Attrib.add_del add del) text
+ #> Global_Theory.add_thms_dynamic (name, content)
+ end
+
+val setup =
+ relator_eq_setup
+ #> relator_domain_setup
+ #> Attrib.setup @{binding transfer_rule} transfer_attribute
+ "transfer rule for transfer method"
+ #> Global_Theory.add_thms_dynamic
+ (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
+ #> Attrib.setup @{binding transfer_domain_rule} transfer_domain_attribute
+ "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)
+ "generic theorem transfer method"
+ #> Method.setup @{binding transfer'} (transfer_method false)
+ "generic theorem transfer method"
+ #> Method.setup @{binding transfer_prover} transfer_prover_method
+ "for proving transfer rules"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Thu Apr 10 17:48:18 2014 +0200
@@ -0,0 +1,353 @@
+(* Title: HOL/Tools/Transfer/transfer_bnf.ML
+ Author: Ondrej Kuncar, TU Muenchen
+
+Setup for Transfer for types that are BNF.
+*)
+
+signature TRANSFER_BNF =
+sig
+ val base_name_of_bnf: BNF_Def.bnf -> binding
+ val type_name_of_bnf: BNF_Def.bnf -> string
+ val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data
+ val map_local_theory: (local_theory -> local_theory) -> theory -> theory
+ val bnf_only_type_ctr: (BNF_Def.bnf -> 'a -> 'a) -> BNF_Def.bnf -> 'a -> 'a
+end
+
+structure Transfer_BNF : TRANSFER_BNF =
+struct
+
+open BNF_Util
+open BNF_Def
+open BNF_FP_Def_Sugar
+
+(* util functions *)
+
+fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf))
+fun mk_Frees_free x Ts ctxt = Variable.variant_frees ctxt [] (mk_names (length Ts) x ~~ Ts) |> map Free
+
+fun mk_Domainp P =
+ let
+ val PT = fastype_of P
+ val argT = hd (binder_types PT)
+ in
+ Const (@{const_name Domainp}, PT --> argT --> HOLogic.boolT) $ P
+ end
+
+fun mk_pred pred_def args T =
+ let
+ val pred_name = pred_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
+ |> head_of |> fst o dest_Const
+ val argsT = map fastype_of args
+ in
+ list_comb (Const (pred_name, argsT ---> (T --> HOLogic.boolT)), args)
+ end
+
+fun mk_eq_onp arg =
+ let
+ val argT = domain_type (fastype_of arg)
+ in
+ Const (@{const_name eq_onp}, (argT --> HOLogic.boolT) --> argT --> argT --> HOLogic.boolT)
+ $ arg
+ end
+
+fun subst_conv thm =
+ Conv.top_sweep_conv (K (Conv.rewr_conv (safe_mk_meta_eq thm))) @{context}
+
+fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst
+
+fun is_Type (Type _) = true
+ | is_Type _ = false
+
+fun map_local_theory f = Named_Target.theory_init #> f #> Local_Theory.exit_global
+
+fun bnf_only_type_ctr f bnf = if is_Type (T_of_bnf bnf) then f bnf else I
+
+fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar)
+
+fun fp_sugar_only_type_ctr f fp_sugar =
+ if is_Type (T_of_bnf (bnf_of_fp_sugar fp_sugar)) then f fp_sugar else I
+
+(* relation constraints - bi_total & co. *)
+
+fun mk_relation_constraint name arg =
+ (Const (name, fastype_of arg --> HOLogic.boolT)) $ arg
+
+fun side_constraint_tac bnf constr_defs ctxt i =
+ let
+ val thms = constr_defs @ map mk_sym [rel_eq_of_bnf bnf, rel_conversep_of_bnf bnf,
+ rel_OO_of_bnf bnf]
+ in
+ (SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac (rel_mono_of_bnf bnf)
+ THEN_ALL_NEW atac) i
+ end
+
+fun bi_constraint_tac constr_iff sided_constr_intros ctxt i =
+ (SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN'
+ CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW (REPEAT_DETERM o etac conjE THEN' atac)) sided_constr_intros) i
+
+fun generate_relation_constraint_goal ctxt bnf constraint_def =
+ let
+ val constr_name = constraint_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
+ |> head_of |> fst o dest_Const
+ val live = live_of_bnf bnf
+ val (((As, Bs), Ds), ctxt) = ctxt
+ |> mk_TFrees live
+ ||>> mk_TFrees live
+ ||>> mk_TFrees (dead_of_bnf bnf)
+
+ val relator = mk_rel_of_bnf Ds As Bs bnf
+ val relsT = map2 mk_pred2T As Bs
+ val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt
+ val concl = HOLogic.mk_Trueprop (mk_relation_constraint constr_name (list_comb (relator, args)))
+ val assms = map (HOLogic.mk_Trueprop o (mk_relation_constraint constr_name)) args
+ val goal = Logic.list_implies (assms, concl)
+ in
+ (goal, ctxt)
+ end
+
+fun prove_relation_side_constraint ctxt bnf constraint_def =
+ let
+ val old_ctxt = ctxt
+ val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
+ val thm = Goal.prove ctxt [] [] goal
+ (fn {context = ctxt, prems = _} => side_constraint_tac bnf [constraint_def] ctxt 1)
+ in
+ Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
+ end
+
+fun prove_relation_bi_constraint ctxt bnf constraint_def side_constraints =
+ let
+ val old_ctxt = ctxt
+ val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
+ val thm = Goal.prove ctxt [] [] goal
+ (fn {context = ctxt, prems = _} => bi_constraint_tac constraint_def side_constraints ctxt 1)
+ in
+ Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
+ end
+
+val defs = [("left_total_rel", @{thm left_total_alt_def}), ("right_total_rel", @{thm right_total_alt_def}),
+ ("left_unique_rel", @{thm left_unique_alt_def}), ("right_unique_rel", @{thm right_unique_alt_def})]
+
+fun prove_relation_constraints bnf lthy =
+ let
+ val transfer_attr = @{attributes [transfer_rule]}
+ val Tname = base_name_of_bnf bnf
+ fun qualify suffix = Binding.qualified true suffix Tname
+
+ val defs = map (apsnd (prove_relation_side_constraint lthy bnf)) defs
+ val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def}
+ [snd (nth defs 0), snd (nth defs 1)]
+ val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def}
+ [snd (nth defs 2), snd (nth defs 3)]
+ val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs
+ val notes = maps (fn (name, thm) => [((qualify name, []), [([thm], transfer_attr)])]) defs
+ in
+ notes
+ end
+
+(* relator_eq *)
+
+fun relator_eq bnf =
+ [((Binding.empty, []), [([rel_eq_of_bnf bnf], @{attributes [relator_eq]})])]
+
+(* predicator definition and Domainp and eq_onp theorem *)
+
+fun define_pred bnf lthy =
+ let
+ fun mk_pred_name c = Binding.prefix_name "pred_" c
+ val live = live_of_bnf bnf
+ val Tname = base_name_of_bnf bnf
+ val ((As, Ds), lthy) = lthy
+ |> mk_TFrees live
+ ||>> mk_TFrees (dead_of_bnf bnf)
+ val T = mk_T_of_bnf Ds As bnf
+ val sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf
+ val argTs = map mk_pred1T As
+ val args = mk_Frees_free "P" argTs lthy
+ val conjs = map (fn (set, arg) => mk_Ball (set $ Bound 0) arg) (sets ~~ args)
+ val rhs = Abs ("x", T, foldr1 HOLogic.mk_conj conjs)
+ val pred_name = mk_pred_name Tname
+ val headT = argTs ---> (T --> HOLogic.boolT)
+ val head = Free (Binding.name_of pred_name, headT)
+ val lhs = list_comb (head, args)
+ val def = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ val ((_, (_, pred_def)), lthy) = Specification.definition ((SOME (pred_name, SOME headT, NoSyn)),
+ ((Binding.empty, []), def)) lthy
+ in
+ (pred_def, lthy)
+ end
+
+fun Domainp_tac bnf pred_def ctxt i =
+ let
+ val n = live_of_bnf bnf
+ val set_map's = set_map_of_bnf bnf
+ in
+ EVERY' [rtac ext, SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Domainp.simps},
+ in_rel_of_bnf bnf, pred_def]), rtac iffI,
+ REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], hyp_subst_tac ctxt,
+ CONJ_WRAP' (fn set_map => EVERY' [rtac ballI, dtac (set_map RS equalityD1 RS set_mp),
+ etac imageE, dtac set_rev_mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}],
+ hyp_subst_tac ctxt, rtac @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]},
+ etac @{thm DomainPI}]) set_map's,
+ REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI],
+ rtac refl, rtac (box_equals OF [map_cong0_of_bnf bnf, map_comp_of_bnf bnf RS sym,
+ map_id_of_bnf bnf]),
+ REPEAT_DETERM_N n o (EVERY' [rtac @{thm box_equals[OF _ sym[OF o_apply] sym[OF id_apply]]},
+ rtac @{thm fst_conv}]), rtac CollectI,
+ CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}),
+ REPEAT_DETERM o resolve_tac [@{thm image_subsetI}, CollectI, @{thm case_prodI}],
+ dtac (rotate_prems 1 bspec), atac, etac @{thm DomainpE}, etac @{thm someI}]) set_map's
+ ] i
+ end
+
+fun prove_Domainp_rel ctxt bnf pred_def =
+ let
+ val live = live_of_bnf bnf
+ val old_ctxt = ctxt
+ val (((As, Bs), Ds), ctxt) = ctxt
+ |> mk_TFrees live
+ ||>> mk_TFrees live
+ ||>> mk_TFrees (dead_of_bnf bnf)
+
+ val relator = mk_rel_of_bnf Ds As Bs bnf
+ val relsT = map2 mk_pred2T As Bs
+ val T = mk_T_of_bnf Ds As bnf
+ val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt
+ val lhs = mk_Domainp (list_comb (relator, args))
+ val rhs = mk_pred pred_def (map mk_Domainp args) T
+ val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
+ val thm = Goal.prove ctxt [] [] goal
+ (fn {context = ctxt, prems = _} => Domainp_tac bnf pred_def ctxt 1)
+ in
+ Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
+ end
+
+fun pred_eq_onp_tac bnf pred_def ctxt i =
+ (SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm eq_onp_Grp},
+ @{thm Ball_Collect}, pred_def]) THEN' CONVERSION (subst_conv (map_id0_of_bnf bnf RS sym))
+ THEN' rtac (rel_Grp_of_bnf bnf)) i
+
+fun prove_rel_eq_onp ctxt bnf pred_def =
+ let
+ val live = live_of_bnf bnf
+ val old_ctxt = ctxt
+ val ((As, Ds), ctxt) = ctxt
+ |> mk_TFrees live
+ ||>> mk_TFrees (dead_of_bnf bnf)
+ val T = mk_T_of_bnf Ds As bnf
+ val argTs = map mk_pred1T As
+ val (args, ctxt) = mk_Frees "P" argTs ctxt
+ val relator = mk_rel_of_bnf Ds As As bnf
+ val lhs = list_comb (relator, map mk_eq_onp args)
+ val rhs = mk_eq_onp (mk_pred pred_def args T)
+ val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
+ val thm = Goal.prove ctxt [] [] goal
+ (fn {context = ctxt, prems = _} => pred_eq_onp_tac bnf pred_def ctxt 1)
+ in
+ Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
+ end
+
+fun predicator bnf lthy =
+ let
+ val (pred_def, lthy) = define_pred bnf lthy
+ val pred_def = Morphism.thm (Local_Theory.target_morphism lthy) pred_def
+ val Domainp_rel = prove_Domainp_rel lthy bnf pred_def
+ val rel_eq_onp = prove_rel_eq_onp lthy bnf pred_def
+ fun qualify defname suffix = Binding.qualified true suffix defname
+ val Domainp_rel_thm_name = qualify (base_name_of_bnf bnf) "Domainp_rel"
+ val rel_eq_onp_thm_name = qualify (base_name_of_bnf bnf) "rel_eq_onp"
+ val pred_data = {rel_eq_onp = rel_eq_onp}
+ val type_name = type_name_of_bnf bnf
+ val relator_domain_attr = @{attributes [relator_domain]}
+ val notes = [((Domainp_rel_thm_name, []), [([Domainp_rel], relator_domain_attr)]),
+ ((rel_eq_onp_thm_name, []), [([rel_eq_onp], [])])]
+ val lthy = Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data)) lthy
+ in
+ (notes, lthy)
+ end
+
+(* BNF interpretation *)
+
+fun transfer_bnf_interpretation bnf lthy =
+ let
+ val constr_notes = if dead_of_bnf bnf > 0 then []
+ else prove_relation_constraints bnf lthy
+ val relator_eq_notes = if dead_of_bnf bnf > 0 then []
+ else relator_eq bnf
+ val (pred_notes, lthy) = predicator bnf lthy
+ in
+ snd (Local_Theory.notes (constr_notes @ relator_eq_notes @ pred_notes) lthy)
+ end
+
+val _ = Context.>> (Context.map_theory (bnf_interpretation
+ (bnf_only_type_ctr (fn bnf => map_local_theory (transfer_bnf_interpretation bnf)))))
+
+(* simplification rules for the predicator *)
+
+fun lookup_defined_pred_data lthy name =
+ case (Transfer.lookup_pred_data lthy name) of
+ SOME data => data
+ | NONE => (error "lookup_pred_data: something went utterly wrong")
+
+fun prove_pred_inject lthy (fp_sugar:fp_sugar) =
+ let
+ val involved_types = distinct op= (
+ map type_name_of_bnf (#nested_bnfs fp_sugar)
+ @ map type_name_of_bnf (#nesting_bnfs fp_sugar)
+ @ map type_name_of_bnf (#bnfs (#fp_res fp_sugar)))
+ val eq_onps = map (Transfer.rel_eq_onp o lookup_defined_pred_data lthy) involved_types
+ val live = live_of_bnf (bnf_of_fp_sugar fp_sugar)
+ val old_lthy = lthy
+ val (As, lthy) = mk_TFrees live lthy
+ val predTs = map mk_pred1T As
+ val (preds, lthy) = mk_Frees "P" predTs lthy
+ val args = map mk_eq_onp preds
+ val cTs = map (SOME o certifyT lthy) (maps (replicate 2) As)
+ val cts = map (SOME o certify lthy) args
+ fun get_rhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
+ fun is_eqn thm = can get_rhs thm
+ fun rel2pred_massage thm =
+ let
+ fun pred_eq_onp_conj 0 = error "not defined"
+ | pred_eq_onp_conj 1 = @{thm eq_onp_same_args}
+ | pred_eq_onp_conj n =
+ let
+ val conj_cong = @{thm arg_cong2[of _ _ _ _ "op \<and>"]}
+ val start = @{thm eq_onp_same_args} RS conj_cong
+ in
+ @{thm eq_onp_same_args} RS (funpow (n - 2) (fn thm => start RS thm) start)
+ end
+ val n = if is_eqn thm then thm |> get_rhs |> HOLogic.dest_conj |> length else 0
+ in
+ thm
+ |> Drule.instantiate' cTs cts
+ |> Local_Defs.unfold lthy eq_onps
+ |> (fn thm => if n > 0 then @{thm box_equals}
+ OF [thm, @{thm eq_onp_same_args}, pred_eq_onp_conj n]
+ else thm RS (@{thm eq_onp_same_args} RS iffD1))
+ end
+ val rel_injects = #rel_injects fp_sugar
+ in
+ rel_injects
+ |> map rel2pred_massage
+ |> Variable.export lthy old_lthy
+ |> map Drule.zero_var_indexes
+ end
+
+(* fp_sugar interpretation *)
+
+fun transfer_fp_sugar_interpretation fp_sugar lthy =
+ let
+ val pred_injects = prove_pred_inject lthy fp_sugar
+ fun qualify defname suffix = Binding.qualified true suffix defname
+ val pred_inject_thm_name = qualify (base_name_of_bnf (bnf_of_fp_sugar fp_sugar)) "pred_inject"
+ val simp_attrs = @{attributes [simp]}
+ in
+ snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
+ end
+
+val _ = Context.>> (Context.map_theory (fp_sugar_interpretation
+ (fp_sugar_only_type_ctr (fn fp_sugar => map_local_theory (transfer_fp_sugar_interpretation fp_sugar)))))
+
+end
--- a/src/HOL/Tools/transfer.ML Thu Apr 10 17:48:17 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,840 +0,0 @@
-(* Title: HOL/Tools/transfer.ML
- Author: Brian Huffman, TU Muenchen
- Author: Ondrej Kuncar, TU Muenchen
-
-Generic theorem transfer method.
-*)
-
-signature TRANSFER =
-sig
- val bottom_rewr_conv: thm list -> conv
- val top_rewr_conv: thm list -> conv
-
- val prep_conv: conv
- val get_transfer_raw: Proof.context -> thm list
- val get_relator_eq_item_net: Proof.context -> thm Item_Net.T
- val get_relator_eq: Proof.context -> thm list
- val get_sym_relator_eq: Proof.context -> thm list
- val get_relator_eq_raw: Proof.context -> thm list
- val get_relator_domain: Proof.context -> thm list
- val get_compound_lhs: Proof.context -> (term * thm) Item_Net.T
- val get_compound_rhs: Proof.context -> (term * thm) Item_Net.T
- val transfer_add: attribute
- val transfer_del: attribute
- val transfer_raw_add: thm -> Context.generic -> Context.generic
- val transfer_raw_del: thm -> Context.generic -> Context.generic
- val transferred_attribute: thm list -> attribute
- val untransferred_attribute: thm list -> attribute
- val prep_transfer_domain_thm: Proof.context -> thm -> thm
- val transfer_domain_add: attribute
- val transfer_domain_del: attribute
- val transfer_rule_of_term: Proof.context -> bool -> term -> thm
- val transfer_rule_of_lhs: Proof.context -> term -> thm
- val eq_tac: Proof.context -> int -> tactic
- val transfer_step_tac: Proof.context -> int -> tactic
- val transfer_tac: bool -> Proof.context -> int -> tactic
- val transfer_prover_tac: Proof.context -> int -> tactic
- val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic
- val setup: theory -> theory
-end
-
-structure Transfer : TRANSFER =
-struct
-
-(** Theory Data **)
-
-val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o pairself snd) (single o fst);
-val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq
- o HOLogic.dest_Trueprop o Thm.concl_of);
-
-structure Data = Generic_Data
-(
- type T =
- { transfer_raw : thm Item_Net.T,
- known_frees : (string * typ) list,
- compound_lhs : (term * thm) Item_Net.T,
- compound_rhs : (term * thm) Item_Net.T,
- relator_eq : thm Item_Net.T,
- relator_eq_raw : thm Item_Net.T,
- relator_domain : thm Item_Net.T }
- val empty =
- { transfer_raw = Thm.intro_rules,
- known_frees = [],
- compound_lhs = compound_xhs_empty_net,
- compound_rhs = compound_xhs_empty_net,
- relator_eq = rewr_rules,
- relator_eq_raw = Thm.full_rules,
- relator_domain = Thm.full_rules }
- val extend = I
- fun merge
- ( { transfer_raw = t1, known_frees = k1,
- compound_lhs = l1,
- compound_rhs = c1, relator_eq = r1,
- relator_eq_raw = rw1, relator_domain = rd1 },
- { transfer_raw = t2, known_frees = k2,
- compound_lhs = l2,
- compound_rhs = c2, relator_eq = r2,
- relator_eq_raw = rw2, relator_domain = rd2 } ) =
- { transfer_raw = Item_Net.merge (t1, t2),
- known_frees = Library.merge (op =) (k1, k2),
- compound_lhs = Item_Net.merge (l1, l2),
- compound_rhs = Item_Net.merge (c1, c2),
- relator_eq = Item_Net.merge (r1, r2),
- relator_eq_raw = Item_Net.merge (rw1, rw2),
- relator_domain = Item_Net.merge (rd1, rd2) }
-)
-
-fun get_transfer_raw ctxt = ctxt
- |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
-
-fun get_known_frees ctxt = ctxt
- |> (#known_frees o Data.get o Context.Proof)
-
-fun get_compound_lhs ctxt = ctxt
- |> (#compound_lhs o Data.get o Context.Proof)
-
-fun get_compound_rhs ctxt = ctxt
- |> (#compound_rhs o Data.get o Context.Proof)
-
-fun get_relator_eq_item_net ctxt = (#relator_eq o Data.get o Context.Proof) ctxt
-
-fun get_relator_eq ctxt = ctxt
- |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
- |> map safe_mk_meta_eq
-
-fun get_sym_relator_eq ctxt = ctxt
- |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
- |> map (Thm.symmetric o safe_mk_meta_eq)
-
-fun get_relator_eq_raw ctxt = ctxt
- |> (Item_Net.content o #relator_eq_raw o Data.get o Context.Proof)
-
-fun get_relator_domain ctxt = ctxt
- |> (Item_Net.content o #relator_domain o Data.get o Context.Proof)
-
-fun map_data f1 f2 f3 f4 f5 f6 f7
- { transfer_raw, known_frees, compound_lhs, compound_rhs,
- relator_eq, relator_eq_raw, relator_domain } =
- { transfer_raw = f1 transfer_raw,
- known_frees = f2 known_frees,
- compound_lhs = f3 compound_lhs,
- compound_rhs = f4 compound_rhs,
- relator_eq = f5 relator_eq,
- relator_eq_raw = f6 relator_eq_raw,
- relator_domain = f7 relator_domain }
-
-fun map_transfer_raw f = map_data f I I I I I I
-fun map_known_frees f = map_data I f I I I I I
-fun map_compound_lhs f = map_data I I f I I I I
-fun map_compound_rhs f = map_data I I I f I I I
-fun map_relator_eq f = map_data I I I I f I I
-fun map_relator_eq_raw f = map_data I I I I I f I
-fun map_relator_domain f = map_data I I I I I I f
-
-fun add_transfer_thm thm = Data.map
- (map_transfer_raw (Item_Net.update thm) o
- map_compound_lhs
- (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
- Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>
- Item_Net.update (lhs, thm)
- | _ => I) o
- map_compound_rhs
- (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
- Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>
- Item_Net.update (rhs, thm)
- | _ => I) o
- map_known_frees (Term.add_frees (Thm.concl_of thm)))
-
-fun del_transfer_thm thm = Data.map
- (map_transfer_raw (Item_Net.remove thm) o
- map_compound_lhs
- (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
- Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>
- Item_Net.remove (lhs, thm)
- | _ => I) o
- map_compound_rhs
- (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
- Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>
- Item_Net.remove (rhs, thm)
- | _ => I))
-
-fun transfer_raw_add thm ctxt = add_transfer_thm thm ctxt
-fun transfer_raw_del thm ctxt = del_transfer_thm thm ctxt
-
-(** Conversions **)
-
-fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
-fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
-
-fun transfer_rel_conv conv =
- Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv)))
-
-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 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
-
-(* Conversion to preprocess a transfer rule *)
-fun safe_Rel_conv ct =
- Conv.try_conv (HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))) ct
-
-fun prep_conv ct = (
- Conv.implies_conv safe_Rel_conv prep_conv
- else_conv
- safe_Rel_conv
- else_conv
- Conv.all_conv) ct
-
-(** Replacing explicit equalities with is_equality premises **)
-
-fun mk_is_equality t =
- Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t
-
-val is_equality_lemma =
- @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))"
- by (unfold is_equality_def, rule, drule meta_spec,
- erule meta_mp, rule refl, simp)}
-
-fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
- let
- val thy = Thm.theory_of_thm thm
- val prop = Thm.prop_of thm
- val (t, mk_prop') = dest prop
- (* Only consider "op =" at non-base types *)
- fun is_eq (Const (@{const_name HOL.eq}, Type ("fun", [T, _]))) =
- (case T of Type (_, []) => false | _ => true)
- | is_eq _ = false
- val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)
- val eq_consts = rev (add_eqs t [])
- val eqTs = map (snd o dest_Const) eq_consts
- val used = Term.add_free_names prop []
- val names = map (K "") eqTs |> Name.variant_list used
- val frees = map Free (names ~~ eqTs)
- val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
- val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
- val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
- val cprop = Thm.cterm_of thy prop2
- val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
- fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
- in
- forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
- end
- handle TERM _ => thm
-
-fun abstract_equalities_transfer ctxt thm =
- let
- fun dest prop =
- let
- val prems = Logic.strip_imp_prems prop
- val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
- val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
- in
- (rel, fn rel' =>
- Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))
- end
- val contracted_eq_thm =
- Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
- handle CTERM _ => thm
- in
- gen_abstract_equalities ctxt dest contracted_eq_thm
- end
-
-fun abstract_equalities_relator_eq ctxt rel_eq_thm =
- gen_abstract_equalities ctxt (fn x => (x, I))
- (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
-
-fun abstract_equalities_domain ctxt thm =
- let
- fun dest prop =
- let
- val prems = Logic.strip_imp_prems prop
- val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
- val ((eq, dom), y) = apfst Term.dest_comb (Term.dest_comb concl)
- in
- (dom, fn dom' => Logic.list_implies (prems, HOLogic.mk_Trueprop (eq $ dom' $ y)))
- end
- fun transfer_rel_conv conv =
- Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.arg1_conv (Conv.arg_conv conv)))
- val contracted_eq_thm =
- Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
- in
- gen_abstract_equalities ctxt dest contracted_eq_thm
- end
-
-
-(** Replacing explicit Domainp predicates with Domainp assumptions **)
-
-fun mk_Domainp_assm (T, R) =
- HOLogic.mk_eq ((Const (@{const_name Domainp}, Term.fastype_of T --> Term.fastype_of R) $ T), R)
-
-val Domainp_lemma =
- @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))"
- by (rule, drule meta_spec,
- erule meta_mp, rule refl, simp)}
-
-fun fold_Domainp f (t as Const (@{const_name Domainp},_) $ (Var (_,_))) = f t
- | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u
- | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t
- | fold_Domainp _ _ = I
-
-fun subst_terms tab t =
- let
- val t' = Termtab.lookup tab t
- in
- case t' of
- SOME t' => t'
- | NONE =>
- (case t of
- u $ v => (subst_terms tab u) $ (subst_terms tab v)
- | Abs (a, T, t) => Abs (a, T, subst_terms tab t)
- | t => t)
- end
-
-fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
- let
- val thy = Thm.theory_of_thm thm
- val prop = Thm.prop_of thm
- val (t, mk_prop') = dest prop
- val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])
- val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_tms
- val used = Term.add_free_names t []
- val rels = map (snd o dest_comb) Domainp_tms
- val rel_names = map (fst o fst o dest_Var) rels
- val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used
- val frees = map Free (names ~~ Domainp_Ts)
- val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees);
- val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t
- val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
- val prop2 = Logic.list_rename_params (rev names) prop1
- val cprop = Thm.cterm_of thy prop2
- val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
- fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
- in
- forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
- end
- handle TERM _ => thm
-
-fun abstract_domains_transfer ctxt thm =
- let
- fun dest prop =
- let
- val prems = Logic.strip_imp_prems prop
- val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
- val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
- in
- (x, fn x' =>
- Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
- end
- in
- gen_abstract_domains ctxt dest thm
- end
-
-fun abstract_domains_relator_domain ctxt thm =
- let
- fun dest prop =
- let
- val prems = Logic.strip_imp_prems prop
- val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
- val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
- in
- (y, fn y' =>
- Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x $ y')))
- end
- in
- gen_abstract_domains ctxt dest thm
- end
-
-fun detect_transfer_rules thm =
- let
- fun is_transfer_rule tm = case (HOLogic.dest_Trueprop tm) of
- (Const (@{const_name HOL.eq}, _)) $ ((Const (@{const_name Domainp}, _)) $ _) $ _ => false
- | _ $ _ $ _ => true
- | _ => false
- fun safe_transfer_rule_conv ctm =
- if is_transfer_rule (term_of ctm) then safe_Rel_conv ctm else Conv.all_conv ctm
- in
- Conv.fconv_rule (Conv.prems_conv ~1 safe_transfer_rule_conv) thm
- end
-
-(** Adding transfer domain rules **)
-
-fun prep_transfer_domain_thm ctxt thm =
- (abstract_equalities_domain ctxt o detect_transfer_rules) thm
-
-fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o
- prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
-
-fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o
- prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
-
-(** Transfer proof method **)
-
-val post_simps =
- @{thms transfer_forall_eq [symmetric]
- transfer_implies_eq [symmetric] transfer_bforall_unfold}
-
-fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) =>
- let
- val keepers = keepers @ get_known_frees ctxt
- val vs = rev (Term.add_frees t [])
- val vs' = filter_out (member (op =) keepers) vs
- in
- Induct.arbitrary_tac ctxt 0 vs' i
- end)
-
-fun mk_relT (T, U) = T --> U --> HOLogic.boolT
-
-fun mk_Rel t =
- let val T = fastype_of t
- in Const (@{const_name Transfer.Rel}, T --> T) $ t end
-
-fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u =
- let
- val thy = Proof_Context.theory_of ctxt
- (* precondition: prj(T,U) must consist of only TFrees and type "fun" *)
- fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
- let
- val r1 = rel T1 U1
- val r2 = rel T2 U2
- val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
- in
- Const (@{const_name rel_fun}, rT) $ r1 $ r2
- end
- | rel T U =
- let
- val (a, _) = dest_TFree (prj (T, U))
- in
- Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
- end
- fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
- | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =
- let
- val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
- val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
- val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
- val thm0 = Thm.assume cprop
- val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
- val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
- val r2 = Thm.dest_fun2 (Thm.dest_arg (cprop_of thm1))
- val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r1))
- val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r2))
- val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
- val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
- val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
- val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
- in
- (thm2 COMP rule, hyps)
- end
- | zip ctxt thms (f $ t) (g $ u) =
- let
- val (thm1, hyps1) = zip ctxt thms f g
- val (thm2, hyps2) = zip ctxt thms t u
- in
- (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
- end
- | zip _ _ t u =
- let
- val T = fastype_of t
- val U = fastype_of u
- val prop = mk_Rel (rel T U) $ t $ u
- val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
- in
- (Thm.assume cprop, [cprop])
- end
- val r = mk_Rel (rel (fastype_of t) (fastype_of u))
- val goal = HOLogic.mk_Trueprop (r $ t $ u)
- val rename = Thm.trivial (cterm_of thy goal)
- val (thm, hyps) = zip ctxt [] t u
- in
- Drule.implies_intr_list hyps (thm RS rename)
- end
-
-(* create a lambda term of the same shape as the given term *)
-fun skeleton (is_atom : term -> bool) ctxt t =
- let
- fun dummy ctxt =
- let
- val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt
- in
- (Free (c, dummyT), ctxt)
- end
- fun go (Bound i) ctxt = (Bound i, ctxt)
- | go (Abs (x, _, t)) ctxt =
- let
- val (t', ctxt) = go t ctxt
- in
- (Abs (x, dummyT, t'), ctxt)
- end
- | go (tu as (t $ u)) ctxt =
- if is_atom tu andalso not (Term.is_open tu) then dummy ctxt else
- let
- val (t', ctxt) = go t ctxt
- val (u', ctxt) = go u ctxt
- in
- (t' $ u', ctxt)
- end
- | go _ ctxt = dummy ctxt
- in
- go t ctxt |> fst |> Syntax.check_term ctxt |>
- map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type})))
- end
-
-(** Monotonicity analysis **)
-
-(* TODO: Put extensible table in theory data *)
-val monotab =
- Symtab.make
- [(@{const_name transfer_implies}, [~1, 1]),
- (@{const_name transfer_forall}, [1])(*,
- (@{const_name implies}, [~1, 1]),
- (@{const_name All}, [1])*)]
-
-(*
-Function bool_insts determines the set of boolean-relation variables
-that can be instantiated to implies, rev_implies, or iff.
-
-Invariants: bool_insts p (t, u) requires that
- u :: _ => _ => ... => bool, and
- t is a skeleton of u
-*)
-fun bool_insts p (t, u) =
- let
- fun strip2 (t1 $ t2, u1 $ u2, tus) =
- strip2 (t1, u1, (t2, u2) :: tus)
- | strip2 x = x
- fun or3 ((a, b, c), (x, y, z)) = (a orelse x, b orelse y, c orelse z)
- fun go Ts p (Abs (_, T, t), Abs (_, _, u)) tab = go (T :: Ts) p (t, u) tab
- | go Ts p (t, u) tab =
- let
- val (a, _) = dest_TFree (Term.body_type (Term.fastype_of1 (Ts, t)))
- val (_, tf, tus) = strip2 (t, u, [])
- val ps_opt = case tf of Const (c, _) => Symtab.lookup monotab c | _ => NONE
- val tab1 =
- case ps_opt of
- SOME ps =>
- let
- val ps' = map (fn x => p * x) (take (length tus) ps)
- in
- fold I (map2 (go Ts) ps' tus) tab
- end
- | NONE => tab
- val tab2 = Symtab.make [(a, (p >= 0, p <= 0, is_none ps_opt))]
- in
- Symtab.join (K or3) (tab1, tab2)
- end
- val tab = go [] p (t, u) Symtab.empty
- fun f (a, (true, false, false)) = SOME (a, @{const implies})
- | f (a, (false, true, false)) = SOME (a, @{const rev_implies})
- | f (a, (true, true, _)) = SOME (a, HOLogic.eq_const HOLogic.boolT)
- | f _ = NONE
- in
- map_filter f (Symtab.dest tab)
- end
-
-fun retrieve_terms t net = map fst (Item_Net.retrieve net t)
-
-fun matches_list ctxt term =
- is_some o find_first (fn pat => Pattern.matches (Proof_Context.theory_of ctxt) (pat, term))
-
-fun transfer_rule_of_term ctxt equiv t : thm =
- let
- val compound_rhs = get_compound_rhs ctxt
- fun is_rhs t = compound_rhs |> retrieve_terms t |> matches_list ctxt t
- val s = skeleton is_rhs ctxt t
- val frees = map fst (Term.add_frees s [])
- val tfrees = map fst (Term.add_tfrees s [])
- fun prep a = "R" ^ Library.unprefix "'" a
- val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
- val tab = tfrees ~~ rnames
- fun prep a = the (AList.lookup (op =) tab a)
- val thm = transfer_rule_of_terms fst ctxt' tab s t
- val binsts = bool_insts (if equiv then 0 else 1) (s, t)
- val cbool = @{ctyp bool}
- val relT = @{typ "bool => bool => bool"}
- val idx = Thm.maxidx_of thm + 1
- val thy = Proof_Context.theory_of ctxt
- fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
- fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
- in
- thm
- |> Thm.generalize (tfrees, rnames @ frees) idx
- |> Thm.instantiate (map tinst binsts, map inst binsts)
- end
-
-fun transfer_rule_of_lhs ctxt t : thm =
- let
- val compound_lhs = get_compound_lhs ctxt
- fun is_lhs t = compound_lhs |> retrieve_terms t |> matches_list ctxt t
- val s = skeleton is_lhs ctxt t
- val frees = map fst (Term.add_frees s [])
- val tfrees = map fst (Term.add_tfrees s [])
- fun prep a = "R" ^ Library.unprefix "'" a
- val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
- val tab = tfrees ~~ rnames
- fun prep a = the (AList.lookup (op =) tab a)
- val thm = transfer_rule_of_terms snd ctxt' tab t s
- val binsts = bool_insts 1 (s, t)
- val cbool = @{ctyp bool}
- val relT = @{typ "bool => bool => bool"}
- val idx = Thm.maxidx_of thm + 1
- val thy = Proof_Context.theory_of ctxt
- fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
- fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
- in
- thm
- |> Thm.generalize (tfrees, rnames @ frees) idx
- |> Thm.instantiate (map tinst binsts, map inst binsts)
- end
-
-fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules)
- THEN_ALL_NEW rtac @{thm is_equality_eq}
-
-fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt)
-
-fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac (get_transfer_raw ctxt))
- THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt)))
-
-fun transfer_tac equiv ctxt i =
- let
- val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
- val start_rule =
- if equiv then @{thm transfer_start} else @{thm transfer_start'}
- val rules = get_transfer_raw ctxt
- val eq_rules = get_relator_eq_raw ctxt
- (* allow unsolved subgoals only for standard transfer method, not for transfer' *)
- val end_tac = if equiv then K all_tac else K no_tac
- val err_msg = "Transfer failed to convert goal to an object-logic formula"
- fun main_tac (t, i) =
- rtac start_rule i THEN
- (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))
- THEN_ALL_NEW
- (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))
- ORELSE' end_tac)) (i + 1)
- handle TERM (_, ts) => raise TERM (err_msg, ts)
- in
- EVERY
- [rewrite_goal_tac ctxt pre_simps i THEN
- SUBGOAL main_tac i,
- (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
- rewrite_goal_tac ctxt post_simps i,
- Goal.norm_hhf_tac ctxt i]
- end
-
-fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
- let
- val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
- val rule1 = transfer_rule_of_term ctxt false rhs
- val rules = get_transfer_raw ctxt
- val eq_rules = get_relator_eq_raw ctxt
- val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm rel_fun_eq[symmetric,THEN eq_reflection]}])
- in
- EVERY
- [CONVERSION prep_conv i,
- rtac @{thm transfer_prover_start} i,
- ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
- THEN_ALL_NEW
- (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))) (i+1),
- rtac @{thm refl} i]
- end)
-
-(** Transfer attribute **)
-
-fun transferred ctxt extra_rules thm =
- let
- val start_rule = @{thm transfer_start}
- val start_rule' = @{thm transfer_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 ctxt 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_lhs ctxt' t
- val tac =
- resolve_tac [thm2 RS start_rule', thm2 RS start_rule] 1 THEN
- (rtac rule
- THEN_ALL_NEW
- (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
- THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
- handle TERM (_, ts) => raise TERM (err_msg, ts)
- val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
- val tnames = map (fst o dest_TFree o snd) instT
- in
- thm3
- |> Raw_Simplifier.rewrite_rule ctxt' post_simps
- |> Simplifier.norm_hhf ctxt'
- |> Drule.generalize (tnames, [])
- |> Drule.zero_var_indexes
- end
-(*
- 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 ctxt 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_rules_tac eq_rules)))) 1
- handle TERM (_, ts) => raise TERM (err_msg, ts)
- val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
- val tnames = map (fst o dest_TFree o snd) instT
- in
- thm3
- |> Raw_Simplifier.rewrite_rule ctxt' post_simps
- |> Simplifier.norm_hhf ctxt'
- |> Drule.generalize (tnames, [])
- |> Drule.zero_var_indexes
- end
-
-(** Methods and attributes **)
-
-val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
- error ("Bad free variable: " ^ Syntax.string_of_term ctxt t))
-
-val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon)
- |-- Scan.repeat free) []
-
-fun transfer_method equiv : (Proof.context -> Proof.method) context_parser =
- fixing >> (fn vs => fn ctxt =>
- SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt))
-
-val transfer_prover_method : (Proof.context -> Proof.method) context_parser =
- Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
-
-(* Attribute for transfer rules *)
-
-fun prep_rule ctxt =
- abstract_domains_transfer ctxt o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv
-
-val transfer_add =
- Thm.declaration_attribute (fn thm => fn ctxt =>
- (add_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
-
-val transfer_del =
- Thm.declaration_attribute (fn thm => fn ctxt =>
- (del_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
-
-val transfer_attribute =
- Attrib.add_del transfer_add transfer_del
-
-(* Attributes for transfer domain rules *)
-
-val transfer_domain_add = Thm.declaration_attribute add_transfer_domain_thm
-
-val transfer_domain_del = Thm.declaration_attribute del_transfer_domain_thm
-
-val transfer_domain_attribute =
- Attrib.add_del transfer_domain_add transfer_domain_del
-
-(* Attributes for transferred rules *)
-
-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 =
- let
- val name = @{binding relator_eq}
- fun add_thm thm context = context
- |> Data.map (map_relator_eq (Item_Net.update thm))
- |> Data.map (map_relator_eq_raw
- (Item_Net.update (abstract_equalities_relator_eq (Context.proof_of context) thm)))
- fun del_thm thm context = context
- |> Data.map (map_relator_eq (Item_Net.remove thm))
- |> Data.map (map_relator_eq_raw
- (Item_Net.remove (abstract_equalities_relator_eq (Context.proof_of context) thm)))
- val add = Thm.declaration_attribute add_thm
- val del = Thm.declaration_attribute del_thm
- val text = "declaration of relator equality rule (used by transfer method)"
- val content = Item_Net.content o #relator_eq o Data.get
- in
- Attrib.setup name (Attrib.add_del add del) text
- #> Global_Theory.add_thms_dynamic (name, content)
- end
-
-val relator_domain_setup =
- let
- val name = @{binding relator_domain}
- fun add_thm thm context =
- let
- val thm = abstract_domains_relator_domain (Context.proof_of context) thm
- in
- context |> Data.map (map_relator_domain (Item_Net.update thm)) |> add_transfer_domain_thm thm
- end
- fun del_thm thm context =
- let
- val thm = abstract_domains_relator_domain (Context.proof_of context) thm
- in
- context |> Data.map (map_relator_domain (Item_Net.remove thm)) |> del_transfer_domain_thm thm
- end
- val add = Thm.declaration_attribute add_thm
- val del = Thm.declaration_attribute del_thm
- val text = "declaration of relator domain rule (used by transfer method)"
- val content = Item_Net.content o #relator_domain o Data.get
- in
- Attrib.setup name (Attrib.add_del add del) text
- #> Global_Theory.add_thms_dynamic (name, content)
- end
-
-val setup =
- relator_eq_setup
- #> relator_domain_setup
- #> Attrib.setup @{binding transfer_rule} transfer_attribute
- "transfer rule for transfer method"
- #> Global_Theory.add_thms_dynamic
- (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
- #> Attrib.setup @{binding transfer_domain_rule} transfer_domain_attribute
- "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)
- "generic theorem transfer method"
- #> Method.setup @{binding transfer'} (transfer_method false)
- "generic theorem transfer method"
- #> Method.setup @{binding transfer_prover} transfer_prover_method
- "for proving transfer rules"
-
-end
--- a/src/HOL/Topological_Spaces.thy Thu Apr 10 17:48:17 2014 +0200
+++ b/src/HOL/Topological_Spaces.thy Thu Apr 10 17:48:18 2014 +0200
@@ -2508,7 +2508,7 @@
lemma bi_total_rel_filter [transfer_rule]:
assumes "bi_total A" "bi_unique A"
shows "bi_total (rel_filter A)"
-unfolding bi_total_conv_left_right using assms
+unfolding bi_total_alt_def using assms
by(simp add: left_total_rel_filter right_total_rel_filter)
lemma left_unique_rel_filter [transfer_rule]:
@@ -2535,7 +2535,7 @@
lemma bi_unique_rel_filter [transfer_rule]:
"bi_unique A \<Longrightarrow> bi_unique (rel_filter A)"
-by(simp add: bi_unique_conv_left_right left_unique_rel_filter right_unique_rel_filter)
+by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter)
lemma top_filter_parametric [transfer_rule]:
"bi_total A \<Longrightarrow> (rel_filter A) top top"
--- a/src/HOL/Transfer.thy Thu Apr 10 17:48:17 2014 +0200
+++ b/src/HOL/Transfer.thy Thu Apr 10 17:48:18 2014 +0200
@@ -6,9 +6,13 @@
header {* Generic theorem transfer using relations *}
theory Transfer
-imports Hilbert_Choice Basic_BNFs Metis
+imports Hilbert_Choice Basic_BNFs BNF_FP_Base Metis Option
begin
+(* We include Option here altough it's not needed here.
+ By doing this, we avoid a diamond problem for BNF and
+ FP sugar interpretation defined in this file. *)
+
subsection {* Relator for function space *}
locale lifting_syntax
@@ -105,33 +109,6 @@
shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
using assms unfolding Rel_def rel_fun_def by fast
-end
-
-ML_file "Tools/transfer.ML"
-setup Transfer.setup
-
-declare refl [transfer_rule]
-
-declare rel_fun_eq [relator_eq]
-
-hide_const (open) Rel
-
-context
-begin
-interpretation lifting_syntax .
-
-text {* Handling of domains *}
-
-lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
- by auto
-
-lemma Domaimp_refl[transfer_domain_rule]:
- "Domainp T = Domainp T" ..
-
-lemma Domainp_prod_fun_eq[relator_domain]:
- "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))"
-by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff)
-
subsection {* Predicates on relations, i.e. ``class constraints'' *}
definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
@@ -181,7 +158,7 @@
lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
unfolding right_unique_def by fast
-lemma right_total_alt_def:
+lemma right_total_alt_def2:
"right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
unfolding right_total_def rel_fun_def
apply (rule iffI, fast)
@@ -191,11 +168,11 @@
apply fast
done
-lemma right_unique_alt_def:
+lemma right_unique_alt_def2:
"right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)"
unfolding right_unique_def rel_fun_def by auto
-lemma bi_total_alt_def:
+lemma bi_total_alt_def2:
"bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All"
unfolding bi_total_def rel_fun_def
apply (rule iffI, fast)
@@ -208,7 +185,7 @@
apply fast
done
-lemma bi_unique_alt_def:
+lemma bi_unique_alt_def2:
"bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
unfolding bi_unique_def rel_fun_def by auto
@@ -228,24 +205,72 @@
lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R"
by(auto simp add: bi_total_def)
-lemma bi_total_iff: "bi_total A = (right_total A \<and> left_total A)"
+lemma right_unique_alt_def: "right_unique R = (conversep R OO R \<le> op=)" unfolding right_unique_def by blast
+lemma left_unique_alt_def: "left_unique R = (R OO (conversep R) \<le> op=)" unfolding left_unique_def by blast
+
+lemma right_total_alt_def: "right_total R = (conversep R OO R \<ge> op=)" unfolding right_total_def by blast
+lemma left_total_alt_def: "left_total R = (R OO conversep R \<ge> op=)" unfolding left_total_def by blast
+
+lemma bi_total_alt_def: "bi_total A = (left_total A \<and> right_total A)"
unfolding left_total_def right_total_def bi_total_def by blast
-lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R"
-by(simp add: left_total_def right_total_def bi_total_def)
-
-lemma bi_unique_iff: "bi_unique A \<longleftrightarrow> right_unique A \<and> left_unique A"
+lemma bi_unique_alt_def: "bi_unique A = (left_unique A \<and> right_unique A)"
unfolding left_unique_def right_unique_def bi_unique_def by blast
-lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R"
-by(auto simp add: left_unique_def right_unique_def bi_unique_def)
-
lemma bi_totalI: "left_total R \<Longrightarrow> right_total R \<Longrightarrow> bi_total R"
-unfolding bi_total_iff ..
+unfolding bi_total_alt_def ..
lemma bi_uniqueI: "left_unique R \<Longrightarrow> right_unique R \<Longrightarrow> bi_unique R"
-unfolding bi_unique_iff ..
+unfolding bi_unique_alt_def ..
+
+end
+
+subsection {* Equality restricted by a predicate *}
+
+definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
+
+lemma eq_onp_Grp: "eq_onp P = BNF_Util.Grp (Collect P) id"
+unfolding eq_onp_def Grp_def by auto
+
+lemma eq_onp_to_eq:
+ assumes "eq_onp P x y"
+ shows "x = y"
+using assms by (simp add: eq_onp_def)
+
+lemma eq_onp_same_args:
+ shows "eq_onp P x x = P x"
+using assms by (auto simp add: eq_onp_def)
+
+lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))"
+by (metis mem_Collect_eq subset_eq)
+ML_file "Tools/Transfer/transfer.ML"
+setup Transfer.setup
+declare refl [transfer_rule]
+
+ML_file "Tools/Transfer/transfer_bnf.ML"
+
+declare pred_fun_def [simp]
+declare rel_fun_eq [relator_eq]
+
+hide_const (open) Rel
+
+context
+begin
+interpretation lifting_syntax .
+
+text {* Handling of domains *}
+
+lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
+ by auto
+
+lemma Domaimp_refl[transfer_domain_rule]:
+ "Domainp T = Domainp T" ..
+
+lemma Domainp_prod_fun_eq[relator_domain]:
+ "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))"
+by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff)
text {* Properties are preserved by relation composition. *}
@@ -333,12 +358,12 @@
lemma bi_total_fun[transfer_rule]:
"\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)"
- unfolding bi_unique_iff bi_total_iff
+ unfolding bi_unique_alt_def bi_total_alt_def
by (blast intro: right_total_fun left_total_fun)
lemma bi_unique_fun[transfer_rule]:
"\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)"
- unfolding bi_unique_iff bi_total_iff
+ unfolding bi_unique_alt_def bi_total_alt_def
by (blast intro: right_unique_fun left_unique_fun)
subsection {* Transfer rules *}
@@ -376,7 +401,7 @@
lemma eq_imp_transfer [transfer_rule]:
"right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
- unfolding right_unique_alt_def .
+ unfolding right_unique_alt_def2 .
text {* Transfer rules using equality. *}
@@ -490,6 +515,18 @@
using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
by metis
+lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
+unfolding eq_onp_def rel_fun_def by auto
+
+lemma rel_fun_eq_onp_rel:
+ shows "((eq_onp R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
+by (auto simp add: eq_onp_def rel_fun_def)
+
+lemma eq_onp_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "((A ===> op=) ===> A ===> A ===> op=) eq_onp eq_onp"
+unfolding eq_onp_def[abs_def] by transfer_prover
+
end
end