diff --git a/thys/ML_Unification/Logger/logger.ML b/thys/ML_Unification/Logger/logger.ML --- a/thys/ML_Unification/Logger/logger.ML +++ b/thys/ML_Unification/Logger/logger.ML @@ -1,225 +1,225 @@ (* Title: Logger/logger.ML Author: Kevin Kappelmann, Paul Bachmann Hierarchical logger, indexed on bindings. The log levels are based on Apache's Log4J 2 https://logging.apache.org/log4j/2.x/manual/customloglevels.html *) signature LOGGER = sig type log_level = int val OFF : log_level val FATAL : log_level (*error log level*) val ERR : log_level val WARN : log_level val INFO : log_level val DEBUG : log_level val TRACE : log_level val ALL : log_level type logger_name = bstring type logger_binding val root_logger : logger_binding (*takes parent logger and creates a child logger with the given name*) val create_child_logger : logger_binding -> logger_name -> logger_binding val pretty_binding : logger_binding -> Pretty.T type logger_output = log_level -> string -> unit val default_output : logger_output type msg_filter = string -> bool type logger_config val config : logger_output -> log_level -> msg_filter -> bool -> logger_config val default_config : logger_config val set_config_output : logger_output -> logger_config -> logger_config val set_config_log_level : log_level -> logger_config -> logger_config (*set message filter: only log messages with positive results*) val set_config_msg_filter : msg_filter -> logger_config -> logger_config (*set whether to print the logger's name when logging*) val set_config_show_logger : bool -> logger_config -> logger_config val lookup_logger : logger_binding -> Context.generic -> logger_config option val insert_logger : (logger_binding * logger_config) -> Context.generic -> Context.generic val insert_logger_safe : (logger_binding * logger_config) -> Context.generic -> Context.generic val delete_logger : logger_binding -> Context.generic -> Context.generic val cut_loggers : logger_binding -> Context.generic -> Context.generic val set_logger : logger_binding -> (logger_config -> logger_config) -> Context.generic -> Context.generic val set_loggers : logger_binding -> (logger_config -> logger_config) -> Context.generic -> Context.generic val set_output : logger_binding -> logger_output -> Context.generic -> Context.generic val set_outputs : logger_binding -> logger_output -> Context.generic -> Context.generic val set_log_level : logger_binding -> log_level -> Context.generic -> Context.generic val set_log_levels : logger_binding -> log_level -> Context.generic -> Context.generic val set_msg_filter : logger_binding -> msg_filter -> Context.generic -> Context.generic val set_msg_filters : logger_binding -> msg_filter -> Context.generic -> Context.generic val set_show_logger : logger_binding -> bool -> Context.generic -> Context.generic val set_show_loggers : logger_binding -> bool -> Context.generic -> Context.generic (*creates and inserts child logger with default configuration into context*) val new_logger : logger_binding -> logger_name -> Context.generic -> (logger_binding * Context.generic) - (*registers new logger to background theory*) + (*registers new logger to background context*) val setup_new_logger : logger_binding -> logger_name -> logger_binding (*prints message created by passed function to the logger's output if the logger's log_level is greater or equal than the passed level and the message filter answers positively; uses lazy computation of the message to avoid computations in case the log level blocks the logging.*) val log : logger_binding -> log_level -> Proof.context -> (unit -> string) -> unit (* logging functions for different log levels *) val fatal : logger_binding -> Proof.context -> (unit -> string) -> unit val err : logger_binding -> Proof.context -> (unit -> string) -> unit val warn : logger_binding -> Proof.context -> (unit -> string) -> unit val info : logger_binding -> Proof.context -> (unit -> string) -> unit val debug : logger_binding -> Proof.context -> (unit -> string) -> unit val trace : logger_binding -> Proof.context -> (unit -> string) -> unit end structure Logger : LOGGER = struct type log_level = int (*values for different log levels*) val OFF = 0 val FATAL = 100 val ERR = 200 val WARN = 300 val INFO = 400 val DEBUG = 500 val TRACE = 600 val ALL = 1000 type logger_name = bstring datatype logger_binding = Logger_Binding of binding fun binding_of (Logger_Binding binding) = binding val root_logger_name = "Root" val root_logger = Binding.name root_logger_name |> Logger_Binding fun create_child_logger (Logger_Binding parent) child_name = let val child = Binding.qualify_name true parent child_name in if Symbol_Pos.is_identifier (Binding.name_of child) then Logger_Binding child else error ("Bad identifier for child logger " ^ ML_Syntax.print_string child_name) end val pretty_binding = Binding.pretty o binding_of type logger_output = log_level -> string -> unit fun default_output log_level = if log_level <= WARN then warning else if log_level < DEBUG then writeln else tracing type msg_filter = string -> bool type logger_config = { log_level : log_level, msg_filter : msg_filter, output : logger_output, show_logger : bool } fun config output log_level msg_filter show_logger = {log_level = log_level, output = output, msg_filter = msg_filter, show_logger = show_logger} val default_config = config default_output INFO (K true) true fun set_config_log_level log_level {output, show_logger, msg_filter,...} = {log_level = log_level, output = output, msg_filter = msg_filter, show_logger = show_logger} fun set_config_output output {log_level, show_logger, msg_filter,...} = {log_level = log_level, output = output, msg_filter = msg_filter, show_logger = show_logger} fun set_config_msg_filter msg_filter {output, log_level, show_logger,...} = {log_level = log_level, output = output, msg_filter = msg_filter, show_logger = show_logger} fun set_config_show_logger show_logger {output, log_level, msg_filter,...} = {log_level = log_level, output = output, msg_filter = msg_filter, show_logger = show_logger} fun log_config binding {log_level, output, msg_filter, show_logger} level message_f = if level > log_level then () else let val msg = message_f () |> show_logger ? (fn msg => cat_lines [ "Logger: " ^ Pretty.string_of (pretty_binding binding), msg]) in if msg_filter msg then output level msg else () end structure BT = Binding_Tree val init_tree = BT.insert (binding_of root_logger, default_config) BT.empty structure Logger_Data = Generic_Data( type T = logger_config BT.binding_tree val empty = init_tree val merge = BT.merge ) fun lookup_logger (Logger_Binding binding) = Logger_Data.get #> (fn bt => BT.lookup bt binding) fun insert_logger bcp context = (Logger_Data.map (apfst binding_of bcp |> BT.insert) context) handle (exn as BT.INSERT) => (warning (Pretty.block [ Pretty.str "Logger ", pretty_binding (fst bcp), Pretty.str " already added." ] |> Pretty.string_of); Exn.reraise exn) fun insert_logger_safe bcp = Logger_Data.map (apfst binding_of bcp |> BT.insert_safe) fun delete_logger (Logger_Binding binding) = Logger_Data.map (BT.delete_safe binding) fun cut_loggers (Logger_Binding binding) = Logger_Data.map (BT.cut_safe binding) fun set_logger (Logger_Binding binding) f = Logger_Data.map (BT.map binding (Option.map f)) fun set_loggers (Logger_Binding binding) f = Logger_Data.map (BT.map_below binding (Option.map f)) fun set_output binding = set_logger binding o set_config_output fun set_outputs binding = set_loggers binding o set_config_output fun set_log_level binding = set_logger binding o set_config_log_level fun set_log_levels binding = set_loggers binding o set_config_log_level fun set_msg_filter binding = set_logger binding o set_config_msg_filter fun set_msg_filters binding = set_loggers binding o set_config_msg_filter fun set_show_logger binding = set_logger binding o set_config_show_logger fun set_show_loggers binding = set_loggers binding o set_config_show_logger fun new_logger parent child_name context = let val child = create_child_logger parent child_name in (child, insert_logger (child, default_config) context) end fun setup_new_logger parent child_name = Context.>>> (new_logger parent child_name) fun log binding log_level ctxt message_f = case lookup_logger binding (Context.Proof ctxt) of SOME config => log_config binding config log_level message_f | NONE => let fun warn_msg _ = "Logger " ^ Pretty.string_of (pretty_binding binding) ^ " not found." in if binding = root_logger then default_output WARN (warn_msg ()) else log root_logger WARN ctxt warn_msg end fun fatal binding = log binding FATAL fun err binding = log binding ERR fun warn binding = log binding WARN fun info binding = log binding INFO fun debug binding = log binding DEBUG fun trace binding = log binding TRACE end (*structures that use a logger should implement this signature*) signature HAS_LOGGER = sig val logger : Logger.logger_binding end diff --git a/thys/ML_Unification/ML_Unification_Base.thy b/thys/ML_Unification/ML_Unification_Base.thy --- a/thys/ML_Unification/ML_Unification_Base.thy +++ b/thys/ML_Unification/ML_Unification_Base.thy @@ -1,16 +1,17 @@ \<^marker>\creator "Kevin Kappelmann"\ section \ML Unification Basics\ theory ML_Unification_Base imports ML_Logger ML_Binders ML_Normalisations + ML_Theorem_Utils begin paragraph \Summary\ text \Basic definitions and utilities for unification algorithms.\ ML_file\unification_base.ML\ ML_file\unification_util.ML\ end diff --git a/thys/ML_Unification/ML_Utils/Tactics/ML_Tactic_Utils.thy b/thys/ML_Unification/ML_Utils/Tactics/ML_Tactic_Utils.thy --- a/thys/ML_Unification/ML_Utils/Tactics/ML_Tactic_Utils.thy +++ b/thys/ML_Unification/ML_Utils/Tactics/ML_Tactic_Utils.thy @@ -1,15 +1,16 @@ \<^marker>\creator "Kevin Kappelmann"\ section \ML Tactic Utils\ theory ML_Tactic_Utils imports ML_Logger ML_Term_Utils ML_Conversion_Utils + ML_Unification_Base begin paragraph \Summary\ text \Utilities for tactics.\ ML_file\tactic_util.ML\ end \ No newline at end of file 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,234 +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 with matching and without lifting of premises and parameters*) + (*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*) - val eq_subgoal_from_eq_concl : cterm Binders.binders -> cterm list -> thm -> Proof.context -> thm + (*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.thm_normaliser -> - Envir_Normalisation.thm_normaliser -> term Binders.binders -> (Envir.env * thm) -> - Proof.context -> int -> tactic + 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)) + 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 = true, incremented = true} + 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.abstract_rule x cfree - #> Drule.arg_cong_rule all_const + Thm_Util.abstract_rule ctxt x cfree + #> Option.map (Drule.arg_cong_rule all_const) end in (*introduce the premises*) - fold_rev (Drule.imp_cong_rule o Thm.reflexive) cprems eq_thm + SOME (fold_rev (Drule.imp_cong_rule o Thm.reflexive) cprems eq_thm) (*introduce abstractions for the fresh Frees*) - |> fold all_abstract cbinders + |> fold (Option.mapPartial o all_abstract) cbinders end -fun rewrite_subgoal_unif_concl norm_state norm_eq_thm binders (env, eq_thm) ctxt i state = +fun rewrite_subgoal_unif_concl norm_binders norm_state norm_eq_thm binders (env_eq_thm as (env, _)) + ctxt i = let - fun rewrite_tac (rparams, (prems, _)) = + val binders = Binders.norm_binders (norm_binders env) binders + 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 cterm_of = Thm.cterm_of ctxt val cprems = map (cterm_of o Binders.replace_binders binders) prems - val eq_thm = eq_subgoal_from_eq_concl (map (apsnd cterm_of) binders) cprems - (norm_eq_thm ctxt env eq_thm) ctxt - in rewrite_subgoal_tac eq_thm ctxt end + 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 - ((PRIMITIVE (norm_state ctxt env) |> K) - THEN' SUBGOAL_STRIPPED I rewrite_tac) i state + (*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 - val protected_eq_thm = @{thm Pure.prop_def} - |> Thm.instantiate' [] [SOME cconcl_protected] - |> (fn eq_thm => eq_subgoal_from_eq_concl cbinders cprems_unprotected eq_thm ctxt) - in rewrite_subgoal_tac protected_eq_thm ctxt i end + 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/ML_Utils/Theorems/ML_Theorem_Utils.thy b/thys/ML_Unification/ML_Utils/Theorems/ML_Theorem_Utils.thy --- a/thys/ML_Unification/ML_Utils/Theorems/ML_Theorem_Utils.thy +++ b/thys/ML_Unification/ML_Utils/Theorems/ML_Theorem_Utils.thy @@ -1,12 +1,12 @@ \<^marker>\creator "Kevin Kappelmann"\ section \ML Theorem Utils\ theory ML_Theorem_Utils - imports Pure + imports ML_Logger begin paragraph \Summary\ text \Utilities for theorems.\ ML_file\thm_util.ML\ end \ No newline at end of file diff --git a/thys/ML_Unification/ML_Utils/Theorems/thm_util.ML b/thys/ML_Unification/ML_Utils/Theorems/thm_util.ML --- a/thys/ML_Unification/ML_Utils/Theorems/thm_util.ML +++ b/thys/ML_Unification/ML_Utils/Theorems/thm_util.ML @@ -1,25 +1,47 @@ (* Title: ML_Utils/thm_util.ML Author: Kevin Kappelmann Theorem utilities. *) signature THM_UTIL = sig + include HAS_LOGGER + + val pretty_THM : Proof.context -> string * int * thm list -> Pretty.T + + (*fails if the equality theorem contains a tpair or implicit Assumption mentioning the bound variables*) + val abstract_rule : Proof.context -> string -> cterm -> thm -> thm option (*"match_implies_elim prem thm" matches the first premise of thm against prem and then removes the premise; without lifting*) val match_implies_elim : thm -> thm -> thm val protect : thm -> thm end structure Thm_Util : THM_UTIL = struct +val logger = Logger.setup_new_logger Logger.root_logger "Thm_Util" + +fun pretty_THM ctxt (msg, subgoal, thms) = Pretty.block [ + Pretty.str msg, + Pretty.fbrk, + Pretty.str "Subgoal number ", + Pretty.str (string_of_int subgoal), + Pretty.fbrk, + Pretty.str "Theorems ", + Pretty.list "[" "]" (map (Thm.pretty_thm ctxt) thms) + ] + +fun abstract_rule ctxt n ct thm = SOME (Thm.abstract_rule n ct thm) + handle THM data => (@{log Logger.DEBUG} ctxt (fn _ => pretty_THM ctxt data |> Pretty.string_of); + NONE) + fun match_implies_elim prem thm = Thm.instantiate (Thm.first_order_match (Thm.cprem_of thm 1, Thm.cprop_of prem)) thm |> (fn thm => Thm.implies_elim thm prem) fun protect thm = Drule.protectI |> Thm.instantiate (TVars.empty, Vars.make [((("A", 0), propT), Thm.cprop_of thm)]) |> Thm.elim_implies thm -end \ No newline at end of file +end diff --git a/thys/ML_Unification/Unification_Tactics/Assumption/unify_assumption_base.ML b/thys/ML_Unification/Unification_Tactics/Assumption/unify_assumption_base.ML --- a/thys/ML_Unification/Unification_Tactics/Assumption/unify_assumption_base.ML +++ b/thys/ML_Unification/Unification_Tactics/Assumption/unify_assumption_base.ML @@ -1,96 +1,96 @@ (* Title: ML_Unification/unify_assumption_base.ML Author: Kevin Kappelmann Assumption tactic with adjustable unifier. *) signature UNIFY_ASSUMPTION_BASE = sig include HAS_LOGGER val unify_assumption_tac_index : Unification_Base.normalisers -> Unification_Base.unifier -> Proof.context -> int -> thm -> (int * thm) Seq.seq val unify_assumption_tac : Unification_Base.normalisers -> Unification_Base.unifier -> Proof.context -> int -> tactic end structure Unify_Assumption_Base : UNIFY_ASSUMPTION_BASE = struct val logger = Logger.setup_new_logger Unification_Base.logger "Unify_Assumption_Base" structure UBase = Unification_Base local (*returns unification result and updated state where the unified assumption is moved to the front*) fun unify_assumption unify ctxt i state = (let val strip_subgoal = Term_Util.strip_nth_subgoal i val (rparams, (prems, _)) = strip_subgoal state val nprems = length prems in if nprems < 1 then Seq.empty else let val (binders, unif_ctxt) = Binders.fix_binders rparams ctxt fun prepare_nth_prem n prem = let val (params, nprems_prem) = Term_Util.strip_all prem ||> Logic.count_prems in if nprems - n < nprems_prem then Seq.empty (*too many subpremises in given premise*) else let val nprems_new = nprems - nprems_prem in (*protect conclusion*) Tactic_Util.protect_tac nprems_new ctxt i state (*move premise to the front*) |> Seq.maps (rotate_tac (n - 1) i) (*remove all other premises*) |> Seq.maps (Tactic_Util.thin_tacs (2 upto nprems_new) i) (*remove outermost parameters of premise*) |> Seq.maps (REPEAT_DETERM_N (length params) (dresolve_tac ctxt [@{thm Pure.meta_spec}] i)) (*protect premise*) |> Seq.maps (dmatch_tac ctxt [Drule.protectI] i) end end fun mk_result prem_index state = (*unified assumption must be the first premise in the passed state*) (let val (_, (prem :: _, concl)) = strip_subgoal state in unify binders unif_ctxt (prem, concl) (Envir.empty (Thm.maxidx_of state)) |> Seq.map (pair (prem_index, binders) o rpair state) end) handle TERM _ => Seq.empty fun unify_prem (n, prem) = let val prem_index = n + 1 in prepare_nth_prem prem_index prem |> Seq.maps (mk_result prem_index) |> Seq.append end in General_Util.fold_rev_index unify_prem prems Seq.empty end end) handle TERM _ => Seq.empty in fun unify_assumption_tac_index norms unify ctxt i state = let val _ = @{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "Trying proof by assumption for subgoal ", Pretty.str (Int.toString i), Pretty.str ": ", (Thm.prop_of state |> Logic.nth_prem o pair i |> Syntax.pretty_term ctxt) handle TERM _ => Pretty.str "" ] |> Pretty.string_of) fun rewrite_subgoal ((n, binders), (res, state)) = (*rewrite conclusion to match the premise*) - Tactic_Util.rewrite_subgoal_unif_concl (#norm_thm norms) (#norm_unif_thm norms) - binders res ctxt i state + Tactic_Util.rewrite_subgoal_unif_concl (#norm_term norms) (#norm_thm norms) + (#norm_unif_thm norms) binders res ctxt i state (*unified premise is moved to the front; now close by equality assumption*) |> Seq.maps (DETERM (Tactic_Util.nth_eq_assume_tac 1 i)) |> Seq.map (pair n) in unify_assumption unify ctxt i state |> Seq.maps rewrite_subgoal end fun unify_assumption_tac norms = Seq.map snd oooo unify_assumption_tac_index norms end end \ No newline at end of file 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,48 +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 }\} \ 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_base.ML b/thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve_base.ML --- a/thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve_base.ML +++ b/thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve_base.ML @@ -1,201 +1,201 @@ (* Title: ML_Unification/unify_resolve_base.ML Author: Kevin Kappelmann Resolution with adjustable unifier. *) signature UNIFY_RESOLVE_BASE = sig include HAS_LOGGER (*unify the conclusions of the rule and the subgoal and resolve*) val unify_resolve_tac : Unification_Base.normalisers -> Unification_Base.unifier -> thm -> Proof.context -> int -> tactic val unify_resolve_every_tac : Unification_Base.normalisers -> Unification_Base.unifier -> thm list -> Proof.context -> int -> tactic val unify_resolve_any_tac : Unification_Base.normalisers -> Unification_Base.unifier -> thm list -> Proof.context -> int -> tactic (*treats the rule and subgoal as atomic propositions; example: resolving rule A ==> B and subgoal A ==> B leads to A ==> A while resolving rule A ==> B and subgoal A ==> B atomically solves the subgoal*) val unify_resolve_atomic_tac : Unification_Base.normalisers -> Unification_Base.unifier -> thm -> Proof.context -> int -> tactic val unify_resolve_atomic_every_tac : Unification_Base.normalisers -> Unification_Base.unifier -> thm list -> Proof.context -> int -> tactic val unify_resolve_atomic_any_tac : Unification_Base.normalisers -> Unification_Base.unifier -> thm list -> Proof.context -> int -> tactic val unify_eresolve_tac_index : Unification_Base.normalisers -> Unification_Base.unifier -> Unification_Base.normalisers -> Unification_Base.unifier -> thm -> Proof.context -> int -> thm -> (int * thm) Seq.seq val unify_eresolve_tac : Unification_Base.normalisers -> Unification_Base.unifier -> Unification_Base.normalisers -> Unification_Base.unifier -> thm -> Proof.context -> int -> tactic val unify_eresolve_every_tac : Unification_Base.normalisers -> Unification_Base.unifier -> Unification_Base.normalisers -> Unification_Base.unifier -> thm list -> Proof.context -> int -> tactic val unify_eresolve_any_tac : Unification_Base.normalisers -> Unification_Base.unifier -> Unification_Base.normalisers -> Unification_Base.unifier -> thm list -> Proof.context -> int -> tactic val unify_dresolve_tac : Unification_Base.normalisers -> Unification_Base.unifier -> thm -> Proof.context -> int -> tactic val unify_dresolve_every_tac : Unification_Base.normalisers -> Unification_Base.unifier -> thm list -> Proof.context -> int -> tactic val unify_dresolve_any_tac : Unification_Base.normalisers -> Unification_Base.unifier -> thm list -> Proof.context -> int -> tactic val unify_fresolve_tac : Unification_Base.normalisers -> Unification_Base.unifier -> thm -> Proof.context -> int -> tactic val unify_fresolve_every_tac : Unification_Base.normalisers -> Unification_Base.unifier -> thm list -> Proof.context -> int -> tactic val unify_fresolve_any_tac : Unification_Base.normalisers -> Unification_Base.unifier -> thm list -> Proof.context -> int -> tactic end structure Unify_Resolve_Base : UNIFY_RESOLVE_BASE = struct val logger = Logger.setup_new_logger Unification_Base.logger "Unify_Resolve_Base" structure Util = Unification_Util structure HOPU = Higher_Order_Pattern_Unification fun unify_resolve_tac norms unify rule ctxt = let fun tac cgoal i state = let val _ = @{log Logger.TRACE} ctxt (fn _ => Pretty.block [ Pretty.str ("Calling unification resolution tactic on subgoal "), Pretty.str (Int.toString i), Pretty.str ": ", Util.pretty_terms ctxt [Thm.term_of cgoal], Pretty.str (" and rule: "), Thm.pretty_thm ctxt rule ] |> Pretty.string_of ) val lifted_rule = Thm.lift_rule cgoal (Drule.incr_indexes state rule) val nprems_rule = Thm.nprems_of rule val rparams = Term_Util.strip_all (Thm.term_of cgoal) |> fst val (binders, ctxt) = Binders.fix_binders rparams ctxt val conclp = (*only unify the conclusion of the rule and the goal*) apply2 Logic.strip_assums_concl (Thm.prop_of lifted_rule, Thm.term_of cgoal) val env_thmq = unify binders ctxt conclp (Envir.empty (Thm.maxidx_of lifted_rule)) val norm_thm = #norm_thm norms fun rewrite_tac (env, unif_thm) = - Tactic_Util.rewrite_subgoal_unif_concl norm_thm (#norm_unif_thm norms) + Tactic_Util.rewrite_subgoal_unif_concl (#norm_term norms) norm_thm (#norm_unif_thm norms) binders (env, unif_thm) ctxt THEN' Tactic_Util.no_lift_resolve_tac (norm_thm ctxt env lifted_rule) nprems_rule ctxt in Seq.maps (fn res => rewrite_tac res i state) env_thmq end in Tactic_Util.CSUBGOAL_DATA I tac end fun unify_resolve_tacs norms unify rules ctxt = map (fn rule => unify_resolve_tac norms unify rule ctxt) rules fun unify_resolve_every_tac norms unify rules = unify_resolve_tacs norms unify rules #> EVERY' fun unify_resolve_any_tac norms unify rules = unify_resolve_tacs norms unify rules #> Tactic_Util.CONCAT' fun unify_resolve_atomic_tac norms unify rule ctxt = Tactic_Util.protect_tac 0 ctxt THEN' unify_resolve_tac norms unify (Thm_Util.protect rule) ctxt fun unify_resolve_atomic_tacs norms unify rules ctxt = map (fn rule => unify_resolve_atomic_tac norms unify rule ctxt) rules fun unify_resolve_atomic_every_tac norms unify rules = unify_resolve_atomic_tacs norms unify rules #> EVERY' fun unify_resolve_atomic_any_tac norms unify rules = unify_resolve_atomic_tacs norms unify rules #> Tactic_Util.CONCAT' fun unify_eresolve_tac_index norms_resolve unify_resolve norms_assume unify_assume rule ctxt i state = unify_resolve_tac norms_resolve unify_resolve rule ctxt i state |> Seq.maps (Unify_Assumption_Base.unify_assumption_tac_index norms_assume unify_assume ctxt i) fun unify_eresolve_tac norms_resolve unify_resolve norms_assume unify_assume rule ctxt i state = let val nprems = Thm.nprems_of rule in if nprems = 0 then (@{log Logger.WARN} ctxt (fn _ => Pretty.block [ Pretty.str "elim-resolution rule ", Thm.pretty_thm ctxt rule, Pretty.str " has no premises." ] |> Pretty.string_of ); Seq.empty) else unify_eresolve_tac_index norms_resolve unify_resolve norms_assume unify_assume rule ctxt i state |> Seq.maps (fn (n, state) => Tactic_Util.EVERY_ARG (Tactic_Util.thin_tac n) (i upto i + nprems - 2) state) end fun unify_eresolve_tacs norms_resolve unify_resolve norms_assume unify_assume rules ctxt = map (fn rule => unify_eresolve_tac norms_resolve unify_resolve norms_assume unify_assume rule ctxt) rules fun unify_eresolve_every_tac norms_resolve unify_resolve norms_assume unify_assume rules = unify_eresolve_tacs norms_resolve unify_resolve norms_assume unify_assume rules #> EVERY' fun unify_eresolve_any_tac norms_resolve unify_resolve norms_assume unify_assume rules = unify_eresolve_tacs norms_resolve unify_resolve norms_assume unify_assume rules #> Tactic_Util.CONCAT' fun unify_dresolve_tac norms unify rule ctxt = let val nprems = Thm.nprems_of rule in if nprems = 0 then (@{log Logger.WARN} ctxt (fn _ => Pretty.block [ Pretty.str "destruct-resolution rule ", Thm.pretty_thm ctxt rule, Pretty.str " has no premises." ] |> Pretty.string_of ); K no_tac) else unify_eresolve_tac HOPU.norms_unify HOPU.unify norms unify (Tactic.make_elim rule) ctxt end fun unify_dresolve_tacs norms unify rules ctxt = map (fn rule => unify_dresolve_tac norms unify rule ctxt) rules fun unify_dresolve_every_tac norms unify rules = unify_dresolve_tacs norms unify rules #> EVERY' fun unify_dresolve_any_tac norms unify rules = unify_dresolve_tacs norms unify rules #> Tactic_Util.CONCAT' fun unify_fresolve_tac norms unify rule ctxt i state = let val nprems = Thm.nprems_of rule in if nprems = 0 then (@{log Logger.WARN} ctxt (fn _ => Pretty.block [ Pretty.str "forward-resolution rule ", Thm.pretty_thm ctxt rule, Pretty.str " has no premises." ] |> Pretty.string_of ); Seq.empty) else unify_eresolve_tac_index HOPU.norms_unify HOPU.unify norms unify (Tactic.make_elim rule) ctxt i state |> Seq.map snd end fun unify_fresolve_tacs norms unify rules ctxt = map (fn rule => unify_fresolve_tac norms unify rule ctxt) rules fun unify_fresolve_every_tac norms unify rules = unify_fresolve_tacs norms unify rules #> EVERY' fun unify_fresolve_any_tac norms unify rules = unify_fresolve_tacs norms unify rules #> Tactic_Util.CONCAT' end diff --git a/thys/ML_Unification/Unifiers/higher_order_unification.ML b/thys/ML_Unification/Unifiers/higher_order_unification.ML --- a/thys/ML_Unification/Unifiers/higher_order_unification.ML +++ b/thys/ML_Unification/Unifiers/higher_order_unification.ML @@ -1,59 +1,60 @@ (* Title: ML_Unification/higher_order_unification.ML Author: Kevin Kappelmann TU Muenchen Higher-order unification from the Pure kernel adjusted to fit the Unification_Base.unifier type, i.e. moving flex-flex pairs into the theorem and support of open term unification. *) signature HIGHER_ORDER_UNIFICATION = sig include HAS_LOGGER val unify : Unification_Base.unifier val norms : Unification_Base.normalisers end structure Higher_Order_Unification : HIGHER_ORDER_UNIFICATION = struct val logger = Logger.setup_new_logger Unification_Base.logger "Higher_Order_Unification" structure Util = Unification_Util fun unify binders ctxt tp env = let fun unif env = let val init_goal = Logic.mk_equals #> Thm.cterm_of ctxt #> Goal.init fun create_env_thmq env = (*replace binders and apply the computed unifier*) apply2 (Envir_Normalisation.beta_eta_short_norm_term_unif env o Binders.replace_binders binders) tp (*create a goal such that we can create a theorem including the flex-flex pairs*) |> init_goal (*kind of a hack: resolving against the equality theorem will add the flex-flex pairs to the theorem*) |> HEADGOAL (match_tac ctxt @{thms Pure.reflexive}) (*conclude the goal and pair with the environment*) |> Seq.map (pair env o Goal.conclude) in (*find the unifiers*) Unify.hounifiers (map fst binders) (Context.Proof ctxt, env, [tp]) (*add the flex-flex pairs to the theorem*) |> Seq.maps (create_env_thmq o fst) end in ((@{log Logger.DEBUG} ctxt (fn _ => Pretty.block [ Pretty.str "Higher-order unifying ", Util.pretty_unif_problem ctxt (apply2 (Envir.norm_term env) tp) ] |> Pretty.string_of); - unif (Util.unify_types ctxt (apply2 Term.fastype_of tp) env)) + Util.unify_types ctxt (apply2 (Envir.fastype env (Binders.binder_types binders)) tp) env + |> unif) handle Unification_Base.UNIF => Seq.empty) (*types do not match*) end val norms = Unification_Util.beta_eta_short_norms_unif end diff --git a/thys/ML_Unification/unification_base.ML b/thys/ML_Unification/unification_base.ML --- a/thys/ML_Unification/unification_base.ML +++ b/thys/ML_Unification/unification_base.ML @@ -1,74 +1,74 @@ (* Title: ML_Unification/unification_base.ML Author: Kevin Kappelmann Basic definitions for unifiers. *) signature UNIFICATION_BASE = sig include HAS_LOGGER val reflexive : cterm -> thm val combination : thm -> thm -> thm val symmetric : thm -> thm - val abstract_rule : string -> cterm -> thm -> thm + val abstract_rule : Proof.context -> string -> cterm -> thm -> thm option val reflexive_term : Proof.context -> term -> thm (*raised on unsupported input*) exception PATTERN (*raised on unification failure for non-sequence outputs (e.g. type unification)*) exception UNIF type type_unifier = Proof.context -> typ * typ -> Envir.env -> Envir.env type type_matcher = type_unifier type closed_unifier = Proof.context -> term * term -> Envir.env -> (Envir.env * thm) Seq.seq (*term binders stores fresh free variables associated to each loose bound variable*) type unifier = term Binders.binders -> closed_unifier type e_unifier = unifier -> unifier type closed_matcher = closed_unifier type matcher = unifier type e_matcher = matcher -> matcher (* normalisers for matchers/unifiers *) type normalisers = { norm_unif_thm : Envir_Normalisation.thm_normaliser, norm_thm : Envir_Normalisation.thm_normaliser, norm_term : Envir_Normalisation.term_normaliser } end structure Unification_Base : UNIFICATION_BASE = struct val logger = Logger.setup_new_logger Logger.root_logger "Unification_Base" val reflexive = Thm.reflexive val combination = Thm.combination val symmetric = Thm.symmetric -val abstract_rule = Thm.abstract_rule +val abstract_rule = Thm_Util.abstract_rule val reflexive_term = reflexive oo Thm.cterm_of exception PATTERN = Pattern.Pattern exception UNIF = Pattern.Unif type type_unifier = Proof.context -> typ * typ -> Envir.env -> Envir.env type type_matcher = type_unifier type closed_unifier = Proof.context -> term * term -> Envir.env -> (Envir.env * thm) Seq.seq type unifier = term Binders.binders -> closed_unifier type e_unifier = unifier -> unifier type closed_matcher = closed_unifier type matcher = unifier type e_matcher = matcher -> matcher type normalisers = { norm_unif_thm : Envir_Normalisation.thm_normaliser, norm_thm : Envir_Normalisation.thm_normaliser, norm_term : Envir_Normalisation.term_normaliser } 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,253 +1,293 @@ (* 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 (* 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 + ] + (* 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 Unification_Base.UNIF) + 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 Unification_Base.UNIF) + 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 (Envir.Envir {tyenv,...}) thm = - let val bvar' = norm_term_type tyenv bvar - in Unification_Base.abstract_rule name (Thm.cterm_of ctxt' bvar') thm end - in - unify (binder :: binders) ctxt' tbp - #> Seq.map (fn (env, thm) => (env, norm_abstract env thm)) - end + 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', Unification_Base.reflexive_term ctxt (norm_term_type tyenv s)) + (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 |> Unification_Base.reflexive_term ctxt |> Seq.single + 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 Unification_Base.combination + |> 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 |> Unification_Base.combination thm + 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 _ (env, thm) = - @{log Logger.INFO} ctxt (fn _ => Pretty.block [ - Pretty.str "Environment: ", - pretty_env ctxt env, - Pretty.fbrk, - Pretty.str "Theorem: ", - Thm.pretty_thm ctxt thm - ] |> Pretty.string_of) +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.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,409 @@ (* Title: Transport/transport.ML - Author: Kevin Kappelmann, Paul Bachmann + 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 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 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