diff --git a/thys/ML_Unification/Examples/E_Unification_Examples.thy b/thys/ML_Unification/Examples/E_Unification_Examples.thy --- a/thys/ML_Unification/Examples/E_Unification_Examples.thy +++ b/thys/ML_Unification/Examples/E_Unification_Examples.thy @@ -1,156 +1,156 @@ \<^marker>\creator "Kevin Kappelmann"\ section \E-Unification Examples\ theory E_Unification_Examples imports Main ML_Unification_HOL_Setup Unify_Fact_Tactic begin paragraph \Summary\ text \Sample applications of e-unifiers, methods, etc. introduced in this session.\ experiment begin subsection \Using The Simplifier For Unification.\ inductive_set even :: "nat set" where zero: "0 \ even" | step: "n \ even \ Suc (Suc n) \ even" text \Premises of the form @{term "SIMPS_TO_UNIF lhs rhs"} are solved by @{ML_structure Simplifier_Unification}. It first normalises @{term lhs} and then unifies the normalisation with @{term rhs}. See also @{theory ML_Unification.ML_Unification_HOL_Setup}.\ lemma [uhint where prio = Prio.LOW]: "n \ 0 \ PROP SIMPS_TO_UNIF (n - 1) m \ n \ Suc m" unfolding SIMPS_TO_UNIF_eq by linarith text \By default, below unification methods use -@{ML Standard_Mixed_Unification.first_higherp_first_comb_higher_unify}, which is a combination of +@{ML Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify}, which is a combination of various practical unification algorithms.\ schematic_goal "(\x. x + 4 = n) \ Suc ?x = n" by uassm lemma "6 \ even" apply (urule step) apply (urule step) apply (urule step) apply (urule zero) done lemma "(220 + (80 - 2 * 2)) \ even" apply (urule step) apply (urule step)+ apply (urule zero) done lemma assumes "[a,b,c] = [c,b,a]" shows "[a] @ [b,c] = [c,b,a]" using assms by uassm lemma "x \ ({z, y, x} \ S) \ {x}" by (ufact TrueI) lemma "(x + (y :: nat))^2 \ x^2 + 2*x*y + y^2 + 4 * y + x - y" supply power2_sum[simp] by (ufact TrueI) lemma assumes "\s. P (Suc (Suc 0)) (s(x := (1 :: nat), x := 1 + 1 * 4 - 3))" shows "P 2 (s(x := 2))" by (ufact assms[of s]) subsection \Providing Canonical Solutions With Unification Hints\ lemma length_nil_eq_zero [uhint]: "length [] \ 0" by simp schematic_goal "length ?xs = 0" by (ufact refl) lemma sub_self_eq_zero [uhint]: "(n :: nat) - n \ 0" by simp schematic_goal "n - ?m = (0 :: nat)" by (ufact refl) text \The following fails because, by default, @{ML Standard_Unification_Hints.try_hints} uses the higher-order pattern unifier to unify hints against a given disagreement pair, and @{term 0} cannot be higher-order pattern unified with @{term "length []"}. The unification of the hint requires the use of yet another hint, namely @{term "length [] = 0"} (cf. above).\ schematic_goal "n - ?m = length []" \ \by (ufact refl)\ oops text \There are two ways to fix this: \<^enum> We allow the recursive use of unification hints when unifying @{thm sub_self_eq_zero} and our goal. \<^enum> We use a different unification hint that makes the recursive use of unification hints explicit.\ text \Solution 1: we can use @{attribute rec_uhint} for recursive usages of hints. Warning: recursive hint applications easily loop.\ schematic_goal "n - ?m = length []" supply sub_self_eq_zero[rec_uhint] by (ufact refl) text \Solution 2: make the recursion explicit in the hint.\ lemma [uhint]: "k \ 0 \ (n :: nat) \ m \ n - m \ k" by simp schematic_goal "n - ?m = length []" by (ufact refl) subsection \Strenghten Unification With Unification Hints\ lemma assumes [uhint]: "n = m" shows "n - m = (0 :: nat)" by (ufact refl) lemma assumes "x = y" shows "y = x" supply eq_commute[uhint] by (ufact assms) paragraph \Unfolding definitions.\ definition "mysuc n = Suc n" lemma assumes "\m. Suc n > mysuc m" shows "mysuc n > Suc 3" supply mysuc_def[uhint] by (ufact assms) paragraph \Discharging meta impliciations with object-level implications\ lemma [uhint]: "Trueprop A \ A' \ Trueprop B \ B' \ Trueprop (A \ B) \ (PROP A' \ PROP B')" using atomize_imp[symmetric] by simp lemma assumes "A \ (B \ C) \ D" shows "A \ (B \ C) \ D" using assms by ufact subsection \Better Control Over Meta Variable Instantiations\ text \Consider the following type-inference problem.\ schematic_goal assumes app_typeI: "\f x. (\x. ArgT x \ DomT x (f x)) \ ArgT x \ DomT x (f x)" and f_type: "\x. ArgT x \ DomT x (f x)" and x_type: "ArgT x" shows "?T (f x)" apply (urule app_typeI) \\compare with the following application, creating an (unintuitive) higher-order instantiation\ (* apply (rule app_typeI) *) oops end end diff --git a/thys/ML_Unification/ML_Unification_HOL_Setup.thy b/thys/ML_Unification/ML_Unification_HOL_Setup.thy --- a/thys/ML_Unification/ML_Unification_HOL_Setup.thy +++ b/thys/ML_Unification/ML_Unification_HOL_Setup.thy @@ -1,34 +1,36 @@ \<^marker>\creator "Kevin Kappelmann"\ section \Setup for HOL\ theory ML_Unification_HOL_Setup imports HOL.HOL ML_Unification_Hints begin lemma eq_eq_True: "P \ (P \ Trueprop True)" by standard+ simp_all declare [[uhint where hint_preprocessor = \Unification_Hints_Base.obj_logic_hint_preprocessor @{thm atomize_eq[symmetric]} (Conv.rewr_conv @{thm eq_eq_True})\]] and [[rec_uhint where hint_preprocessor = \Unification_Hints_Base.obj_logic_hint_preprocessor @{thm atomize_eq[symmetric]} (Conv.rewr_conv @{thm eq_eq_True})\]] lemma eq_TrueI: "PROP P \ PROP P \ Trueprop True" by (standard) simp declare [[ucombine add = \Standard_Unification_Combine.eunif_data (Simplifier_Unification.SIMPS_TO_unify @{thm eq_TrueI} |> Unification_Combinator.norm_closed_unifier - (#norm_term Standard_Mixed_Unification.norms_first_higherp_first_comb_higher_unify) + (#norm_term Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify) |> Unification_Combinator.unifier_from_closed_unifier |> K) (Standard_Unification_Combine.default_metadata \<^binding>\SIMPS_TO_unif\)\]] declare [[ucombine add = \Standard_Unification_Combine.eunif_data (Simplifier_Unification.SIMPS_TO_UNIF_unify @{thm eq_TrueI} - Standard_Mixed_Unification.norms_first_higherp_first_comb_higher_unify - (Standard_Mixed_Unification.first_higherp_first_comb_higher_unify + Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify + (Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify |> Unification_Combinator.norm_unifier Envir_Normalisation.beta_norm_term_unif) - |> Unification_Combinator.norm_unifier - (#norm_term Standard_Mixed_Unification.norms_first_higherp_first_comb_higher_unify) + |> Unification_Combinator.norm_closed_unifier + (#norm_term Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify) + |> Unification_Combinator.unifier_from_closed_unifier |> K) (Standard_Unification_Combine.default_metadata \<^binding>\SIMPS_TO_UNIF_unif\)\]] + end diff --git a/thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML b/thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML --- a/thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML +++ b/thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML @@ -1,260 +1,260 @@ (* Title: ML_Utils/tactic_util.ML Author: Kevin Kappelmann Tactic utilities. *) signature TACTIC_UTIL = sig include HAS_LOGGER (* tactic combinators*) val HEADGOAL : (int -> 'a) -> 'a val TRY' : ('a -> tactic) -> 'a -> tactic val EVERY_ARG : ('a -> tactic) -> 'a list -> tactic val EVERY_ARG' : ('a -> 'b -> tactic) -> 'a list -> 'b -> tactic val CONCAT : tactic list -> tactic val CONCAT' : ('a -> tactic) list -> 'a -> tactic val FOCUS_PARAMS' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic val FOCUS_PARAMS_CTXT : (Proof.context -> tactic) -> Proof.context -> int -> tactic val FOCUS_PARAMS_CTXT' : (Proof.context -> int -> tactic) -> Proof.context -> int -> tactic val FOCUS_PARAMS_FIXED' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic val FOCUS_PREMS' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic val FOCUS' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic val SUBPROOF' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic val CSUBGOAL_DATA : (cterm -> 'a) -> ('a -> int -> tactic) -> int -> tactic val CSUBGOAL_STRIPPED : (cterm Binders.binders * (cterm list * cterm) -> 'a) -> ('a -> int -> tactic) -> int -> tactic val SUBGOAL_DATA : (term -> 'a) -> ('a -> int -> tactic) -> int -> tactic val SUBGOAL_STRIPPED : ((string * typ) list * (term list * term) -> 'a) -> ('a -> int -> tactic) -> int -> tactic (* tactics *) val insert_tac : thm list -> Proof.context -> int -> tactic (*thin_tac n i deletes nth premise of the ith subgoal*) val thin_tac : int -> int -> tactic val thin_tacs : int list -> int -> tactic val set_kernel_ho_unif_bounds : int -> int -> Proof.context -> Proof.context val silence_kernel_ho_bounds_exceeded : Proof.context -> Proof.context val safe_simp_tac : Proof.context -> int -> tactic (*nth_eq_assume_tac n i solves ith subgoal by assumption, without unification, preferring premise n*) val nth_eq_assume_tac : int -> int -> tactic (*resolution without lifting of premises and parameters*) val no_lift_biresolve_tac : bool -> thm -> int -> Proof.context -> int -> tactic val no_lift_resolve_tac : thm -> int -> Proof.context -> int -> tactic val no_lift_eresolve_tac : thm -> int -> Proof.context -> int -> tactic (*rewrite subgoal according to the given equality theorem "lhs \ subgoal"*) val rewrite_subgoal_tac : thm -> Proof.context -> int -> tactic (*creates equality theorem for a subgoal from an equality theorem for the subgoal's conclusion; fails if the equality theorem contains a tpair or implicit Assumption mentioning one of the bound variables*) val eq_subgoal_from_eq_concl : cterm Binders.binders -> cterm list -> thm -> Proof.context -> thm option (*rewrite a subgoal given an equality theorem and environment for the subgoal's conclusion*) val rewrite_subgoal_unif_concl : Envir_Normalisation.term_normaliser -> Envir_Normalisation.thm_normaliser -> Envir_Normalisation.thm_normaliser -> term Binders.binders -> (Envir.env * thm) -> Proof.context -> int -> tactic (*protect premises starting from (and excluding) the given index in the specified subgoal*) val protect_tac : int -> Proof.context -> int -> tactic (*unprotect the subgoal*) val unprotect_tac : Proof.context -> int -> tactic (*protect, then apply tactic, then unprotect*) val protected_tac : int -> (int -> tactic) -> Proof.context -> int -> tactic (*focus on the specified subgoal, introducing only the specified list of premises as theorems in the focus*) val focus_prems_tac : int list -> (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic (*focus_prems_tac and then deletes all focused premises*) val focus_delete_prems_tac : int list -> (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic (*apply tactic to the specified subgoal, where the state is given as a cterm*) val apply_tac : (int -> tactic) -> int -> cterm -> thm Seq.seq end structure Tactic_Util : TACTIC_UTIL = struct val logger = Logger.setup_new_logger Logger.root_logger "Tactic_Util" (* tactic combinators *) fun HEADGOAL f = f 1 fun TRY' tac = tac ORELSE' K all_tac fun EVERY_ARG tac = EVERY o map tac fun EVERY_ARG' tac = EVERY' o map tac fun CONCAT tacs = fold_rev (curry op APPEND) tacs no_tac fun CONCAT' tacs = fold_rev (curry op APPEND') tacs (K no_tac) fun FOCUS_PARAMS' tac = Subgoal.FOCUS_PARAMS (HEADGOAL o tac) fun FOCUS_PARAMS_FIXED' tac = Subgoal.FOCUS_PARAMS_FIXED (HEADGOAL o tac) fun FOCUS_PREMS' tac = Subgoal.FOCUS_PREMS (HEADGOAL o tac) fun FOCUS' tac = Subgoal.FOCUS (HEADGOAL o tac) fun SUBPROOF' tac = Subgoal.SUBPROOF (HEADGOAL o tac) fun FOCUS_PARAMS_CTXT tac = Subgoal.FOCUS_PARAMS (#context #> tac) fun FOCUS_PARAMS_CTXT' tac = FOCUS_PARAMS' (#context #> tac) fun CSUBGOAL_DATA f tac = CSUBGOAL (uncurry tac o apfst f) fun CSUBGOAL_STRIPPED f = CSUBGOAL_DATA (f o Term_Util.strip_csubgoal) fun SUBGOAL_DATA f tac = SUBGOAL (uncurry tac o apfst f) fun SUBGOAL_STRIPPED f = SUBGOAL_DATA (f o Term_Util.strip_subgoal) (* tactics *) fun insert_tac thms ctxt = Method.insert_tac ctxt thms fun thin_tac n = if n < 1 then K no_tac else rotate_tac (n - 1) THEN' (DETERM o eresolve0_tac [thin_rl]) THEN' rotate_tac (~n + 1) val thin_tacs = sort int_ord #> map_index ((op -) o swap) #> EVERY_ARG' thin_tac fun set_kernel_ho_unif_bounds trace_bound search_bound = Config.put Unify.trace_bound trace_bound #> Config.put Unify.search_bound search_bound val silence_kernel_ho_bounds_exceeded = Context_Position.set_visible false (*some "safe" solvers create instantiations via flex-flex pairs, which we disallow here*) fun safe_simp_tac ctxt i state = let val eq_flexps = Thm.tpairs_of #> pair (Thm.tpairs_of state) #> eq_list (eq_pair (op aconv) (op aconv)) (*stop higher-order unifier from entering difficult unification problems*) val ctxt = set_kernel_ho_unif_bounds 1 1 ctxt |> silence_kernel_ho_bounds_exceeded in Simplifier.safe_simp_tac ctxt i state |> Seq.filter eq_flexps end fun nth_eq_assume_tac n = if n < 1 then K no_tac else rotate_tac (n - 1) THEN' eq_assume_tac (*resolution*) fun no_lift_biresolve_tac eres brule nsubgoals ctxt = Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true} (eres, brule, nsubgoals) #> PRIMSEQ val no_lift_resolve_tac = no_lift_biresolve_tac false val no_lift_eresolve_tac = no_lift_biresolve_tac true fun rewrite_subgoal_tac eq_thm = let val (lhs, rhs) = Thm.dest_equals (Thm.cconcl_of eq_thm) val eq_elim = Thm.instantiate' [] [SOME lhs, SOME rhs] Drule.equal_elim_rule1 val thm = Thm.implies_elim eq_elim eq_thm in no_lift_resolve_tac thm 1 end fun eq_subgoal_from_eq_concl cbinders cprems eq_thm ctxt = let fun all_abstract ((x, T), cfree) = let val all_const = Logic.all_const T |> Thm.cterm_of ctxt in Thm_Util.abstract_rule ctxt x cfree #> Option.map (Drule.arg_cong_rule all_const) end in (*introduce the premises*) SOME (fold_rev (Drule.imp_cong_rule o Thm.reflexive) cprems eq_thm) (*introduce abstractions for the fresh Frees*) |> fold (Option.mapPartial o all_abstract) cbinders end fun rewrite_subgoal_unif_concl norm_binders norm_state norm_eq_thm binders (env_eq_thm as (env, _)) ctxt i = let - val binders = Binders.norm_binders (norm_binders env) binders + (*updates binders with their normalised type*) + fun updated_binders env = Binders.norm_binders (norm_binders env) binders + val binders = updated_binders env fun smash_tpairs_if_occurs (_, bvar) = Seq.maps (Unification_Util.smash_tpairs_if_occurs ctxt bvar) fun rewrite_tac env eq_thm (rparams, (prems, _)) = let - (*update binders with their normalised type*) - val binders = map2 (fn (_, T) => fn ((n, _), Free (n', _)) => ((n, T), Free (n', T))) - rparams binders + val binders = updated_binders env val cterm_of = Thm.cterm_of ctxt val cprems = map (cterm_of o Binders.replace_binders binders) prems in eq_subgoal_from_eq_concl (map (apsnd cterm_of) binders) cprems (norm_eq_thm ctxt env eq_thm) ctxt |> Option.map (fn eq_thm => rewrite_subgoal_tac eq_thm ctxt) |> the_default (K no_tac) end in (*smash tpairs in case some binder occurs*) fold smash_tpairs_if_occurs binders (Seq.single env_eq_thm) |> Seq.lifts (fn (env, eq_thm) => PRIMITIVE (norm_state ctxt env) THEN SUBGOAL_STRIPPED I (rewrite_tac env eq_thm) i) end fun protect_tac n ctxt = let fun protect cbinders (cprems, cconcl) i = let val nprems = length cprems in if nprems < n then (@{log Logger.WARN} ctxt (fn _ => Pretty.block [ Pretty.str "Not enough premises to protect. Given number: ", Pretty.str (string_of_int n), Pretty.str ". But there are only ", Pretty.str (string_of_int nprems), Pretty.str " premise(s) in subgoal ", Pretty.str (string_of_int i), Pretty.str ": ", Logic.close_prop (map (apfst fst o apsnd Thm.term_of) cbinders) (map Thm.term_of cprems) (Thm.term_of cconcl) |> Syntax.pretty_term ctxt ] |> Pretty.string_of); no_tac) else let val (cprems_unprotected, cconcl_protected) = chop n cprems ||> Drule.list_implies o rpair cconcl in @{thm Pure.prop_def} |> Thm.instantiate' [] [SOME cconcl_protected] |> (fn eq_thm => eq_subgoal_from_eq_concl cbinders cprems_unprotected eq_thm ctxt) |> Option.map (fn protected_eq_thm => rewrite_subgoal_tac protected_eq_thm ctxt i) |> the_default no_tac end end in if n < 0 then K no_tac else CSUBGOAL_STRIPPED I (uncurry protect) end fun unprotect_tac ctxt = match_tac ctxt [Drule.protectI] fun protected_tac n tac ctxt = protect_tac n ctxt THEN' tac THEN_ALL_NEW (unprotect_tac ctxt) fun focus_prems_tac is tac ctxt = CONVERSION (Conversion_Util.move_prems_to_front_conv is) THEN' protect_tac (length is) ctxt THEN' FOCUS_PREMS' (fn {context=ctxt, params=params, prems=prems, asms=asms, concl=concl, schematics=schematics} => let val concl = Term_Util.unprotect concl in unprotect_tac ctxt THEN' tac {context=ctxt, params=params, prems=prems, asms=asms, concl=concl, schematics=schematics} end ) ctxt fun focus_delete_prems_tac is tac ctxt = focus_prems_tac is tac ctxt THEN' thin_tacs (1 upto length is) fun apply_tac tac i = Goal.init #> tac i #> Seq.map Goal.conclude end diff --git a/thys/ML_Unification/Unification_Attributes/Unification_Attributes.thy b/thys/ML_Unification/Unification_Attributes/Unification_Attributes.thy --- a/thys/ML_Unification/Unification_Attributes/Unification_Attributes.thy +++ b/thys/ML_Unification/Unification_Attributes/Unification_Attributes.thy @@ -1,72 +1,72 @@ \<^marker>\creator "Kevin Kappelmann"\ section \Unification Attributes\ theory Unification_Attributes imports Unify_Resolve_Tactics begin paragraph \Summary\ text \OF attribute with adjustable unifier.\ ML_file\unify_of_base.ML\ ML_file\unify_of.ML\ ML\ @{functor_instance struct_name = Standard_Unify_OF and functor_name = Unify_OF and id = \""\ and more_args = \val init_args = { - normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_first_comb_higher_unify, - unifier = SOME Standard_Mixed_Unification.first_higherp_first_comb_higher_unify, + normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify, + unifier = SOME Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify, mode = SOME (Unify_OF_Args.PM.key Unify_OF_Args.PM.fact) }\} \ local_setup \Standard_Unify_OF.setup_attribute NONE\ paragraph \Examples\ experiment begin lemma assumes h1: "(PROP A \ PROP D) \ PROP E \ PROP C" assumes h2: "PROP B \ PROP D" and h3: "PROP F \ PROP E" shows "(PROP A \ PROP B) \ PROP F \ PROP C" by (fact h1[uOF h2 h3 where mode = resolve]) \\the line below is equivalent\ (* by (fact h1[OF h2 h3]) *) lemma assumes h1: "(PROP A \ PROP A)" assumes h2: "(PROP A \ PROP A) \ PROP B" shows "PROP B" by (fact h2[uOF h1]) \\the line below is equivalent\ (* by (fact h2[uOF h1 where mode = fact]) *) \\Note: @{attribute OF} would not work in this case:\ (* thm h2[OF h1] *) lemma assumes h1: "\x y z. PROP P x y \ PROP P y y \ (PROP A \ PROP A) \ (PROP A \ PROP B) \ PROP C" and h2: "\x y. PROP P x y" and h3 : "PROP A \ PROP A" and h4 : "PROP D \ PROP B" shows "(PROP A \ PROP D) \ PROP C" by (fact h1[uOF h2 h2 h3, uOF h4 where mode = resolve]) lemma assumes h1: "\P x. PROP P x \ PROP E P x" and h2: "PROP P x" shows "PROP E P x" by (fact h1[uOF h2]) \\the following line does not work (multiple unifiers error)\ (* by (fact h1[OF h2]) *) text\We can also specify the unifier to be used:\ lemma assumes h1: "\P. PROP P \ PROP E" and h2: "\P. PROP P" shows "PROP E" by (fact h1[uOF h2 where unifier = First_Order_Unification.unify]) \\the line below is equivalent\ (* using [[uOF unifier = First_Order_Unification.unify]] by (fact h1[uOF h2]) *) end end diff --git a/thys/ML_Unification/Unification_Hints/ML_Unification_Hints.thy b/thys/ML_Unification/Unification_Hints/ML_Unification_Hints.thy --- a/thys/ML_Unification/Unification_Hints/ML_Unification_Hints.thy +++ b/thys/ML_Unification/Unification_Hints/ML_Unification_Hints.thy @@ -1,103 +1,108 @@ \<^marker>\creator "Kevin Kappelmann"\ section \Unification Hints\ theory ML_Unification_Hints imports ML_Generic_Data_Utils ML_Term_Index ML_Unifiers ML_Unification_Parsers begin paragraph \Summary\ text \A generalisation of unification hints, originally introduced in \<^cite>\"unif-hints"\. We support a generalisation that \<^enum> allows additional universal variables in premises \<^enum> allows non-atomic left-hand sides for premises \<^enum> allows arbitrary functions to perform the matching/unification of a hint with a disagreement pair. General shape of a hint: \\y1...yn. (\x1...xn1. lhs1 \ rhs1) \ ... \ (\x1...xnk. lhsk \ rhsk) \ lhs \ rhs\ \ ML_file\unification_hints_base.ML\ ML_file\unification_hints.ML\ ML_file\term_index_unification_hints.ML\ text \We now set up two unifiers using unification hints. The first one allows for recursive applications of unification hints when unifying a hint's conclusion \lhs \ rhs\ with a goal \lhs' \ rhs'\. The second only uses a combination of higher-order pattern and first-order unification. This particularly implies that recursive applications of unification hints have to be made explicit in the hint itself (cf. @{dir "../Examples"}). While the former can be convenient for local hint registrations and quick developments, it is advisable to use the second for global hints to avoid unexpected looping behaviour.\ ML\ @{functor_instance struct_name = Standard_Unification_Hints_Rec and functor_name = Term_Index_Unification_Hints and id = \"rec"\ and more_args = \ structure TI = Discrimination_Tree val init_args = { - concl_unifier = SOME Standard_Mixed_Unification.first_higherp_first_comb_higher_unify, - prems_unifier = SOME (Standard_Mixed_Unification.first_higherp_first_comb_higher_unify + concl_unifier = SOME Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify, + prems_unifier = SOME (Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify |> Unification_Combinator.norm_unifier Envir_Normalisation.beta_norm_term_unif), - normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_first_comb_higher_unify, + normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify, retrieval = SOME (Term_Index_Unification_Hints_Args.mk_sym_retrieval TI.norm_term TI.unifiables), hint_preprocessor = SOME (K I) }\} \ local_setup \Standard_Unification_Hints_Rec.setup_attribute NONE\ text\Standard unification hints using -@{ML Standard_Mixed_Unification.first_higherp_first_comb_higher_unify} +@{ML Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify} when looking for hints are accessible via @{attribute rec_uhint}. \<^emph>\Note:\ when we retrieve a potential unification hint with conclusion \lhs \ rhs\ for a goal \lhs' \ rhs'\, we only consider those hints whose lhs potentially higher-order unifies with lhs' or rhs' \<^emph>\without using hints\. For otherwise, any hint \lhs \ rhs\ applied to a goal \rhs \ lhs\ leads to an immediate loop.\ ML\ @{functor_instance struct_name = Standard_Unification_Hints and functor_name = Term_Index_Unification_Hints and id = \""\ and more_args = \ structure TI = Discrimination_Tree val init_args = { - concl_unifier = SOME Higher_Ordern_Pattern_First_Decomp_Unification.unify, - prems_unifier = SOME (Standard_Mixed_Unification.first_higherp_first_comb_higher_unify + concl_unifier = SOME (fn binders => + Standard_Unification_Combine.map_eunif_datas (K Prio.Table.empty) + |> Context.proof_map + #> Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify binders), + prems_unifier = SOME (Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify |> Unification_Combinator.norm_unifier Envir_Normalisation.beta_norm_term_unif), - normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_first_comb_higher_unify, + normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify, retrieval = SOME (Term_Index_Unification_Hints_Args.mk_sym_retrieval TI.norm_term TI.unifiables), hint_preprocessor = SOME (K I) }\} \ local_setup \Standard_Unification_Hints.setup_attribute NONE\ -text\Standard unification hints using @{ML Higher_Ordern_Pattern_First_Decomp_Unification.unify} -when looking for hints are accessible via @{attribute uhint}. +text\Standard unification hints using +@{ML Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify} when looking for hints, +without using fallback list of unifiers, are accessible via @{attribute uhint}. \<^emph>\Note:\ there will be no recursive usage of unification hints when searching for potential unification hints in this case. See also @{dir "../Examples"}.\ declare [[ucombine add = \Standard_Unification_Combine.eunif_data (Standard_Unification_Hints_Rec.try_hints |> Unification_Combinator.norm_unifier - (#norm_term Standard_Mixed_Unification.norms_first_higherp_first_comb_higher_unify) + (#norm_term Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify) |> K) (Standard_Unification_Combine.default_metadata Standard_Unification_Hints_Rec.binding)\]] -and [[ucombine add = \Standard_Unification_Combine.eunif_data + +declare [[ucombine add = \Standard_Unification_Combine.eunif_data (Standard_Unification_Hints.try_hints |> Unification_Combinator.norm_unifier - (#norm_term Standard_Mixed_Unification.norms_first_higherp_first_comb_higher_unify) + (#norm_term Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify) |> K) (Standard_Unification_Combine.default_metadata Standard_Unification_Hints.binding)\]] text\Examples see @{dir "../Examples"}.\ end diff --git a/thys/ML_Unification/Unification_Tactics/Assumption/Unify_Assumption_Tactic.thy b/thys/ML_Unification/Unification_Tactics/Assumption/Unify_Assumption_Tactic.thy --- a/thys/ML_Unification/Unification_Tactics/Assumption/Unify_Assumption_Tactic.thy +++ b/thys/ML_Unification/Unification_Tactics/Assumption/Unify_Assumption_Tactic.thy @@ -1,70 +1,70 @@ \<^marker>\creator "Kevin Kappelmann"\ subsection \Assumption Tactic\ theory Unify_Assumption_Tactic imports ML_Functor_Instances ML_Unifiers ML_Unification_Parsers begin paragraph \Summary\ text \Assumption tactic and method with adjustable unifier.\ ML_file\unify_assumption_base.ML\ ML_file\unify_assumption.ML\ ML\ @{functor_instance struct_name = Standard_Unify_Assumption and functor_name = Unify_Assumption and id = \""\ and more_args = \val init_args = { - normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_first_comb_higher_unify, - unifier = SOME Standard_Mixed_Unification.first_higherp_first_comb_higher_unify + normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify, + unifier = SOME Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify }\} \ local_setup \Standard_Unify_Assumption.setup_attribute NONE\ local_setup \Standard_Unify_Assumption.setup_method NONE\ paragraph \Examples\ experiment begin lemma "PROP P \ PROP P" by uassm lemma assumes h: "\P. PROP P" shows "PROP P x" using h by uassm schematic_goal "\x. PROP P (c :: 'a) \ PROP ?Y (x :: 'a)" by uassm schematic_goal a: "PROP ?P (y :: 'a) \ PROP ?P (?x :: 'a)" by uassm \\compare the result with following call\ (* by assumption *) schematic_goal "PROP ?P (x :: 'a) \ PROP P (?x :: 'a)" by uassm \\compare the result with following call\ (* by assumption *) schematic_goal "\x. PROP D \ (\P y. PROP P y x) \ PROP C \ PROP P x" by (uassm unifier = Higher_Order_Unification.unify) \\the line below is equivalent\ (* using [[uassm unifier = Higher_Order_Unification.unify]] by uassm *) text \Unlike @{method assumption}, @{method uassm} will not close the goal if the order of premises of the assumption and the goal are different. Compare the following two examples:\ lemma "\x. PROP D \ (\y. PROP A y \ PROP B x) \ PROP C \ PROP A x \ PROP B x" by uassm lemma "\x. PROP D \ (\y. PROP A y \ PROP B x) \ PROP A x \ PROP C \ PROP B x" by assumption (* by uassm *) end end diff --git a/thys/ML_Unification/Unification_Tactics/Fact/Unify_Fact_Tactic.thy b/thys/ML_Unification/Unification_Tactics/Fact/Unify_Fact_Tactic.thy --- a/thys/ML_Unification/Unification_Tactics/Fact/Unify_Fact_Tactic.thy +++ b/thys/ML_Unification/Unification_Tactics/Fact/Unify_Fact_Tactic.thy @@ -1,47 +1,47 @@ \<^marker>\creator "Kevin Kappelmann"\ subsection \Fact Tactic\ theory Unify_Fact_Tactic imports Unify_Resolve_Tactics begin paragraph \Summary\ text \Fact tactic with adjustable unifier.\ ML_file\unify_fact_base.ML\ ML_file\unify_fact.ML\ ML\ @{functor_instance struct_name = Standard_Unify_Fact and functor_name = Unify_Fact and id = \""\ and more_args = \val init_args = { - normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_first_comb_higher_unify, - unifier = SOME Standard_Mixed_Unification.first_higherp_first_comb_higher_unify + normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify, + unifier = SOME Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify }\} \ local_setup \Standard_Unify_Fact.setup_attribute NONE\ local_setup \Standard_Unify_Fact.setup_method NONE\ paragraph \Examples\ experiment begin lemma assumes h: "\x y. PROP P x y" shows "PROP P x y" by (ufact h) lemma assumes "\P y. PROP P y x" shows "PROP P x" by (ufact assms where unifier = Higher_Order_Unification.unify) \\the line below is equivalent\ (* using [[ufact unifier = Higher_Order_Unification.unify]] by (ufact assms) *) lemma assumes "\x y. PROP A x \ PROP B x \ PROP P x" shows "\x y. PROP A x \ PROP B x \ PROP P x" using assms by ufact end end diff --git a/thys/ML_Unification/Unification_Tactics/Resolution/Unify_Resolve_Tactics.thy b/thys/ML_Unification/Unification_Tactics/Resolution/Unify_Resolve_Tactics.thy --- a/thys/ML_Unification/Unification_Tactics/Resolution/Unify_Resolve_Tactics.thy +++ b/thys/ML_Unification/Unification_Tactics/Resolution/Unify_Resolve_Tactics.thy @@ -1,92 +1,91 @@ \<^marker>\creator "Kevin Kappelmann"\ subsection \Resolution Tactics\ theory Unify_Resolve_Tactics imports Unify_Assumption_Tactic ML_Method_Utils begin paragraph \Summary\ text \Resolution tactics and methods with adjustable unifier.\ ML_file\unify_resolve_base.ML\ ML_file\unify_resolve.ML\ ML\ @{functor_instance struct_name = Standard_Unify_Resolve and functor_name = Unify_Resolve and id = \""\ and more_args = \val init_args = { - normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_first_comb_higher_unify, - unifier = SOME Standard_Mixed_Unification.first_higherp_first_comb_higher_unify, + normalisers = SOME Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify, + unifier = SOME Standard_Mixed_Unification.first_higherp_decomp_comb_higher_unify, mode = SOME (Unify_Resolve_Args.PM.key Unify_Resolve_Args.PM.any), chained = SOME (Unify_Resolve_Args.PCM.key Unify_Resolve_Args.PCM.resolve) }\} \ local_setup \Standard_Unify_Resolve.setup_attribute NONE\ local_setup \Standard_Unify_Resolve.setup_method NONE\ - paragraph \Examples\ experiment begin lemma assumes h: "\x. PROP D x \ PROP C x" shows "\x. PROP A x \ PROP B x \ PROP C x" apply (urule h) \\the line below is equivalent\ (* apply (rule h) *) oops lemma assumes h: "PROP C x" shows "PROP C x" by (urule h where unifier = First_Order_Unification.unify) \\the line below is equivalent\ (* using [[urule unifier = First_Order_Unification.unify]] by (urule h) *) lemma assumes h: "\x. PROP A x \ PROP D x" shows "\x. PROP A x \ PROP B x \ PROP C x" \\use (r,e,d,f) to specify the resolution mode (resolution, elim, dest, forward)\ apply (urule (d) h) \\the line below is equivalent\ (* apply (drule h) *) oops text\You can specify how chained facts should be used. By default, @{method urule} works like @{method rule}: it uses chained facts to resolve against the premises of the passed rules.\ lemma assumes h1: "\x. (PROP F x \ PROP E x) \ PROP C x" and h2: "\x. PROP F x \ PROP E x" shows "\x. PROP A x \ PROP B x \ PROP C x" \\Compare all of the following calls:\ (* apply (rule h1) *) (* apply (urule h1) *) (* using h2 apply (rule h1) *) (* using h2 apply (urule h1) *) using h2 apply (urule h1 where chained = fact) (* using h2 apply (urule h1 where chained = insert) *) done text\You can specify whether any or every rule must resolve against the goal:\ lemma assumes h1: "\x y. PROP C y \ PROP D x \ PROP C x" and h2: "\x y. PROP C x \ PROP D x" and h3: "\x y. PROP C x" shows "\x. PROP A x \ PROP B x \ PROP C x" using h3 apply (urule h1 h2 where mode = every) (* using h3 apply (urule h1 h2) *) done lemma assumes h1: "\x y. PROP C y \ PROP A x \ PROP C x" and h2: "\x y. PROP C x \ PROP B x \ PROP D x" and h3: "\x y. PROP C x" shows "\x. PROP A x \ PROP B x \ PROP C x" using h3 apply (urule (d) h1 h2 where mode = every) oops end end diff --git a/thys/ML_Unification/Unifiers/ML_Unifiers.thy b/thys/ML_Unification/Unifiers/ML_Unifiers.thy --- a/thys/ML_Unification/Unifiers/ML_Unifiers.thy +++ b/thys/ML_Unification/Unifiers/ML_Unifiers.thy @@ -1,63 +1,73 @@ \<^marker>\creator "Kevin Kappelmann"\ section \ML Unifiers\ theory ML_Unifiers imports ML_Unification_Base ML_Functor_Instances ML_Priorities Simps_To begin paragraph \Summary\ text \Unification modulo equations and combinators for unifiers.\ paragraph \Combinators\ ML_file\unification_combinator.ML\ ML_file\unification_combine.ML\ ML\ @{functor_instance struct_name = Standard_Unification_Combine and functor_name = Unification_Combine and id = \""\} \ local_setup \Standard_Unification_Combine.setup_attribute NONE\ paragraph \Standard Unifiers\ ML_file\higher_order_unification.ML\ ML_file\higher_order_pattern_unification.ML\ ML_file\first_order_unification.ML\ +subparagraph \Derived Unifiers\ + +ML_file\higher_order_pattern_decomp_unification.ML\ +ML_file\var_higher_order_pattern_unification.ML\ + paragraph \Unification via Tactics\ ML_file\tactic_unification.ML\ subparagraph \Unification via Simplification\ ML_file\simplifier_unification.ML\ - paragraph \Mixture of Unifiers\ -ML_file\higher_ordern_pattern_first_decomp_unification.ML\ - ML_file\mixed_unification.ML\ ML\ @{functor_instance struct_name = Standard_Mixed_Unification and functor_name = Mixed_Unification and id = \""\ and more_args = \structure UC = Standard_Unification_Combine\} \ declare [[ucombine add = \Standard_Unification_Combine.eunif_data + (Var_Higher_Order_Pattern_Unification.e_unify Unification_Combinator.fail_unify + |> Unification_Combinator.norm_unifier + (#norm_term Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify) + |> K) + (Standard_Unification_Combine.metadata \<^binding>\var_hop_unif\ Prio.HIGH)\]] + +declare [[ucombine add = \Standard_Unification_Combine.eunif_data (Simplifier_Unification.simp_unify |> Unification_Combinator.norm_closed_unifier - (#norm_term Standard_Mixed_Unification.norms_first_higherp_first_comb_higher_unify) + (#norm_term Standard_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify) |> Unification_Combinator.unifier_from_closed_unifier |> K) (Standard_Unification_Combine.default_metadata \<^binding>\simp_unif\)\]] + end diff --git a/thys/ML_Unification/Unifiers/first_order_unification.ML b/thys/ML_Unification/Unifiers/first_order_unification.ML --- a/thys/ML_Unification/Unifiers/first_order_unification.ML +++ b/thys/ML_Unification/Unifiers/first_order_unification.ML @@ -1,235 +1,235 @@ (* Title: ML_Unification/first_order_unification.ML Author: Kevin Kappelmann, Paul Bachmann First-order E-unification. *) signature FIRST_ORDER_UNIFICATION = sig include HAS_LOGGER (* e-matching *) val e_match : Unification_Base.type_matcher -> Unification_Base.e_matcher val match : Unification_Base.matcher val norms_match : Unification_Base.normalisers (* e-unification *) val e_unify : Unification_Base.type_unifier -> Unification_Base.e_unifier val unify : Unification_Base.unifier val norms_unify : Unification_Base.normalisers end structure First_Order_Unification : FIRST_ORDER_UNIFICATION = struct val logger = Logger.setup_new_logger Unification_Base.logger "First_Order_Unification" (* shared utils *) structure Util = Unification_Util structure Norm = Envir_Normalisation exception FALLBACK (*check if sequence is empty or raise FALLBACK exception*) fun seq_try sq = General_Util.seq_try FALLBACK sq (* e-matching *) val norms_match = Util.eta_short_norms_match (*Note: by E-matching we mean "matching modulo equalities" in the general sense, i.e. when matching p \? t, t may contain variables.*) fun e_match match_types match_theory binders ctxt pt env = let val norm_pt = apfst o (#norm_term norms_match) fun rigid_rigid ctxt p n env = (*normalise the types in rigid-rigid cases*) Util.rigid_rigid Norm.norm_term_types_match match_types ctxt p n env |> seq_try handle Unification_Base.UNIF => Seq.empty (*types do not match*) (*standard first-order matcher that calls match_theory on failure; generated theorem is already normalised wrt. the resulting environment*) fun match binders ctxt (pt as (p, t)) (env as Envir.Envir {tenv, tyenv,...}) = (case pt of (Var (x, Tx), _) => (case Envir.lookup1 tenv (x, Norm.norm_type_match tyenv Tx) of NONE => if Term.is_open t then (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "Failed to match (open term) ", Util.pretty_unif_problem ctxt (norm_pt env pt) ] |> Pretty.string_of); (*directly return empty sequence because the theory unifier cannot do anything meaningful at this point*) raise FALLBACK) else let val Tt = fastype_of1 (Binders.binder_types binders, t) in ((match_types ctxt (Tx, Tt) env, Unification_Base.reflexive_term ctxt t) (*insert new substitution x \ t*) |>> Envir.update ((x, Tt), t) |> Seq.single) handle Unification_Base.UNIF => Seq.empty (*types do not match*) end | SOME p' => if Envir.aeconv (apply2 Envir.beta_norm (p', t)) then Seq.single (env, Unification_Base.reflexive_term ctxt t) else raise FALLBACK) | (Abs (np, Tp, tp), Abs (nt, Tt, tt)) => ((let val name = if np = "" then nt else np in match_types ctxt (Tp, Tt) env |> Util.abstract_abstract (K I) match binders ctxt name Tt (tp, tt) |> seq_try end) handle Unification_Base.UNIF => Seq.empty) (*types do not match*) (*eta-expand on the fly*) | (Abs (np, Tp, tp), _) => ((let val Ttarg = fastype_of1 (Binders.binder_types binders, t) |> Term.dest_funT |> fst in match_types ctxt (Tp, Ttarg) env |> Util.abstract_abstract (K I) match binders ctxt np Ttarg (tp, incr_boundvars 1 t $ Bound 0) |> seq_try end) handle TYPE _ => (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "First-order matching failed. Term is not of function type ", Util.pretty_unif_problem ctxt (norm_pt env pt) ] |> Pretty.string_of); Seq.empty) | Unification_Base.UNIF => Seq.empty) (*types do not match*) | (_, Abs (nt, Tt, tt)) => ((let val Tp = Envir.fastype env (Binders.binder_types binders) p in match_types ctxt (Tp, fastype_of1 (Binders.binder_types binders, t)) env |> Util.abstract_abstract (K I) match binders ctxt nt Tt (incr_boundvars 1 p $ Bound 0, tt) |> seq_try end) handle Unification_Base.UNIF => Seq.empty) (*types do not match*) | (Bound i, Bound j) => Util.bound_bound binders ctxt (i, j) |> Seq.map (pair env) | (Free _, Free g) => rigid_rigid ctxt p g env | (Const _, Const d) => rigid_rigid ctxt p d env | (f $ x, g $ y) => (*Note: types of recursive theorems are already normalised ==> we have to pass the identity type normaliser*) Util.comb_comb (K o K I) (match binders) ctxt (f, x) (g, y) env |> seq_try | _ => raise FALLBACK) handle FALLBACK => - (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ - Pretty.str "First-order matching failed. Calling theory matcher for ", - Util.pretty_unif_problem ctxt (norm_pt env pt) - ] |> Pretty.string_of); + (@{log Logger.DEBUG} ctxt (fn _ => Pretty.breaks [ + Pretty.str "First-order matching failed.", + Util.pretty_call_theory_match ctxt (norm_pt env pt) + ] |> Pretty.block |> Pretty.string_of); match_theory binders ctxt pt env) in (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "First-order matching ", Util.pretty_unif_problem ctxt (norm_pt env pt) ] |> Pretty.string_of); match binders ctxt pt env) end (*standard first-order matching*) val match = e_match Util.match_types Unification_Combinator.fail_match (* e-unification *) (*occurs check*) fun occurs v (Var (x, _)) = x = v | occurs v (s $ t) = occurs v s orelse occurs v t | occurs v (Abs (_, _, t)) = occurs v t | occurs _ _ = false val norms_unify = Util.eta_short_norms_unif fun e_unify unify_types unify_theory binders ctxt st env = let val norm_st = apply2 o (#norm_term norms_unify) fun rigid_rigid ctxt t n env = (*we do not have to normalise types in rigid-rigid cases*) Util.rigid_rigid (K I) unify_types ctxt t n env |> seq_try handle Unification_Base.UNIF => Seq.empty (*types do not unify*) (*standard first-order unifier that calls unify_theory on failure*) fun unif binders ctxt (st as (s, t)) env = (case st of (Var (x, Tx), _) => let val unif' = unif binders ctxt in (unif' (Envir.norm_term_same env s, t) env handle Same.SAME => (unif' (s, Envir.norm_term_same env t) env handle Same.SAME => if Term.is_open t then (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "Failed to unify (open term) ", Util.pretty_unif_problem ctxt (norm_st env st) ] |> Pretty.string_of); raise FALLBACK) else let val vars_eq = is_Var t andalso x = fst (dest_Var t) fun update_env env = (*unifying x=x ==> no new term substitution necessary*) if vars_eq then env (*insert new substitution x \ t*) else Envir.vupdate ((x, Tx), t) env in if not vars_eq andalso occurs x t then (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "Failed to unify (occurs check) ", Util.pretty_unif_problem ctxt (norm_st env st) ] |> Pretty.string_of); raise FALLBACK) else ((unify_types ctxt (Tx, Envir.fastype env (Binders.binder_types binders) t) env, Unification_Base.reflexive_term ctxt s) |>> update_env |> Seq.single) handle Unification_Base.UNIF => Seq.empty (*types do not unify*) end)) end | (_, Var _) => unif binders ctxt (t, s) env |> Seq.map (apsnd Unification_Base.symmetric) | (Abs (ns, Ts, ts), Abs (nt, Tt, tt)) => ((let val name = if ns = "" then nt else ns in unify_types ctxt (Ts, Tt) env |> Util.abstract_abstract Norm.norm_term_types_unif unif binders ctxt name Ts (ts, tt) |> seq_try end) handle Unification_Base.UNIF => Seq.empty) (*types do not unify*) (*eta-expand on the fly*) | (Abs (ns, Ts, ts), _) => ((let val Tp = apply2 (Envir.fastype env (Binders.binder_types binders)) (s, t) in unify_types ctxt Tp env |> Util.abstract_abstract Norm.norm_term_types_unif unif binders ctxt ns Ts (ts, incr_boundvars 1 t $ Bound 0) |> seq_try end) handle Unification_Base.UNIF => Seq.empty) (*types do not unify*) | (_, Abs _) => unif binders ctxt (t, s) env |> Seq.map (apsnd Unification_Base.symmetric) | (Bound i, Bound j) => Util.bound_bound binders ctxt (i, j) |> Seq.map (pair env) | (Free _, Free g) => rigid_rigid ctxt s g env | (Const _, Const d) => rigid_rigid ctxt s d env (*we have to normalise types in comb cases*) | (f $ x, g $ y) => Util.comb_comb Norm.norm_thm_types_unif (unif binders) ctxt (f, x) (g, y) env |> seq_try | _ => raise FALLBACK) handle FALLBACK => - (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ - Pretty.str "First-order unification failed. Calling theory unifier for ", - Util.pretty_unif_problem ctxt (norm_st env st) - ] |> Pretty.string_of); + (@{log Logger.DEBUG} ctxt (fn _ => Pretty.breaks [ + Pretty.str "First-order unification failed.", + Util.pretty_call_theory_unif ctxt (norm_st env st) + ] |> Pretty.block |> Pretty.string_of); unify_theory binders ctxt st env) in (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "First-order unifying ", Util.pretty_unif_problem ctxt (norm_st env st) ] |> Pretty.string_of); unif binders ctxt st env) end (*standard first-order unification*) val unify = e_unify Util.unify_types Unification_Combinator.fail_unify end diff --git a/thys/ML_Unification/Unifiers/higher_order_pattern_decomp_unification.ML b/thys/ML_Unification/Unifiers/higher_order_pattern_decomp_unification.ML new file mode 100644 --- /dev/null +++ b/thys/ML_Unification/Unifiers/higher_order_pattern_decomp_unification.ML @@ -0,0 +1,141 @@ +(* Title: ML_Unification/higher_order_pattern_decomp_unification.ML + Author: Kevin Kappelmann + +Tries to decompose terms that are outside the higher-order pattern fragment +into a higher-order pattern prefix and a list of remaining arguments. + +Example: Let 0, 1 be bound variables and f, g, c be constants. +The unification problem ?x 0 1 (?y c 0) \\<^sup>? f (g c 0) is outside the HO-pattern +fragment, but it can be decomposed into ?x 0 1 \\<^sup>? f and (?y c 0) \\<^sup>? (g c 0). +The latter, in turn, can be decomposed into ?y \\<^sup>? g and c \\<^sup>? c and 0 \\<^sup>? 0. +*) +signature HIGHER_ORDER_PATTERN_DECOMP_UNIFICATION = +sig + include HAS_LOGGER + + val e_match : Unification_Base.matcher -> Unification_Base.e_matcher + val e_unify : Unification_Base.unifier -> Unification_Base.e_unifier +end + +structure Higher_Order_Pattern_Decomp_Unification : + HIGHER_ORDER_PATTERN_DECOMP_UNIFICATION = +struct + +val logger = Logger.setup_new_logger Unification_Base.logger + "Higher_Order_Pattern_Decomp_Unification" + +structure UUtil = Unification_Util +structure HOP = Higher_Order_Pattern_Unification +structure UC = Unification_Combinator + +exception FALLBACK of Pretty.T + +(*check if sequence is empty or raise FALLBACK exception*) +fun seq_try msg sq = General_Util.seq_try (FALLBACK msg) sq + +(*compute pattern prefixes*) +fun bounds_prefix bounds [] = (rev bounds, []) + | bounds_prefix bounds (t :: ts) = + if is_Bound t andalso not (member (op =) bounds t) + then bounds_prefix (t :: bounds) ts + else (rev bounds, t :: ts) +val bounds_prefix = bounds_prefix [] + +datatype ('a, 'b) either = Left of 'a | Right of 'b + +fun bounds_prefix2 (bounds1, _) ([], _) = Left (rev bounds1, []) + | bounds_prefix2 (_, bounds2) (_, []) = Right (rev bounds2, []) + | bounds_prefix2 (bounds1, bounds2) (s :: ss, t :: ts) = + if is_Bound s andalso not (member (op =) bounds1 s) + then if is_Bound t andalso not (member (op =) bounds2 t) + then bounds_prefix2 (s :: bounds1, t :: bounds2) (ss, ts) + else Right (rev bounds2, t :: ts) + else Left (rev bounds1, s :: ss) +val bounds_prefix2 = bounds_prefix2 ([], []) + +fun mk_decomp _ (_, []) = NONE (*no decomposition took place*) + | mk_decomp h (args, rem) = SOME (list_comb (h, args), rem) + +fun mk_bounds_decomp h args = bounds_prefix args |> mk_decomp h + +fun pattern_prefix_match p = case strip_comb p of + (v as Var _, args) => mk_bounds_decomp v args + | _ => NONE + +fun pattern_prefix_unif tp = case apply2 strip_comb tp of + ((vl as Var _, argsl), (vr as Var _, argsr)) => (case bounds_prefix2 (argsl, argsr) of + Left res => mk_decomp vl res |> Option.map Left + | Right res => mk_decomp vr res |> Option.map Right) + | ((v as Var _, args), _) => mk_bounds_decomp v args |> Option.map Left + | (_, (v as Var _, args)) => mk_bounds_decomp v args |> Option.map Right + | _ => NONE + +fun mk_decomp_other ss t = + let + val (th, ts) = strip_comb t + val n = length ts - length ss + in if n < 0 then NONE else chop n ts |> mk_decomp th end + +fun decompose_msg ctxt tp = Pretty.block [ + Pretty.str "Decomposing ", + UUtil.pretty_unif_problem ctxt tp, + Pretty.str " into higher-order pattern prefix and list of remaining arguments." + ] |> Pretty.string_of + +fun decomposed_msg ctxt (ph, th) (ps, ts) = Pretty.block [ + Pretty.str "Decomposition result ", + map (UUtil.pretty_unif_problem ctxt) ((ph, th) :: (ps ~~ ts)) + |> Pretty.separate "," |> Pretty.block + ] |> Pretty.string_of + +val failed_decompose_msg = Pretty.str "Decomposition failed." + +fun e_match match_pattern match_theory binders ctxt (pt as (p, t)) env = + let val failed_sub_patterns_msg = Pretty.str "Matching of sub-patterns failed." + in + (@{log Logger.DEBUG} ctxt (fn _ => decompose_msg ctxt pt); + case pattern_prefix_match p of + SOME (ph, ps) => (case mk_decomp_other ps t of + SOME (th, ts) => + (@{log Logger.TRACE} ctxt (fn _ => decomposed_msg ctxt (ph, th) (ps, ts)); + UUtil.strip_comb_strip_comb (K o K I) match_pattern + binders ctxt (ph, th) (ps, ts) env + |> seq_try failed_sub_patterns_msg) + | NONE => raise FALLBACK failed_decompose_msg) + | NONE => raise FALLBACK failed_decompose_msg) + handle FALLBACK msg => (@{log Logger.DEBUG} ctxt (fn _ => Pretty.breaks [ + msg, + UUtil.pretty_call_theory_match ctxt pt + ] |> Pretty.block |> Pretty.string_of); + match_theory binders ctxt pt env) + end + +fun e_unify unif_pattern unif_theory binders ctxt (tp as (s, t)) env = + let + val unif_patterns = + UUtil.strip_comb_strip_comb Envir_Normalisation.norm_thm_types_unif unif_pattern + val failed_sub_patterns_msg = Pretty.str "Unification of sub-patterns failed." + in + (@{log Logger.DEBUG} ctxt (fn _ => decompose_msg ctxt tp); + case pattern_prefix_unif tp of + SOME (Left (sh, ss)) => (case mk_decomp_other ss t of + SOME (th, ts) => + (@{log Logger.TRACE} ctxt (fn _ => decomposed_msg ctxt (sh, th) (ss, ts)); + unif_patterns binders ctxt (sh, th) (ss, ts) env + |> seq_try failed_sub_patterns_msg) + | NONE => raise FALLBACK failed_decompose_msg) + | SOME (Right (th, ts)) => (case mk_decomp_other ts s of + SOME (sh, ss) => + (@{log Logger.TRACE} ctxt (fn _ => decomposed_msg ctxt (sh, th) (ss, ts)); + unif_patterns binders ctxt (sh, th) (ss, ts) env + |> seq_try failed_sub_patterns_msg) + | NONE => raise FALLBACK failed_decompose_msg) + | NONE => raise FALLBACK failed_decompose_msg) + handle FALLBACK msg => (@{log Logger.DEBUG} ctxt (fn _ => Pretty.breaks [ + msg, + UUtil.pretty_call_theory_unif ctxt tp + ] |> Pretty.block |> Pretty.string_of); + unif_theory binders ctxt tp env) + end + +end diff --git a/thys/ML_Unification/Unifiers/higher_order_pattern_unification.ML b/thys/ML_Unification/Unifiers/higher_order_pattern_unification.ML --- a/thys/ML_Unification/Unifiers/higher_order_pattern_unification.ML +++ b/thys/ML_Unification/Unifiers/higher_order_pattern_unification.ML @@ -1,482 +1,476 @@ (* Title: ML_Unification/higher_order_pattern_unification.ML Author: Tobias Nipkow, Christine Heinzelmann, Stefan Berghofer, and Kevin Kappelmann TU Muenchen Higher-Order Patterns due to Tobias Nipkow. E-Unification and theorem construction due to Kevin Kappelmann. See also: Tobias Nipkow. Functional Unification of Higher-Order Patterns. In Proceedings of the 8th IEEE Symposium Logic in Computer Science, 1993. TODO: optimize red by special-casing it *) signature HIGHER_ORDER_PATTERN_UNIFICATION = sig include HAS_LOGGER (* e-matching *) val e_match : Unification_Base.type_matcher -> Unification_Base.matcher -> Unification_Base.e_matcher val match : Unification_Base.matcher val norms_match : Unification_Base.normalisers (* e-unification *) val e_unify : Unification_Base.type_unifier -> Unification_Base.unifier -> Unification_Base.e_unifier val unify : Unification_Base.unifier val norms_unify : Unification_Base.normalisers end structure Higher_Order_Pattern_Unification : HIGHER_ORDER_PATTERN_UNIFICATION = struct val logger = Logger.setup_new_logger Unification_Base.logger "Higher_Order_Pattern_Unification" (* shared utils *) structure Util = Unification_Util structure Norm = Envir_Normalisation exception FALLBACK (*check if sequence is empty or raise FALLBACK exception*) fun seq_try sq = General_Util.seq_try FALLBACK sq (*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*) fun downto0 ([], n) = n = ~1 | downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1) fun mkabs (binders, is, t) = let fun abstract i acc = let val ((x, T), _) = nth binders i in Abs (x, T, acc) end in fold_rev abstract is t end exception IDX fun idx [] _ = raise IDX | idx (i :: is) j = if i = j then length is else idx is j fun ints_of bs = (*collects arguments and checks if they are all distinct, bound variables*) let fun dest_check (Bound i) acc = if member (op =) acc i then raise Unification_Base.PATTERN else i :: acc | dest_check _ _ = raise Unification_Base.PATTERN in fold_rev dest_check bs [] end fun app (s, []) = s | app (s, (i :: is)) = app (s $ Bound i, is) (* matching *) fun mapbnd f = let fun mpb d (Bound i) = if i < d then Bound i else Bound (f (i - d) + d) | mpb d (Abs (s, T, t)) = Abs (s, T, mpb (d + 1) t) | mpb d (u1 $ u2) = (mpb d u1) $ (mpb d u2) | mpb _ atom = atom in mpb 0 end fun red (Abs (_, _, s)) (i :: is) js = red s is (i :: js) | red t [] [] = t | red t is jn = app (mapbnd (nth jn) t, is) exception OPEN_TERM fun match_bind (tenv, binders, ixn, T, is, t) = let val js = loose_bnos t in if null is then if null js then Vartab.update_new (ixn, (T, t)) tenv else raise OPEN_TERM else if subset (op =) (js, is) then let val t' = if downto0 (is, length binders - 1) then t else mapbnd (idx is) t in Vartab.update_new (ixn, (T, mkabs (binders, is, t'))) tenv end else raise OPEN_TERM end (** higher-order pattern E-unification **) val norms_match = Util.beta_eta_short_norms_match fun e_match match_types match_theory_pattern match_theory_fail binders ctxt (pt as (p, t)) env = let val norm_pt = apfst o (#norm_term norms_match) fun rigid_rigid ctxt p n env = (*normalise the types in rigid-rigid cases*) Util.rigid_rigid Norm.norm_term_types_match match_types ctxt p n env |> seq_try handle Unification_Base.UNIF => Seq.empty (*types do not match*) (*generated theorem is already normalised wrt. the resulting environment*) fun match binders ctxt (pt as (p, t)) (env as Envir.Envir {maxidx, tenv, tyenv}) = let (*call match_theory on failure*) fun handle_failure match_theory failure_msg = (@{log Logger.DEBUG} ctxt (fn _ => Pretty.breaks [ failure_msg (), - Pretty.block [ - Pretty.str "Calling theory matcher for ", - Util.pretty_unif_problem ctxt (norm_pt env pt) - ] + Util.pretty_call_theory_match ctxt (norm_pt env pt) ] |> Pretty.block |> Pretty.string_of); match_theory binders ctxt pt env) in (case pt of (Abs (np, _, tp), Abs (nt, Tt, tt)) => let val name = if np = "" then nt else np in Util.abstract_abstract (K I) match binders ctxt name Tt (tp, tt) env |> seq_try end (*eta-expand on the fly*) | (Abs (np, Tp, tp), _) => let val Tp' = Envir.subst_type tyenv Tp in Util.abstract_abstract (K I) match binders ctxt np Tp' (tp, incr_boundvars 1 t $ Bound 0) env |> seq_try end | (_, Abs (nt, Tt, tt)) => Util.abstract_abstract (K I) match binders ctxt nt Tt (incr_boundvars 1 p $ Bound 0, tt) env |> seq_try | (Bound i, Bound j) => Util.bound_bound binders ctxt (i, j) |> Seq.map (pair env) | (Free _, Free g) => rigid_rigid ctxt p g env | (Const _, Const d) => rigid_rigid ctxt p d env | _ => case strip_comb p of (Var (x, T), ps) => let val is = ints_of ps val T' = Norm.norm_type_match tyenv T in case Envir.lookup1 tenv (x, T') of NONE => ((let val tenv' = match_bind (tenv, binders, x, T', is, t) val env' = Envir.Envir {maxidx=maxidx, tenv=tenv', tyenv=tyenv} val t' = Binders.replace_binders binders t in Seq.single (env', Unification_Base.reflexive_term ctxt t') end) handle OPEN_TERM => (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "Failed to unify (open term) ", Util.pretty_unif_problem ctxt (norm_pt env pt) ] |> Pretty.string_of); Seq.empty)) | SOME ph' => if Envir.aeconv (red ph' is [], t) then Seq.single (env, Unification_Base.reflexive_term ctxt (Binders.replace_binders binders t)) else raise FALLBACK end | (ph, ps) => let val (th, ts) = strip_comb t in case (ph, th) of (Abs _, _) => raise Unification_Base.PATTERN | (_, Abs _) => raise Unification_Base.PATTERN | _ => if null ps orelse null ts then raise FALLBACK else (*Note: types of theorems are already normalised ==> we pass the identity type normaliser*) Util.strip_comb_strip_comb (K o K I) match binders ctxt (ph, th) (ps, ts) env |> seq_try end) handle FALLBACK => handle_failure match_theory_fail (fn _ => Pretty.str "Higher-order pattern matching failed.") | Unification_Base.PATTERN => handle_failure match_theory_pattern (fn _ => Pretty.str "Terms not in Pattern fragment.") end val binder_types = Binders.binder_types binders in (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "Higher-order pattern matching ", Util.pretty_unif_problem ctxt (norm_pt env pt) ] |> Pretty.string_of); match_types ctxt (Envir.fastype env binder_types p, fastype_of1 (binder_types, t)) env |> match binders ctxt pt) handle Unification_Base.UNIF => Seq.empty (*types do not match*) end (*standard higher-order pattern matching*) val match = e_match Util.match_types Unification_Combinator.fail_match Unification_Combinator.fail_match (*unification*) fun string_of_term ctxt env binders t = (map (Free o fst) binders, t) |> subst_bounds |> Norm.norm_term_unif env |> Syntax.string_of_term ctxt fun bname binders = fst o fst o nth binders fun bnames binders is = map (bname binders) is |> space_implode " " fun proj_fail ctxt (env, binders, F, _, is, t) reason = @{log Logger.DEBUG} ctxt (fn _ => let val f = Term.string_of_vname F val xs = bnames binders is val u = string_of_term ctxt env binders t in cat_lines [ "Cannot unify variable " ^ f ^ " (depending on bound variables [" ^ xs ^ "])", "with term " ^ u, reason () ] end) fun proj_fail_unif ctxt (params as (_, binders, _, _, is, t)) = let fun reason () = let val ys = bnames binders (subtract (op =) is (loose_bnos t)) in "Term contains additional bound variable(s) " ^ ys end in proj_fail ctxt params reason end fun proj_fail_type_app ctxt (params as (env, binders, _, _, _, _)) var_app = let fun reason () = let val var_app = string_of_term ctxt env binders var_app in "Projection " ^ var_app ^ " is not well-typed." end in proj_fail ctxt params reason end fun ocheck_fail ctxt (F, t, binders, env) = @{log Logger.DEBUG} ctxt (fn _ => cat_lines [ "Variable " ^ Term.string_of_vname F ^ " occurs in term", string_of_term ctxt env binders t, "Cannot unify!" ]) fun occurs (F, t, env) = let fun occ (Var (G, T)) = (case Envir.lookup env (G, T) of SOME t => occ t | NONE => F = G) | occ (t1 $ t2) = occ t1 orelse occ t2 | occ (Abs (_, _, t)) = occ t | occ _ = false in occ t end fun ints_of' env ts = ints_of (map (Envir.head_norm env) ts) (*split_type ([T1,....,Tn]---> T) n = ([Tn,...,T1], T)*) fun split_type t n = let fun split (T, 0, Ts) = (Ts, T) | split (Type ("fun", [T1, T2]), n, Ts) = split (T2, n - 1, T1 :: Ts) | split _ = raise Fail "split_type" in split (t, n, []) end fun type_of_G (Envir.Envir {tyenv,...}) (T, n, is) = let val (Ts, U) = split_type (Norm.norm_type_unif tyenv T) n in map (nth Ts) is ---> U end fun mk_hnf (binders, is, G, js) = mkabs (binders, is, app (G, js)) fun mk_new_hnf (env, binders, is, F as (a, _), T, js) = let val (env', G) = Envir.genvar a (env, type_of_G env (T, length is, js)) in Envir.update ((F, T), mk_hnf (binders, is, G, js)) env' end (*mk_proj_list is = [ |is| - k - 1 | 0 <= k < |is| and is[k] >= 0 ]*) fun mk_proj_list is = let fun mk (SOME _) (acc, j) = (j :: acc, j + 1) | mk NONE (acc, j) = (acc, j + 1) in fold_rev mk is ([], 0) |> fst end fun proj ctxt (s, env, binders, is) = let fun trans d i = if i < d then i else idx is (i - d) + d fun pr (s, env, d, binders) = (case Envir.head_norm env s of Abs (a, T, t) => let val (binder, _) = Binders.fix_binder (a, T) ctxt val (t', env') = pr (t, env, d + 1, binder :: binders) in (Abs (a, T, t'), env') end | t => (case strip_comb t of (c as Const _, ts) => let val (ts', env') = prs (ts, env, d, binders) in (list_comb (c, ts'), env') end | (f as Free _, ts) => let val (ts', env') = prs (ts, env, d, binders) in (list_comb (f, ts'), env') end | (Bound i, ts) => let val j = trans d i val (ts', env') = prs (ts, env, d, binders) in (list_comb (Bound j, ts'), env') end | (Var (F as (a, _), Fty), ts) => let val js = ints_of' env ts val js' = map (try (trans d)) js val ks = mk_proj_list js' val ls = map_filter I js' val Hty = type_of_G env (Fty, length js, ks) val (env', H) = Envir.genvar a (env, Hty) val env'' = Envir.update ((F, Fty), mk_hnf (binders, js, H, ks)) env' in (app (H, ls), env'') end | _ => raise Unification_Base.PATTERN)) and prs (s :: ss, env, d, binders) = let val (s', env1) = pr (s, env, d, binders) val (ss', env2) = prs (ss, env1, d, binders) in (s' :: ss', env2) end | prs ([], env, _, _) = ([], env) in if downto0 (is, length binders - 1) then (s, env) else pr (s, env, 0, binders) end (*mk_ff_list (is, js) = [ |is| - k - 1 | 0 <= k < |is| and is[k] = js[k] ]*) fun mk_ff_list (is,js) = let fun mk ([], [], _) = [] | mk (i :: is, j :: js, k) = if i = j then k :: mk (is, js, k - 1) else mk (is, js, k - 1) | mk _ = raise Fail "mk_ff_list" in mk (is, js, length is - 1) end; fun app_free (Envir.Envir {tyenv,...}) binders n T is = let val norm_type = Norm.norm_type_unif tyenv in list_comb (Var (n, norm_type T), map (map_types norm_type o Binders.nth_binder_data binders) is) end fun flexflex1 unify_types ctxt (env, binders, F, Fty, Fty', is, js) = let val env' = unify_types ctxt (Fty, Fty') env val thm = app_free env binders F Fty is |> Unification_Base.reflexive_term ctxt in if is = js then (env', thm) else let val ks = mk_ff_list (is, js) val env'' = mk_new_hnf (env', binders, is, F, Fty, ks) in (env'', thm) end end fun flexflex2 unify_types ctxt (env, binders, F, Fty, is, G, Gty, js) = let val var_app = app_free env binders F Fty is val binder_types = Binders.binder_types binders val env' = unify_types ctxt (apply2 (Envir.fastype env binder_types) (var_app, app (Var (G, Gty), js))) env val thm = Unification_Base.reflexive_term ctxt var_app fun ff (F, Fty, is, G as (a, _), Gty, js) = if subset (op =) (js, is) then let val t = mkabs (binders, is, app (Var (G, Gty), map (idx is) js)) val env'' = Envir.update ((F, Fty), t) env' in (env'', thm) end else let val ks = inter (op =) js is val Hty = type_of_G env' (Fty, length is, map (idx is) ks) val (env'', H) = Envir.genvar a (env', Hty) fun lam is = mkabs (binders, is, app (H, map (idx is) ks)) val env''' = Envir.update ((F, Fty), lam is) env'' |> Envir.update ((G, Gty), lam js) in (env''', thm) end in if is_less (Term_Ord.indexname_ord (G, F)) then ff (F, Fty, is, G, Gty, js) else ff (G, Gty, js, F, Fty, is) end fun flexrigid unify_types ctxt (params as (env, binders, F, Fty, is, t)) = if occurs (F, t, env) then (ocheck_fail ctxt (F, t, binders, env); raise FALLBACK) else let val var_app = app_free env binders F Fty is in let val binder_types = Binders.binder_types binders val env' = unify_types ctxt (apply2 (Envir.fastype env binder_types) (var_app, t)) env val (u, env'') = proj ctxt (t, env', binders, is) val env''' = Envir.update ((F, Fty), mkabs (binders, is, u)) env'' val thm = Unification_Base.reflexive_term ctxt var_app in (env''', thm) end handle IDX => (proj_fail_unif ctxt params; raise OPEN_TERM) | TYPE _ => (proj_fail_type_app ctxt params var_app; raise Unification_Base.UNIF) end (** higher-order pattern E-unification **) val norms_unify = Util.beta_eta_short_norms_unif fun e_unify unify_types unify_theory_pattern unify_theory_fail binders ctxt st env = let fun unif binders ctxt st env = let val (st' as (s', t')) = apply2 (Envir.head_norm env) st fun rigid_rigid ctxt t n env = (*we do not normalise types in base cases*) Util.rigid_rigid (K I) unify_types ctxt t n env |> seq_try handle Unification_Base.UNIF => Seq.empty (*types do not match*) (*call unify_theory on failure*) fun handle_failure unify_theory failure_msg = (@{log Logger.DEBUG} ctxt (fn _ => Pretty.breaks [ failure_msg (), - Pretty.block [ - Pretty.str "Calling theory unifier for ", - Util.pretty_unif_problem ctxt st' - ] + Util.pretty_call_theory_unif ctxt st' ] |> Pretty.block |> Pretty.string_of); (*Note: st' is already normalised*) unify_theory binders ctxt st' env) in (case st' of (Abs (ns, Ts, ts), Abs (nt, Tt, tt)) => ((let val name = if ns = "" then nt else ns in unify_types ctxt (Ts, Tt) env |> Util.abstract_abstract Norm.norm_term_types_unif unif binders ctxt name Ts (ts, tt) |> seq_try end) handle Unification_Base.UNIF => Seq.empty) (*types do not unify*) (*eta-expand on the fly*) | (Abs (ns, Ts, ts), _) => ((let val st = apply2 (Envir.fastype env (Binders.binder_types binders)) st' in unify_types ctxt st env |> Util.abstract_abstract Norm.norm_term_types_unif unif binders ctxt ns Ts (ts, incr_boundvars 1 t' $ Bound 0) |> seq_try end) handle Unification_Base.UNIF => Seq.empty) (*types do not unify*) | (_, Abs _) => unif binders ctxt (t', s') env |> Seq.map (apsnd Unification_Base.symmetric) | (Bound i, Bound j) => Util.bound_bound binders ctxt (i, j) |> Seq.map (pair env) | (Free _, Free g) => rigid_rigid ctxt s' g env | (Const _, Const d) => rigid_rigid ctxt s' d env (*case distinctions on head term*) | _ => case apply2 strip_comb st' of ((Var (F, Fty), ss), (Var (G, Gty), ts)) => (((if F = G then flexflex1 unify_types ctxt (env, binders, F, Fty, Gty, ints_of' env ss, ints_of' env ts) else flexflex2 unify_types ctxt (env, binders, F, Fty, ints_of' env ss, G, Gty, ints_of' env ts)) |> Seq.single) handle Unification_Base.UNIF => Seq.empty) (*types do not unify*) | ((Var (F, Fty), ss), _) => (flexrigid unify_types ctxt (env, binders, F, Fty, ints_of' env ss, t')|> Seq.single handle OPEN_TERM => Seq.empty | Unification_Base.UNIF => Seq.empty) (*types do not unify*) | (_, (Var (F, Fty), ts)) => (flexrigid unify_types ctxt (env, binders, F, Fty, ints_of' env ts, s') |> Seq.single handle OPEN_TERM => Seq.empty | Unification_Base.UNIF => Seq.empty) (*types do not unify*) | ((sh, ss), (th, ts)) => if null ss orelse null ts then raise FALLBACK else (*but we have to normalise in comb cases*) Util.strip_comb_strip_comb Norm.norm_thm_types_unif unif binders ctxt (sh, th) (ss, ts) env |> seq_try) handle FALLBACK => handle_failure unify_theory_fail (fn _ => Pretty.str "Higher-order pattern unification failed.") | Unification_Base.PATTERN => handle_failure unify_theory_pattern (fn _ => Pretty.str "Terms not in Pattern fragment.") end val binder_types = Binders.binder_types binders in (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "Higher-order pattern unifying ", Util.pretty_unif_problem ctxt (apply2 (Norm.norm_term_unif env) st) ] |> Pretty.string_of); unif binders ctxt st (unify_types ctxt (apply2 (Envir.fastype env binder_types) st) env)) handle Unification_Base.UNIF => Seq.empty (*types do not unify*) end (*standard higher-order pattern unification*) val unify = e_unify Util.unify_types Unification_Combinator.fail_unify Unification_Combinator.fail_unify end diff --git a/thys/ML_Unification/Unifiers/higher_ordern_pattern_first_decomp_unification.ML b/thys/ML_Unification/Unifiers/higher_ordern_pattern_first_decomp_unification.ML deleted file mode 100644 --- a/thys/ML_Unification/Unifiers/higher_ordern_pattern_first_decomp_unification.ML +++ /dev/null @@ -1,150 +0,0 @@ -(* Title: ML_Unification/higher_ordern_pattern_first_decomp_unification.ML - Author: Kevin Kappelmann - -Higher-order pattern matching/unification with decomposition of non-pattern terms into a -higher-order pattern prefix and a list of remaining arguments. This is essentially -a combination of higher-order pattern and first-order matching/unification. - -Example: Let 0, 1 be bound variables and f, g, c be constants. -The unification problem ?x 0 1 (?y c 0) \\<^sup>? f (g c 0) -is decomposed into ?x 0 1 \\<^sup>? f and (?y c 0) \\<^sup>? (g c 0). -The latter, in turn, is decomposed into ?y \\<^sup>? g and c \\<^sup>? c and 0 \\<^sup>? 0. -*) -signature HIGHER_ORDERN_PATTERN_FIRST_DECOMP_UNIFICATION = -sig - include HAS_LOGGER - - val e_match : Unification_Base.type_matcher -> Unification_Base.matcher -> - Unification_Base.e_matcher - val match : Unification_Base.matcher - val norms_match : Unification_Base.normalisers - - val e_unify : Unification_Base.type_unifier -> Unification_Base.unifier -> - Unification_Base.e_unifier - val unify : Unification_Base.unifier - val norms_unify : Unification_Base.normalisers -end - -structure Higher_Ordern_Pattern_First_Decomp_Unification : - HIGHER_ORDERN_PATTERN_FIRST_DECOMP_UNIFICATION = -struct - -val logger = Logger.setup_new_logger Unification_Base.logger - "Higher_Ordern_Pattern_First_Decomp_Unification" - -structure UUtil = Unification_Util -structure HOP = Higher_Order_Pattern_Unification -structure UC = Unification_Combinator - -(*compute pattern prefixes*) -fun bounds_prefix bounds [] = (rev bounds, []) - | bounds_prefix bounds (t :: ts) = - if is_Bound t andalso not (member (op =) bounds t) - then bounds_prefix (t :: bounds) ts - else (rev bounds, t :: ts) -val bounds_prefix = bounds_prefix [] - -datatype ('a, 'b) either = Left of 'a | Right of 'b - -fun bounds_prefix2 (bounds1, _) ([], _) = Left (rev bounds1, []) - | bounds_prefix2 (_, bounds2) (_, []) = Right (rev bounds2, []) - | bounds_prefix2 (bounds1, bounds2) (s :: ss, t :: ts) = - if is_Bound s andalso not (member (op =) bounds1 s) - then if is_Bound t andalso not (member (op =) bounds2 t) - then bounds_prefix2 (s :: bounds1, t :: bounds2) (ss, ts) - else Right (rev bounds2, t :: ts) - else Left (rev bounds1, s :: ss) -val bounds_prefix2 = bounds_prefix2 ([], []) - -fun mk_decomp _ (_, []) = NONE (*no decomposition took place*) - | mk_decomp h (args, rem) = SOME (list_comb (h, args), rem) - -fun mk_bounds_decomp h args = bounds_prefix args |> mk_decomp h - -fun pattern_prefix_match p = case strip_comb p of - (v as Var _, args) => mk_bounds_decomp v args - | _ => NONE - -fun pattern_prefix_unif tp = case apply2 strip_comb tp of - ((vl as Var _, argsl), (vr as Var _, argsr)) => (case bounds_prefix2 (argsl, argsr) of - Left res => mk_decomp vl res |> Option.map Left - | Right res => mk_decomp vr res |> Option.map Right) - | ((v as Var _, args), _) => mk_bounds_decomp v args |> Option.map Left - | (_, (v as Var _, args)) => mk_bounds_decomp v args |> Option.map Right - | _ => NONE - -fun mk_decomp_other ss t = - let - val (th, ts) = strip_comb t - val n = length ts - length ss - in if n < 0 then NONE else chop n ts |> mk_decomp th end - -fun decompose_msg ctxt tp = Pretty.block [ - Pretty.str "Decomposing ", - UUtil.pretty_unif_problem ctxt tp, - Pretty.str " into higher-order pattern prefix and list of remaining arguments." - ] |> Pretty.string_of - -fun decomposed_msg ctxt (ph, th) (ps, ts) = Pretty.block [ - Pretty.str "Decomposition result ", - map (UUtil.pretty_unif_problem ctxt) ((ph, th) :: (ps ~~ ts)) - |> Pretty.separate "," |> Pretty.block - ] |> Pretty.string_of - -fun e_match match_types match_pattern match_theory = - let fun fallback_pattern binders ctxt (pt as (p, t)) = - let fun failure () = - (@{log Logger.DEBUG} ctxt (fn _ => "Decomposition failed. Calling theory matcher."); - match_theory binders ctxt pt) - in - (@{log Logger.DEBUG} ctxt (fn _ => decompose_msg ctxt pt); - case pattern_prefix_match p of - SOME (ph, ps) => (case mk_decomp_other ps t of - SOME (th, ts) => - (@{log Logger.TRACE} ctxt (fn _ => decomposed_msg ctxt (ph, th) (ps, ts)); - UUtil.strip_comb_strip_comb (K o K I) match_pattern - binders ctxt (ph, th) (ps, ts)) - | NONE => failure ()) - | NONE => failure ()) - end - in - HOP.e_match match_types (UC.norm_matcher (#norm_term HOP.norms_match) fallback_pattern) - match_theory - end - -val match = e_match UUtil.match_types UC.fail_match UC.fail_match -val norms_match = HOP.norms_match - -fun e_unify unif_types unif_pattern unif_theory = - let - val unif_patterns = - UUtil.strip_comb_strip_comb Envir_Normalisation.norm_thm_types_unif unif_pattern - fun fallback_pattern binders ctxt (tp as (s, t)) = - let fun failure () = - (@{log Logger.DEBUG} ctxt (fn _ => "Decomposition failed. Calling theory unifier."); - unif_theory binders ctxt tp) - in - (@{log Logger.DEBUG} ctxt (fn _ => decompose_msg ctxt tp); - case pattern_prefix_unif tp of - SOME (Left (sh, ss)) => (case mk_decomp_other ss t of - SOME (th, ts) => - (@{log Logger.TRACE} ctxt (fn _ => decomposed_msg ctxt (sh, th) (ss, ts)); - unif_patterns binders ctxt (sh, th) (ss, ts)) - | NONE => failure ()) - | SOME (Right (th, ts)) => (case mk_decomp_other ts s of - SOME (sh, ss) => - (@{log Logger.TRACE} ctxt (fn _ => decomposed_msg ctxt (sh, th) (ss, ts)); - unif_patterns binders ctxt (sh, th) (ss, ts)) - | NONE => failure ()) - | NONE => failure ()) - end - in - HOP.e_unify unif_types (UC.norm_unifier (#norm_term HOP.norms_unify) fallback_pattern) - unif_theory - end - -val unify = e_unify UUtil.unify_types UC.fail_unify UC.fail_unify - -val norms_unify = HOP.norms_unify - -end diff --git a/thys/ML_Unification/Unifiers/mixed_unification.ML b/thys/ML_Unification/Unifiers/mixed_unification.ML --- a/thys/ML_Unification/Unifiers/mixed_unification.ML +++ b/thys/ML_Unification/Unifiers/mixed_unification.ML @@ -1,52 +1,55 @@ (* Title: ML_Unification/mixed_unification.ML Author: Kevin Kappelmann Mixture of unification algorithms. *) signature MIXED_UNIFICATION = sig include HAS_LOGGER structure UC : UNIFICATION_COMBINE - (*first-order, then higher-order pattern with first-order decomposition, then UC.e_unify, + (*first-order, then higher-order pattern with decomposition, then UC.e_unify, then higher-order unification fallback*) - val first_higherp_first_comb_higher_unify : Unification_Base.unifier - val norms_first_higherp_first_comb_higher_unify : Unification_Base.normalisers + val first_higherp_decomp_comb_higher_unify : Unification_Base.unifier + val norms_first_higherp_decomp_comb_higher_unify : Unification_Base.normalisers end functor Mixed_Unification (A : sig structure FIA : FUNCTOR_INSTANCE_ARGS structure UC : UNIFICATION_COMBINE end) : MIXED_UNIFICATION = struct val logger = Logger.setup_new_logger Unification_Base.logger A.FIA.full_name structure UUtil = Unification_Util structure UCO = Unification_Combinator structure UC = A.UC -fun first_higherp_first_comb_higher_unify binders ctxt tp env = +fun first_higherp_decomp_comb_higher_unify binders ctxt tp env = let val unify_types = UUtil.unify_types val comb_higher = UCO.add_fallback_unifier UC.e_unify Higher_Order_Unification.unify - val higherp_comb_higher = UCO.add_fallback_unifier - (Higher_Ordern_Pattern_First_Decomp_Unification.e_unify unify_types - first_higherp_first_comb_higher_unify) + val decomp_comb_higher = UCO.add_fallback_unifier + (Higher_Order_Pattern_Decomp_Unification.e_unify first_higherp_decomp_comb_higher_unify) comb_higher - val fo_higherp_comb_higher = UCO.add_fallback_unifier - (First_Order_Unification.e_unify unify_types) higherp_comb_higher + val higherp_decomp_comb_higher = UCO.add_fallback_unifier + (Higher_Order_Pattern_Unification.e_unify unify_types decomp_comb_higher) + comb_higher + val fo_higherp_decomp_comb_higher = UCO.add_fallback_unifier + (First_Order_Unification.e_unify unify_types) + higherp_decomp_comb_higher in (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ - Pretty.str "First-order with higher-order pattern with first-order decomposition with ", + Pretty.str "First-order with higher-order pattern with decomposition with ", Binding.pretty UC.binding, Pretty.str " with higher-order fallback unifying ", UUtil.pretty_unif_problem ctxt (apply2 (Envir_Normalisation.norm_term_unif env) tp)] |> Pretty.string_of); - fo_higherp_comb_higher binders ctxt tp env) + fo_higherp_decomp_comb_higher binders ctxt tp env) end -val norms_first_higherp_first_comb_higher_unify = UUtil.beta_eta_short_norms_unif +val norms_first_higherp_decomp_comb_higher_unify = UUtil.beta_eta_short_norms_unif end diff --git a/thys/ML_Unification/Unifiers/simplifier_unification.ML b/thys/ML_Unification/Unifiers/simplifier_unification.ML --- a/thys/ML_Unification/Unifiers/simplifier_unification.ML +++ b/thys/ML_Unification/Unifiers/simplifier_unification.ML @@ -1,74 +1,75 @@ (* Title: ML_Unification/simplifier_unification.ML Author: Kevin Kappelmann Solving equations for unification problems with the simplifier. *) signature SIMPLIFIER_UNIFICATION = sig include HAS_LOGGER (*solves "s \\<^sup>? t" via simplification*) val simp_unify : Unification_Base.closed_unifier (*solves "SIMPS_TO s t \ rhs" via simplification of s when given a matching theorem "SIMPS_TO s t \ SIMPS_TO s t \ rhs"*) val SIMPS_TO_unify : thm -> Unification_Base.closed_unifier (*solves "SIMPS_TO_UNIF s t \ rhs" via simplification of s to s', followed by unification of "s' \\<^sup>? t", when given a matching theorem "SIMPS_TO_UNIF s t \ SIMPS_TO_UNIF s t \ rhs"*) - val SIMPS_TO_UNIF_unify : thm -> Unification_Base.normalisers -> Unification_Base.e_unifier + val SIMPS_TO_UNIF_unify : thm -> Unification_Base.normalisers -> Unification_Base.unifier -> + Unification_Base.closed_unifier end structure Simplifier_Unification : SIMPLIFIER_UNIFICATION = struct val logger = Logger.setup_new_logger Unification_Base.logger "Simplifier_Unification" (*some "safe" solvers create instantiations via flex-flex pairs, which we disallow*) val safe_simp_tac = Tactic_Util.safe_simp_tac fun simp_unify ctxt tp = (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "Solving unification problem via simplification ", Unification_Util.pretty_unif_problem ctxt tp ] |> Pretty.string_of); Tactic_Unification.unify (Tactic_Unification.env_tac_from_no_inst_tac (safe_simp_tac ctxt) |> K) ctxt tp) fun preprocess_tac ctxt = match_tac ctxt o single fun SIMPS_TO_unify preprocess_rule ctxt = let fun tac (tp as (lhs, _)) = if can Simps_To.dest_SIMPS_TO lhs then (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "Solving ", Syntax.pretty_term ctxt @{term SIMPS_TO}, Pretty.str " unification problem ", Unification_Util.pretty_unif_problem ctxt tp ] |> Pretty.string_of); preprocess_tac ctxt preprocess_rule THEN' safe_simp_tac ctxt THEN' Simps_To.finish_SIMPS_TO_tac ctxt) else K no_tac in Tactic_Unification.unify (Tactic_Unification.env_tac_from_no_inst_tac o tac) ctxt end -fun SIMPS_TO_UNIF_unify preprocess_rule norms unif binders ctxt = +fun SIMPS_TO_UNIF_unify preprocess_rule norms unif ctxt = let fun tac ctxt (tp as (lhs, _)) i (env, state) = (let val simps_to_tp = Simps_To_Unif.dest_SIMPS_TO_UNIF lhs fun solve_tac state = - Simps_To_Unif.SIMPS_TO_UNIF_env_thmsq (safe_simp_tac ctxt) norms unif binders ctxt + Simps_To_Unif.SIMPS_TO_UNIF_env_thmsq (safe_simp_tac ctxt) norms unif [] ctxt simps_to_tp env |> Seq.map (fn (env, thm) => (env, #norm_thm norms ctxt env state |> Thm.elim_implies thm)) in (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "Solving ", Syntax.pretty_term ctxt @{term SIMPS_TO_UNIF}, Pretty.str " unification problem ", Unification_Util.pretty_unif_problem ctxt tp ] |> Pretty.string_of); preprocess_tac ctxt preprocess_rule i state |> Seq.maps solve_tac) end) handle TERM _ => Seq.empty in Tactic_Unification.unify (tac ctxt) ctxt end end diff --git a/thys/ML_Unification/Unifiers/var_higher_order_pattern_unification.ML b/thys/ML_Unification/Unifiers/var_higher_order_pattern_unification.ML new file mode 100644 --- /dev/null +++ b/thys/ML_Unification/Unifiers/var_higher_order_pattern_unification.ML @@ -0,0 +1,70 @@ +(* Title: ML_Unification/var_higher_order_pattern_unification.ML + Author: Kevin Kappelmann + +Unifies terms of the form ?H b1 ... bn \\<^sup>? t where +(1) b1,...,bn are bound variables and +(2) ?H does not occur in t +with the higher-order pattern matcher. This pattern occurs frequently when unifying theorems with a +goal containing bound variables. + +Example: If we want to solve the goal "\x. ?P x 0" with a lemma ?Q by resolution, +the bound variables of the goal are first lifted to lemma, resulting in "?Q x". +Next, the terms "?Q x \\<^sup>? ?P x 0" are unified. Unfortunately, this problem falls outside the +higher-order pattern fragment since 0 is a constant. +However, the problem seems essentially first-order before lifting the bound variables: +we should be able to use ?Q to solve any goal G by setting ?Q to G. +The unifier of this file returns the expected substitution "?Q := \x. ?P x 0" in this case. +*) +signature VAR_HIGHER_ORDER_PATTERN_UNIFICATION = +sig + include HAS_LOGGER + + val can_var_pattern_unif : term * term -> bool * term list + val e_unify : Unification_Base.e_unifier +end + +structure Var_Higher_Order_Pattern_Unification : VAR_HIGHER_ORDER_PATTERN_UNIFICATION = +struct + +val logger = Logger.setup_new_logger Unification_Base.logger "Var_Higher_Order_Pattern_Unification" + +structure Util = Unification_Util + +fun can_var_pattern_unif (p, t) = let val (head, args) = strip_comb p + in + if is_Var head andalso forall is_Bound args andalso not (has_duplicates (op aconv) args) + andalso not (Term.exists_subterm (curry (op =) head) t) + then (true, args) + else (false, []) + end + +fun e_unify unif_theory binders ctxt (tp as (t, p)) env = + let + exception FALLBACK of Pretty.T + val hop_match_type_unif = Higher_Order_Pattern_Unification.e_match Util.unify_types + Unification_Combinator.fail_match Unification_Combinator.fail_match binders ctxt + val hop_match_type_unif_tp = hop_match_type_unif tp + val hop_match_type_unif_pt = hop_match_type_unif (p, t) #> Seq.map (apsnd Unification_Base.symmetric) + val seq_try = General_Util.seq_try (FALLBACK (Pretty.str "Higher-order pattern matching failed.")) + in + (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ + Pretty.str "Variable head higher-order pattern unifying ", + Util.pretty_unif_problem ctxt tp + ] |> Pretty.string_of); + case apply2 can_var_pattern_unif (tp, (p, t)) of + ((true, boundst), (true, boundsp)) => + if length boundst >= length boundsp + then hop_match_type_unif_tp env |> seq_try + else hop_match_type_unif_pt env |> seq_try + | ((true, _), _) => hop_match_type_unif_tp env |> seq_try + | (_, (true, _)) => hop_match_type_unif_pt env |> seq_try + | _ => raise FALLBACK + (Pretty.str "Terms not of the form ?H b1 ... bn \\<^sup>? t where ?H does not occur in t.")) + handle FALLBACK msg => (@{log Logger.DEBUG} ctxt (fn _ => Pretty.breaks [ + msg, + Util.pretty_call_theory_unif ctxt tp + ] |> Pretty.block |> Pretty.string_of); + unif_theory binders ctxt tp env) + end + +end diff --git a/thys/ML_Unification/unification_util.ML b/thys/ML_Unification/unification_util.ML --- a/thys/ML_Unification/unification_util.ML +++ b/thys/ML_Unification/unification_util.ML @@ -1,293 +1,306 @@ (* Title: ML_Unification/unification_util.ML Author: Kevin Kappelmann Utilities used for e-unifications. *) signature UNIFICATION_UTIL = sig include HAS_LOGGER (* pretty-printing *) val pretty_types : Proof.context -> typ list -> Pretty.T val pretty_terms : Proof.context -> term list -> Pretty.T val pretty_tyenv : Proof.context -> Type.tyenv -> Pretty.T val pretty_tenv : Proof.context -> Envir.tenv -> Pretty.T val pretty_env : Proof.context -> Envir.env -> Pretty.T val pretty_unif_problem : Proof.context -> (term * term) -> Pretty.T val pretty_unif_result : Proof.context -> (Envir.env * thm) -> Pretty.T + val pretty_call_theory_match : Proof.context -> (term * term) -> Pretty.T + val pretty_call_theory_unif : Proof.context -> (term * term) -> Pretty.T + (* terms and environments *) val maxidx_of_terms : term list -> int (*returns empty environment with maxidx set to maximum of given terms*) val empty_envir : term * term -> Envir.env (* type unification *) (*raises Unification_Base.UNIF on failure*) val unify_types : Unification_Base.type_unifier (*raises Unification_Base.UNIF on failure*) val match_types : Unification_Base.type_matcher (* normalisers *) val eta_short_norms_match : Unification_Base.normalisers val beta_eta_short_norms_match : Unification_Base.normalisers val eta_short_norms_unif : Unification_Base.normalisers val beta_eta_short_norms_unif : Unification_Base.normalisers (* shared standard cases for unifiers *) val smash_tpairs_if_occurs : Proof.context -> term -> Envir.env * thm -> (Envir.env * thm) Seq.seq val abstract_abstract : Envir_Normalisation.term_type_normaliser -> Unification_Base.unifier -> term Binders.binders -> Proof.context -> string -> typ -> (term * term) -> Envir.env -> (Envir.env * thm) Seq.seq (*raises UNIF if types do not unify*) val rigid_rigid : Envir_Normalisation.term_type_normaliser -> Unification_Base.type_unifier -> Proof.context -> term -> (string * typ) -> Envir.env -> (Envir.env * thm) Seq.seq val bound_bound : term Binders.binders -> Proof.context -> (int * int) -> thm Seq.seq val comb_comb : Envir_Normalisation.thm_type_normaliser -> Unification_Base.closed_unifier -> Proof.context -> (term * term) -> (term * term) -> Envir.env -> (Envir.env * thm) Seq.seq val args_args : Envir_Normalisation.thm_type_normaliser -> Unification_Base.closed_unifier -> Proof.context -> (term list * term list) -> (Envir.env * thm) Seq.seq -> (Envir.env * thm) Seq.seq val strip_comb_strip_comb : Envir_Normalisation.thm_type_normaliser -> Unification_Base.unifier -> term Binders.binders -> Proof.context -> (term * term) -> (term list * term list) -> Envir.env -> (Envir.env * thm) Seq.seq (* logging *) val log_unif_result : Proof.context -> term * term -> Envir.env * thm -> unit val log_unif_results : Proof.context -> term * term -> Unification_Base.closed_unifier -> unit val log_unif_results' : int -> Proof.context -> term * term -> Unification_Base.closed_unifier -> unit end structure Unification_Util : UNIFICATION_UTIL = struct val logger = Logger.setup_new_logger Unification_Base.logger "Util" structure Norm = Envir_Normalisation structure UBase = Unification_Base (* pretty-printing *) local val pretty_term = Syntax.pretty_term val pretty_type = Syntax.pretty_typ fun pretty_env_aux show_entry = Vartab.dest #> map show_entry #> Pretty.list "[" "]" fun pretty_env_entry show (s, t) = Pretty.block [show s, Pretty.str " := ", show t] val pretty_record = map (fn (key, entry) => Pretty.block [Pretty.str key, Pretty.str "=", entry]) #> Pretty.enum "," "{" "}" in fun pretty_types ctxt = Pretty.block o Pretty.commas o map (pretty_type ctxt) fun pretty_terms ctxt = Pretty.block o Pretty.commas o map (pretty_term ctxt) fun pretty_tyenv ctxt = let val show_entry = pretty_env_entry (pretty_type ctxt) fun get_typs (v, (s, T)) = (TVar (v, s), T) in pretty_env_aux (show_entry o get_typs) end fun pretty_tenv ctxt = let val show_entry = pretty_env_entry (pretty_term ctxt) fun get_trms (v, (T, t)) = (Var (v, T), t) in pretty_env_aux (show_entry o get_trms) end fun pretty_env ctxt (Envir.Envir {maxidx, tyenv, tenv}) = pretty_record [ ("maxidx", Pretty.str (string_of_int maxidx)), ("tyenv", pretty_tyenv ctxt tyenv), ("tenv", pretty_tenv ctxt tenv) ] end fun pretty_unif_problem ctxt (t1, t2) = Pretty.block [pretty_terms ctxt [t1], Pretty.str " \\<^sup>? " , pretty_terms ctxt [t2]] fun pretty_unif_result ctxt (env, thm) = Pretty.block [ Pretty.str "Environment: ", pretty_env ctxt env, Pretty.fbrk, Pretty.str "Theorem: ", Thm.pretty_thm ctxt thm ] +fun pretty_call_theory_match ctxt pt = Pretty.block [ + Pretty.str "Calling theory matcher for ", + pretty_unif_problem ctxt pt + ] + +fun pretty_call_theory_unif ctxt tp = Pretty.block [ + Pretty.str "Calling theory unifier for ", + pretty_unif_problem ctxt tp + ] + (* terms and environments *) fun maxidx_of_terms ts = fold (Integer.max o maxidx_of_term) ts ~1 fun empty_envir (t1, t2) = Envir.empty (maxidx_of_terms [t1, t2]) (* type unification *) fun match_types ctxt (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) = (if pointer_eq (T, U) then env else let val tyenv' = Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv in Envir.Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv'} end) handle Type.TYPE_MATCH => (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "Failed to match types ", pretty_types ctxt [Envir_Normalisation.norm_type_match tyenv T, U] ] |> Pretty.string_of); raise UBase.UNIF) fun unify_types ctxt (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) = (if pointer_eq (T, U) then env else let val (tyenv', maxidx') = Sign.typ_unify (Proof_Context.theory_of ctxt) (T, U) (tyenv, maxidx) in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end) handle Type.TUNIFY => (@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "Failed to unify types ", pretty_types ctxt (map (Envir_Normalisation.norm_type_unif tyenv) [T, U]) ] |> Pretty.string_of); raise UBase.UNIF) (* normalisers *) val eta_short_norms_match = { (*Precondition: the matcher must already normalise the types in its theorem!*) norm_unif_thm = Norm.eta_short_norm_thm (K I) Norm.eta_short_norm_term_match, norm_thm = Norm.eta_short_norm_thm_match, norm_term = Norm.eta_short_norm_term_match } val beta_eta_short_norms_match = { (*Precondition: the matcher must already normalise the types in its theorem!*) norm_unif_thm = Norm.beta_eta_short_norm_thm (K I) Norm.beta_eta_short_norm_term_match, norm_thm = Norm.beta_eta_short_norm_thm_match, norm_term = Norm.beta_eta_short_norm_term_match } val eta_short_norms_unif = { norm_unif_thm = Norm.eta_short_norm_thm_unif, norm_thm = Norm.eta_short_norm_thm_unif, norm_term = Norm.eta_short_norm_term_unif } val beta_eta_short_norms_unif = { norm_unif_thm = Norm.beta_eta_short_norm_thm_unif, norm_thm = Norm.beta_eta_short_norm_thm_unif, norm_term = Norm.beta_eta_short_norm_term_unif } (* shared standard cases for unifiers *) fun smash_tpairs_if_occurs ctxt t (env, thm) = let val tpairs = Thm.tpairs_of thm fun occs_t s = Logic.occs (t, s) in if exists (fn (t1, t2) => occs_t t1 orelse occs_t t2) tpairs then let (*in a perfect world, we would make the relevant tpairs of the theorem equality premises that can be solved by an arbitrary solver; however, Isabelle's kernel only allows one to solve tpairs with the built-in higher-order (pattern) unifier.*) (*only the kernel HO-unifier may add flex-flex pairs -> safe to normalise wrt. unification*) val normed_thm = Norm.norm_thm_unif ctxt env thm val normed_tpairs = Thm.tpairs_of normed_thm in (*note: we need to use the same unifier and environment as Thm.flexflex_rule here so that the final environment and theorem agree*) Unify.smash_unifiers (Context.Proof ctxt) normed_tpairs (Envir.empty (Thm.maxidx_of normed_thm)) |> Seq.maps (fn smash_env => (let val new_env = Envir.merge (smash_env, env) in Thm.flexflex_rule (SOME ctxt) normed_thm |> Seq.map (pair new_env) end) handle Vartab.DUP _ => (@{log Logger.INFO} ctxt (fn _ => Pretty.block [ Pretty.str "Failed to merge environment for smashed tpairs and environment created by flexflex_rule: ", pretty_unif_result ctxt (env, thm) ]|> Pretty.string_of); Seq.empty)) end else Seq.single (env, thm) end fun abstract_abstract norm_term_type unify binders ctxt name T tbp = let val (binder as (_, bvar), ctxt') = Binders.fix_binder (name, T) ctxt fun norm_abstract (env, thm) = let fun norm_bvar env = norm_term_type (Envir.type_env env) bvar in smash_tpairs_if_occurs ctxt' (norm_bvar env) (env, thm) |> Seq.map_filter (fn (env, thm) => UBase.abstract_rule ctxt' name (Thm.cterm_of ctxt' (norm_bvar env)) thm |> Option.map (pair env)) end in unify (binder :: binders) ctxt' tbp #> Seq.maps norm_abstract end fun rigid_rigid norm_term_type unify_types ctxt s (nt, Tt) env = let val (ns, Ts) = (if is_Const s then dest_Const else dest_Free) s in if ns = nt then let val (env' as Envir.Envir {tyenv,...}) = unify_types ctxt (Ts, Tt) env in (env', UBase.reflexive_term ctxt (norm_term_type tyenv s)) |> Seq.single end else Seq.empty end fun bound_bound binders ctxt (i, j) = if i = j then Binders.nth_binder_data binders i |> UBase.reflexive_term ctxt |> Seq.single else Seq.empty fun comb_comb norm_thm_types unify ctxt (f, x) (g, y) env = let val unif' = unify ctxt val env_thmq = unif' (f, g) env |> Seq.maps (fn (env, thm_fg) => unif' (x, y) env |> Seq.map (apsnd (pair thm_fg))) fun combine (env, thmp) = (*normalise types for the combination theorem to succeed*) apply2 (norm_thm_types ctxt env) thmp |> uncurry UBase.combination |> pair env in Seq.map combine env_thmq end fun args_args norm_thm_types unify ctxt (ss, ts) env_thmhq = (let val args = ss ~~ ts fun unif_arg tp = Seq.maps (fn (env, thms) => unify ctxt tp env |> Seq.map (apsnd (fn thm => thm :: thms))) fun unif_args env = fold unif_arg args (Seq.single (env, [])) (*combine the theorems*) fun combine thmh (env_res, arg_thms) = let (*normalise types for the combination theorem to succeed*) val norm_thm_types' = norm_thm_types ctxt env_res fun norm_combine thm_arg thm = norm_thm_types' thm_arg |> UBase.combination thm in (env_res, fold_rev norm_combine arg_thms (norm_thm_types' thmh)) end in Seq.maps (fn (env, thmh) => unif_args env |> Seq.map (combine thmh)) env_thmhq end) handle ListPair.UnequalLengths => Seq.empty fun strip_comb_strip_comb norm_thm_types unify binders ctxt (sh, th) (ss, ts) = unify binders ctxt (sh, th) #> args_args norm_thm_types (unify binders) ctxt (ss, ts) (* logging *) fun log_unif_result ctxt _ res = @{log Logger.INFO} ctxt (fn _ => pretty_unif_result ctxt res |> Pretty.string_of) fun log_unif_results ctxt tp unify = let val res = unify ctxt tp (empty_envir tp) |> Seq.list_of in fold (log_unif_result ctxt tp #> K) res () end fun log_unif_results' limit ctxt tp unify = let val res = unify ctxt tp (empty_envir tp) |> Seq.take limit |> Seq.list_of in fold (log_unif_result ctxt tp #> K) res () end end diff --git a/thys/Transport/Transport/Examples/Prototype/Transport_Prototype.thy b/thys/Transport/Transport/Examples/Prototype/Transport_Prototype.thy --- a/thys/Transport/Transport/Examples/Prototype/Transport_Prototype.thy +++ b/thys/Transport/Transport/Examples/Prototype/Transport_Prototype.thy @@ -1,168 +1,168 @@ \<^marker>\creator "Kevin Kappelmann"\ section \Transport via Equivalences on PERs (Prototype)\ theory Transport_Prototype imports Transport_Rel_If ML_Unification.ML_Unification_HOL_Setup ML_Unification.Unify_Resolve_Tactics keywords "trp_term" :: thy_goal_defn begin paragraph \Summary\ text \We implement a simple Transport prototype. The prototype is restricted to work with equivalences on partial equivalence relations. It is also not forming the compositions of equivalences so far. The support for dependent function relators is restricted to the form described in @{thm transport_Dep_Fun_Rel_no_dep_fun.partial_equivalence_rel_equivalenceI}: The relations can be dependent, but the functions must be simple. This is not production ready, but a proof of concept. The package provides a command @{command trp_term}, which sets up the required goals to prove a given term. See the examples in this directory for some use cases and refer to \<^cite>\"transport"\ for more details.\ paragraph \Theorem Setups\ context transport begin lemma left_Galois_left_if_left_rel_if_partial_equivalence_rel_equivalence: assumes "((\\<^bsub>L\<^esub>) \\<^bsub>PER\<^esub> (\\<^bsub>R\<^esub>)) l r" and "x \\<^bsub>L\<^esub> x'" shows "x \<^bsub>L\<^esub>\ l x" using assms by (intro left_Galois_left_if_left_rel_if_inflationary_on_in_fieldI) (blast elim: preorder_equivalence_order_equivalenceE)+ definition "transport_per x y \ ((\\<^bsub>L\<^esub>) \\<^bsub>PER\<^esub> (\\<^bsub>R\<^esub>)) l r \ x \<^bsub>L\<^esub>\ y" text \The choice of @{term "x'"} is arbitrary. All we need is @{term "in_dom (\\<^bsub>L\<^esub>) x"}.\ lemma transport_per_start: assumes "((\\<^bsub>L\<^esub>) \\<^bsub>PER\<^esub> (\\<^bsub>R\<^esub>)) l r" and "x \\<^bsub>L\<^esub> x'" shows "transport_per x (l x)" using assms unfolding transport_per_def by (blast intro: left_Galois_left_if_left_rel_if_partial_equivalence_rel_equivalence) lemma left_Galois_if_transport_per: assumes "transport_per x y" shows "x \<^bsub>L\<^esub>\ y" using assms unfolding transport_per_def by blast end context transport_Fun_Rel begin text \Simplification of Galois relator for simple function relator.\ corollary left_Galois_eq_Fun_Rel_left_Galois: assumes "((\\<^bsub>L1\<^esub>) \\<^bsub>PER\<^esub> (\\<^bsub>R1\<^esub>)) l1 r1" and "((\\<^bsub>L2\<^esub>) \\<^bsub>PER\<^esub> (\\<^bsub>R2\<^esub>)) l2 r2" shows "(\<^bsub>L\<^esub>\) = ((\<^bsub>L1\<^esub>\) \ (\<^bsub>L2\<^esub>\))" proof (intro ext) fix f g show "f \<^bsub>L\<^esub>\ g \ ((\<^bsub>L1\<^esub>\) \ (\<^bsub>L2\<^esub>\)) f g" proof assume "f \<^bsub>L\<^esub>\ g" moreover have "g \\<^bsub>R\<^esub> g" proof - from assms have per: "((\\<^bsub>L\<^esub>) \\<^bsub>PER\<^esub> (\\<^bsub>R\<^esub>)) l r" by (intro partial_equivalence_rel_equivalenceI) auto with \f \<^bsub>L\<^esub>\ g\ show ?thesis by blast qed ultimately show "((\<^bsub>L1\<^esub>\) \ (\<^bsub>L2\<^esub>\)) f g" using assms by (intro Fun_Rel_left_Galois_if_left_GaloisI) (auto elim!: tdfrs.t1.partial_equivalence_rel_equivalenceE tdfrs.t1.preorder_equivalence_galois_equivalenceE tdfrs.t1.galois_equivalenceE intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom) next assume "((\<^bsub>L1\<^esub>\) \ (\<^bsub>L2\<^esub>\)) f g" with assms have "((\<^bsub>L1\<^esub>\) \ (\<^bsub>L2\<^esub>\))\\<^bsub>in_dom (\\<^bsub>L\<^esub>)\<^esub>\\<^bsub>in_codom (\\<^bsub>R\<^esub>)\<^esub> f g" by (subst Fun_Rel_left_Galois_restrict_left_right_eq_Fun_Rel_left_GaloisI) blast+ with assms show "f \<^bsub>L\<^esub>\ g" by (intro left_Galois_if_Fun_Rel_left_GaloisI) blast+ qed qed end lemmas related_Fun_Rel_combI = Dep_Fun_Rel_relD[where ?S="\_ _. S" for S, rotated] lemma related_Fun_Rel_lambdaI: assumes "\x y. R x y \ S (f x) (g y)" and "T = (R \ S)" shows "T f g" using assms by blast paragraph \General ML setups\ ML_file\transport_util.ML\ paragraph \Unification Setup\ ML\ @{functor_instance struct_name = Transport_Unification_Combine and functor_name = Unification_Combine and id = Transport_Util.transport_id} \ local_setup \Transport_Unification_Combine.setup_attribute NONE\ ML\ @{functor_instance struct_name = Transport_Mixed_Unification and functor_name = Mixed_Unification and id = Transport_Util.transport_id and more_args = \structure UC = Transport_Unification_Combine\} \ ML\ @{functor_instance struct_name = Transport_Unification_Hints and functor_name = Term_Index_Unification_Hints and id = Transport_Util.transport_id and more_args = \ structure TI = Discrimination_Tree val init_args = { concl_unifier = SOME Higher_Order_Pattern_Unification.unify, - prems_unifier = SOME (Transport_Mixed_Unification.first_higherp_first_comb_higher_unify + prems_unifier = SOME (Transport_Mixed_Unification.first_higherp_decomp_comb_higher_unify |> Unification_Combinator.norm_unifier Envir_Normalisation.beta_norm_term_unif), - normalisers = SOME Transport_Mixed_Unification.norms_first_higherp_first_comb_higher_unify, + normalisers = SOME Transport_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify, retrieval = SOME (Term_Index_Unification_Hints_Args.mk_sym_retrieval TI.norm_term TI.unifiables), hint_preprocessor = SOME (K I) }\} \ local_setup \Transport_Unification_Hints.setup_attribute NONE\ declare [[trp_uhint where hint_preprocessor = \Unification_Hints_Base.obj_logic_hint_preprocessor @{thm atomize_eq[symmetric]} (Conv.rewr_conv @{thm eq_eq_True})\]] declare [[trp_ucombine add = \Transport_Unification_Combine.eunif_data (Transport_Unification_Hints.try_hints |> Unification_Combinator.norm_unifier - (#norm_term Transport_Mixed_Unification.norms_first_higherp_first_comb_higher_unify) + (#norm_term Transport_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify) |> K) (Transport_Unification_Combine.default_metadata Transport_Unification_Hints.binding)\]] paragraph \Prototype\ ML_file\transport.ML\ declare transport_Dep_Fun_Rel.transport_defs[trp_def] transport_Fun_Rel.transport_defs[trp_def] declare (*dependent case currently disabled by default since they easily make the unifier enumerate many undesired instantiations*) (* transport_Dep_Fun_Rel.partial_equivalence_rel_equivalenceI[per_intro] *) (* transport.rel_if_partial_equivalence_rel_equivalence_if_iff_if_partial_equivalence_rel_equivalenceI[rotated, per_intro] transport_Dep_Fun_Rel_no_dep_fun.partial_equivalence_rel_equivalenceI [ML_Krattr \Conversion_Util.move_prems_to_front_conv [1] |> Conversion_Util.thm_conv\, ML_Krattr \Conversion_Util.move_prems_to_front_conv [2,3] |> Conversion_Util.thm_conv\, per_intro] *) transport_Fun_Rel.partial_equivalence_rel_equivalenceI[rotated, per_intro] transport_eq_id.partial_equivalence_rel_equivalenceI[per_intro] transport_eq_restrict_id.partial_equivalence_rel_equivalence[per_intro] declare transport_id.left_Galois_eq_left[trp_relator_rewrite] transport_Fun_Rel.left_Galois_eq_Fun_Rel_left_Galois[trp_relator_rewrite] end diff --git a/thys/Transport/Transport/Examples/Prototype/transport.ML b/thys/Transport/Transport/Examples/Prototype/transport.ML --- a/thys/Transport/Transport/Examples/Prototype/transport.ML +++ b/thys/Transport/Transport/Examples/Prototype/transport.ML @@ -1,409 +1,408 @@ (* Title: Transport/transport.ML Author: Kevin Kappelmann Prototype for Transport. See README.md for future work. *) (*TODO: signature for final implementation*) structure Transport = struct structure Util = Transport_Util (*definitions used by Transport that need to be folded before a PER proof and unfolded after success.*) structure Transport_Defs = Named_Thms( val name = @{binding "trp_def"} val description = "Definitions used by Transport" ) val _ = Theory.setup Transport_Defs.setup (* simplifying definitions *) val simp_rhs = Simplifier.rewrite #> Conversion_Util.rhs_conv #> Conversion_Util.thm_conv (*simplifies the generated definition of a transported term*) fun simp_transported_def ctxt simps y_def = let val ctxt = ctxt addsimps simps val y_def_eta_expanded = Util.equality_eta_expand ctxt "x" y_def in apply2 (simp_rhs ctxt) (y_def, y_def_eta_expanded) end (* resolution setup *) val any_unify_trp_hints_resolve_tac = Unify_Resolve_Base.unify_resolve_any_tac - Transport_Mixed_Unification.norms_first_higherp_first_comb_higher_unify - Transport_Mixed_Unification.first_higherp_first_comb_higher_unify + Transport_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify + Transport_Mixed_Unification.first_higherp_decomp_comb_higher_unify fun get_theorems_tac f get_theorems ctxt = f (get_theorems ctxt) ctxt val get_theorems_resolve_tac = get_theorems_tac any_unify_trp_hints_resolve_tac val _ = Theory.setup ( Method.setup @{binding trp_hints_resolve} (Attrib.thms >> (SIMPLE_METHOD' oo any_unify_trp_hints_resolve_tac)) "Resolution with unification hints for Transport" ) (* PER equivalence prover *) (*introduction rules*) structure PER_Intros = Named_Thms( val name = @{binding "per_intro"} val description = "Introduction rules for per_prover" ) val _ = Theory.setup PER_Intros.setup fun per_prover_tac ctxt = REPEAT_ALL_NEW (get_theorems_resolve_tac PER_Intros.get ctxt) val _ = Theory.setup ( Method.setup @{binding per_prover} (Scan.succeed (SIMPLE_METHOD' o per_prover_tac)) "PER prover for Transport" ) (* domain prover *) structure Transport_in_dom = Named_Thms( val name = @{binding "trp_in_dom"} val description = "In domain theorems for Transport" ) val _ = Theory.setup Transport_in_dom.setup (*discharges the @{term "L x x'"} goals by registered lemmas*) fun transport_in_dom_prover_tac ctxt = get_theorems_resolve_tac Transport_in_dom.get ctxt val _ = Theory.setup ( Method.setup @{binding trp_in_dom_prover} (Scan.succeed (SIMPLE_METHOD' o transport_in_dom_prover_tac)) "in_dom prover for Transport" ) (* blackbox prover *) (*first derives the PER equivalence, then looks for registered domain lemmas.*) fun unfold_tac thms ctxt = simp_tac (clear_simpset ctxt addsimps thms) val unfold_transport_defs_tac = get_theorems_tac unfold_tac Transport_Defs.get fun transport_prover ctxt i = per_prover_tac ctxt i THEN TRY (SOMEGOAL (TRY o unfold_transport_defs_tac ctxt THEN' transport_in_dom_prover_tac ctxt) ) val _ = Theory.setup ( Method.setup @{binding trp_prover} (Scan.succeed (SIMPLE_METHOD' o transport_prover)) "Blackbox prover for Transport" ) (* whitebox prover intro rules *) structure Transport_Related_Intros = Named_Thms( val name = @{binding "trp_related_intro"} val description = "Introduction rules for Transport whitebox proofs" ) val _ = Theory.setup Transport_Related_Intros.setup (* relator rewriter *) (*rewrite rules to simplify the derived Galois relator*) structure Transport_Relator_Rewrites = Named_Thms( val name = @{binding "trp_relator_rewrite"} val description = "Rewrite rules for relators used by Transport" ) val _ = Theory.setup Transport_Relator_Rewrites.setup (*simple rewrite tactic for Galois relators*) fun per_simp_prover ctxt thm = let val prems = Thm.cprems_of thm val per_prover_tac = per_prover_tac ctxt fun prove_prem prem = Goal.prove_internal ctxt [] prem (fn _ => HEADGOAL per_prover_tac) in try (map prove_prem) prems |> Option.map (curry (op OF) thm) end fun transport_relator_rewrite ctxt thm = let val transport_defs = Transport_Defs.get ctxt val transport_relator_rewrites = Transport_Relator_Rewrites.get ctxt val ctxt = (clear_simpset ctxt) addsimps transport_relator_rewrites in Local_Defs.fold ctxt transport_defs thm |> Raw_Simplifier.rewrite_thm (false, false, false) per_simp_prover ctxt end fun transport_relator_rewrite_tac ctxt = EqSubst.eqsubst_tac ctxt [0] (Transport_Relator_Rewrites.get ctxt) THEN_ALL_NEW TRY o SOLVED' (per_prover_tac ctxt) val _ = Theory.setup ( Method.setup @{binding trp_relator_rewrite} (Scan.succeed (SIMPLE_METHOD' o transport_relator_rewrite_tac)) "Rewrite Transport relator" ) (* term transport command *) (*parsing*) @{parse_entries (struct) PA [L, R, x, y]} val parse_cmd_entries = let val parse_value = PA.parse_entry Parse.term Parse.term Parse.term Parse.term val parse_entry = Parse_Key_Value.parse_entry PA.parse_key Parse_Util.eq parse_value in PA.parse_entries_required Parse.and_list1 [PA.key PA.x] parse_entry (PA.empty_entries ()) end (*some utilities to destruct terms*) val transport_per_start_thm = @{thm "transport.transport_per_start"} val related_if_transport_per_thm = @{thm "transport.left_Galois_if_transport_per"} fun dest_transport_per \<^Const_>\transport.transport_per S T for L R l r x y\ = ((S, T), (L, R, l, r, x, y)) val dest_transport_per_y = dest_transport_per #> (fn (_, (_, _, _, _, _, y)) => y) fun mk_hom_Galois Ta Tb L R r x y = \<^Const>\galois_rel.Galois Ta Ta Tb Tb for L R r x y\ fun dest_hom_Galois \<^Const_>\galois_rel.Galois Ta _ Tb _ for L R r x y\ = ((Ta, Tb), (L, R, r, x, y)) val dest_hom_Galois_y = dest_hom_Galois #> (fn (_, (_, _, _, _, y)) => y) (*bindings for generated theorems and definitions*) val binding_transport_per = \<^binding>\transport_per\ val binding_per = \<^binding>\per\ val binding_in_dom = \<^binding>\in_dom\ val binding_related = \<^binding>\related\ val binding_related_rewritten = \<^binding>\related'\ val binding_def_simplified = \<^binding>\eq\ val binding_def_eta_expanded_simplified = \<^binding>\app_eq\ fun note_facts (binding, mixfix) ctxt related_thm y binding_thms_attribs = let val ((_, (_, y_def)), ctxt) = Util.create_local_theory_def (binding, mixfix) [] y ctxt (*create simplified definition theorems*) val transport_defs = Transport_Defs.get ctxt val (y_def_simplified, y_def_eta_expanded_simplified) = simp_transported_def ctxt transport_defs y_def (*create relatedness theorems*) val related_thm_rewritten = transport_relator_rewrite ctxt related_thm fun prepare_fact (suffix, thm, attribs) = let val binding = (Util.add_suffix binding suffix, []) val ctxt = (clear_simpset ctxt) addsimps transport_defs val folded_thm = (*fold definition of transported term*) Local_Defs.fold ctxt [y_def] thm (*simplify other transport definitions in theorem*) |> (Simplifier.rewrite ctxt |> Conversion_Util.thm_conv) val thm_attribs = ([folded_thm], attribs) in (binding, [thm_attribs]) end val facts = map prepare_fact ([ (binding_related, related_thm, []), (binding_related_rewritten, related_thm_rewritten, [Util.attrib_to_src (Binding.pos_of binding) Transport_Related_Intros.add]), (binding_def_simplified, y_def_simplified, []), (binding_def_eta_expanded_simplified, y_def_eta_expanded_simplified, []) ] @ binding_thms_attribs) in Local_Theory.notes facts ctxt |> snd end (*black-box transport as described in the Transport paper*) fun after_qed_blackbox (binding, mixfix) [thms as [per_thm, in_dom_thm]] ctxt = let val transport_per_thm = List.foldl (op INCR_COMP) transport_per_start_thm thms (*fix possibly occurring meta type variables*) val ((_, [transport_per_thm]), ctxt) = Variable.importT [transport_per_thm] ctxt val y = Util.real_thm_concl transport_per_thm |> dest_transport_per_y val related_thm = transport_per_thm INCR_COMP related_if_transport_per_thm val binding_thms = [ (binding_transport_per, transport_per_thm, []), (binding_per, per_thm, []), (binding_in_dom, in_dom_thm, [Util.attrib_to_src (Binding.pos_of binding) Transport_in_dom.add]) ] in note_facts (binding, mixfix) ctxt related_thm y binding_thms end (*experimental white-box transport support*) fun after_qed_whitebox (binding, mixfix) [[related_thm]] ctxt = let (*fix possibly occurring meta type variables*) val ((_, [related_thm]), ctxt) = Variable.importT [related_thm] ctxt val y = Util.real_thm_concl related_thm |> dest_hom_Galois_y in note_facts (binding, mixfix) ctxt related_thm y [] end fun setup_goals_blackbox ctxt (L, R, cx) maxidx = let (*check*) val [cL, cR] = Syntax.check_terms ctxt [L, R] |> map (Thm.cterm_of ctxt) (*instantiate theorem*) val transport_per_start_thm = Thm.incr_indexes (maxidx + 1) transport_per_start_thm val args = [SOME cL, SOME cR, NONE, NONE, SOME cx] val transport_per_start_thm = Drule.infer_instantiate' ctxt args transport_per_start_thm val transport_defs = Transport_Defs.get ctxt val goals = Local_Defs.fold ctxt transport_defs transport_per_start_thm |> Thm.prems_of |> map (rpair []) in goals end fun setup_goals_whitebox ctxt (yT, L, R, cx, y) maxidx = let val (r, _) = Term_Util.fresh_var "r" dummyT maxidx (*check*) val Galois = mk_hom_Galois (Thm.typ_of_cterm cx) yT L R r (Thm.term_of cx) y |> Syntax.check_term ctxt val goal = Util.mk_judgement Galois |> rpair [] in [goal] end fun setup_proof ((((binding, opt_yT, mixfix), params), unfolds), whitebox) lthy = let val ctxt = Util.set_proof_mode_schematic lthy (*type of transported term*) val yT = Option.map (Syntax.read_typ ctxt) opt_yT |> the_default dummyT (*theorems to unfold*) val unfolds = map (Proof_Context.get_fact ctxt o fst) unfolds |> flat (*term to transport*) val cx = (**read term**) Syntax.read_term ctxt (PA.get_x params) |> Thm.cterm_of ctxt (**unfold passed theorems**) |> Drule.cterm_rule (Local_Defs.unfold ctxt unfolds) (*transport relations and transport term goal*) val ([L, R, y], maxidx) = let (**configuration**) val opts = [PA.get_L_safe params, PA.get_R_safe params, PA.get_y_safe params] val opts_default_names = ["L", "R", "y"] val opts_constraints = [Util.mk_hom_rel_type (Thm.typ_of_cterm cx), Util.mk_hom_rel_type yT, yT] |> map Type.constraint (**parse**) val opts = map (Syntax.parse_term ctxt |> Option.map) opts val params_maxidx = Util.list_max (the_default ~1 o Option.map Term.maxidx_of_term) (Thm.maxidx_of_cterm cx) opts fun create_var (NONE, n) maxidx = Term_Util.fresh_var n dummyT params_maxidx ||> Integer.max maxidx | create_var (SOME t, _) created = (t, created) val (ts, maxidx) = fold_map create_var (opts ~~ opts_default_names) params_maxidx |>> map2 I opts_constraints in (ts, maxidx) end (*initialise goals and callback*) val (goals, after_qed) = if whitebox then (setup_goals_whitebox ctxt (yT, L, R, cx, y) maxidx, after_qed_whitebox) (*TODO: consider y in blackbox proofs*) else (setup_goals_blackbox ctxt (L, R, cx) maxidx, after_qed_blackbox) in Proof.theorem NONE (after_qed (binding, mixfix)) [goals] ctxt |> Proof.refine_singleton Util.split_conjunctions end val parse_strings = (*binding for transported term*) Parse_Spec.constdecl (*other params*) -- parse_cmd_entries (*optionally pass unfold theorems in case of white-box transports*) -- Scan.optional (Parse.reserved "unfold" |-- Parse.thms1) [] (*use a bang "!" to start white-box transport mode (experimental)*) -- Parse.opt_bang val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\trp_term\ "Transport term" (parse_strings >> setup_proof) (* experimental white-box prover *) val any_match_resolve_related_tac = - let fun unif binders = Higher_Ordern_Pattern_First_Decomp_Unification.e_match - Unification_Util.match_types unif Unification_Combinator.fail_unify binders - in - Unify_Resolve_Base.unify_resolve_any_tac - Higher_Ordern_Pattern_First_Decomp_Unification.norms_match unif - end + let fun unif binders = + Higher_Order_Pattern_Unification.e_match Unification_Util.match_types + (Higher_Order_Pattern_Decomp_Unification.e_match unif Unification_Combinator.fail_match) + Unification_Combinator.fail_match binders + in Unify_Resolve_Base.unify_resolve_any_tac Higher_Order_Pattern_Unification.norms_match unif end val related_comb_tac = any_match_resolve_related_tac @{thms related_Fun_Rel_combI} val related_lambda_tac = any_match_resolve_related_tac @{thms related_Fun_Rel_lambdaI} val related_tac = any_unify_trp_hints_resolve_tac val related_assume_tac = assume_tac fun mk_transport_related_tac cc_comb cc_lambda ctxt = let val transport_related_intros = Transport_Related_Intros.get ctxt val related_tac = related_tac transport_related_intros ctxt val comb_tac = related_comb_tac ctxt val lambda_tac = related_lambda_tac ctxt val assume_tac = related_assume_tac ctxt in Tactic_Util.CONCAT' [ related_tac, cc_comb comb_tac, cc_lambda lambda_tac, assume_tac ] end val transport_related_step_tac = let fun cc_comb tac i = tac i THEN prefer_tac i THEN prefer_tac (i + 1) in mk_transport_related_tac cc_comb I end fun transport_related_tac ctxt = let fun transport_related_tac cc = let fun cc_comb tac = tac THEN_ALL_NEW TRY o cc fun cc_lambda tac = tac THEN' TRY o cc in mk_transport_related_tac cc_comb cc_lambda ctxt end fun fix tac i thm = tac (fix tac) i thm in fix transport_related_tac end val _ = Theory.setup ( Method.setup @{binding trp_related_prover} (Scan.succeed (SIMPLE_METHOD' o transport_related_tac)) "Relatedness prover for Transport" ) fun instantiate_tac name ct ctxt = PRIMITIVE (Drule.infer_instantiate_types ctxt [((name, Thm.typ_of_cterm ct), ct)]) |> CHANGED val map_dummyT = Term.map_types (K dummyT) fun mk_term_skeleton maxidx t = let val consts = Term.add_consts t [] val (vars, _) = fold_map (uncurry Term_Util.fresh_var o apfst Long_Name.base_name) consts maxidx val t' = Term.subst_atomic (map2 (pair o Const) consts vars) t in t' end fun instantiate_skeleton_tac ctxt = let fun tac ct = let val (x, y) = Transport_Util.cdest_judgement ct |> Thm.dest_binop val default_sort = Proof_Context.default_sort ctxt val skeleton = mk_term_skeleton (Thm.maxidx_of_cterm ct) (Thm.term_of x) |> map_dummyT |> Type.constraint (Thm.typ_of_cterm y) |> Syntax.check_term (Util.set_proof_mode_pattern ctxt) (*add sort constraints for type variables*) |> Term.map_types (Term.map_atyps (map_type_tvar (fn (n, _) => TVar (n, default_sort n)))) |> Thm.cterm_of ctxt in instantiate_tac (Thm.term_of y |> dest_Var |> fst) skeleton ctxt end in Tactic_Util.CSUBGOAL_DATA I (K o tac) end fun transport_whitebox_tac ctxt = instantiate_skeleton_tac ctxt THEN' transport_related_tac ctxt THEN_ALL_NEW ( TRY o REPEAT1 o transport_relator_rewrite_tac ctxt THEN' TRY o any_unify_trp_hints_resolve_tac @{thms refl} ctxt ) val _ = Theory.setup ( Method.setup @{binding trp_whitebox_prover} (Scan.succeed (SIMPLE_METHOD' o transport_whitebox_tac)) "Whitebox prover for Transport" ) end \ No newline at end of file