# HG changeset patch # User kuncar # Date 1397144898 -7200 # Node ID f4ba736040faae691835a321f0e049a11e4255a2 # Parent 2ae16e3d8b6d316edbcb694151e5f254fd6fb9e6 setup for Transfer and Lifting from BNF; tuned thm names diff -r 2ae16e3d8b6d -r f4ba736040fa src/HOL/Library/FSet.thy --- 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 \ 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 \ 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] diff -r 2ae16e3d8b6d -r f4ba736040fa src/HOL/Lifting.thy --- 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 @@ (\a b. T a b \ Abs a = b) \ (\b. T (Rep b) b) \ R = T OO conversep T" unfolding Quotient_alt_def3 fun_eq_iff by auto +lemma Quotient_alt_def5: + "Quotient R Abs Rep T \ + T \ BNF_Util.Grp UNIV Abs \ BNF_Util.Grp UNIV Rep \ T\\ \ R = T OO T\\" + 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 \ Respects R \ R x x" unfolding Respects_def by simp -subsection {* Invariant *} - -definition eq_onp :: "('a \ bool) \ 'a \ 'a \ bool" - where "eq_onp R = (\x y. R x \ 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 (\f. \x. P(f x))" -unfolding eq_onp_def rel_fun_def by auto - -lemma rel_fun_eq_onp_rel: - shows "((eq_onp R) ===> S) = (\f g. \x. R x \ 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 \ 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 \ (\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" diff -r 2ae16e3d8b6d -r f4ba736040fa src/HOL/Lifting_Set.thy --- 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 \ 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 \ bi_unique (rel_set A)" diff -r 2ae16e3d8b6d -r f4ba736040fa src/HOL/Tools/Lifting/lifting_bnf.ML --- /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 diff -r 2ae16e3d8b6d -r f4ba736040fa src/HOL/Tools/Lifting/lifting_def.ML --- 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 diff -r 2ae16e3d8b6d -r f4ba736040fa src/HOL/Tools/Quotient/quotient_def.ML --- 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 diff -r 2ae16e3d8b6d -r f4ba736040fa src/HOL/Tools/Transfer/transfer.ML --- /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 diff -r 2ae16e3d8b6d -r f4ba736040fa src/HOL/Tools/Transfer/transfer_bnf.ML --- /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 \"]} + 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 diff -r 2ae16e3d8b6d -r f4ba736040fa src/HOL/Tools/transfer.ML --- 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 diff -r 2ae16e3d8b6d -r f4ba736040fa src/HOL/Topological_Spaces.thy --- 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 \ 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 \ (rel_filter A) top top" diff -r 2ae16e3d8b6d -r f4ba736040fa src/HOL/Transfer.thy --- 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) (\x. f x) (\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 \ (\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) = (\f. \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 \ 'b \ bool) \ bool" @@ -181,7 +158,7 @@ lemma right_uniqueD: "\ right_unique A; A x y; A x z \ \ y = z" unfolding right_unique_def by fast -lemma right_total_alt_def: +lemma right_total_alt_def2: "right_total R \ ((R ===> op \) ===> op \) 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 \ (R ===> R ===> op \) (op =) (op =)" unfolding right_unique_def rel_fun_def by auto -lemma bi_total_alt_def: +lemma bi_total_alt_def2: "bi_total R \ ((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 \ (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\\ = bi_total R" by(auto simp add: bi_total_def) -lemma bi_total_iff: "bi_total A = (right_total A \ left_total A)" +lemma right_unique_alt_def: "right_unique R = (conversep R OO R \ op=)" unfolding right_unique_def by blast +lemma left_unique_alt_def: "left_unique R = (R OO (conversep R) \ op=)" unfolding left_unique_def by blast + +lemma right_total_alt_def: "right_total R = (conversep R OO R \ op=)" unfolding right_total_def by blast +lemma left_total_alt_def: "left_total R = (R OO conversep R \ op=)" unfolding left_total_def by blast + +lemma bi_total_alt_def: "bi_total A = (left_total A \ right_total A)" unfolding left_total_def right_total_def bi_total_def by blast -lemma bi_total_conv_left_right: "bi_total R \ left_total R \ right_total R" -by(simp add: left_total_def right_total_def bi_total_def) - -lemma bi_unique_iff: "bi_unique A \ right_unique A \ left_unique A" +lemma bi_unique_alt_def: "bi_unique A = (left_unique A \ right_unique A)" unfolding left_unique_def right_unique_def bi_unique_def by blast -lemma bi_unique_conv_left_right: "bi_unique R \ left_unique R \ right_unique R" -by(auto simp add: left_unique_def right_unique_def bi_unique_def) - lemma bi_totalI: "left_total R \ right_total R \ bi_total R" -unfolding bi_total_iff .. +unfolding bi_total_alt_def .. lemma bi_uniqueI: "left_unique R \ right_unique R \ bi_unique R" -unfolding bi_unique_iff .. +unfolding bi_unique_alt_def .. +end + +subsection {* Equality restricted by a predicate *} + +definition eq_onp :: "('a \ bool) \ 'a \ 'a \ bool" + where "eq_onp R = (\x y. R x \ 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 \ (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 \ (\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) = (\f. \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]: "\bi_unique A; bi_total B\ \ 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]: "\bi_total A; bi_unique B\ \ 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 \ (A ===> A ===> op \) (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 (\f. \x. P(f x))" +unfolding eq_onp_def rel_fun_def by auto + +lemma rel_fun_eq_onp_rel: + shows "((eq_onp R) ===> S) = (\f g. \x. R x \ 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