diff --git a/src/HOL/TPTP/atp_problem_import.ML b/src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML +++ b/src/HOL/TPTP/atp_problem_import.ML @@ -1,326 +1,327 @@ (* Title: HOL/TPTP/atp_problem_import.ML Author: Jasmin Blanchette, TU Muenchen Copyright 2012 Import TPTP problems as Isabelle terms or goals. *) signature ATP_PROBLEM_IMPORT = sig val read_tptp_file : theory -> (string * term -> 'a) -> string -> 'a list * ('a list * 'a list) * local_theory val nitpick_tptp_file : theory -> int -> string -> unit val refute_tptp_file : theory -> int -> string -> unit val can_tac : Proof.context -> (Proof.context -> tactic) -> term -> bool val SOLVE_TIMEOUT : int -> string -> tactic -> tactic val atp_tac : local_theory -> int -> (string * string) list -> int -> term list -> string -> int -> tactic val smt_solver_tac : string -> local_theory -> int -> tactic val make_conj : term list * term list -> term list -> term val sledgehammer_tptp_file : theory -> int -> string -> unit val isabelle_tptp_file : theory -> int -> string -> unit val isabelle_hot_tptp_file : theory -> int -> string -> unit val translate_tptp_file : theory -> string -> string -> unit end; structure ATP_Problem_Import : ATP_PROBLEM_IMPORT = struct open ATP_Util open ATP_Problem open ATP_Proof open ATP_Problem_Generate val debug = false val overlord = false (** TPTP parsing **) fun exploded_absolute_path file_name = Path.explode file_name |> (fn path => path |> not (Path.is_absolute path) ? Path.append (Path.explode "$PWD")) fun read_tptp_file thy postproc file_name = let fun has_role role (_, role', _, _) = (role' = role) fun get_prop f (name, _, P, _) = P |> f |> close_form |> pair name |> postproc val path = exploded_absolute_path file_name val ((_, _, problem), thy) = TPTP_Interpret.interpret_file true [Path.dir path, Path.explode "$TPTP"] path [] [] thy val (conjs, defs_and_nondefs) = problem |> List.partition (has_role TPTP_Syntax.Role_Conjecture) ||> List.partition (has_role TPTP_Syntax.Role_Definition) in (map (get_prop I) conjs, apply2 (map (get_prop Logic.varify_global)) defs_and_nondefs, Named_Target.theory_init thy) end (** Nitpick **) fun aptrueprop f ((t0 as \<^Const_>\Trueprop\) $ t1) = t0 $ f t1 | aptrueprop f t = f t fun is_legitimate_tptp_def \<^Const_>\Trueprop for t\ = is_legitimate_tptp_def t | is_legitimate_tptp_def \<^Const_>\HOL.eq _ for t u\ = (is_Const t orelse is_Free t) andalso not (exists_subterm (curry (op =) t) u) | is_legitimate_tptp_def _ = false fun nitpick_tptp_file thy timeout file_name = let val (conjs, (defs, nondefs), lthy) = read_tptp_file thy snd file_name val thy = Proof_Context.theory_of lthy val (defs, pseudo_defs) = defs |> map (ATP_Util.abs_extensionalize_term lthy #> aptrueprop (hol_open_form I)) |> List.partition (is_legitimate_tptp_def o perhaps (try HOLogic.dest_Trueprop) o ATP_Util.unextensionalize_def) val nondefs = pseudo_defs @ nondefs val state = Proof.init lthy val params = [("card", "1-100"), ("box", "false"), ("max_threads", "1"), ("batch_size", "5"), ("falsify", if null conjs then "false" else "true"), ("verbose", "true"), ("debug", if debug then "true" else "false"), ("overlord", if overlord then "true" else "false"), ("show_consts", "true"), ("format", "1"), ("max_potential", "0"), ("timeout", string_of_int timeout), ("tac_timeout", string_of_int ((timeout + 49) div 50))] |> Nitpick_Commands.default_params thy val i = 1 val n = 1 val step = 0 val subst = [] in Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst defs nondefs (case conjs of conj :: _ => conj | [] => \<^prop>\True\); () end (** Refute **) fun refute_tptp_file thy timeout file_name = let fun print_szs_of_outcome falsify s = "% SZS status " ^ (if s = "genuine" then if falsify then "CounterSatisfiable" else "Satisfiable" else "GaveUp") |> writeln val (conjs, (defs, nondefs), lthy) = read_tptp_file thy snd file_name val params = [("maxtime", string_of_int timeout), ("maxvars", "100000")] in Refute.refute_term lthy params (defs @ nondefs) (case conjs of conj :: _ => conj | [] => \<^prop>\True\) |> print_szs_of_outcome (not (null conjs)) end (** Sledgehammer and Isabelle (combination of provers) **) fun can_tac ctxt tactic conj = - can (Goal.prove_internal ctxt [] (Thm.cterm_of ctxt conj)) (fn [] => tactic ctxt) + \<^can>\Goal.prove_internal ctxt [] (Thm.cterm_of ctxt conj) + (fn {context = goal_ctxt, prems = []} => tactic goal_ctxt)\ fun SOLVE_TIMEOUT seconds name tac st = let val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s") val result = Timeout.apply (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) () handle Timeout.TIMEOUT _ => NONE | ERROR _ => NONE in (case result of NONE => (writeln ("FAILURE: " ^ name); Seq.empty) | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st')) end fun nitpick_finite_oracle_tac lthy timeout i th = let fun is_safe (Type (\<^type_name>\fun\, Ts)) = forall is_safe Ts | is_safe \<^typ>\prop\ = true | is_safe \<^typ>\bool\ = true | is_safe _ = false val conj = Thm.term_of (Thm.cprem_of th i) in if exists_type (not o is_safe) conj then Seq.empty else let val thy = Proof_Context.theory_of lthy val state = Proof.init lthy val params = [("box", "false"), ("max_threads", "1"), ("verbose", "true"), ("debug", if debug then "true" else "false"), ("overlord", if overlord then "true" else "false"), ("max_potential", "0"), ("timeout", string_of_int timeout)] |> Nitpick_Commands.default_params thy val i = 1 val n = 1 val step = 0 val subst = [] val (outcome, _) = Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst [] [] conj in if outcome = "none" then ALLGOALS (Skip_Proof.cheat_tac lthy) th else Seq.empty end end fun atp_tac lthy completeness override_params timeout assms prover = let val thy = Proof_Context.theory_of lthy val assm_ths0 = map (Skip_Proof.make_thm thy) assms val ((assm_name, _), lthy) = lthy |> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 3 else 0) |> Local_Theory.note ((\<^binding>\thms\, []), assm_ths0) fun ref_of th = (Facts.named (Thm.derivation_name th), []) val ref_of_assms = (Facts.named assm_name, []) in Sledgehammer_Tactics.sledgehammer_as_oracle_tac lthy ([("debug", if debug then "true" else "false"), ("overlord", if overlord then "true" else "false"), ("provers", prover), ("timeout", string_of_int timeout)] @ (if completeness > 0 then [("type_enc", if completeness = 1 then "mono_native" else "poly_tags")] else []) @ override_params) {add = ref_of_assms :: map ref_of [ext, @{thm someI}], del = [], only = true} [] end fun sledgehammer_tac demo lthy timeout assms i = let val frac = if demo then 16 else 12 fun slice mult completeness prover = SOLVE_TIMEOUT (mult * timeout div frac) (prover ^ (if completeness > 0 then "(" ^ string_of_int completeness ^ ")" else "")) (atp_tac lthy completeness [] (mult * timeout div frac) assms prover i) in slice 2 0 ATP_Proof.spassN ORELSE slice 2 0 ATP_Proof.vampireN ORELSE slice 2 0 ATP_Proof.eN ORELSE slice 2 0 ATP_Proof.z3_tptpN ORELSE slice 1 1 ATP_Proof.spassN ORELSE slice 1 2 ATP_Proof.eN ORELSE slice 1 1 ATP_Proof.vampireN ORELSE slice 1 2 ATP_Proof.vampireN ORELSE (if demo then slice 2 0 ATP_Proof.satallaxN ORELSE slice 2 0 ATP_Proof.leo2N else no_tac) end fun smt_solver_tac solver lthy = let val lthy = lthy |> Context.proof_map (SMT_Config.select_solver solver) in SMT_Solver.smt_tac lthy [] end fun auto_etc_tac lthy timeout assms i = SOLVE_TIMEOUT (timeout div 20) "nitpick" (nitpick_finite_oracle_tac lthy (timeout div 20) i) ORELSE SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac lthy i) ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac lthy i) ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass" (auto_tac lthy THEN ALLGOALS (atp_tac lthy 0 [] (timeout div 5) assms ATP_Proof.spassN)) ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac lthy i) ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" lthy i) ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc4" (smt_solver_tac "cvc4" lthy i) ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac lthy i) ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac lthy i) ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac lthy [] i) ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac lthy i) fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator fun make_conj (defs, nondefs) conjs = Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => \<^prop>\False\) fun print_szs_of_success conjs success = writeln ("% SZS status " ^ (if success then if null conjs then "Unsatisfiable" else "Theorem" else "GaveUp")) fun sledgehammer_tptp_file thy timeout file_name = let val (conjs, assms, lthy) = read_tptp_file thy snd file_name val conj = make_conj ([], []) conjs val assms = op @ assms in can_tac lthy (fn lthy => sledgehammer_tac true lthy timeout assms 1) conj |> print_szs_of_success conjs end fun generic_isabelle_tptp_file demo thy timeout file_name = let val (conjs, assms, lthy) = read_tptp_file thy snd file_name val conj = make_conj ([], []) conjs val full_conj = make_conj assms conjs val assms = op @ assms val (last_hope_atp, last_hope_completeness) = if demo then (ATP_Proof.satallaxN, 0) else (ATP_Proof.vampireN, 2) in (can_tac lthy (fn lthy => auto_etc_tac lthy (timeout div 2) assms 1) full_conj orelse can_tac lthy (fn lthy => sledgehammer_tac demo lthy (timeout div 2) assms 1) conj orelse can_tac lthy (fn lthy => SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)") (atp_tac lthy last_hope_completeness [] timeout assms last_hope_atp 1)) full_conj) |> print_szs_of_success conjs end val isabelle_tptp_file = generic_isabelle_tptp_file false val isabelle_hot_tptp_file = generic_isabelle_tptp_file true (** Translator between TPTP(-like) file formats **) fun translate_tptp_file thy format_str file_name = let val (conjs, (defs, nondefs), lthy) = read_tptp_file thy I file_name val conj = make_conj ([], []) (map snd conjs) val (format, type_enc, lam_trans) = (case format_str of "FOF" => (FOF, "mono_guards??", liftingN) | "TF0" => (TFF (Without_FOOL, Monomorphic), "mono_native", liftingN) | "TH0" => (THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN) | "DFG" => (DFG Monomorphic, "mono_native", liftingN) | _ => error ("Unknown format " ^ quote format_str ^ " (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")")) val generate_info = false val uncurried_aliases = false val readable_names = true val presimp = true val facts = map (apfst (rpair (Global, Non_Rec_Def))) defs @ map (apfst (rpair (Global, General))) nondefs val (atp_problem, _, _, _) = generate_atp_problem lthy generate_info format Hypothesis (type_enc_of_string Strict type_enc) Translator lam_trans uncurried_aliases readable_names presimp [] conj facts val ord = Sledgehammer_ATP_Systems.effective_term_order lthy spassN val ord_info = K [] val lines = lines_of_atp_problem format ord ord_info atp_problem in List.app Output.physical_stdout lines end end; diff --git a/src/HOL/Tools/Function/function_lib.ML b/src/HOL/Tools/Function/function_lib.ML --- a/src/HOL/Tools/Function/function_lib.ML +++ b/src/HOL/Tools/Function/function_lib.ML @@ -1,141 +1,141 @@ (* Title: HOL/Tools/Function/function_lib.ML Author: Alexander Krauss, TU Muenchen Ad-hoc collection of function waiting to be eliminated, generalized, moved elsewhere or otherwise cleaned up. *) signature FUNCTION_LIB = sig val function_internals: bool Config.T val derived_name: binding -> string -> binding val derived_name_suffix: binding -> string -> binding val plural: string -> string -> 'a list -> string val dest_all_all: term -> term list * term val unordered_pairs: 'a list -> ('a * 'a) list val rename_bound: string -> term -> term val mk_forall_rename: (string * term) -> term -> term val forall_intr_rename: (string * cterm) -> thm -> thm datatype proof_attempt = Solved of thm | Stuck of thm | Fail val try_proof: Proof.context -> cterm -> tactic -> proof_attempt val dest_binop_list: string -> term -> term list val regroup_conv: Proof.context -> string -> string -> thm list -> int list -> conv val regroup_union_conv: Proof.context -> int list -> conv val inst_constrs_of: Proof.context -> typ -> term list end structure Function_Lib: FUNCTION_LIB = struct val function_internals = Attrib.setup_config_bool \<^binding>\function_internals\ (K false) fun derived_name binding name = Binding.reset_pos (Binding.qualify_name true binding name) fun derived_name_suffix binding sffx = Binding.reset_pos (Binding.map_name (suffix sffx) binding) (* "The variable" ^ plural " is" "s are" vs *) fun plural sg pl [x] = sg | plural sg pl _ = pl (* Removes all quantifiers from a term, replacing bound variables by frees. *) fun dest_all_all \<^Const>\Pure.all _ for t\ = let val (v,b) = Term.dest_abs_global t |>> Free val (vs, b') = dest_all_all b in (v :: vs, b') end | dest_all_all t = ([],t) (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *) fun unordered_pairs [] = [] | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs (* renaming bound variables *) fun rename_bound n (Q $ Abs (_, T, b)) = (Q $ Abs (n, T, b)) | rename_bound n _ = raise Match fun mk_forall_rename (n, v) = rename_bound n o Logic.all v fun forall_intr_rename (n, cv) thm = let val allthm = Thm.forall_intr cv thm val (_ $ abs) = Thm.prop_of allthm in Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy)) allthm end datatype proof_attempt = Solved of thm | Stuck of thm | Fail fun try_proof ctxt cgoal tac = (case SINGLE tac (Goal.init cgoal) of NONE => Fail | SOME st => if Thm.no_prems st then Solved (Goal.finish ctxt st) else Stuck st) fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ] | dest_binop_list _ t = [ t ] (* separate two parts in a +-expression: "a + b + c + d + e" --> "(a + b + d) + (c + e)" Here, + can be any binary operation that is AC. cn - The name of the binop-constructor (e.g. @{const_name Un}) ac - the AC rewrite rules for cn is - the list of indices of the expressions that should become the first part (e.g. [0,1,3] in the above example) *) fun regroup_conv ctxt neu cn ac is ct = let val mk = HOLogic.mk_binop cn val t = Thm.term_of ct val xs = dest_binop_list cn t val js = subtract (op =) is (0 upto (length xs) - 1) val ty = fastype_of t in Goal.prove_internal ctxt [] (Thm.cterm_of ctxt (Logic.mk_equals (t, if null is then mk (Const (neu, ty), foldr1 mk (map (nth xs) js)) else if null js then mk (foldr1 mk (map (nth xs) is), Const (neu, ty)) else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js))))) - (K (rewrite_goals_tac ctxt ac - THEN resolve_tac ctxt [Drule.reflexive_thm] 1)) + (fn {context = goal_ctxt, ...} => + rewrite_goals_tac goal_ctxt ac THEN resolve_tac goal_ctxt [Drule.reflexive_thm] 1) end (* instance for unions *) fun regroup_union_conv ctxt = regroup_conv ctxt \<^const_abbrev>\Set.empty\ \<^const_name>\Lattices.sup\ (map (fn t => t RS eq_reflection) (@{thms Un_ac} @ @{thms Un_empty_right} @ @{thms Un_empty_left})) fun inst_constrs_of ctxt (Type (name, Ts)) = map (Ctr_Sugar.mk_ctr Ts) (#ctrs (the (Ctr_Sugar.ctr_sugar_of ctxt name))) | inst_constrs_of _ _ = raise Match end diff --git a/src/HOL/Tools/Function/partial_function.ML b/src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML +++ b/src/HOL/Tools/Function/partial_function.ML @@ -1,323 +1,324 @@ (* Title: HOL/Tools/Function/partial_function.ML Author: Alexander Krauss, TU Muenchen Partial function definitions based on least fixed points in ccpos. *) signature PARTIAL_FUNCTION = sig val init: string -> term -> term -> thm -> thm -> thm option -> declaration val mono_tac: Proof.context -> int -> tactic val add_partial_function: string -> (binding * typ option * mixfix) list -> Attrib.binding * term -> local_theory -> (term * thm) * local_theory val add_partial_function_cmd: string -> (binding * string option * mixfix) list -> Attrib.binding * string -> local_theory -> (term * thm) * local_theory val transform_result: morphism -> term * thm -> term * thm end; structure Partial_Function: PARTIAL_FUNCTION = struct open Function_Lib (*** Context Data ***) datatype setup_data = Setup_Data of {fixp: term, mono: term, fixp_eq: thm, fixp_induct: thm, fixp_induct_user: thm option}; fun transform_setup_data phi (Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user}) = let val term = Morphism.term phi; val thm = Morphism.thm phi; in Setup_Data {fixp = term fixp, mono = term mono, fixp_eq = thm fixp_eq, fixp_induct = thm fixp_induct, fixp_induct_user = Option.map thm fixp_induct_user} end; structure Modes = Generic_Data ( type T = setup_data Symtab.table; val empty = Symtab.empty; val extend = I; fun merge data = Symtab.merge (K true) data; ) fun init mode fixp mono fixp_eq fixp_induct fixp_induct_user phi = let val data' = Setup_Data {fixp = fixp, mono = mono, fixp_eq = fixp_eq, fixp_induct = fixp_induct, fixp_induct_user = fixp_induct_user} |> transform_setup_data (phi $> Morphism.trim_context_morphism); in Modes.map (Symtab.update (mode, data')) end; val known_modes = Symtab.keys o Modes.get o Context.Proof; fun lookup_mode ctxt = Symtab.lookup (Modes.get (Context.Proof ctxt)) #> Option.map (transform_setup_data (Morphism.transfer_morphism' ctxt)); (*** Automated monotonicity proofs ***) (*rewrite conclusion with k-th assumtion*) fun rewrite_with_asm_tac ctxt k = Subgoal.FOCUS (fn {context = ctxt', prems, ...} => Local_Defs.unfold0_tac ctxt' [nth prems k]) ctxt; fun dest_case ctxt t = case strip_comb t of (Const (case_comb, _), args) => (case Ctr_Sugar.ctr_sugar_of_case ctxt case_comb of NONE => NONE | SOME {case_thms, ...} => let val lhs = Thm.prop_of (hd case_thms) |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst; val arity = length (snd (strip_comb lhs)); val conv = funpow (length args - arity) Conv.fun_conv (Conv.rewrs_conv (map mk_meta_eq case_thms)); in SOME (nth args (arity - 1), conv) end) | _ => NONE; (*split on case expressions*) val split_cases_tac = Subgoal.FOCUS_PARAMS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) => case t of _ $ (_ $ Abs (_, _, body)) => (case dest_case ctxt body of NONE => no_tac | SOME (arg, conv) => let open Conv in if Term.is_open arg then no_tac else ((DETERM o Induct.cases_tac ctxt false [[SOME arg]] NONE []) THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0) THEN_ALL_NEW eresolve_tac ctxt @{thms thin_rl} THEN_ALL_NEW (CONVERSION (params_conv ~1 (fn ctxt' => arg_conv (arg_conv (abs_conv (K conv) ctxt'))) ctxt))) i end) | _ => no_tac) 1); (*monotonicity proof: apply rules + split case expressions*) fun mono_tac ctxt = K (Local_Defs.unfold0_tac ctxt [@{thm curry_def}]) THEN' (TRY o REPEAT_ALL_NEW (resolve_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\partial_function_mono\)) ORELSE' split_cases_tac ctxt)); (*** Auxiliary functions ***) (*Returns t $ u, but instantiates the type of t to make the application type correct*) fun apply_inst ctxt t u = let val thy = Proof_Context.theory_of ctxt; val T = domain_type (fastype_of t); val T' = fastype_of u; val subst = Sign.typ_match thy (T, T') Vartab.empty handle Type.TYPE_MATCH => raise TYPE ("apply_inst", [T, T'], [t, u]) in map_types (Envir.norm_type subst) t $ u end; fun head_conv cv ct = if can Thm.dest_comb ct then Conv.fun_conv (head_conv cv) ct else cv ct; (*** currying transformation ***) fun curry_const (A, B, C) = Const (\<^const_name>\Product_Type.curry\, [HOLogic.mk_prodT (A, B) --> C, A, B] ---> C); fun mk_curry f = case fastype_of f of Type ("fun", [Type (_, [S, T]), U]) => curry_const (S, T, U) $ f | T => raise TYPE ("mk_curry", [T], [f]); (* iterated versions. Nonstandard left-nested tuples arise naturally from "split o split o split"*) fun curry_n arity = funpow (arity - 1) mk_curry; fun uncurry_n arity = funpow (arity - 1) HOLogic.mk_case_prod; val curry_uncurry_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps [@{thm Product_Type.curry_case_prod}, @{thm Product_Type.case_prod_curry}]) val split_conv_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps [@{thm Product_Type.split_conv}]); val curry_K_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps [@{thm Product_Type.curry_K}]); (* instantiate generic fixpoint induction and eliminate the canonical assumptions; curry induction predicate *) fun specialize_fixp_induct ctxt fT fT_uc curry uncurry mono_thm f_def rule = let val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0)) in (* FIXME ctxt vs. ctxt' (!?) *) rule |> infer_instantiate' ctxt ((map o Option.map) (Thm.cterm_of ctxt) [SOME uncurry, NONE, SOME curry, NONE, SOME P_inst]) |> Tactic.rule_by_tactic ctxt (Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 (* discharge U (C f) = f *) THEN Simplifier.simp_tac (put_simpset curry_K_ss ctxt) 4 (* simplify bot case *) THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *) |> (fn thm => thm OF [mono_thm, f_def]) |> Conv.fconv_rule (Conv.concl_conv ~1 (* simplify conclusion *) (Raw_Simplifier.rewrite ctxt false [mk_meta_eq @{thm Product_Type.curry_case_prod}])) |> singleton (Variable.export ctxt' ctxt) end fun mk_curried_induct args ctxt inst_rule = let val cert = Thm.cterm_of ctxt (* FIXME ctxt vs. ctxt' (!?) *) val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt val split_paired_all_conv = Conv.every_conv (replicate (length args - 1) (Conv.rewr_conv @{thm split_paired_all})) val split_params_conv = Conv.params_conv ~1 (fn _ => Conv.implies_conv split_paired_all_conv Conv.all_conv) val (P_var, x_var) = Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |> strip_comb |> apsnd hd |> apply2 dest_Var val P_rangeT = range_type (snd P_var) val PT = map (snd o dest_Free) args ---> P_rangeT val x_inst = cert (foldl1 HOLogic.mk_prod args) val P_inst = cert (uncurry_n (length args) (Free (P, PT))) val inst_rule' = inst_rule |> Tactic.rule_by_tactic ctxt (Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 4 THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 THEN CONVERSION (split_params_conv ctxt then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3) |> Thm.instantiate (TVars.empty, Vars.make [(P_var, P_inst), (x_var, x_inst)]) |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt) |> singleton (Variable.export ctxt' ctxt) in inst_rule' end; (*** partial_function definition ***) fun transform_result phi (t, thm) = (Morphism.term phi t, Morphism.thm phi thm); fun gen_add_partial_function prep mode fixes_raw eqn_raw lthy = let val setup_data = the (lookup_mode lthy mode) handle Option.Option => error (cat_lines ["Unknown mode " ^ quote mode ^ ".", "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]); val Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user} = setup_data; val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [(eqn_raw, [], [])] lthy; val ((_, plain_eqn), args_ctxt) = Variable.focus NONE eqn lthy; val ((f_binding, fT), mixfix) = the_single fixes; val f_bname = Binding.name_of f_binding; fun note_qualified (name, thms) = Local_Theory.note ((derived_name f_binding name, []), thms) #> snd val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn); val (head, args) = strip_comb lhs; val argnames = map (fst o dest_Free) args; val F = fold_rev lambda (head :: args) rhs; val arity = length args; val (aTs, bTs) = chop arity (binder_types fT); val tupleT = foldl1 HOLogic.mk_prodT aTs; val fT_uc = tupleT :: bTs ---> body_type fT; val f_uc = Var ((f_bname, 0), fT_uc); val x_uc = Var (("x", 1), tupleT); val uncurry = lambda head (uncurry_n arity head); val curry = lambda f_uc (curry_n arity f_uc); val F_uc = lambda f_uc (uncurry_n arity (F $ curry_n arity f_uc)); val mono_goal = apply_inst lthy mono (lambda f_uc (F_uc $ f_uc $ x_uc)) |> HOLogic.mk_Trueprop |> Logic.all x_uc; - val mono_thm = Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal) - (K (mono_tac lthy 1)) + val mono_thm = + Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal) + (fn {context = goal_ctxt, ...} => mono_tac goal_ctxt 1) val inst_mono_thm = Thm.forall_elim (Thm.cterm_of lthy x_uc) mono_thm val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc); val f_def_binding = Thm.make_def_binding (Config.get lthy Function_Lib.function_internals) f_binding val ((f, (_, f_def)), lthy') = Local_Theory.define ((f_binding, mixfix), ((f_def_binding, []), f_def_rhs)) lthy; val eqn = HOLogic.mk_eq (list_comb (f, args), Term.betapplys (F, f :: args)) |> HOLogic.mk_Trueprop; val unfold = (infer_instantiate' lthy' (map (SOME o Thm.cterm_of lthy') [uncurry, F, curry]) fixp_eq OF [inst_mono_thm, f_def]) |> Tactic.rule_by_tactic lthy' (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy') 1); val specialized_fixp_induct = specialize_fixp_induct lthy' fT fT_uc curry uncurry inst_mono_thm f_def fixp_induct |> Drule.rename_bvars' (map SOME (f_bname :: f_bname :: argnames)); val mk_raw_induct = infer_instantiate' args_ctxt ((map o Option.map) (Thm.cterm_of args_ctxt) [SOME uncurry, NONE, SOME curry]) #> mk_curried_induct args args_ctxt #> singleton (Variable.export args_ctxt lthy') #> (fn thm => infer_instantiate' lthy' [SOME (Thm.cterm_of lthy' F)] thm OF [inst_mono_thm, f_def]) #> Drule.rename_bvars' (map SOME (f_bname :: argnames @ argnames)) val raw_induct = Option.map mk_raw_induct fixp_induct_user val rec_rule = let open Conv in Goal.prove lthy' (map (fst o dest_Free) args) [] eqn (fn _ => CONVERSION ((arg_conv o arg1_conv o head_conv o rewr_conv) (mk_meta_eq unfold)) 1 THEN resolve_tac lthy' @{thms refl} 1) end; val ((_, [rec_rule']), lthy'') = lthy' |> Local_Theory.note (eq_abinding, [rec_rule]) in lthy'' |> Spec_Rules.add Binding.empty Spec_Rules.equational_recdef [f] [rec_rule'] |> note_qualified ("simps", [rec_rule']) |> note_qualified ("mono", [mono_thm]) |> (case raw_induct of NONE => I | SOME thm => note_qualified ("raw_induct", [thm])) |> note_qualified ("fixp_induct", [specialized_fixp_induct]) |> pair (f, rec_rule') end; val add_partial_function = gen_add_partial_function Specification.check_multi_specs; val add_partial_function_cmd = gen_add_partial_function Specification.read_multi_specs; val mode = \<^keyword>\(\ |-- Parse.name --| \<^keyword>\)\; val _ = Outer_Syntax.local_theory \<^command_keyword>\partial_function\ "define partial function" ((mode -- (Parse.vars -- (Parse.where_ |-- Parse_Spec.simple_spec))) >> (fn (mode, (vars, spec)) => add_partial_function_cmd mode vars spec #> #2)); end; diff --git a/src/HOL/Tools/Meson/meson_clausify.ML b/src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML +++ b/src/HOL/Tools/Meson/meson_clausify.ML @@ -1,385 +1,386 @@ (* Title: HOL/Tools/Meson/meson_clausify.ML Author: Jia Meng, Cambridge University Computer Laboratory and NICTA Author: Jasmin Blanchette, TU Muenchen Transformation of HOL theorems into CNF forms. *) signature MESON_CLAUSIFY = sig val new_skolem_var_prefix : string val new_nonskolem_var_prefix : string val is_zapped_var_name : string -> bool val is_quasi_lambda_free : term -> bool val introduce_combinators_in_cterm : Proof.context -> cterm -> thm val introduce_combinators_in_theorem : Proof.context -> thm -> thm val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool val ss_only : thm list -> Proof.context -> Proof.context val cnf_axiom : Meson.simp_options -> Proof.context -> bool -> bool -> int -> thm -> (thm * term) option * thm list end; structure Meson_Clausify : MESON_CLAUSIFY = struct (* the extra "Meson" helps prevent clashes (FIXME) *) val new_skolem_var_prefix = "MesonSK" val new_nonskolem_var_prefix = "MesonV" fun is_zapped_var_name s = exists (fn prefix => String.isPrefix prefix s) [new_skolem_var_prefix, new_nonskolem_var_prefix] (**** Transformation of Elimination Rules into First-Order Formulas****) val cfalse = Thm.cterm_of \<^theory_context>\HOL\ \<^term>\False\; val ctp_false = Thm.cterm_of \<^theory_context>\HOL\ (HOLogic.mk_Trueprop \<^term>\False\); (* Converts an elim-rule into an equivalent theorem that does not have the predicate variable. Leaves other theorems unchanged. We simply instantiate the conclusion variable to False. (Cf. "transform_elim_prop" in "Sledgehammer_Util".) *) fun transform_elim_theorem th = (case Thm.concl_of th of (*conclusion variable*) \<^Const_>\Trueprop for \Var (v as (_, \<^Type>\bool\))\\ => Thm.instantiate (TVars.empty, Vars.make [(v, cfalse)]) th | Var (v as (_, \<^Type>\prop\)) => Thm.instantiate (TVars.empty, Vars.make [(v, ctp_false)]) th | _ => th) (**** SKOLEMIZATION BY INFERENCE (lcp) ****) fun mk_old_skolem_term_wrapper t = let val T = fastype_of t in \<^Const>\Meson.skolem T for t\ end fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t') | beta_eta_in_abs_body t = Envir.beta_eta_contract t (*Traverse a theorem, accumulating Skolem function definitions.*) fun old_skolem_defs th = let fun dec_sko \<^Const_>\Ex _ for \body as Abs (_, T, p)\\ rhss = (*Existential: declare a Skolem function, then insert into body and continue*) let val args = Misc_Legacy.term_frees body (* Forms a lambda-abstraction over the formal parameters *) val rhs = fold_rev (absfree o dest_Free) args (HOLogic.choice_const T $ beta_eta_in_abs_body body) |> mk_old_skolem_term_wrapper val comb = list_comb (rhs, args) in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end | dec_sko \<^Const_>\All _ for \t as Abs _\\ rhss = dec_sko (#2 (Term.dest_abs_global t)) rhss | dec_sko \<^Const_>\conj for p q\ rhss = rhss |> dec_sko p |> dec_sko q | dec_sko \<^Const_>\disj for p q\ rhss = rhss |> dec_sko p |> dec_sko q | dec_sko \<^Const_>\Trueprop for p\ rhss = dec_sko p rhss | dec_sko _ rhss = rhss in dec_sko (Thm.prop_of th) [] end; (**** REPLACING ABSTRACTIONS BY COMBINATORS ****) fun is_quasi_lambda_free \<^Const_>\Meson.skolem _ for _\ = true | is_quasi_lambda_free (t1 $ t2) = is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2 | is_quasi_lambda_free (Abs _) = false | is_quasi_lambda_free _ = true fun abstract ctxt ct = let val Abs (_, _, body) = Thm.term_of ct val (x, cbody) = Thm.dest_abs_global ct val (A, cbodyT) = Thm.dest_funT (Thm.ctyp_of_cterm ct) fun makeK () = Thm.instantiate' [SOME A, SOME cbodyT] [SOME cbody] @{thm abs_K} in case body of Const _ => makeK() | Free _ => makeK() | Var _ => makeK() (*though Var isn't expected*) | Bound 0 => Thm.instantiate' [SOME A] [] @{thm abs_I} (*identity: I*) | rator$rand => if Term.is_dependent rator then (*C or S*) if Term.is_dependent rand then (*S*) let val crator = Thm.lambda x (Thm.dest_fun cbody) val crand = Thm.lambda x (Thm.dest_arg cbody) val (C, B) = Thm.dest_funT (Thm.dest_ctyp1 (Thm.ctyp_of_cterm crator)) val abs_S' = @{thm abs_S} |> instantiate'_normalize [SOME A, SOME B, SOME C] [SOME crator, SOME crand] val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_S') in Thm.transitive abs_S' (Conv.binop_conv (abstract ctxt) rhs) end else (*C*) let val crator = Thm.lambda x (Thm.dest_fun cbody) val crand = Thm.dest_arg cbody val (C, B) = Thm.dest_funT (Thm.dest_ctyp1 (Thm.ctyp_of_cterm crator)) val abs_C' = @{thm abs_C} |> instantiate'_normalize [SOME A, SOME B, SOME C] [SOME crator, SOME crand] val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_C') in Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv (abstract ctxt)) rhs) end else if Term.is_dependent rand then (*B or eta*) if rand = Bound 0 then Thm.eta_conversion ct else (*B*) let val crator = Thm.dest_fun cbody val crand = Thm.lambda x (Thm.dest_arg cbody) val (C, B) = Thm.dest_funT (Thm.ctyp_of_cterm crator) val abs_B' = @{thm abs_B} |> instantiate'_normalize [SOME A, SOME B, SOME C] [SOME crator, SOME crand] val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_B') in Thm.transitive abs_B' (Conv.arg_conv (abstract ctxt) rhs) end else makeK () | _ => raise Fail "abstract: Bad term" end; (* Traverse a theorem, replacing lambda-abstractions with combinators. *) fun introduce_combinators_in_cterm ctxt ct = if is_quasi_lambda_free (Thm.term_of ct) then Thm.reflexive ct else case Thm.term_of ct of Abs _ => let val (cv, cta) = Thm.dest_abs_global ct val (v, _) = dest_Free (Thm.term_of cv) val u_th = introduce_combinators_in_cterm ctxt cta val cu = Thm.rhs_of u_th val comb_eq = abstract ctxt (Thm.lambda cv cu) in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end | _ $ _ => let val (ct1, ct2) = Thm.dest_comb ct in Thm.combination (introduce_combinators_in_cterm ctxt ct1) (introduce_combinators_in_cterm ctxt ct2) end fun introduce_combinators_in_theorem ctxt th = if is_quasi_lambda_free (Thm.prop_of th) then th else let val th = Drule.eta_contraction_rule th val eqth = introduce_combinators_in_cterm ctxt (Thm.cprop_of th) in Thm.equal_elim eqth th end handle THM (msg, _, _) => (warning ("Error in the combinator translation of " ^ Thm.string_of_thm ctxt th ^ "\nException message: " ^ msg); (* A type variable of sort "{}" will make "abstraction" fail. *) TrueI) (*cterms are used throughout for efficiency*) val cTrueprop = Thm.cterm_of \<^theory_context>\HOL\ HOLogic.Trueprop; (*Given an abstraction over n variables, replace the bound variables by free ones. Return the body, along with the list of free variables.*) fun c_variant_abs_multi (ct0, vars) = let val (cv,ct) = Thm.dest_abs_global ct0 in c_variant_abs_multi (ct, cv::vars) end handle CTERM _ => (ct0, rev vars); (* Given the definition of a Skolem function, return a theorem to replace an existential formula by a use of that function. Example: "\x. x \ A \ x \ B \ sko A B \ A \ sko A B \ B" *) fun old_skolem_theorem_of_def ctxt rhs0 = let + val thy = Proof_Context.theory_of ctxt val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of ctxt val rhs' = rhs |> Thm.dest_comb |> snd val (ch, frees) = c_variant_abs_multi (rhs', []) val (hilbert, cabs) = ch |> Thm.dest_comb |>> Thm.term_of val T = case hilbert of Const (_, Type (\<^type_name>\fun\, [_, T])) => T | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"", [hilbert]) val cex = Thm.cterm_of ctxt (HOLogic.exists_const T) val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs) val conc = Drule.list_comb (rhs, frees) |> Drule.beta_conv cabs |> Thm.apply cTrueprop - fun tacf [prem] = - rewrite_goals_tac ctxt @{thms skolem_def [abs_def]} - THEN resolve_tac ctxt - [(prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]}) - RS Global_Theory.get_thm (Proof_Context.theory_of ctxt) "Hilbert_Choice.someI_ex"] 1 in - Goal.prove_internal ctxt [ex_tm] conc tacf + Goal.prove_internal ctxt [ex_tm] conc + (fn {context = goal_ctxt, prems = [prem]} => + rewrite_goals_tac goal_ctxt @{thms skolem_def [abs_def]} THEN + resolve_tac goal_ctxt + [(prem |> rewrite_rule goal_ctxt @{thms skolem_def [abs_def]}) + RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex"] 1) |> forall_intr_list frees |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) |> Thm.varifyT_global end fun to_definitional_cnf_with_quantifiers ctxt th = let val eqth = CNF.make_cnfx_thm ctxt (HOLogic.dest_Trueprop (Thm.prop_of th)) val eqth = eqth RS @{thm eq_reflection} val eqth = eqth RS @{thm TruepropI} in Thm.equal_elim eqth th end fun zapped_var_name ((ax_no, cluster_no), skolem) index_no s = (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^ "_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^ string_of_int index_no ^ "_" ^ Name.desymbolize (SOME false) s fun cluster_of_zapped_var_name s = let val get_int = the o Int.fromString o nth (space_explode "_" s) in ((get_int 1, (get_int 2, get_int 3)), String.isPrefix new_skolem_var_prefix s) end fun rename_bound_vars_to_be_zapped ax_no = let fun aux (cluster as (cluster_no, cluster_skolem)) index_no pos t = case t of (t1 as Const (s, _)) $ Abs (s', T, t') => if s = \<^const_name>\Pure.all\ orelse s = \<^const_name>\All\ orelse s = \<^const_name>\Ex\ then let val skolem = (pos = (s = \<^const_name>\Ex\)) val (cluster, index_no) = if skolem = cluster_skolem then (cluster, index_no) else ((cluster_no ||> cluster_skolem ? Integer.add 1, skolem), 0) val s' = zapped_var_name cluster index_no s' in t1 $ Abs (s', T, aux cluster (index_no + 1) pos t') end else t | (t1 as Const (s, _)) $ t2 $ t3 => if s = \<^const_name>\Pure.imp\ orelse s = \<^const_name>\HOL.implies\ then t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3 else if s = \<^const_name>\HOL.conj\ orelse s = \<^const_name>\HOL.disj\ then t1 $ aux cluster index_no pos t2 $ aux cluster index_no pos t3 else t | (t1 as Const (s, _)) $ t2 => if s = \<^const_name>\Trueprop\ then t1 $ aux cluster index_no pos t2 else if s = \<^const_name>\Not\ then t1 $ aux cluster index_no (not pos) t2 else t | _ => t in aux ((ax_no, 0), true) 0 true end fun zap pos ct = ct |> (case Thm.term_of ct of Const (s, _) $ Abs _ => if s = \<^const_name>\Pure.all\ orelse s = \<^const_name>\All\ orelse s = \<^const_name>\Ex\ then Thm.dest_comb #> snd #> Thm.dest_abs_global #> snd #> zap pos else Conv.all_conv | Const (s, _) $ _ $ _ => if s = \<^const_name>\Pure.imp\ orelse s = \<^const_name>\implies\ then Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos) else if s = \<^const_name>\conj\ orelse s = \<^const_name>\disj\ then Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos) else Conv.all_conv | Const (s, _) $ _ => if s = \<^const_name>\Trueprop\ then Conv.arg_conv (zap pos) else if s = \<^const_name>\Not\ then Conv.arg_conv (zap (not pos)) else Conv.all_conv | _ => Conv.all_conv) fun ss_only ths ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths val cheat_choice = \<^prop>\\x. \y. Q x y \ \f. \x. Q x (f x)\ |> Logic.varify_global |> Skip_Proof.make_thm \<^theory> (* Converts an Isabelle theorem into NNF. *) fun nnf_axiom simp_options choice_ths new_skolem ax_no th ctxt = let val thy = Proof_Context.theory_of ctxt val th = th |> transform_elim_theorem |> zero_var_indexes |> new_skolem ? Thm.forall_intr_vars val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt) |> Meson.cong_extensionalize_thm ctxt |> Meson.abs_extensionalize_thm ctxt |> Meson.make_nnf simp_options ctxt in if new_skolem then let fun skolemize choice_ths = Meson.skolemize_with_choice_theorems simp_options ctxt choice_ths #> simplify (ss_only @{thms all_simps[symmetric]} ctxt) val no_choice = null choice_ths val pull_out = if no_choice then simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]} ctxt) else skolemize choice_ths val discharger_th = th |> pull_out val discharger_th = discharger_th |> Meson.has_too_many_clauses ctxt (Thm.concl_of discharger_th) ? (to_definitional_cnf_with_quantifiers ctxt #> pull_out) val zapped_th = discharger_th |> Thm.prop_of |> rename_bound_vars_to_be_zapped ax_no |> (if no_choice then Skip_Proof.make_thm thy #> skolemize [cheat_choice] #> Thm.cprop_of else Thm.cterm_of ctxt) |> zap true val fixes = [] |> Term.add_free_names (Thm.prop_of zapped_th) |> filter is_zapped_var_name val ctxt' = ctxt |> Variable.add_fixes_direct fixes val fully_skolemized_t = zapped_th |> singleton (Variable.export ctxt' ctxt) |> Thm.cprop_of |> Thm.dest_equals |> snd |> Thm.term_of in if exists_subterm (fn Var ((s, _), _) => String.isPrefix new_skolem_var_prefix s | _ => false) fully_skolemized_t then let val (fully_skolemized_ct, ctxt) = yield_singleton (Variable.import_terms true) fully_skolemized_t ctxt |>> Thm.cterm_of ctxt in (SOME (discharger_th, fully_skolemized_ct), (Thm.assume fully_skolemized_ct, ctxt)) end else (NONE, (th, ctxt)) end else (NONE, (th |> Meson.has_too_many_clauses ctxt (Thm.concl_of th) ? to_definitional_cnf_with_quantifiers ctxt, ctxt)) end (* Convert a theorem to CNF, with additional premises due to skolemization. *) fun cnf_axiom simp_options ctxt0 new_skolem combinators ax_no th = let val choice_ths = Meson.choice_theorems (Proof_Context.theory_of ctxt0) val (opt, (nnf_th, ctxt1)) = nnf_axiom simp_options choice_ths new_skolem ax_no th ctxt0 fun clausify th = Meson.make_cnf (if new_skolem orelse null choice_ths then [] else map (old_skolem_theorem_of_def ctxt1) (old_skolem_defs th)) th ctxt1 val (cnf_ths, ctxt2) = clausify nnf_th fun intr_imp ct th = Thm.instantiate (TVars.empty, Vars.make [(\<^var>\?i::nat\, Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no))]) (zero_var_indexes @{thm skolem_COMBK_D}) RS Thm.implies_intr ct th in (opt |> Option.map (I #>> singleton (Variable.export ctxt2 ctxt0) ##> (Thm.term_of #> HOLogic.dest_Trueprop #> singleton (Variable.export_terms ctxt2 ctxt0))), cnf_ths |> map (combinators ? introduce_combinators_in_theorem ctxt2 #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I)) |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf |> map (Thm.close_derivation \<^here>)) end handle THM _ => (NONE, []) end; diff --git a/src/HOL/Tools/Metis/metis_tactic.ML b/src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML +++ b/src/HOL/Tools/Metis/metis_tactic.ML @@ -1,311 +1,315 @@ (* Title: HOL/Tools/Metis/metis_tactic.ML Author: Kong W. Susanto, Cambridge University Computer Laboratory Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Copyright Cambridge University 2007 HOL setup for the Metis prover. *) signature METIS_TACTIC = sig val trace : bool Config.T val verbose : bool Config.T val new_skolem : bool Config.T val advisory_simp : bool Config.T val metis_tac_unused : string list -> string -> Proof.context -> thm list -> int -> thm -> thm list * thm Seq.seq val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic val metis_method : (string list option * string option) * thm list -> Proof.context -> thm list -> tactic val metis_lam_transs : string list val parse_metis_options : (string list option * string option) parser end structure Metis_Tactic : METIS_TACTIC = struct open ATP_Problem_Generate open ATP_Proof_Reconstruct open Metis_Generate open Metis_Reconstruct val new_skolem = Attrib.setup_config_bool \<^binding>\metis_new_skolem\ (K false) val advisory_simp = Attrib.setup_config_bool \<^binding>\metis_advisory_simp\ (K true) (* Designed to work also with monomorphic instances of polymorphic theorems. *) fun have_common_thm ctxt ths1 ths2 = exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1) (map (Meson.make_meta_clause ctxt) ths2) (*Determining which axiom clauses are actually used*) fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) | used_axioms _ _ = NONE (* Lightweight predicate type information comes in two flavors, "t = t'" and "t => t'", where "t" and "t'" are the same term modulo type tags. In Isabelle, type tags are stripped away, so we are left with "t = t" or "t => t". Type tag idempotence is also handled this way. *) fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth = (case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of \<^Const_>\HOL.eq _ for _ t\ => let val ct = Thm.cterm_of ctxt t val cT = Thm.ctyp_of_cterm ct in refl |> Thm.instantiate' [SOME cT] [SOME ct] end | \<^Const_>\disj for t1 t2\ => (if can HOLogic.dest_not t1 then t2 else t1) |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial | _ => raise Fail "expected reflexive or trivial clause") |> Meson.make_meta_clause ctxt fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth = let - val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac ctxt [refl] 1 val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t) in - Goal.prove_internal ctxt [] ct (K tac) + Goal.prove_internal ctxt [] ct + (fn {context = goal_ctxt, ...} => + rewrite_goals_tac goal_ctxt @{thms lambda_def [abs_def]} THEN + resolve_tac goal_ctxt [refl] 1) |> Meson.make_meta_clause ctxt end fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u] | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t | add_vars_and_frees (t as Var _) = insert (op =) t | add_vars_and_frees (t as Free _) = insert (op =) t | add_vars_and_frees _ = I fun introduce_lam_wrappers ctxt th = if Meson_Clausify.is_quasi_lambda_free (Thm.prop_of th) then th else let fun conv first ctxt ct = if Meson_Clausify.is_quasi_lambda_free (Thm.term_of ct) then Thm.reflexive ct else (case Thm.term_of ct of Abs (_, _, u) => if first then (case add_vars_and_frees u [] of [] => Conv.abs_conv (conv false o snd) ctxt ct |> (fn th => Meson.first_order_resolve ctxt th @{thm Metis.eq_lambdaI}) | v :: _ => Abs (Name.uu, fastype_of v, abstract_over (v, Thm.term_of ct)) $ v |> Thm.cterm_of ctxt |> Conv.comb_conv (conv true ctxt)) else Conv.abs_conv (conv false o snd) ctxt ct | \<^Const_>\Meson.skolem _ for _\ => Thm.reflexive ct | _ => Conv.comb_conv (conv true ctxt) ct) val eq_th = conv true ctxt (Thm.cprop_of th) (* We replace the equation's left-hand side with a beta-equivalent term so that "Thm.equal_elim" works below. *) val t0 $ _ $ t2 = Thm.prop_of eq_th val eq_ct = t0 $ Thm.prop_of th $ t2 |> Thm.cterm_of ctxt - val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (resolve_tac ctxt [eq_th] 1)) + val eq_th' = + Goal.prove_internal ctxt [] eq_ct + (fn {context = goal_ctxt, ...} => resolve_tac goal_ctxt [eq_th] 1) in Thm.equal_elim eq_th' th end fun clause_params ordering = {ordering = ordering, orderLiterals = Metis_Clause.UnsignedLiteralOrder, orderTerms = true} fun active_params ordering = {clause = clause_params ordering, prefactor = #prefactor Metis_Active.default, postfactor = #postfactor Metis_Active.default} val waiting_params = {symbolsWeight = 1.0, variablesWeight = 0.05, literalsWeight = 0.01, models = []} fun resolution_params ordering = {active = active_params ordering, waiting = waiting_params} fun kbo_advisory_simp_ordering ord_info = let fun weight (m, _) = AList.lookup (op =) ord_info (Metis_Name.toString m) |> the_default 1 fun precedence p = (case int_ord (apply2 weight p) of EQUAL => #precedence Metis_KnuthBendixOrder.default p | ord => ord) in {weight = weight, precedence = precedence} end fun metis_call type_enc lam_trans = let val type_enc = (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of [alias] => alias | _ => type_enc) val opts = [] |> type_enc <> partial_typesN ? cons type_enc |> lam_trans <> default_metis_lam_trans ? cons lam_trans in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end exception METIS_UNPROVABLE of unit (* Main function to start Metis proof and reconstruction *) fun FOL_SOLVE unused type_encs lam_trans ctxt cls ths0 = let val thy = Proof_Context.theory_of ctxt val new_skolem = Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy) val do_lams = lam_trans = liftingN ? introduce_lam_wrappers ctxt val th_cls_pairs = map2 (fn j => fn th => (Thm.get_name_hint th, th |> Drule.eta_contraction_rule |> Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt new_skolem (lam_trans = combsN) j ||> map do_lams)) (0 upto length ths0 - 1) ths0 val ths = maps (snd o snd) th_cls_pairs val dischargers = map (fst o snd) th_cls_pairs val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES") val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls val type_enc :: fallback_type_encs = type_encs val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) val type_enc = type_enc_of_string Strict type_enc val (sym_tab, axioms, ord_info, concealed) = generate_metis_problem ctxt type_enc lam_trans cls ths fun get_isa_thm mth Isa_Reflexive_or_Trivial = reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth | get_isa_thm mth Isa_Lambda_Lifted = lam_lifted_of_metis ctxt type_enc sym_tab concealed mth | get_isa_thm _ (Isa_Raw ith) = ith val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith |> Thm.close_derivation \<^here>)) val _ = trace_msg ctxt (K "ISABELLE CLAUSES") val _ = List.app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms val _ = trace_msg ctxt (K "METIS CLAUSES") val _ = List.app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms val _ = trace_msg ctxt (K "START METIS PROVE PROCESS") val ordering = if Config.get ctxt advisory_simp then kbo_advisory_simp_ordering (ord_info ()) else Metis_KnuthBendixOrder.default fun fall_back () = (verbose_warning ctxt ("Falling back on " ^ quote (metis_call (hd fallback_type_encs) lam_trans) ^ "..."); FOL_SOLVE unused fallback_type_encs lam_trans ctxt cls ths0) in (case filter (fn t => Thm.prop_of t aconv \<^prop>\False\) cls of false_th :: _ => [false_th RS @{thm FalseE}] | [] => (case Metis_Resolution.loop (Metis_Resolution.new (resolution_params ordering) {axioms = axioms |> map fst, conjecture = []}) of Metis_Resolution.Contradiction mth => let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ Metis_Thm.toString mth) val ctxt' = fold Variable.declare_constraints (map Thm.prop_of cls) ctxt (*add constraints arising from converting goal to clause form*) val proof = Metis_Proof.proof mth val result = fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof axioms val used = map_filter (used_axioms axioms) proof val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:") val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used val unused_th_cls_pairs = filter_out (have_common_thm ctxt used o #2 o #2) th_cls_pairs val _ = unused := maps (#2 o #2) unused_th_cls_pairs; val _ = if not (null unused_th_cls_pairs) then verbose_warning ctxt ("Unused theorems: " ^ commas_quote (map #1 unused_th_cls_pairs)) else (); val _ = if not (null cls) andalso not (have_common_thm ctxt used cls) then verbose_warning ctxt "The assumptions are inconsistent" else (); in (case result of (_, ith) :: _ => (trace_msg ctxt (fn () => "Success: " ^ Thm.string_of_thm ctxt ith); [discharge_skolem_premises ctxt dischargers ith]) | _ => (trace_msg ctxt (K "Metis: No result"); [])) end | Metis_Resolution.Satisfiable _ => (trace_msg ctxt (K "Metis: No first-order proof with the supplied lemmas"); raise METIS_UNPROVABLE ())) handle METIS_UNPROVABLE () => if null fallback_type_encs then [] else fall_back () | METIS_RECONSTRUCT (loc, msg) => if null fallback_type_encs then (verbose_warning ctxt ("Failed to replay Metis proof\n" ^ loc ^ ": " ^ msg); []) else fall_back ()) end fun neg_clausify ctxt combinators = single #> Meson.make_clauses_unsorted ctxt #> combinators ? map (Meson_Clausify.introduce_combinators_in_theorem ctxt) #> Meson.finish_cnf fun preskolem_tac ctxt st0 = (if exists (Meson.has_too_many_clauses ctxt) (Logic.prems_of_goal (Thm.prop_of st0) 1) then Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex} ctxt) 1 THEN CNF.cnfx_rewrite_tac ctxt 1 else all_tac) st0 fun metis_tac_unused type_encs0 lam_trans ctxt ths i st0 = let val unused = Unsynchronized.ref [] val type_encs = if null type_encs0 then partial_type_encs else type_encs0 val _ = trace_msg ctxt (fn () => "Metis called with theorems\n" ^ cat_lines (map (Thm.string_of_thm ctxt) ths)) val type_encs = type_encs |> maps unalias_type_enc val combs = (lam_trans = combsN) fun tac clause = resolve_tac ctxt (FOL_SOLVE unused type_encs lam_trans ctxt clause ths) 1 val seq = Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt combs)) tac ctxt i st0 in (!unused, seq) end fun metis_tac type_encs lam_trans ctxt ths i = snd o metis_tac_unused type_encs lam_trans ctxt ths i (* Whenever "X" has schematic type variables, we treat "using X by metis" as "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables. We don't do it for nonschematic facts "X" because this breaks a few proofs (in the rare and subtle case where a proof relied on extensionality not being applied) and brings few benefits. *) val has_tvar = exists_type (exists_subtype (fn TVar _ => true | _ => false)) o Thm.prop_of fun metis_method ((override_type_encs, lam_trans), ths) ctxt facts = let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in HEADGOAL (Method.insert_tac ctxt nonschem_facts THEN' CHANGED_PROP o metis_tac (these override_type_encs) (the_default default_metis_lam_trans lam_trans) ctxt (schem_facts @ ths)) end val metis_lam_transs = [opaque_liftingN, liftingN, combsN] fun set_opt _ x NONE = SOME x | set_opt get x (SOME x0) = error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x)) fun consider_opt s = if s = "hide_lams" then error "\"hide_lams\" has been renamed \"opaque_lifting\"" else if member (op =) metis_lam_transs s then apsnd (set_opt I s) else apfst (set_opt hd [s]) val parse_metis_options = Scan.optional (Args.parens (Args.name -- Scan.option (\<^keyword>\,\ |-- Args.name)) >> (fn (s, s') => (NONE, NONE) |> consider_opt s |> (case s' of SOME s' => consider_opt s' | _ => I))) (NONE, NONE) val _ = Theory.setup (Method.setup \<^binding>\metis\ (Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo metis_method)) "Metis for FOL and HOL problems") end; diff --git a/src/HOL/Tools/Qelim/cooper.ML b/src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML +++ b/src/HOL/Tools/Qelim/cooper.ML @@ -1,917 +1,918 @@ (* Title: HOL/Tools/Qelim/cooper.ML Author: Amine Chaieb, TU Muenchen Presburger arithmetic by Cooper's algorithm. *) signature COOPER = sig type entry val get: Proof.context -> entry val del: term list -> attribute val add: term list -> attribute exception COOPER of string val conv: Proof.context -> conv val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic end; structure Cooper: COOPER = struct type entry = simpset * term list; val allowed_consts = [\<^term>\(+) :: int => _\, \<^term>\(+) :: nat => _\, \<^term>\(-) :: int => _\, \<^term>\(-) :: nat => _\, \<^term>\(*) :: int => _\, \<^term>\(*) :: nat => _\, \<^term>\(div) :: int => _\, \<^term>\(div) :: nat => _\, \<^term>\(mod) :: int => _\, \<^term>\(mod) :: nat => _\, \<^term>\HOL.conj\, \<^term>\HOL.disj\, \<^term>\HOL.implies\, \<^term>\(=) :: int => _\, \<^term>\(=) :: nat => _\, \<^term>\(=) :: bool => _\, \<^term>\(<) :: int => _\, \<^term>\(<) :: nat => _\, \<^term>\(<=) :: int => _\, \<^term>\(<=) :: nat => _\, \<^term>\(dvd) :: int => _\, \<^term>\(dvd) :: nat => _\, \<^term>\abs :: int => _\, \<^term>\max :: int => _\, \<^term>\max :: nat => _\, \<^term>\min :: int => _\, \<^term>\min :: nat => _\, \<^term>\uminus :: int => _\, (*@ {term "uminus :: nat => _"},*) \<^term>\Not\, \<^term>\Suc\, \<^term>\Ex :: (int => _) => _\, \<^term>\Ex :: (nat => _) => _\, \<^term>\All :: (int => _) => _\, \<^term>\All :: (nat => _) => _\, \<^term>\nat\, \<^term>\int\, \<^term>\Num.One\, \<^term>\Num.Bit0\, \<^term>\Num.Bit1\, \<^term>\Num.numeral :: num => int\, \<^term>\Num.numeral :: num => nat\, \<^term>\0::int\, \<^term>\1::int\, \<^term>\0::nat\, \<^term>\1::nat\, \<^term>\True\, \<^term>\False\]; structure Data = Generic_Data ( type T = simpset * term list; val empty = (HOL_ss, allowed_consts); val extend = I; fun merge ((ss1, ts1), (ss2, ts2)) = (merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2)); ); val get = Data.get o Context.Proof; fun add ts = Thm.declaration_attribute (fn th => fn context => context |> Data.map (fn (ss, ts') => (simpset_map (Context.proof_of context) (fn ctxt => ctxt addsimps [th]) ss, merge (op aconv) (ts', ts)))) fun del ts = Thm.declaration_attribute (fn th => fn context => context |> Data.map (fn (ss, ts') => (simpset_map (Context.proof_of context) (fn ctxt => ctxt delsimps [th]) ss, subtract (op aconv) ts' ts))) fun simp_thms_conv ctxt = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms}); val FWD = Drule.implies_elim_list; val true_tm = \<^cterm>\True\; val false_tm = \<^cterm>\False\; val presburger_ss = simpset_of (\<^context> addsimps @{thms zdvd1_eq}); val lin_ss = simpset_of (put_simpset presburger_ss \<^context> addsimps (@{thms dvd_eq_mod_eq_0 add.assoc [where 'a = int] add.commute [where 'a = int] add.left_commute [where 'a = int] mult.assoc [where 'a = int] mult.commute [where 'a = int] mult.left_commute [where 'a = int] })); val iT = HOLogic.intT val bT = HOLogic.boolT; val dest_number = HOLogic.dest_number #> snd; val perhaps_number = try dest_number; val is_number = can dest_number; val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] = map (Thm.instantiate' [SOME \<^ctyp>\int\] []) @{thms "minf"}; val [infDconj, infDdisj, infDdvd,infDndvd,infDP] = map (Thm.instantiate' [SOME \<^ctyp>\int\] []) @{thms "inf_period"}; val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] = map (Thm.instantiate' [SOME \<^ctyp>\int\] []) @{thms "pinf"}; val [miP, piP] = map (Thm.instantiate' [SOME \<^ctyp>\bool\] []) [miP, piP]; val infDP = Thm.instantiate' (map SOME [\<^ctyp>\int\, \<^ctyp>\bool\]) [] infDP; val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle, asetgt, asetge, asetdvd, asetndvd,asetP], [bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle, bsetgt, bsetge, bsetdvd, bsetndvd,bsetP]] = [@{thms "aset"}, @{thms "bset"}]; val [cpmi, cppi] = [@{thm "cpmi"}, @{thm "cppi"}]; val unity_coeff_ex = Thm.instantiate' [SOME \<^ctyp>\int\] [] @{thm "unity_coeff_ex"}; val [zdvd_mono,simp_from_to,all_not_ex] = [@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}]; val [dvd_uminus, dvd_uminus'] = @{thms "uminus_dvd_conv"}; val eval_ss = simpset_of (put_simpset presburger_ss \<^context> addsimps [simp_from_to] delsimps [insert_iff, bex_triv]); fun eval_conv ctxt = Simplifier.rewrite (put_simpset eval_ss ctxt); (* recognising cterm without moving to terms *) datatype fm = And of cterm*cterm| Or of cterm*cterm| Eq of cterm | NEq of cterm | Lt of cterm | Le of cterm | Gt of cterm | Ge of cterm | Dvd of cterm*cterm | NDvd of cterm*cterm | Nox fun whatis x ct = ( case Thm.term_of ct of Const(\<^const_name>\HOL.conj\,_)$_$_ => And (Thm.dest_binop ct) | Const (\<^const_name>\HOL.disj\,_)$_$_ => Or (Thm.dest_binop ct) | Const (\<^const_name>\HOL.eq\,_)$y$_ => if Thm.term_of x aconv y then Eq (Thm.dest_arg ct) else Nox | Const (\<^const_name>\Not\,_) $ (Const (\<^const_name>\HOL.eq\,_)$y$_) => if Thm.term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox | Const (\<^const_name>\Orderings.less\, _) $ y$ z => if Thm.term_of x aconv y then Lt (Thm.dest_arg ct) else if Thm.term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox | Const (\<^const_name>\Orderings.less_eq\, _) $ y $ z => if Thm.term_of x aconv y then Le (Thm.dest_arg ct) else if Thm.term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox | Const (\<^const_name>\Rings.dvd\,_)$_$(Const(\<^const_name>\Groups.plus\,_)$y$_) => if Thm.term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox | Const (\<^const_name>\Not\,_) $ (Const (\<^const_name>\Rings.dvd\,_)$_$(Const(\<^const_name>\Groups.plus\,_)$y$_)) => if Thm.term_of x aconv y then NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox | _ => Nox) handle CTERM _ => Nox; fun get_pmi_term t = let val (x,eq) = (Thm.dest_abs_global o Thm.dest_arg o snd o Thm.dest_abs_global o Thm.dest_arg) (Thm.dest_arg t) in (Thm.lambda x o Thm.dest_arg o Thm.dest_arg) eq end; val get_pmi = get_pmi_term o Thm.cprop_of; val p_v' = (("P'", 0), \<^typ>\int \ bool\); val q_v' = (("Q'", 0), \<^typ>\int \ bool\); val p_v = (("P", 0), \<^typ>\int \ bool\); val q_v = (("Q", 0), \<^typ>\int \ bool\); fun myfwd (th1, th2, th3) p q [(th_1,th_2,th_3), (th_1',th_2',th_3')] = let val (mp', mq') = (get_pmi th_1, get_pmi th_1') val mi_th = FWD (Drule.instantiate_normalize (TVars.empty, Vars.make [(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1) [th_1, th_1'] val infD_th = FWD (Drule.instantiate_normalize (TVars.empty, Vars.make [(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3'] val set_th = FWD (Drule.instantiate_normalize (TVars.empty, Vars.make [(p_v,p), (q_v,q)]) th2) [th_2, th_2'] in (mi_th, set_th, infD_th) end; val inst' = fn cts => Thm.instantiate' [] (map SOME cts); val infDTrue = Thm.instantiate' [] [SOME true_tm] infDP; val infDFalse = Thm.instantiate' [] [SOME false_tm] infDP; val cadd = \<^cterm>\(+) :: int => _\ val cmulC = \<^cterm>\(*) :: int => _\ val cminus = \<^cterm>\(-) :: int => _\ val cone = \<^cterm>\1 :: int\ val [addC, mulC, subC] = map Thm.term_of [cadd, cmulC, cminus] val [zero, one] = [\<^term>\0 :: int\, \<^term>\1 :: int\]; fun numeral1 f n = HOLogic.mk_number iT (f (dest_number n)); fun numeral2 f m n = HOLogic.mk_number iT (f (dest_number m) (dest_number n)); val [minus1,plus1] = map (fn c => fn t => Thm.apply (Thm.apply c t) cone) [cminus,cadd]; fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle, asetgt, asetge,asetdvd,asetndvd,asetP, infDdvd, infDndvd, asetconj, asetdisj, infDconj, infDdisj] cp = case (whatis x cp) of And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.lambda x p) (Thm.lambda x q)) | Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.lambda x p) (Thm.lambda x q)) | Eq t => ([], K (inst' [t] pieq, FWD (inst' [t] aseteq) [inS (plus1 t)], infDFalse)) | NEq t => ([], K (inst' [t] pineq, FWD (inst' [t] asetneq) [inS t], infDTrue)) | Lt t => ([], K (inst' [t] pilt, FWD (inst' [t] asetlt) [inS t], infDFalse)) | Le t => ([], K (inst' [t] pile, FWD (inst' [t] asetle) [inS (plus1 t)], infDFalse)) | Gt t => ([], K (inst' [t] pigt, (inst' [t] asetgt), infDTrue)) | Ge t => ([], K (inst' [t] pige, (inst' [t] asetge), infDTrue)) | Dvd (d,s) => ([],let val dd = dvd d in K (inst' [d,s] pidvd, FWD (inst' [d,s] asetdvd) [dd],FWD (inst' [d,s] infDdvd) [dd]) end) | NDvd(d,s) => ([],let val dd = dvd d in K (inst' [d,s] pindvd, FWD (inst' [d,s] asetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end) | _ => ([], K (inst' [cp] piP, inst' [cp] asetP, inst' [cp] infDP)); fun decomp_minf x dvd inS [bseteq,bsetneq,bsetlt, bsetle, bsetgt, bsetge,bsetdvd,bsetndvd,bsetP, infDdvd, infDndvd, bsetconj, bsetdisj, infDconj, infDdisj] cp = case (whatis x cp) of And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.lambda x p) (Thm.lambda x q)) | Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.lambda x p) (Thm.lambda x q)) | Eq t => ([], K (inst' [t] mieq, FWD (inst' [t] bseteq) [inS (minus1 t)], infDFalse)) | NEq t => ([], K (inst' [t] mineq, FWD (inst' [t] bsetneq) [inS t], infDTrue)) | Lt t => ([], K (inst' [t] milt, (inst' [t] bsetlt), infDTrue)) | Le t => ([], K (inst' [t] mile, (inst' [t] bsetle), infDTrue)) | Gt t => ([], K (inst' [t] migt, FWD (inst' [t] bsetgt) [inS t], infDFalse)) | Ge t => ([], K (inst' [t] mige,FWD (inst' [t] bsetge) [inS (minus1 t)], infDFalse)) | Dvd (d,s) => ([],let val dd = dvd d in K (inst' [d,s] midvd, FWD (inst' [d,s] bsetdvd) [dd] , FWD (inst' [d,s] infDdvd) [dd]) end) | NDvd (d,s) => ([],let val dd = dvd d in K (inst' [d,s] mindvd, FWD (inst' [d,s] bsetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end) | _ => ([], K (inst' [cp] miP, inst' [cp] bsetP, inst' [cp] infDP)) (* Canonical linear form for terms, formulae etc.. *) fun provelin ctxt t = Goal.prove ctxt [] [] t (fn _ => EVERY [simp_tac (put_simpset lin_ss ctxt) 1, TRY (Lin_Arith.tac ctxt 1)]); fun linear_cmul 0 tm = zero | linear_cmul n tm = case tm of Const (\<^const_name>\Groups.plus\, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b | Const (\<^const_name>\Groups.times\, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x | Const (\<^const_name>\Groups.minus\, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b | (m as Const (\<^const_name>\Groups.uminus\, _)) $ a => m $ linear_cmul n a | _ => numeral1 (fn m => n * m) tm; fun earlier [] x y = false | earlier (h::t) x y = if h aconv y then false else if h aconv x then true else earlier t x y; fun linear_add vars tm1 tm2 = case (tm1, tm2) of (Const (\<^const_name>\Groups.plus\, _) $ (Const (\<^const_name>\Groups.times\, _) $ c1 $ x1) $ r1, Const (\<^const_name>\Groups.plus\, _) $ (Const (\<^const_name>\Groups.times\, _) $ c2 $ x2) $ r2) => if x1 = x2 then let val c = numeral2 Integer.add c1 c2 in if c = zero then linear_add vars r1 r2 else addC$(mulC$c$x1)$(linear_add vars r1 r2) end else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2 | (Const (\<^const_name>\Groups.plus\, _) $ (Const (\<^const_name>\Groups.times\, _) $ c1 $ x1) $ r1, _) => addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 | (_, Const (\<^const_name>\Groups.plus\, _) $ (Const (\<^const_name>\Groups.times\, _) $ c2 $ x2) $ r2) => addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2 | (_, _) => numeral2 Integer.add tm1 tm2; fun linear_neg tm = linear_cmul ~1 tm; fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); exception COOPER of string; fun lint vars tm = if is_number tm then tm else case tm of Const (\<^const_name>\Groups.uminus\, _) $ t => linear_neg (lint vars t) | Const (\<^const_name>\Groups.plus\, _) $ s $ t => linear_add vars (lint vars s) (lint vars t) | Const (\<^const_name>\Groups.minus\, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t) | Const (\<^const_name>\Groups.times\, _) $ s $ t => let val s' = lint vars s val t' = lint vars t in case perhaps_number s' of SOME n => linear_cmul n t' | NONE => (case perhaps_number t' of SOME n => linear_cmul n s' | NONE => raise COOPER "lint: not linear") end | _ => addC $ (mulC $ one $ tm) $ zero; fun lin (vs as _::_) (Const (\<^const_name>\Not\, _) $ (Const (\<^const_name>\Orderings.less\, T) $ s $ t)) = lin vs (Const (\<^const_name>\Orderings.less_eq\, T) $ t $ s) | lin (vs as _::_) (Const (\<^const_name>\Not\,_) $ (Const(\<^const_name>\Orderings.less_eq\, T) $ s $ t)) = lin vs (Const (\<^const_name>\Orderings.less\, T) $ t $ s) | lin vs (Const (\<^const_name>\Not\,T)$t) = Const (\<^const_name>\Not\,T)$ (lin vs t) | lin (vs as _::_) (Const(\<^const_name>\Rings.dvd\,_)$d$t) = HOLogic.mk_binrel \<^const_name>\Rings.dvd\ (numeral1 abs d, lint vs t) | lin (vs as x::_) ((b as Const(\<^const_name>\HOL.eq\,_))$s$t) = (case lint vs (subC$t$s) of (t as _$(m$c$y)$r) => if x <> y then b$zero$t else if dest_number c < 0 then b$(m$(numeral1 ~ c)$y)$r else b$(m$c$y)$(linear_neg r) | t => b$zero$t) | lin (vs as x::_) (b$s$t) = (case lint vs (subC$t$s) of (t as _$(m$c$y)$r) => if x <> y then b$zero$t else if dest_number c < 0 then b$(m$(numeral1 ~ c)$y)$r else b$(linear_neg r)$(m$c$y) | t => b$zero$t) | lin vs fm = fm; fun lint_conv ctxt vs ct = let val t = Thm.term_of ct in (provelin ctxt ((HOLogic.eq_const iT)$t$(lint vs t) |> HOLogic.mk_Trueprop)) RS eq_reflection end; fun is_intrel_type T = T = \<^typ>\int => int => bool\; fun is_intrel (b$_$_) = is_intrel_type (fastype_of b) | is_intrel (\<^term>\Not\$(b$_$_)) = is_intrel_type (fastype_of b) | is_intrel _ = false; fun linearize_conv ctxt vs ct = case Thm.term_of ct of Const(\<^const_name>\Rings.dvd\,_)$_$_ => let val th = Conv.binop_conv (lint_conv ctxt vs) ct val (d',t') = Thm.dest_binop (Thm.rhs_of th) val (dt',tt') = (Thm.term_of d', Thm.term_of t') in if is_number dt' andalso is_number tt' then Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (put_simpset presburger_ss ctxt))) th else let val dth = case perhaps_number (Thm.term_of d') of SOME d => if d < 0 then (Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (lint_conv ctxt vs))) (Thm.transitive th (inst' [d',t'] dvd_uminus)) handle TERM _ => th) else th | NONE => raise COOPER "linearize_conv: not linear" val d'' = Thm.rhs_of dth |> Thm.dest_arg1 in case tt' of Const(\<^const_name>\Groups.plus\,_)$(Const(\<^const_name>\Groups.times\,_)$c$_)$_ => let val x = dest_number c in if x < 0 then Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (lint_conv ctxt vs))) (Thm.transitive dth (inst' [d'',t'] dvd_uminus')) else dth end | _ => dth end end | Const (\<^const_name>\Not\,_)$(Const(\<^const_name>\Rings.dvd\,_)$_$_) => Conv.arg_conv (linearize_conv ctxt vs) ct | t => if is_intrel t then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop)) RS eq_reflection else Thm.reflexive ct; val dvdc = \<^cterm>\(dvd) :: int => _\; fun unify ctxt q = let val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs_global val x = Thm.term_of cx val ins = insert (op = : int * int -> bool) fun h (acc,dacc) t = case Thm.term_of t of Const(s,_)$(Const(\<^const_name>\Groups.times\,_)$c$y)$ _ => if x aconv y andalso member (op =) [\<^const_name>\HOL.eq\, \<^const_name>\Orderings.less\, \<^const_name>\Orderings.less_eq\] s then (ins (dest_number c) acc,dacc) else (acc,dacc) | Const(s,_)$_$(Const(\<^const_name>\Groups.times\,_)$c$y) => if x aconv y andalso member (op =) [\<^const_name>\Orderings.less\, \<^const_name>\Orderings.less_eq\] s then (ins (dest_number c) acc, dacc) else (acc,dacc) | Const(\<^const_name>\Rings.dvd\,_)$_$(Const(\<^const_name>\Groups.plus\,_)$(Const(\<^const_name>\Groups.times\,_)$c$y)$_) => if x aconv y then (acc,ins (dest_number c) dacc) else (acc,dacc) | Const(\<^const_name>\HOL.conj\,_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) | Const(\<^const_name>\HOL.disj\,_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) | Const (\<^const_name>\Not\,_)$_ => h (acc,dacc) (Thm.dest_arg t) | _ => (acc, dacc) val (cs,ds) = h ([],[]) p val l = Integer.lcms (union (op =) cs ds) fun cv k ct = let val (tm as b$s$t) = Thm.term_of ct in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t)) |> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end fun nzprop x = let val th = Simplifier.rewrite (put_simpset lin_ss ctxt) (Thm.apply \<^cterm>\Trueprop\ (Thm.apply \<^cterm>\Not\ (Thm.apply (Thm.apply \<^cterm>\(=) :: int => _\ (Numeral.mk_cnumber \<^ctyp>\int\ x)) \<^cterm>\0::int\))) in Thm.equal_elim (Thm.symmetric th) TrueI end; val notz = let val tab = fold Inttab.update (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty in fn ct => the (Inttab.lookup tab (ct |> Thm.term_of |> dest_number)) handle Option.Option => (writeln ("noz: Theorems-Table contains no entry for " ^ Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option.Option) end fun unit_conv t = case Thm.term_of t of Const(\<^const_name>\HOL.conj\,_)$_$_ => Conv.binop_conv unit_conv t | Const(\<^const_name>\HOL.disj\,_)$_$_ => Conv.binop_conv unit_conv t | Const (\<^const_name>\Not\,_)$_ => Conv.arg_conv unit_conv t | Const(s,_)$(Const(\<^const_name>\Groups.times\,_)$c$y)$ _ => if x=y andalso member (op =) [\<^const_name>\HOL.eq\, \<^const_name>\Orderings.less\, \<^const_name>\Orderings.less_eq\] s then cv (l div dest_number c) t else Thm.reflexive t | Const(s,_)$_$(Const(\<^const_name>\Groups.times\,_)$c$y) => if x=y andalso member (op =) [\<^const_name>\Orderings.less\, \<^const_name>\Orderings.less_eq\] s then cv (l div dest_number c) t else Thm.reflexive t | Const(\<^const_name>\Rings.dvd\,_)$d$(r as (Const(\<^const_name>\Groups.plus\,_)$(Const(\<^const_name>\Groups.times\,_)$c$y)$_)) => if x=y then let val k = l div dest_number c val kt = HOLogic.mk_number iT k val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t] ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono) val (d',t') = (mulC$kt$d, mulC$kt$r) val thc = (provelin ctxt ((HOLogic.eq_const iT)$d'$(lint [] d') |> HOLogic.mk_Trueprop)) RS eq_reflection val tht = (provelin ctxt ((HOLogic.eq_const iT)$t'$(linear_cmul k r) |> HOLogic.mk_Trueprop)) RS eq_reflection in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule dvdc thc) tht) end else Thm.reflexive t | _ => Thm.reflexive t val uth = unit_conv p val clt = Numeral.mk_cnumber \<^ctyp>\int\ l val ltx = Thm.apply (Thm.apply cmulC clt) cx val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth) val th' = inst' [Thm.lambda ltx (Thm.rhs_of uth), clt] unity_coeff_ex val thf = Thm.transitive th (Thm.transitive (Thm.symmetric (Thm.beta_conversion true (Thm.cprop_of th' |> Thm.dest_arg1))) th') val (lth,rth) = Thm.dest_comb (Thm.cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true ||> Thm.beta_conversion true |>> Thm.symmetric in Thm.transitive (Thm.transitive lth thf) rth end; val emptyIS = \<^cterm>\{}::int set\; val insert_tm = \<^cterm>\insert :: int => _\; fun mkISet cts = fold_rev (Thm.apply insert_tm #> Thm.apply) cts emptyIS; val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1; val [A_v,B_v] = map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs_global |> snd |> Thm.dest_arg1 |> Thm.dest_arg |> Thm.dest_abs_global |> snd |> Thm.dest_fun |> Thm.dest_arg |> Thm.term_of |> dest_Var) [asetP, bsetP]; val D_v = (("D", 0), \<^typ>\int\); fun cooperex_conv ctxt vs q = let val uth = unify ctxt q val (x,p) = Thm.dest_abs_global (Thm.dest_arg (Thm.rhs_of uth)) val ins = insert (op aconvc) fun h t (bacc,aacc,dacc) = case (whatis x t) of And (p,q) => h q (h p (bacc,aacc,dacc)) | Or (p,q) => h q (h p (bacc,aacc,dacc)) | Eq t => (ins (minus1 t) bacc, ins (plus1 t) aacc,dacc) | NEq t => (ins t bacc, ins t aacc, dacc) | Lt t => (bacc, ins t aacc, dacc) | Le t => (bacc, ins (plus1 t) aacc,dacc) | Gt t => (ins t bacc, aacc,dacc) | Ge t => (ins (minus1 t) bacc, aacc,dacc) | Dvd (d,_) => (bacc,aacc,insert (op =) (Thm.term_of d |> dest_number) dacc) | NDvd (d,_) => (bacc,aacc,insert (op =) (Thm.term_of d|> dest_number) dacc) | _ => (bacc, aacc, dacc) val (b0,a0,ds) = h p ([],[],[]) val d = Integer.lcms ds val cd = Numeral.mk_cnumber \<^ctyp>\int\ d fun divprop x = let val th = Simplifier.rewrite (put_simpset lin_ss ctxt) (Thm.apply \<^cterm>\Trueprop\ (Thm.apply (Thm.apply dvdc (Numeral.mk_cnumber \<^ctyp>\int\ x)) cd)) in Thm.equal_elim (Thm.symmetric th) TrueI end; val dvd = let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in fn ct => the (Inttab.lookup tab (Thm.term_of ct |> dest_number)) handle Option.Option => (writeln ("dvd: Theorems-Table contains no entry for" ^ Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option.Option) end val dp = let val th = Simplifier.rewrite (put_simpset lin_ss ctxt) (Thm.apply \<^cterm>\Trueprop\ (Thm.apply (Thm.apply \<^cterm>\(<) :: int => _\ \<^cterm>\0::int\) cd)) in Thm.equal_elim (Thm.symmetric th) TrueI end; (* A and B set *) local val insI1 = Thm.instantiate' [SOME \<^ctyp>\int\] [] @{thm "insertI1"} val insI2 = Thm.instantiate' [SOME \<^ctyp>\int\] [] @{thm "insertI2"} in fun provein x S = case Thm.term_of S of Const(\<^const_name>\Orderings.bot\, _) => error "Unexpected error in Cooper, please email Amine Chaieb" | Const(\<^const_name>\insert\, _) $ y $ _ => let val (cy,S') = Thm.dest_binop S in if Thm.term_of x aconv y then Thm.instantiate' [] [SOME x, SOME S'] insI1 else Thm.implies_elim (Thm.instantiate' [] [SOME x, SOME S', SOME cy] insI2) (provein x S') end end val al = map (lint vs o Thm.term_of) a0 val bl = map (lint vs o Thm.term_of) b0 val (sl,s0,f,abths,cpth) = if length (distinct (op aconv) bl) <= length (distinct (op aconv) al) then (bl,b0,decomp_minf, fn B => (map (fn th => Thm.implies_elim (Thm.instantiate (TVars.empty, Vars.make [(B_v,B), (D_v,cd)]) th) dp) [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@ (map (Thm.instantiate (TVars.empty, Vars.make [(B_v,B), (D_v,cd)])) [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj, bsetdisj,infDconj, infDdisj]), cpmi) else (al,a0,decomp_pinf,fn A => (map (fn th => Thm.implies_elim (Thm.instantiate (TVars.empty, Vars.make [(A_v,A), (D_v,cd)]) th) dp) [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@ (map (Thm.instantiate (TVars.empty, Vars.make [(A_v,A), (D_v,cd)])) [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj, asetdisj,infDconj, infDdisj]),cppi) val cpth = let val sths = map (fn (tl,t0) => if tl = Thm.term_of t0 then Thm.instantiate' [SOME \<^ctyp>\int\] [SOME t0] refl else provelin ctxt ((HOLogic.eq_const iT)$tl$(Thm.term_of t0) |> HOLogic.mk_Trueprop)) (sl ~~ s0) val csl = distinct (op aconvc) (map (Thm.cprop_of #> Thm.dest_arg #> Thm.dest_arg1) sths) val S = mkISet csl val inStab = fold (fn ct => fn tab => Termtab.update (Thm.term_of ct, provein ct S) tab) csl Termtab.empty val eqelem_th = Thm.instantiate' [SOME \<^ctyp>\int\] [NONE,NONE, SOME S] eqelem_imp_imp val inS = let val tab = fold Termtab.update (map (fn eq => let val (s,t) = Thm.cprop_of eq |> Thm.dest_arg |> Thm.dest_binop val th = if s aconvc t then the (Termtab.lookup inStab (Thm.term_of s)) else FWD (Thm.instantiate' [] [SOME s, SOME t] eqelem_th) [eq, the (Termtab.lookup inStab (Thm.term_of s))] in (Thm.term_of t, th) end) sths) Termtab.empty in fn ct => the (Termtab.lookup tab (Thm.term_of ct)) handle Option.Option => (writeln ("inS: No theorem for " ^ Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option.Option) end val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p in [dp, inf, nb, pd] MRS cpth end val cpth' = Thm.transitive uth (cpth RS eq_reflection) in Thm.transitive cpth' ((simp_thms_conv ctxt then_conv eval_conv ctxt) (Thm.rhs_of cpth')) end; fun literals_conv bops uops env cv = let fun h t = case Thm.term_of t of b$_$_ => if member (op aconv) bops b then Conv.binop_conv h t else cv env t | u$_ => if member (op aconv) uops u then Conv.arg_conv h t else cv env t | _ => cv env t in h end; fun integer_nnf_conv ctxt env = nnf_conv ctxt then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt); val conv_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps (@{thms simp_thms} @ take 4 @{thms ex_simps} @ [not_all, all_not_ex, @{thm ex_disj_distrib}])); fun conv ctxt p = Qelim.gen_qelim_conv ctxt (Simplifier.rewrite (put_simpset conv_ss ctxt)) (Simplifier.rewrite (put_simpset presburger_ss ctxt)) (Simplifier.rewrite (put_simpset conv_ss ctxt)) (cons o Thm.term_of) (Misc_Legacy.term_frees (Thm.term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt) (cooperex_conv ctxt) p handle CTERM _ => raise COOPER "bad cterm" | THM _ => raise COOPER "bad thm" | TYPE _ => raise COOPER "bad type" fun add_bools t = let val ops = [\<^term>\(=) :: int => _\, \<^term>\(<) :: int => _\, \<^term>\(<=) :: int => _\, \<^term>\HOL.conj\, \<^term>\HOL.disj\, \<^term>\HOL.implies\, \<^term>\(=) :: bool => _\, \<^term>\Not\, \<^term>\All :: (int => _) => _\, \<^term>\Ex :: (int => _) => _\, \<^term>\True\, \<^term>\False\]; val is_op = member (op =) ops; val skip = not (fastype_of t = HOLogic.boolT) in case t of (l as f $ a) $ b => if skip orelse is_op f then add_bools b o add_bools l else insert (op aconv) t | f $ a => if skip orelse is_op f then add_bools a o add_bools f else insert (op aconv) t | Abs _ => add_bools (snd (Term.dest_abs_global t)) | _ => if skip orelse is_op t then I else insert (op aconv) t end; fun descend vs (abs as (_, xT, _)) = let val ((xn', _), p') = Term.dest_abs_global (Abs abs) in ((xn', xT) :: vs, p') end; local structure Proc = Cooper_Procedure in fun num_of_term vs (Free vT) = Proc.Bound (Proc.nat_of_integer (find_index (fn vT' => vT' = vT) vs)) | num_of_term vs (Term.Bound i) = Proc.Bound (Proc.nat_of_integer i) | num_of_term vs \<^term>\0::int\ = Proc.C (Proc.Int_of_integer 0) | num_of_term vs \<^term>\1::int\ = Proc.C (Proc.Int_of_integer 1) | num_of_term vs (t as Const (\<^const_name>\numeral\, _) $ _) = Proc.C (Proc.Int_of_integer (dest_number t)) | num_of_term vs (Const (\<^const_name>\Groups.uminus\, _) $ t') = Proc.Neg (num_of_term vs t') | num_of_term vs (Const (\<^const_name>\Groups.plus\, _) $ t1 $ t2) = Proc.Add (num_of_term vs t1, num_of_term vs t2) | num_of_term vs (Const (\<^const_name>\Groups.minus\, _) $ t1 $ t2) = Proc.Sub (num_of_term vs t1, num_of_term vs t2) | num_of_term vs (Const (\<^const_name>\Groups.times\, _) $ t1 $ t2) = (case perhaps_number t1 of SOME n => Proc.Mul (Proc.Int_of_integer n, num_of_term vs t2) | NONE => (case perhaps_number t2 of SOME n => Proc.Mul (Proc.Int_of_integer n, num_of_term vs t1) | NONE => raise COOPER "reification: unsupported kind of multiplication")) | num_of_term _ _ = raise COOPER "reification: bad term"; fun fm_of_term ps vs (Const (\<^const_name>\True\, _)) = Proc.T | fm_of_term ps vs (Const (\<^const_name>\False\, _)) = Proc.F | fm_of_term ps vs (Const (\<^const_name>\HOL.conj\, _) $ t1 $ t2) = Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2) | fm_of_term ps vs (Const (\<^const_name>\HOL.disj\, _) $ t1 $ t2) = Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2) | fm_of_term ps vs (Const (\<^const_name>\HOL.implies\, _) $ t1 $ t2) = Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2) | fm_of_term ps vs (\<^term>\(=) :: bool => _ \ $ t1 $ t2) = Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2) | fm_of_term ps vs (Const (\<^const_name>\Not\, _) $ t') = Proc.NOT (fm_of_term ps vs t') | fm_of_term ps vs (Const (\<^const_name>\Ex\, _) $ Abs abs) = Proc.E (uncurry (fm_of_term ps) (descend vs abs)) | fm_of_term ps vs (Const (\<^const_name>\All\, _) $ Abs abs) = Proc.A (uncurry (fm_of_term ps) (descend vs abs)) | fm_of_term ps vs (\<^term>\(=) :: int => _\ $ t1 $ t2) = Proc.Eq (Proc.Sub (num_of_term vs t1, num_of_term vs t2)) | fm_of_term ps vs (Const (\<^const_name>\Orderings.less_eq\, _) $ t1 $ t2) = Proc.Le (Proc.Sub (num_of_term vs t1, num_of_term vs t2)) | fm_of_term ps vs (Const (\<^const_name>\Orderings.less\, _) $ t1 $ t2) = Proc.Lt (Proc.Sub (num_of_term vs t1, num_of_term vs t2)) | fm_of_term ps vs (Const (\<^const_name>\Rings.dvd\, _) $ t1 $ t2) = (case perhaps_number t1 of SOME n => Proc.Dvd (Proc.Int_of_integer n, num_of_term vs t2) | NONE => raise COOPER "reification: unsupported dvd") | fm_of_term ps vs t = let val n = find_index (fn t' => t aconv t') ps in if n > 0 then Proc.Closed (Proc.nat_of_integer n) else raise COOPER "reification: unknown term" end; fun term_of_num vs (Proc.C i) = HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) | term_of_num vs (Proc.Bound n) = Free (nth vs (Proc.integer_of_nat n)) | term_of_num vs (Proc.Neg t') = \<^term>\uminus :: int => _\ $ term_of_num vs t' | term_of_num vs (Proc.Add (t1, t2)) = \<^term>\(+) :: int => _\ $ term_of_num vs t1 $ term_of_num vs t2 | term_of_num vs (Proc.Sub (t1, t2)) = \<^term>\(-) :: int => _\ $ term_of_num vs t1 $ term_of_num vs t2 | term_of_num vs (Proc.Mul (i, t2)) = \<^term>\(*) :: int => _\ $ HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) $ term_of_num vs t2 | term_of_num vs (Proc.CN (n, i, t')) = term_of_num vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t')); fun term_of_fm ps vs Proc.T = \<^term>\True\ | term_of_fm ps vs Proc.F = \<^term>\False\ | term_of_fm ps vs (Proc.And (t1, t2)) = HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 | term_of_fm ps vs (Proc.Or (t1, t2)) = HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 | term_of_fm ps vs (Proc.Imp (t1, t2)) = HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 | term_of_fm ps vs (Proc.Iff (t1, t2)) = \<^term>\(=) :: bool => _\ $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 | term_of_fm ps vs (Proc.NOT t') = HOLogic.Not $ term_of_fm ps vs t' | term_of_fm ps vs (Proc.Eq t') = \<^term>\(=) :: int => _ \ $ term_of_num vs t'$ \<^term>\0::int\ | term_of_fm ps vs (Proc.NEq t') = term_of_fm ps vs (Proc.NOT (Proc.Eq t')) | term_of_fm ps vs (Proc.Lt t') = \<^term>\(<) :: int => _ \ $ term_of_num vs t' $ \<^term>\0::int\ | term_of_fm ps vs (Proc.Le t') = \<^term>\(<=) :: int => _ \ $ term_of_num vs t' $ \<^term>\0::int\ | term_of_fm ps vs (Proc.Gt t') = \<^term>\(<) :: int => _ \ $ \<^term>\0::int\ $ term_of_num vs t' | term_of_fm ps vs (Proc.Ge t') = \<^term>\(<=) :: int => _ \ $ \<^term>\0::int\ $ term_of_num vs t' | term_of_fm ps vs (Proc.Dvd (i, t')) = \<^term>\(dvd) :: int => _ \ $ HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) $ term_of_num vs t' | term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.NOT (Proc.Dvd (i, t'))) | term_of_fm ps vs (Proc.Closed n) = nth ps (Proc.integer_of_nat n) | term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.NOT (Proc.Closed n)); fun procedure t = let val vs = Term.add_frees t []; val ps = add_bools t []; in (term_of_fm ps vs o Proc.pa o fm_of_term ps vs) t end; end; val (_, oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (\<^binding>\cooper\, (fn (ctxt, t) => (Thm.cterm_of ctxt o Logic.mk_equals o apply2 HOLogic.mk_Trueprop) (t, procedure t))))); val comp_ss = simpset_of (put_simpset HOL_ss \<^context> addsimps @{thms semiring_norm}); fun strip_objimp ct = (case Thm.term_of ct of Const (\<^const_name>\HOL.implies\, _) $ _ $ _ => let val (A, B) = Thm.dest_binop ct in A :: strip_objimp B end | _ => [ct]); fun strip_objall ct = case Thm.term_of ct of Const (\<^const_name>\All\, _) $ Abs _ => let val (a,(v,t')) = (apsnd Thm.dest_abs_global o Thm.dest_comb) ct in apfst (cons (a,v)) (strip_objall t') end | _ => ([],ct); local val all_maxscope_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps map (fn th => th RS sym) @{thms "all_simps"}) in fun thin_prems_tac ctxt P = simp_tac (put_simpset all_maxscope_ss ctxt) THEN' CSUBGOAL (fn (p', i) => let val (qvs, p) = strip_objall (Thm.dest_arg p') val (ps, c) = split_last (strip_objimp p) val qs = filter P ps val q = if P c then c else \<^cterm>\False\ val ng = fold_rev (fn (a,v) => fn t => Thm.apply a (Thm.lambda v t)) qvs (fold_rev (fn p => fn q => Thm.apply (Thm.apply \<^cterm>\HOL.implies\ p) q) qs q) val g = Thm.apply (Thm.apply \<^cterm>\(==>)\ (Thm.apply \<^cterm>\Trueprop\ ng)) p' val ntac = (case qs of [] => q aconvc \<^cterm>\False\ | _ => false) in if ntac then no_tac else - (case \<^try>\Goal.prove_internal ctxt [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))\ of + (case \<^try>\Goal.prove_internal ctxt [] g + (fn {context = goal_ctxt, ...} => blast_tac (put_claset HOL_cs goal_ctxt) 1)\ of NONE => no_tac | SOME r => resolve_tac ctxt [r] i) end) end; local fun isnum t = case t of Const(\<^const_name>\Groups.zero\,_) => true | Const(\<^const_name>\Groups.one\,_) => true | \<^term>\Suc\$s => isnum s | \<^term>\nat\$s => isnum s | \<^term>\int\$s => isnum s | Const(\<^const_name>\Groups.uminus\,_)$s => isnum s | Const(\<^const_name>\Groups.plus\,_)$l$r => isnum l andalso isnum r | Const(\<^const_name>\Groups.times\,_)$l$r => isnum l andalso isnum r | Const(\<^const_name>\Groups.minus\,_)$l$r => isnum l andalso isnum r | Const(\<^const_name>\Power.power\,_)$l$r => isnum l andalso isnum r | Const(\<^const_name>\Rings.modulo\,_)$l$r => isnum l andalso isnum r | Const(\<^const_name>\Rings.divide\,_)$l$r => isnum l andalso isnum r | _ => is_number t orelse can HOLogic.dest_nat t fun ty cts t = if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (Thm.typ_of_cterm t)) then false else case Thm.term_of t of c$l$r => if member (op =) [\<^term>\(*)::int => _\, \<^term>\(*)::nat => _\] c then not (isnum l orelse isnum r) else not (member (op aconv) cts c) | c$_ => not (member (op aconv) cts c) | c => not (member (op aconv) cts c) val term_constants = let fun h acc t = case t of Const _ => insert (op aconv) t acc | a$b => h (h acc a) b | Abs (_,_,t) => h acc t | _ => acc in h [] end; in fun is_relevant ctxt ct = subset (op aconv) (term_constants (Thm.term_of ct), snd (get ctxt)) andalso forall (fn Free (_, T) => member (op =) [\<^typ>\int\, \<^typ>\nat\] T) (Misc_Legacy.term_frees (Thm.term_of ct)) andalso forall (fn Var (_, T) => member (op =) [\<^typ>\int\, \<^typ>\nat\] T) (Misc_Legacy.term_vars (Thm.term_of ct)); fun int_nat_terms ctxt ct = let val cts = snd (get ctxt) fun h acc t = if ty cts t then insert (op aconvc) t acc else case Thm.term_of t of _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) | Abs _ => Thm.dest_abs_global t ||> h acc |> uncurry (remove (op aconvc)) | _ => acc in h [] ct end end; fun generalize_tac ctxt f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st => let fun all x t = Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t) val ts = sort Thm.fast_term_ord (f p) val p' = fold_rev all ts p in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end)); local val ss1 = simpset_of (put_simpset comp_ss \<^context> addsimps @{thms simp_thms} @ [@{thm "nat_numeral"} RS sym, @{thm int_dvd_int_iff [symmetric]}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] @ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff" [where ?'a = int]}] |> Splitter.add_split @{thm "zdiff_int_split"}) val ss2 = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps [@{thm "nat_0_le"}, @{thm "of_nat_numeral"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "zero_le_numeral"}, @{thm "le_numeral_extra"(3)}, @{thm "of_nat_0"}, @{thm "of_nat_1"}, @{thm "Suc_eq_plus1"}] |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]) val div_mod_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms simp_thms mod_eq_0_iff_dvd mod_add_left_eq mod_add_right_eq mod_add_eq div_add1_eq [symmetric] div_add1_eq [symmetric] mod_self mod_by_0 div_by_0 div_0 mod_0 div_by_1 mod_by_1 div_by_Suc_0 mod_by_Suc_0 Suc_eq_plus1 ac_simps} addsimprocs [\<^simproc>\cancel_div_mod_nat\, \<^simproc>\cancel_div_mod_int\]) val splits_ss = simpset_of (put_simpset comp_ss \<^context> addsimps [@{thm minus_div_mult_eq_mod [symmetric]}] |> fold Splitter.add_split [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]) in fun nat_to_int_tac ctxt = simp_tac (put_simpset ss1 ctxt) THEN_ALL_NEW simp_tac (put_simpset ss2 ctxt) THEN_ALL_NEW simp_tac (put_simpset comp_ss ctxt); fun div_mod_tac ctxt = simp_tac (put_simpset div_mod_ss ctxt); fun splits_tac ctxt = simp_tac (put_simpset splits_ss ctxt); end; fun core_tac ctxt = CSUBGOAL (fn (p, i) => let val cpth = if Config.get ctxt quick_and_dirty then oracle (ctxt, Envir.beta_norm (Envir.eta_long [] (Thm.term_of (Thm.dest_arg p)))) else Conv.arg_conv (conv ctxt) p val p' = Thm.rhs_of cpth val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p')) in resolve_tac ctxt [th] i end handle COOPER _ => no_tac); fun finish_tac ctxt q = SUBGOAL (fn (_, i) => (if q then I else TRY) (resolve_tac ctxt [TrueI] i)); fun tac elim add_ths del_ths = Subgoal.FOCUS_PARAMS (fn {context = ctxt, ...} => let val simpset_ctxt = put_simpset (fst (get ctxt)) ctxt delsimps del_ths addsimps add_ths in Method.insert_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\arith\)) THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt THEN_ALL_NEW CONVERSION Thm.eta_long_conversion THEN_ALL_NEW simp_tac simpset_ctxt THEN_ALL_NEW (TRY o generalize_tac ctxt (int_nat_terms ctxt)) THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt)) THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt THEN_ALL_NEW div_mod_tac ctxt THEN_ALL_NEW splits_tac ctxt THEN_ALL_NEW simp_tac simpset_ctxt THEN_ALL_NEW CONVERSION Thm.eta_long_conversion THEN_ALL_NEW nat_to_int_tac ctxt THEN_ALL_NEW core_tac ctxt THEN_ALL_NEW finish_tac ctxt elim end 1); (* attribute syntax *) local fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); val constsN = "consts"; val any_keyword = keyword constsN val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm); val terms = thms >> map (Thm.term_of o Drule.dest_term); fun optional scan = Scan.optional scan []; in val _ = Theory.setup (Attrib.setup \<^binding>\presburger\ ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del || optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm" #> Arith_Data.add_tactic "Presburger arithmetic" (tac true [] [])); end; end; diff --git a/src/HOL/Tools/Transfer/transfer.ML b/src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML +++ b/src/HOL/Tools/Transfer/transfer.ML @@ -1,932 +1,932 @@ (* Title: HOL/Tools/Transfer/transfer.ML Author: Brian Huffman, TU Muenchen Author: Ondrej Kuncar, TU Muenchen Generic theorem transfer method. *) signature TRANSFER = sig type pred_data val mk_pred_data: thm -> thm -> thm list -> pred_data val rel_eq_onp: pred_data -> thm val pred_def: pred_data -> thm val pred_simps: pred_data -> thm list val update_pred_simps: thm list -> pred_data -> pred_data val bottom_rewr_conv: thm list -> conv val top_rewr_conv: thm list -> conv val top_sweep_rewr_conv: thm list -> conv val prep_conv: conv val fold_relator_eqs_conv: Proof.context -> conv val unfold_relator_eqs_conv: Proof.context -> conv val get_transfer_raw: Proof.context -> thm list val get_relator_eq: Proof.context -> thm list val retrieve_relator_eq: Proof.context -> term -> thm list val get_sym_relator_eq: Proof.context -> thm list val get_relator_eq_raw: Proof.context -> thm list val get_relator_domain: Proof.context -> thm list val morph_pred_data: morphism -> pred_data -> pred_data val lookup_pred_data: Proof.context -> string -> pred_data option val update_pred_data: string -> pred_data -> Context.generic -> Context.generic val is_compound_lhs: Proof.context -> term -> bool val is_compound_rhs: Proof.context -> term -> bool val transfer_add: attribute val transfer_del: attribute val transfer_raw_add: thm -> Context.generic -> Context.generic val transfer_raw_del: thm -> Context.generic -> Context.generic val transferred_attribute: thm list -> attribute val untransferred_attribute: thm list -> attribute val prep_transfer_domain_thm: Proof.context -> thm -> thm val transfer_domain_add: attribute val transfer_domain_del: attribute val transfer_rule_of_term: Proof.context -> bool -> term -> thm val transfer_rule_of_lhs: Proof.context -> term -> thm val eq_tac: Proof.context -> int -> tactic val transfer_start_tac: bool -> Proof.context -> int -> tactic val transfer_prover_start_tac: Proof.context -> int -> tactic val transfer_step_tac: Proof.context -> int -> tactic val transfer_end_tac: Proof.context -> int -> tactic val transfer_prover_end_tac: Proof.context -> int -> tactic val transfer_tac: bool -> Proof.context -> int -> tactic val transfer_prover_tac: Proof.context -> int -> tactic val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic end structure Transfer : TRANSFER = struct fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) \<^context> fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) \<^context> fun top_sweep_rewr_conv rewrs = Conv.top_sweep_conv (K (Conv.rewrs_conv rewrs)) \<^context> (** Theory Data **) val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o apply2 snd) (single o fst); val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of); datatype pred_data = PRED_DATA of {pred_def: thm, rel_eq_onp: thm, pred_simps: thm list} fun mk_pred_data pred_def rel_eq_onp pred_simps = PRED_DATA {pred_def = pred_def, rel_eq_onp = rel_eq_onp, pred_simps = pred_simps} fun map_pred_data' f1 f2 f3 (PRED_DATA {pred_def, rel_eq_onp, pred_simps}) = PRED_DATA {pred_def = f1 pred_def, rel_eq_onp = f2 rel_eq_onp, pred_simps = f3 pred_simps} fun rep_pred_data (PRED_DATA p) = p val rel_eq_onp = #rel_eq_onp o rep_pred_data val pred_def = #pred_def o rep_pred_data val pred_simps = #pred_simps o rep_pred_data fun update_pred_simps new_pred_data = map_pred_data' I I (K new_pred_data) structure Data = Generic_Data ( type T = { transfer_raw : thm Item_Net.T, known_frees : (string * typ) list, compound_lhs : (term * thm) Item_Net.T, compound_rhs : (term * thm) Item_Net.T, relator_eq : thm Item_Net.T, relator_eq_raw : thm Item_Net.T, relator_domain : thm Item_Net.T, pred_data : pred_data Symtab.table } val empty = { transfer_raw = Thm.item_net_intro, known_frees = [], compound_lhs = compound_xhs_empty_net, compound_rhs = compound_xhs_empty_net, relator_eq = rewr_rules, relator_eq_raw = Thm.item_net, relator_domain = Thm.item_net, pred_data = Symtab.empty } val extend = I fun merge ( { transfer_raw = t1, known_frees = k1, compound_lhs = l1, compound_rhs = c1, relator_eq = r1, relator_eq_raw = rw1, relator_domain = rd1, pred_data = pd1 }, { transfer_raw = t2, known_frees = k2, compound_lhs = l2, compound_rhs = c2, relator_eq = r2, relator_eq_raw = rw2, relator_domain = rd2, pred_data = pd2 } ) = { transfer_raw = Item_Net.merge (t1, t2), known_frees = Library.merge (op =) (k1, k2), compound_lhs = Item_Net.merge (l1, l2), compound_rhs = Item_Net.merge (c1, c2), relator_eq = Item_Net.merge (r1, r2), relator_eq_raw = Item_Net.merge (rw1, rw2), relator_domain = Item_Net.merge (rd1, rd2), pred_data = Symtab.merge (K true) (pd1, pd2) } ) fun get_net_content f ctxt = Item_Net.content (f (Data.get (Context.Proof ctxt))) |> map (Thm.transfer' ctxt) val get_transfer_raw = get_net_content #transfer_raw val get_known_frees = #known_frees o Data.get o Context.Proof fun is_compound f ctxt t = Item_Net.retrieve (f (Data.get (Context.Proof ctxt))) t |> exists (fn (pat, _) => Pattern.matches (Proof_Context.theory_of ctxt) (pat, t)); val is_compound_lhs = is_compound #compound_lhs val is_compound_rhs = is_compound #compound_rhs val get_relator_eq = get_net_content #relator_eq #> map safe_mk_meta_eq fun retrieve_relator_eq ctxt t = Item_Net.retrieve (#relator_eq (Data.get (Context.Proof ctxt))) t |> map (Thm.transfer' ctxt) val get_sym_relator_eq = get_net_content #relator_eq #> map (safe_mk_meta_eq #> Thm.symmetric) val get_relator_eq_raw = get_net_content #relator_eq_raw val get_relator_domain = get_net_content #relator_domain val get_pred_data = #pred_data o Data.get o Context.Proof fun map_data f1 f2 f3 f4 f5 f6 f7 f8 { transfer_raw, known_frees, compound_lhs, compound_rhs, relator_eq, relator_eq_raw, relator_domain, pred_data } = { transfer_raw = f1 transfer_raw, known_frees = f2 known_frees, compound_lhs = f3 compound_lhs, compound_rhs = f4 compound_rhs, relator_eq = f5 relator_eq, relator_eq_raw = f6 relator_eq_raw, relator_domain = f7 relator_domain, pred_data = f8 pred_data } fun map_transfer_raw f = map_data f I I I I I I I fun map_known_frees f = map_data I f I I I I I I fun map_compound_lhs f = map_data I I f I I I I I fun map_compound_rhs f = map_data I I I f I I I I fun map_relator_eq f = map_data I I I I f I I I fun map_relator_eq_raw f = map_data I I I I I f I I fun map_relator_domain f = map_data I I I I I I f I fun map_pred_data f = map_data I I I I I I I f val add_transfer_thm = Thm.trim_context #> (fn thm => Data.map (map_transfer_raw (Item_Net.update thm) o map_compound_lhs (case HOLogic.dest_Trueprop (Thm.concl_of thm) of Const (\<^const_name>\Rel\, _) $ _ $ (lhs as (_ $ _)) $ _ => Item_Net.update (lhs, thm) | _ => I) o map_compound_rhs (case HOLogic.dest_Trueprop (Thm.concl_of thm) of Const (\<^const_name>\Rel\, _) $ _ $ _ $ (rhs as (_ $ _)) => Item_Net.update (rhs, thm) | _ => I) o map_known_frees (Term.add_frees (Thm.concl_of thm)))) fun del_transfer_thm thm = Data.map (map_transfer_raw (Item_Net.remove thm) o map_compound_lhs (case HOLogic.dest_Trueprop (Thm.concl_of thm) of Const (\<^const_name>\Rel\, _) $ _ $ (lhs as (_ $ _)) $ _ => Item_Net.remove (lhs, thm) | _ => I) o map_compound_rhs (case HOLogic.dest_Trueprop (Thm.concl_of thm) of Const (\<^const_name>\Rel\, _) $ _ $ _ $ (rhs as (_ $ _)) => Item_Net.remove (rhs, thm) | _ => I)) fun transfer_raw_add thm ctxt = add_transfer_thm thm ctxt fun transfer_raw_del thm ctxt = del_transfer_thm thm ctxt (** Conversions **) fun transfer_rel_conv conv = Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv))) val Rel_rule = Thm.symmetric @{thm Rel_def} fun Rel_conv ct = let val (cT, cT') = Thm.dest_funT (Thm.ctyp_of_cterm ct) val (cU, _) = Thm.dest_funT cT' in Thm.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end (* Conversion to preprocess a transfer rule *) fun safe_Rel_conv ct = Conv.try_conv (HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))) ct fun prep_conv ct = ( Conv.implies_conv safe_Rel_conv prep_conv else_conv safe_Rel_conv else_conv Conv.all_conv) ct fun fold_relator_eqs_conv ctxt ct = (bottom_rewr_conv (get_relator_eq ctxt)) ct; fun unfold_relator_eqs_conv ctxt ct = (top_rewr_conv (get_sym_relator_eq ctxt)) ct; (** Replacing explicit equalities with is_equality premises **) fun mk_is_equality t = Const (\<^const_name>\is_equality\, Term.fastype_of t --> HOLogic.boolT) $ t fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm = let val prop = Thm.prop_of thm val (t, mk_prop') = dest prop (* Only consider "(=)" at non-base types *) fun is_eq (Const (\<^const_name>\HOL.eq\, Type ("fun", [T, _]))) = (case T of Type (_, []) => false | _ => true) | is_eq _ = false val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I) val eq_consts = rev (add_eqs t []) val eqTs = map (snd o dest_Const) eq_consts val used = Term.add_free_names prop [] val names = map (K "") eqTs |> Name.variant_list used val frees = map Free (names ~~ eqTs) val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t) val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1)) val cprop = Thm.cterm_of ctxt prop2 val equal_thm = Raw_Simplifier.rewrite ctxt false @{thms is_equality_lemma} cprop fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm in forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2})) end handle TERM _ => thm fun abstract_equalities_transfer ctxt thm = let fun dest prop = let val prems = Logic.strip_imp_prems prop val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop) val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl) in (rel, fn rel' => Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y))) end val contracted_eq_thm = Conv.fconv_rule (transfer_rel_conv (fold_relator_eqs_conv ctxt)) thm handle CTERM _ => thm in gen_abstract_equalities ctxt dest contracted_eq_thm end fun abstract_equalities_relator_eq ctxt rel_eq_thm = gen_abstract_equalities ctxt (fn x => (x, I)) (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]}) fun abstract_equalities_domain ctxt thm = let fun dest prop = let val prems = Logic.strip_imp_prems prop val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop) val ((eq, dom), y) = apfst Term.dest_comb (Term.dest_comb concl) in (dom, fn dom' => Logic.list_implies (prems, HOLogic.mk_Trueprop (eq $ dom' $ y))) end fun transfer_rel_conv conv = Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.arg1_conv (Conv.arg_conv conv))) val contracted_eq_thm = Conv.fconv_rule (transfer_rel_conv (fold_relator_eqs_conv ctxt)) thm in gen_abstract_equalities ctxt dest contracted_eq_thm end (** Replacing explicit Domainp predicates with Domainp assumptions **) fun mk_Domainp_assm (T, R) = HOLogic.mk_eq ((Const (\<^const_name>\Domainp\, Term.fastype_of T --> Term.fastype_of R) $ T), R) fun fold_Domainp f (t as Const (\<^const_name>\Domainp\,_) $ (Var (_,_))) = f t | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t | fold_Domainp _ _ = I fun subst_terms tab t = let val t' = Termtab.lookup tab t in case t' of SOME t' => t' | NONE => (case t of u $ v => (subst_terms tab u) $ (subst_terms tab v) | Abs (a, T, t) => Abs (a, T, subst_terms tab t) | t => t) end fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm = let val prop = Thm.prop_of thm val (t, mk_prop') = dest prop val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t []) val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_tms val used = Term.add_free_names t [] val rels = map (snd o dest_comb) Domainp_tms val rel_names = map (fst o fst o dest_Var) rels val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used val frees = map Free (names ~~ Domainp_Ts) val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees); val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t')) val prop2 = Logic.list_rename_params (rev names) prop1 val cprop = Thm.cterm_of ctxt prop2 val equal_thm = Raw_Simplifier.rewrite ctxt false @{thms Domainp_lemma} cprop fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm; in forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2})) end handle TERM _ => thm fun abstract_domains_transfer ctxt thm = let fun dest prop = let val prems = Logic.strip_imp_prems prop val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop) val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl) in (x, fn x' => Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y))) end in gen_abstract_domains ctxt dest thm end fun abstract_domains_relator_domain ctxt thm = let fun dest prop = let val prems = Logic.strip_imp_prems prop val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop) val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl) in (y, fn y' => Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x $ y'))) end in gen_abstract_domains ctxt dest thm end fun detect_transfer_rules thm = let fun is_transfer_rule tm = case (HOLogic.dest_Trueprop tm) of (Const (\<^const_name>\HOL.eq\, _)) $ ((Const (\<^const_name>\Domainp\, _)) $ _) $ _ => false | _ $ _ $ _ => true | _ => false fun safe_transfer_rule_conv ctm = if is_transfer_rule (Thm.term_of ctm) then safe_Rel_conv ctm else Conv.all_conv ctm in Conv.fconv_rule (Conv.prems_conv ~1 safe_transfer_rule_conv) thm end (** Adding transfer domain rules **) fun prep_transfer_domain_thm ctxt = abstract_equalities_domain ctxt o detect_transfer_rules fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt (** Transfer proof method **) val post_simps = @{thms transfer_forall_eq [symmetric] transfer_implies_eq [symmetric] transfer_bforall_unfold} fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) => let val keepers = keepers @ get_known_frees ctxt val vs = rev (Term.add_frees t []) val vs' = filter_out (member (op =) keepers) vs in Induct.arbitrary_tac ctxt 0 vs' i end) fun mk_relT (T, U) = T --> U --> HOLogic.boolT fun mk_Rel t = let val T = fastype_of t in Const (\<^const_name>\Transfer.Rel\, T --> T) $ t end fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u = let (* precondition: prj(T,U) must consist of only TFrees and type "fun" *) fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) = let val r1 = rel T1 U1 val r2 = rel T2 U2 val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U) in Const (\<^const_name>\rel_fun\, rT) $ r1 $ r2 end | rel T U = let val (a, _) = dest_TFree (prj (T, U)) in Free (the (AList.lookup (op =) tab a), mk_relT (T, U)) end fun zip _ thms (Bound i) (Bound _) = (nth thms i, []) | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) = let val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U) val cprop = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop prop) val thm0 = Thm.assume cprop val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop)) val r2 = Thm.dest_fun2 (Thm.dest_arg (Thm.cprop_of thm1)) val (a1, (b1, _)) = apsnd Thm.dest_funT (Thm.dest_funT (Thm.ctyp_of_cterm r1)) val (a2, (b2, _)) = apsnd Thm.dest_funT (Thm.dest_funT (Thm.ctyp_of_cterm r2)) val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2] val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)] val rule = Thm.instantiate' tinsts insts @{thm Rel_abs} val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1)) in (thm2 COMP rule, hyps) end | zip ctxt thms (f $ t) (g $ u) = let val (thm1, hyps1) = zip ctxt thms f g val (thm2, hyps2) = zip ctxt thms t u in (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2) end | zip _ _ t u = let val T = fastype_of t val U = fastype_of u val prop = mk_Rel (rel T U) $ t $ u val cprop = Thm.cterm_of ctxt (HOLogic.mk_Trueprop prop) in (Thm.assume cprop, [cprop]) end val r = mk_Rel (rel (fastype_of t) (fastype_of u)) val goal = HOLogic.mk_Trueprop (r $ t $ u) val rename = Thm.trivial (Thm.cterm_of ctxt goal) val (thm, hyps) = zip ctxt [] t u in Drule.implies_intr_list hyps (thm RS rename) end (* create a lambda term of the same shape as the given term *) fun skeleton is_atom = let fun dummy ctxt = let val (c, ctxt') = yield_singleton Variable.variant_fixes "a" ctxt in (Free (c, dummyT), ctxt') end fun skel (Bound i) ctxt = (Bound i, ctxt) | skel (Abs (x, _, t)) ctxt = let val (t', ctxt) = skel t ctxt in (Abs (x, dummyT, t'), ctxt) end | skel (tu as t $ u) ctxt = if is_atom tu andalso not (Term.is_open tu) then dummy ctxt else let val (t', ctxt) = skel t ctxt val (u', ctxt) = skel u ctxt in (t' $ u', ctxt) end | skel _ ctxt = dummy ctxt in fn ctxt => fn t => fst (skel t ctxt) |> Syntax.check_term ctxt (* FIXME avoid syntax operation!? *) end (** Monotonicity analysis **) (* TODO: Put extensible table in theory data *) val monotab = Symtab.make [(\<^const_name>\transfer_implies\, [~1, 1]), (\<^const_name>\transfer_forall\, [1])(*, (@{const_name implies}, [~1, 1]), (@{const_name All}, [1])*)] (* Function bool_insts determines the set of boolean-relation variables that can be instantiated to implies, rev_implies, or iff. Invariants: bool_insts p (t, u) requires that u :: _ => _ => ... => bool, and t is a skeleton of u *) fun bool_insts p (t, u) = let fun strip2 (t1 $ t2, u1 $ u2, tus) = strip2 (t1, u1, (t2, u2) :: tus) | strip2 x = x fun or3 ((a, b, c), (x, y, z)) = (a orelse x, b orelse y, c orelse z) fun go Ts p (Abs (_, T, t), Abs (_, _, u)) tab = go (T :: Ts) p (t, u) tab | go Ts p (t, u) tab = let val (a, _) = dest_TFree (Term.body_type (Term.fastype_of1 (Ts, t))) val (_, tf, tus) = strip2 (t, u, []) val ps_opt = case tf of Const (c, _) => Symtab.lookup monotab c | _ => NONE val tab1 = case ps_opt of SOME ps => let val ps' = map (fn x => p * x) (take (length tus) ps) in fold I (map2 (go Ts) ps' tus) tab end | NONE => tab val tab2 = Symtab.make [(a, (p >= 0, p <= 0, is_none ps_opt))] in Symtab.join (K or3) (tab1, tab2) end val tab = go [] p (t, u) Symtab.empty fun f (a, (true, false, false)) = SOME (a, \<^Const>\implies\) | f (a, (false, true, false)) = SOME (a, \<^Const>\rev_implies\) | f (a, (true, true, _)) = SOME (a, HOLogic.eq_const HOLogic.boolT) | f _ = NONE in map_filter f (Symtab.dest tab) end fun transfer_rule_of_term ctxt equiv t = let val s = skeleton (is_compound_rhs ctxt) ctxt t val frees = map fst (Term.add_frees s []) val tfrees = map fst (Term.add_tfrees s []) fun prep a = "R" ^ Library.unprefix "'" a val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt val tab = tfrees ~~ rnames fun prep a = the (AList.lookup (op =) tab a) val thm = transfer_rule_of_terms fst ctxt' tab s t val binsts = bool_insts (if equiv then 0 else 1) (s, t) val idx = Thm.maxidx_of thm + 1 fun tinst (a, _) = (((a, idx), \<^sort>\type\), \<^ctyp>\bool\) fun inst (a, t) = ((Name.clean_index (prep a, idx), \<^typ>\bool \ bool \ bool\), Thm.cterm_of ctxt' t) in thm |> Thm.generalize (Names.make_set tfrees, Names.make_set (rnames @ frees)) idx |> Thm.instantiate (TVars.make (map tinst binsts), Vars.make (map inst binsts)) end fun transfer_rule_of_lhs ctxt t = let val s = skeleton (is_compound_lhs ctxt) ctxt t val frees = map fst (Term.add_frees s []) val tfrees = map fst (Term.add_tfrees s []) fun prep a = "R" ^ Library.unprefix "'" a val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt val tab = tfrees ~~ rnames fun prep a = the (AList.lookup (op =) tab a) val thm = transfer_rule_of_terms snd ctxt' tab t s val binsts = bool_insts 1 (s, t) val idx = Thm.maxidx_of thm + 1 fun tinst (a, _) = (((a, idx), \<^sort>\type\), \<^ctyp>\bool\) fun inst (a, t) = ((Name.clean_index (prep a, idx), \<^typ>\bool \ bool \ bool\), Thm.cterm_of ctxt' t) in thm |> Thm.generalize (Names.make_set tfrees, Names.make_set (rnames @ frees)) idx |> Thm.instantiate (TVars.make (map tinst binsts), Vars.make (map inst binsts)) end fun eq_rules_tac ctxt eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac ctxt eq_rules) THEN_ALL_NEW resolve_tac ctxt @{thms is_equality_eq} fun eq_tac ctxt = eq_rules_tac ctxt (get_relator_eq_raw ctxt) fun transfer_step_tac ctxt = REPEAT_ALL_NEW (resolve_tac ctxt (get_transfer_raw ctxt)) THEN_ALL_NEW (DETERM o eq_rules_tac ctxt (get_relator_eq_raw ctxt)) fun transfer_start_tac equiv ctxt i = let val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} val start_rule = if equiv then @{thm transfer_start} else @{thm transfer_start'} val err_msg = "Transfer failed to convert goal to an object-logic formula" fun main_tac (t, i) = resolve_tac ctxt [start_rule] i THEN (resolve_tac ctxt [transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t)]) (i + 1) handle TERM (_, ts) => raise TERM (err_msg, ts) in EVERY [rewrite_goal_tac ctxt pre_simps i THEN SUBGOAL main_tac i] end; fun transfer_prover_start_tac ctxt = SUBGOAL (fn (t, i) => let val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t val rule1 = transfer_rule_of_term ctxt false rhs val expand_eqs_in_rel_conv = transfer_rel_conv (unfold_relator_eqs_conv ctxt) in EVERY [CONVERSION prep_conv i, CONVERSION expand_eqs_in_rel_conv i, resolve_tac ctxt @{thms transfer_prover_start} i, resolve_tac ctxt [rule1] (i + 1)] end); fun transfer_end_tac ctxt i = let val post_simps = @{thms transfer_forall_eq [symmetric] transfer_implies_eq [symmetric] transfer_bforall_unfold} in EVERY [rewrite_goal_tac ctxt post_simps i, Goal.norm_hhf_tac ctxt i] end; fun transfer_prover_end_tac ctxt i = resolve_tac ctxt @{thms refl} i local infix 1 THEN_ALL_BUT_FIRST_NEW fun (tac1 THEN_ALL_BUT_FIRST_NEW tac2) i st = st |> (tac1 i THEN (fn st' => Seq.INTERVAL tac2 (i + 1) (i + Thm.nprems_of st' - Thm.nprems_of st) st')); in fun transfer_tac equiv ctxt i = let val rules = get_transfer_raw ctxt val eq_rules = get_relator_eq_raw ctxt (* allow unsolved subgoals only for standard transfer method, not for transfer' *) val end_tac = if equiv then K all_tac else K no_tac fun transfer_search_tac i = (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW (DETERM o eq_rules_tac ctxt eq_rules)) ORELSE' end_tac) i in (transfer_start_tac equiv ctxt THEN_ALL_BUT_FIRST_NEW transfer_search_tac THEN' transfer_end_tac ctxt) i end fun transfer_prover_tac ctxt i = let val rules = get_transfer_raw ctxt val eq_rules = get_relator_eq_raw ctxt fun transfer_prover_search_tac i = (REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW (DETERM o eq_rules_tac ctxt eq_rules)) i in (transfer_prover_start_tac ctxt THEN_ALL_BUT_FIRST_NEW transfer_prover_search_tac THEN' transfer_prover_end_tac ctxt) i end end; (** Transfer attribute **) fun transferred ctxt extra_rules thm = let val rules = extra_rules @ get_transfer_raw ctxt val eq_rules = get_relator_eq_raw ctxt val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} val thm1 = Thm.forall_intr_vars thm val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) []) |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S)))) val thm2 = thm1 |> Thm.instantiate (TVars.make instT, Vars.empty) |> Raw_Simplifier.rewrite_rule ctxt pre_simps val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt val rule = transfer_rule_of_lhs ctxt' (HOLogic.dest_Trueprop (Thm.concl_of thm2)) in Goal.prove_internal ctxt' [] (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), \<^typ>\bool\)))) - (fn _ => - resolve_tac ctxt' [thm2 RS @{thm transfer_start'}, thm2 RS @{thm transfer_start}] 1 THEN - (resolve_tac ctxt' [rule] + (fn {context = goal_ctxt, ...} => + resolve_tac goal_ctxt [thm2 RS @{thm transfer_start'}, thm2 RS @{thm transfer_start}] 1 THEN + (resolve_tac goal_ctxt [rule] THEN_ALL_NEW - (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules) - THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 + (SOLVED' (REPEAT_ALL_NEW (resolve_tac goal_ctxt rules) + THEN_ALL_NEW (DETERM o eq_rules_tac goal_ctxt eq_rules)))) 1 handle TERM (_, ts) => raise TERM ("Transfer failed to convert goal to an object-logic formula", ts)) |> Raw_Simplifier.rewrite_rule ctxt' post_simps |> Simplifier.norm_hhf ctxt' |> Drule.generalize (Names.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Names.empty) |> Drule.zero_var_indexes end (* handle THM _ => thm *) fun untransferred ctxt extra_rules thm = let val rules = extra_rules @ get_transfer_raw ctxt val eq_rules = get_relator_eq_raw ctxt val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} val thm1 = Thm.forall_intr_vars thm val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) []) |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S)))) val thm2 = thm1 |> Thm.instantiate (TVars.make instT, Vars.empty) |> Raw_Simplifier.rewrite_rule ctxt pre_simps val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt val t = HOLogic.dest_Trueprop (Thm.concl_of thm2) val rule = transfer_rule_of_term ctxt' true t in Goal.prove_internal ctxt' [] (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), \<^typ>\bool\)))) - (fn _ => - resolve_tac ctxt' [thm2 RS @{thm untransfer_start}] 1 THEN - (resolve_tac ctxt' [rule] + (fn {context = goal_ctxt, ...} => + resolve_tac goal_ctxt [thm2 RS @{thm untransfer_start}] 1 THEN + (resolve_tac goal_ctxt [rule] THEN_ALL_NEW - (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules) - THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 + (SOLVED' (REPEAT_ALL_NEW (resolve_tac goal_ctxt rules) + THEN_ALL_NEW (DETERM o eq_rules_tac goal_ctxt eq_rules)))) 1 handle TERM (_, ts) => raise TERM ("Transfer failed to convert goal to an object-logic formula", ts)) |> Raw_Simplifier.rewrite_rule ctxt' post_simps |> Simplifier.norm_hhf ctxt' |> Drule.generalize (Names.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Names.empty) |> Drule.zero_var_indexes end (** Methods and attributes **) val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)) val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon) |-- Scan.repeat free) [] val reverse_prems = fn _ => PRIMITIVE (fn thm => fold_rev (fn i => Thm.permute_prems i 1) (0 upto Thm.nprems_of thm - 1) thm); fun transfer_start_method equiv : (Proof.context -> Proof.method) context_parser = fixing >> (fn vs => fn ctxt => SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_start_tac equiv ctxt THEN' reverse_prems)); fun transfer_method equiv : (Proof.context -> Proof.method) context_parser = fixing >> (fn vs => fn ctxt => SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt)) val transfer_prover_start_method : (Proof.context -> Proof.method) context_parser = Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_start_tac ctxt THEN' reverse_prems)) val transfer_prover_method : (Proof.context -> Proof.method) context_parser = Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt)) (* Attribute for transfer rules *) fun prep_rule ctxt = abstract_domains_transfer ctxt o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv val transfer_add = Thm.declaration_attribute (fn thm => fn ctxt => (add_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt) val transfer_del = Thm.declaration_attribute (fn thm => fn ctxt => (del_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt) val transfer_attribute = Attrib.add_del transfer_add transfer_del (* Attributes for transfer domain rules *) val transfer_domain_add = Thm.declaration_attribute add_transfer_domain_thm val transfer_domain_del = Thm.declaration_attribute del_transfer_domain_thm val transfer_domain_attribute = Attrib.add_del transfer_domain_add transfer_domain_del (* Attributes for transferred rules *) fun transferred_attribute thms = Thm.rule_attribute thms (fn context => transferred (Context.proof_of context) thms) fun untransferred_attribute thms = Thm.rule_attribute thms (fn context => untransferred (Context.proof_of context) thms) val transferred_attribute_parser = Attrib.thms >> transferred_attribute val untransferred_attribute_parser = Attrib.thms >> untransferred_attribute fun morph_pred_data phi = let val morph_thm = Morphism.thm phi in map_pred_data' morph_thm morph_thm (map morph_thm) end fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name |> Option.map (morph_pred_data (Morphism.transfer_morphism' ctxt)) fun update_pred_data type_name qinfo ctxt = Data.map (map_pred_data (Symtab.update (type_name, qinfo))) ctxt (* Theory setup *) val _ = Theory.setup let val name = \<^binding>\relator_eq\ fun add_thm thm context = context |> Data.map (map_relator_eq (Item_Net.update (Thm.trim_context thm))) |> Data.map (map_relator_eq_raw (Item_Net.update (Thm.trim_context (abstract_equalities_relator_eq (Context.proof_of context) thm)))) fun del_thm thm context = context |> Data.map (map_relator_eq (Item_Net.remove thm)) |> Data.map (map_relator_eq_raw (Item_Net.remove (abstract_equalities_relator_eq (Context.proof_of context) thm))) val add = Thm.declaration_attribute add_thm val del = Thm.declaration_attribute del_thm val text = "declaration of relator equality rule (used by transfer method)" val content = Item_Net.content o #relator_eq o Data.get in Attrib.setup name (Attrib.add_del add del) text #> Global_Theory.add_thms_dynamic (name, content) end val _ = Theory.setup let val name = \<^binding>\relator_domain\ fun add_thm thm context = let val thm' = thm |> abstract_domains_relator_domain (Context.proof_of context) |> Thm.trim_context in context |> Data.map (map_relator_domain (Item_Net.update thm')) |> add_transfer_domain_thm thm' end fun del_thm thm context = let val thm' = abstract_domains_relator_domain (Context.proof_of context) thm in context |> Data.map (map_relator_domain (Item_Net.remove thm')) |> del_transfer_domain_thm thm' end val add = Thm.declaration_attribute add_thm val del = Thm.declaration_attribute del_thm val text = "declaration of relator domain rule (used by transfer method)" val content = Item_Net.content o #relator_domain o Data.get in Attrib.setup name (Attrib.add_del add del) text #> Global_Theory.add_thms_dynamic (name, content) end val _ = Theory.setup (Attrib.setup \<^binding>\transfer_rule\ transfer_attribute "transfer rule for transfer method" #> Global_Theory.add_thms_dynamic (\<^binding>\transfer_raw\, Item_Net.content o #transfer_raw o Data.get) #> Attrib.setup \<^binding>\transfer_domain_rule\ transfer_domain_attribute "transfer domain rule for transfer method" #> Attrib.setup \<^binding>\transferred\ transferred_attribute_parser "raw theorem transferred to abstract theorem using transfer rules" #> Attrib.setup \<^binding>\untransferred\ untransferred_attribute_parser "abstract theorem transferred to raw theorem using transfer rules" #> Global_Theory.add_thms_dynamic (\<^binding>\relator_eq_raw\, Item_Net.content o #relator_eq_raw o Data.get) #> Method.setup \<^binding>\transfer_start\ (transfer_start_method true) "firtst step in the transfer algorithm (for debugging transfer)" #> Method.setup \<^binding>\transfer_start'\ (transfer_start_method false) "firtst step in the transfer algorithm (for debugging transfer)" #> Method.setup \<^binding>\transfer_prover_start\ transfer_prover_start_method "firtst step in the transfer_prover algorithm (for debugging transfer_prover)" #> Method.setup \<^binding>\transfer_step\ (Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_step_tac ctxt))) "step in the search for transfer rules (for debugging transfer and transfer_prover)" #> Method.setup \<^binding>\transfer_end\ (Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_end_tac ctxt))) "last step in the transfer algorithm (for debugging transfer)" #> Method.setup \<^binding>\transfer_prover_end\ (Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_end_tac ctxt))) "last step in the transfer_prover algorithm (for debugging transfer_prover)" #> Method.setup \<^binding>\transfer\ (transfer_method true) "generic theorem transfer method" #> Method.setup \<^binding>\transfer'\ (transfer_method false) "generic theorem transfer method" #> Method.setup \<^binding>\transfer_prover\ transfer_prover_method "for proving transfer rules") end diff --git a/src/HOL/Tools/datatype_realizer.ML b/src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML +++ b/src/HOL/Tools/datatype_realizer.ML @@ -1,244 +1,245 @@ (* Title: HOL/Tools/datatype_realizer.ML Author: Stefan Berghofer, TU Muenchen Program extraction from proofs involving datatypes: realizers for induction and case analysis. *) signature DATATYPE_REALIZER = sig val add_dt_realizers: Old_Datatype_Aux.config -> string list -> theory -> theory end; structure Datatype_Realizer : DATATYPE_REALIZER = struct fun subsets i j = if i <= j then let val is = subsets (i+1) j in map (fn ks => i::ks) is @ is end else [[]]; fun is_unit t = body_type (fastype_of t) = HOLogic.unitT; fun tname_of (Type (s, _)) = s | tname_of _ = ""; fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Old_Datatype_Aux.info) is thy = let val ctxt = Proof_Context.init_global thy; val recTs = Old_Datatype_Aux.get_rec_types descr; val pnames = if length descr = 1 then ["P"] else map (fn i => "P" ^ string_of_int i) (1 upto length descr); val rec_result_Ts = map (fn ((i, _), P) => if member (op =) is i then TFree ("'" ^ P, \<^sort>\type\) else HOLogic.unitT) (descr ~~ pnames); fun make_pred i T U r x = if member (op =) is i then Free (nth pnames i, T --> U --> HOLogic.boolT) $ r $ x else Free (nth pnames i, U --> HOLogic.boolT) $ x; fun mk_all i s T t = if member (op =) is i then Logic.all (Free (s, T)) t else t; val (prems, rec_fns) = split_list (flat (fst (fold_map (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j => let val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs; val tnames = Name.variant_list pnames (Old_Datatype_Prop.make_tnames Ts); val recs = filter (Old_Datatype_Aux.is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts); val frees = tnames ~~ Ts; fun mk_prems vs [] = let val rT = nth (rec_result_Ts) i; val vs' = filter_out is_unit vs; val f = Old_Datatype_Aux.mk_Free "f" (map fastype_of vs' ---> rT) j; val f' = Envir.eta_contract (fold_rev (absfree o dest_Free) vs (if member (op =) is i then list_comb (f, vs') else HOLogic.unit)); in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs')) (list_comb (Const (cname, Ts ---> T), map Free frees))), f') end | mk_prems vs (((dt, s), T) :: ds) = let val k = Old_Datatype_Aux.body_index dt; val (Us, U) = strip_type T; val i = length Us; val rT = nth (rec_result_Ts) k; val r = Free ("r" ^ s, Us ---> rT); val (p, f) = mk_prems (vs @ [r]) ds; in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies (Logic.list_all (map (pair "x") Us, HOLogic.mk_Trueprop (make_pred k rT U (Old_Datatype_Aux.app_bnds r i) (Old_Datatype_Aux.app_bnds (Free (s, T)) i))), p)), f) end; in (apfst (fold_rev (Logic.all o Free) frees) (mk_prems (map Free frees) recs), j + 1) end) constrs) (descr ~~ recTs) 1))); fun mk_proj _ [] t = t | mk_proj j (i :: is) t = if null is then t else if (j: int) = i then HOLogic.mk_fst t else mk_proj j is (HOLogic.mk_snd t); val tnames = Old_Datatype_Prop.make_tnames recTs; val fTs = map fastype_of rec_fns; val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0))) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names); val r = if null is then Extraction.nullt else foldr1 HOLogic.mk_prod (map_filter (fn (((((i, _), T), U), s), tname) => if member (op =) is i then SOME (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T)) else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames)); val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop \<^const_name>\HOL.conj\) (map (fn ((((i, _), T), U), tname) => make_pred i U T (mk_proj i is r) (Free (tname, T))) (descr ~~ recTs ~~ rec_result_Ts ~~ tnames))); val inst = map (#1 o dest_Var o head_of) (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ map (Thm.cterm_of ctxt) ps; val thm = Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) (Thm.cterm_of ctxt concl) - (fn prems => + (fn {context = goal_ctxt, prems} => EVERY [ - rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]), - resolve_tac ctxt [infer_instantiate ctxt inst induct] 1, - ALLGOALS (Object_Logic.atomize_prems_tac ctxt), - rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites), - REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW (fn i => - REPEAT (eresolve_tac ctxt [allE] i) THEN assume_tac ctxt i)) 1)]) + rewrite_goals_tac goal_ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]), + resolve_tac goal_ctxt [infer_instantiate goal_ctxt inst induct] 1, + ALLGOALS (Object_Logic.atomize_prems_tac goal_ctxt), + rewrite_goals_tac goal_ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites), + REPEAT ((resolve_tac goal_ctxt prems THEN_ALL_NEW (fn i => + REPEAT (eresolve_tac goal_ctxt [allE] i) THEN assume_tac goal_ctxt i)) 1)]) |> Drule.export_without_context; val ind_name = Thm.derivation_name induct; val vs = map (nth pnames) is; val (thm', thy') = thy |> Sign.root_path |> Global_Theory.store_thm (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm) ||> Sign.restore_naming thy; val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []); val rvs = rev (Thm.fold_terms {hyps = false} Term.add_vars thm' []); val ivs1 = map Var (filter_out (fn (_, T) => \<^type_name>\bool\ = tname_of (body_type T)) ivs); val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs; val prf = Extraction.abs_corr_shyps thy' induct vs ivs2 (fold_rev (fn (f, p) => fn prf => (case head_of (strip_abs_body f) of Free (s, T) => let val T' = Logic.varifyT_global T in Abst (s, SOME T', Proofterm.prf_abstract_over (Var ((s, 0), T')) (AbsP ("H", SOME p, prf))) end | _ => AbsP ("H", SOME p, prf))) (rec_fns ~~ Thm.prems_of thm) (Proofterm.proof_combP (Thm.reconstruct_proof_of thm', map PBound (length prems - 1 downto 0)))); val r' = if null is then r else Logic.varify_global (fold_rev lambda (map Logic.unvarify_global ivs1 @ filter_out is_unit (map (head_of o strip_abs_body) rec_fns)) r); in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end; fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy = let val ctxt = Proof_Context.init_global thy; val rT = TFree ("'P", \<^sort>\type\); val rT' = TVar (("'P", 0), \<^sort>\type\); fun make_casedist_prem T (cname, cargs) = let val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs; val frees = Name.variant_list ["P", "y"] (Old_Datatype_Prop.make_tnames Ts) ~~ Ts; val free_ts = map Free frees; val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT) in (r, fold_rev Logic.all free_ts (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))), HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, free_ts))))) end; val SOME (_, _, constrs) = AList.lookup (op =) descr index; val T = nth (Old_Datatype_Aux.get_rec_types descr) index; val (rs, prems) = split_list (map (make_casedist_prem T) constrs); val r = Const (case_name, map fastype_of rs ---> T --> rT); val y = Var (("y", 0), Logic.varifyT_global T); val y' = Free ("y", T); val thm = Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y'])))) - (fn prems => - EVERY [ - resolve_tac ctxt [infer_instantiate ctxt [(#1 (dest_Var y), Thm.cterm_of ctxt y')] exhaust] 1, + (fn {context = goal_ctxt, prems} => + EVERY [ + resolve_tac goal_ctxt + [infer_instantiate goal_ctxt [(#1 (dest_Var y), Thm.cterm_of goal_ctxt y')] exhaust] 1, ALLGOALS (EVERY' - [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites), - resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])]) + [asm_simp_tac (put_simpset HOL_basic_ss goal_ctxt addsimps case_rewrites), + resolve_tac goal_ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss goal_ctxt)])]) |> Drule.export_without_context; val exh_name = Thm.derivation_name exhaust; val (thm', thy') = thy |> Sign.root_path |> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm) ||> Sign.restore_naming thy; val P = Var (("P", 0), rT' --> HOLogic.boolT); val prf = Extraction.abs_corr_shyps thy' exhaust ["P"] [y, P] (fold_rev (fn (p, r) => fn prf => Proofterm.forall_intr_proof' (Logic.varify_global r) (AbsP ("H", SOME (Logic.varify_global p), prf))) (prems ~~ rs) (Proofterm.proof_combP (Thm.reconstruct_proof_of thm', map PBound (length prems - 1 downto 0)))); val prf' = Extraction.abs_corr_shyps thy' exhaust [] (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Thm.reconstruct_proof_of exhaust); val r' = Logic.varify_global (Abs ("y", T, (fold_rev (Term.abs o dest_Free) rs (list_comb (r, map Bound ((length rs - 1 downto 0) @ [length rs])))))); in Extraction.add_realizers_i [(exh_name, (["P"], r', prf)), (exh_name, ([], Extraction.nullt, prf'))] thy' end; fun add_dt_realizers config names thy = if not (Proofterm.proofs_enabled ()) then thy else let val _ = Old_Datatype_Aux.message config "Adding realizers for induction and case analysis ..."; val infos = map (BNF_LFP_Compat.the_info thy []) names; val info :: _ = infos; in thy |> fold_rev (perhaps o try o make_ind info) (subsets 0 (length (#descr info) - 1)) |> fold_rev (perhaps o try o make_casedists) infos end; val _ = Theory.setup (BNF_LFP_Compat.interpretation \<^plugin>\extraction\ [] add_dt_realizers); end; diff --git a/src/Pure/goal.ML b/src/Pure/goal.ML --- a/src/Pure/goal.ML +++ b/src/Pure/goal.ML @@ -1,342 +1,352 @@ (* Title: Pure/goal.ML Author: Makarius Goals in tactical theorem proving, with support for forked proofs. *) signature BASIC_GOAL = sig val quick_and_dirty: bool Config.T val SELECT_GOAL: tactic -> int -> tactic val PREFER_GOAL: tactic -> int -> tactic val CONJUNCTS: tactic -> int -> tactic val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic end; signature GOAL = sig include BASIC_GOAL val init: cterm -> thm val protect: int -> thm -> thm val conclude: thm -> thm val check_finished: Proof.context -> thm -> thm val finish: Proof.context -> thm -> thm val norm_result: Proof.context -> thm -> thm val skip_proofs_enabled: unit -> bool val future_result: Proof.context -> thm future -> term -> thm - val prove_internal: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm + type goal_context = {prems: thm list, context: Proof.context} + val prove_internal: Proof.context -> cterm list -> cterm -> (goal_context -> tactic) -> thm val is_schematic: term -> bool val prove_common: Proof.context -> int option -> string list -> term list -> term list -> - ({prems: thm list, context: Proof.context} -> tactic) -> thm list + (goal_context -> tactic) -> thm list val prove_future: Proof.context -> string list -> term list -> term -> - ({prems: thm list, context: Proof.context} -> tactic) -> thm + (goal_context -> tactic) -> thm val prove: Proof.context -> string list -> term list -> term -> - ({prems: thm list, context: Proof.context} -> tactic) -> thm + (goal_context -> tactic) -> thm val prove_global_future: theory -> string list -> term list -> term -> - ({prems: thm list, context: Proof.context} -> tactic) -> thm + (goal_context -> tactic) -> thm val prove_global: theory -> string list -> term list -> term -> - ({prems: thm list, context: Proof.context} -> tactic) -> thm + (goal_context -> tactic) -> thm val prove_sorry: Proof.context -> string list -> term list -> term -> - ({prems: thm list, context: Proof.context} -> tactic) -> thm + (goal_context -> tactic) -> thm val prove_sorry_global: theory -> string list -> term list -> term -> - ({prems: thm list, context: Proof.context} -> tactic) -> thm + (goal_context -> tactic) -> thm val restrict: int -> int -> thm -> thm val unrestrict: int -> thm -> thm val conjunction_tac: int -> tactic val precise_conjunction_tac: int -> int -> tactic val recover_conjunction_tac: tactic val norm_hhf_tac: Proof.context -> int -> tactic val assume_rule_tac: Proof.context -> int -> tactic end; structure Goal: GOAL = struct (** goals **) (* -------- (init) C \ #C *) fun init C = Thm.instantiate (TVars.empty, Vars.make [((("A", 0), propT), C)]) Drule.protectI; (* A1 \ ... \ An \ C ------------------------ (protect n) A1 \ ... \ An \ #C *) fun protect n th = Drule.comp_no_flatten (th, n) 1 Drule.protectI; (* A \ ... \ #C ---------------- (conclude) A \ ... \ C *) fun conclude th = Drule.comp_no_flatten (th, Thm.nprems_of th) 1 Drule.protectD; (* #C --- (finish) C *) fun check_finished ctxt th = if Thm.no_prems th then th else raise THM ("Proof failed.\n" ^ Pretty.string_of (Goal_Display.pretty_goal ctxt th), 0, [th]); fun finish ctxt = check_finished ctxt #> conclude; (** results **) (* normal form *) fun norm_result ctxt = Drule.flexflex_unique (SOME ctxt) #> Raw_Simplifier.norm_hhf_protect ctxt #> Thm.strip_shyps #> Drule.zero_var_indexes; (* scheduling parameters *) fun skip_proofs_enabled () = let val skip = Options.default_bool "skip_proofs" in if Proofterm.proofs_enabled () andalso skip then (warning "Proof terms enabled -- cannot skip proofs"; false) else skip end; (* future_result *) fun future_result ctxt result prop = let val assms = Assumption.all_assms_of ctxt; val As = map Thm.term_of assms; val frees = Frees.build (fold Frees.add_frees (prop :: As)); val xs = Frees.fold_rev (cons o Thm.cterm_of ctxt o Free o #1) frees []; val tfrees = TFrees.build (fold TFrees.add_tfrees (prop :: As)); val Ts = Names.build (TFrees.fold (Names.add_set o #1 o #1) tfrees); val instT = TVars.build (tfrees |> TFrees.fold (fn ((a, S), _) => TVars.add (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S))))); val global_prop = Logic.list_implies (As, prop) |> Frees.fold_rev (Logic.all o Free o #1) frees |> Logic.varify_types_global |> Thm.cterm_of ctxt |> Thm.weaken_sorts' ctxt; val global_result = result |> Future.map (Drule.flexflex_unique (SOME ctxt) #> Drule.implies_intr_list assms #> Drule.forall_intr_list xs #> Thm.adjust_maxidx_thm ~1 #> Thm.generalize (Ts, Names.empty) 0 #> Thm.strip_shyps #> Thm.solve_constraints); val local_result = Thm.future global_result global_prop |> Thm.close_derivation \<^here> |> Thm.instantiate (instT, Vars.empty) |> Drule.forall_elim_list xs |> fold (Thm.elim_implies o Thm.assume) assms |> Thm.solve_constraints; in local_result end; (** tactical theorem proving **) +type goal_context = {prems: thm list, context: Proof.context}; + + (* prove_internal -- minimal checks, no normalization of result! *) fun prove_internal ctxt casms cprop tac = - (case SINGLE (tac (map (Assumption.assume ctxt) casms)) (init cprop) of - SOME th => Drule.implies_intr_list casms (finish ctxt th) - | NONE => error "Tactic failed"); + let + val (prems, ctxt') = ctxt + |> fold (Variable.declare_term o Thm.term_of) (casms @ [cprop]) + |> fold_map Thm.assume_hyps casms; + in + (case SINGLE (tac {prems = prems, context = ctxt'}) (init cprop) of + SOME th => Drule.implies_intr_list casms (finish ctxt' th) + | NONE => error "Tactic failed") + end; (* prove variations *) fun is_schematic t = Term.exists_subterm Term.is_Var t orelse Term.exists_type (Term.exists_subtype Term.is_TVar) t; fun prove_common ctxt fork_pri xs asms props tac = let val thy = Proof_Context.theory_of ctxt; val schematic = exists is_schematic props; val immediate = is_none fork_pri; val future = Future.proofs_enabled 1 andalso not (Proofterm.proofs_enabled ()); val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled (); val pos = Position.thread_data (); fun err msg = cat_error msg ("The error(s) above occurred for the goal statement" ^ Position.here pos ^ ":\n" ^ Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props))); fun cert_safe t = Thm.cterm_of ctxt (Envir.beta_norm (Term.no_dummy_patterns t)) handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg; val casms = map cert_safe asms; val cprops = map cert_safe props; val (prems, ctxt') = ctxt |> Variable.add_fixes_direct xs |> fold Variable.declare_term (asms @ props) |> Assumption.add_assumes casms ||> Variable.set_body true; val stmt = Thm.weaken_sorts' ctxt' (Conjunction.mk_conjunction_balanced cprops); fun tac' args st = if skip then ALLGOALS (Skip_Proof.cheat_tac ctxt) st before Skip_Proof.report ctxt else tac args st; fun result () = (case SINGLE (tac' {prems = prems, context = ctxt'}) (init stmt) of NONE => err "Tactic failed" | SOME st => let val _ = Context.subthy_id (Thm.theory_id st, Context.theory_id thy) orelse err "Bad background theory of goal state"; val res = (finish ctxt' st |> Drule.flexflex_unique (SOME ctxt') |> Thm.check_shyps ctxt' |> Thm.check_hyps (Context.Proof ctxt')) handle THM (msg, _, _) => err msg | ERROR msg => err msg; in if Unify.matches_list (Context.Proof ctxt') [Thm.term_of stmt] [Thm.prop_of res] then res else err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res)) end); val res = if immediate orelse schematic orelse not future orelse skip then result () else future_result ctxt' (Execution.fork {name = "Goal.prove", pos = Position.thread_data (), pri = the fork_pri} result) (Thm.term_of stmt); in res |> Thm.close_derivation \<^here> |> Conjunction.elim_balanced (length props) |> map (Assumption.export false ctxt' ctxt) |> Variable.export ctxt' ctxt |> map Drule.zero_var_indexes end; fun prove_future_pri ctxt pri xs asms prop tac = hd (prove_common ctxt (SOME pri) xs asms [prop] tac); fun prove_future ctxt = prove_future_pri ctxt ~1; fun prove ctxt xs asms prop tac = hd (prove_common ctxt NONE xs asms [prop] tac); fun prove_global_future thy xs asms prop tac = Drule.export_without_context (prove_future (Proof_Context.init_global thy) xs asms prop tac); fun prove_global thy xs asms prop tac = Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac); (* skip proofs *) val quick_and_dirty = Config.declare_option_bool ("quick_and_dirty", \<^here>); fun prove_sorry ctxt xs asms prop tac = if Config.get ctxt quick_and_dirty then prove ctxt xs asms prop (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt)) else (if Future.proofs_enabled 1 then prove_future_pri ctxt ~2 else prove ctxt) xs asms prop tac; fun prove_sorry_global thy xs asms prop tac = Drule.export_without_context (prove_sorry (Proof_Context.init_global thy) xs asms prop tac); (** goal structure **) (* rearrange subgoals *) fun restrict i n st = if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then raise THM ("Goal.restrict", i, [st]) else rotate_prems (i - 1) st |> protect n; fun unrestrict i = conclude #> rotate_prems (1 - i); (*with structural marker*) fun SELECT_GOAL tac i st = if Thm.nprems_of st = 1 andalso i = 1 then tac st else (PRIMITIVE (restrict i 1) THEN tac THEN PRIMITIVE (unrestrict i)) st; (*without structural marker*) fun PREFER_GOAL tac i st = if i < 1 orelse i > Thm.nprems_of st then Seq.empty else (PRIMITIVE (rotate_prems (i - 1)) THEN tac THEN PRIMITIVE (rotate_prems (1 - i))) st; (* multiple goals *) fun precise_conjunction_tac 0 i = eq_assume_tac i | precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i | precise_conjunction_tac n i = PRIMITIVE (Drule.with_subgoal i (Conjunction.curry_balanced n)); val adhoc_conjunction_tac = REPEAT_ALL_NEW (SUBGOAL (fn (goal, i) => if can Logic.dest_conjunction goal then resolve0_tac [Conjunction.conjunctionI] i else no_tac)); val conjunction_tac = SUBGOAL (fn (goal, i) => precise_conjunction_tac (length (Logic.dest_conjunctions goal)) i ORELSE TRY (adhoc_conjunction_tac i)); val recover_conjunction_tac = PRIMITIVE (fn th => Conjunction.uncurry_balanced (Thm.nprems_of th) th); fun PRECISE_CONJUNCTS n tac = SELECT_GOAL (precise_conjunction_tac n 1 THEN tac THEN recover_conjunction_tac); fun CONJUNCTS tac = SELECT_GOAL (conjunction_tac 1 THEN tac THEN recover_conjunction_tac); (* hhf normal form *) fun norm_hhf_tac ctxt = resolve_tac ctxt [Drule.asm_rl] (*cheap approximation -- thanks to builtin Logic.flatten_params*) THEN' SUBGOAL (fn (t, i) => if Drule.is_norm_hhf t then all_tac else rewrite_goal_tac ctxt Drule.norm_hhf_eqs i); (* non-atomic goal assumptions *) fun non_atomic (Const ("Pure.imp", _) $ _ $ _) = true | non_atomic (Const ("Pure.all", _) $ _) = true | non_atomic _ = false; fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) => let val ((_, goal'), ctxt') = Variable.focus_cterm NONE goal ctxt; val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal'; val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal''); val tacs = Rs |> map (fn R => eresolve_tac ctxt [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac ctxt); in fold_rev (curry op APPEND') tacs (K no_tac) i end); end; structure Basic_Goal: BASIC_GOAL = Goal; open Basic_Goal;