diff --git a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML @@ -1,1225 +1,1227 @@ (* Title: HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Author: Lukas Bulwahn, TU Muenchen Auxilary functions for predicate compiler. *) signature PREDICATE_COMPILE_AUX = sig val find_indices : ('a -> bool) -> 'a list -> int list (* mode *) datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode val eq_mode : mode * mode -> bool val mode_ord: mode ord val list_fun_mode : mode list -> mode val strip_fun_mode : mode -> mode list val dest_fun_mode : mode -> mode list val dest_tuple_mode : mode -> mode list val all_modes_of_typ : typ -> mode list val all_smodes_of_typ : typ -> mode list val fold_map_aterms_prodT : ('a -> 'a -> 'a) -> (typ -> 'b -> 'a * 'b) -> typ -> 'b -> 'a * 'b val map_filter_prod : (term -> term option) -> term -> term option val replace_ho_args : mode -> term list -> term list -> term list val ho_arg_modes_of : mode -> mode list val ho_argsT_of : mode -> typ list -> typ list val ho_args_of : mode -> term list -> term list val ho_args_of_typ : typ -> term list -> term list val ho_argsT_of_typ : typ list -> typ list val split_map_mode : (mode -> term -> term option * term option) -> mode -> term list -> term list * term list val split_map_modeT : (mode -> typ -> typ option * typ option) -> mode -> typ list -> typ list * typ list val split_mode : mode -> term list -> term list * term list val split_modeT : mode -> typ list -> typ list * typ list val string_of_mode : mode -> string val ascii_string_of_mode : mode -> string (* premises *) datatype indprem = Prem of term | Negprem of term | Sidecond of term | Generator of (string * typ) val dest_indprem : indprem -> term val map_indprem : (term -> term) -> indprem -> indprem (* general syntactic functions *) val is_equationlike : thm -> bool val is_pred_equation : thm -> bool val is_intro : string -> thm -> bool val is_predT : typ -> bool val lookup_constr : Proof.context -> (string * typ) -> int option val is_constrt : Proof.context -> term -> bool val strip_ex : term -> (string * typ) list * term val focus_ex : term -> Name.context -> ((string * typ) list * term) * Name.context val strip_all : term -> (string * typ) list * term val strip_intro_concl : thm -> term * term list (* introduction rule combinators *) val map_atoms : (term -> term) -> term -> term val fold_atoms : (term -> 'a -> 'a) -> term -> 'a -> 'a val fold_map_atoms : (term -> 'a -> term * 'a) -> term -> 'a -> term * 'a val maps_premises : (term -> term list) -> term -> term val map_concl : (term -> term) -> term -> term val map_term : theory -> (term -> term) -> thm -> thm (* split theorems of case expressions *) val prepare_split_thm : Proof.context -> thm -> thm val find_split_thm : theory -> term -> thm option (* datastructures and setup for generic compilation *) datatype compilation_funs = CompilationFuns of { mk_monadT : typ -> typ, dest_monadT : typ -> typ, mk_empty : typ -> term, mk_single : term -> term, mk_bind : term * term -> term, mk_plus : term * term -> term, mk_if : term -> term, mk_iterate_upto : typ -> term * term * term -> term, mk_not : term -> term, mk_map : typ -> typ -> term -> term -> term }; val mk_monadT : compilation_funs -> typ -> typ val dest_monadT : compilation_funs -> typ -> typ val mk_empty : compilation_funs -> typ -> term val mk_single : compilation_funs -> term -> term val mk_bind : compilation_funs -> term * term -> term val mk_plus : compilation_funs -> term * term -> term val mk_if : compilation_funs -> term -> term val mk_iterate_upto : compilation_funs -> typ -> term * term * term -> term val mk_not : compilation_funs -> term -> term val mk_map : compilation_funs -> typ -> typ -> term -> term -> term val funT_of : compilation_funs -> mode -> typ -> typ (* Different compilations *) datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq | Pos_Generator_DSeq | Neg_Generator_DSeq | Pos_Generator_CPS | Neg_Generator_CPS val negative_compilation_of : compilation -> compilation val compilation_for_polarity : bool -> compilation -> compilation val is_depth_limited_compilation : compilation -> bool val string_of_compilation : compilation -> string val compilation_names : (string * compilation) list val non_random_compilations : compilation list val random_compilations : compilation list (* Different options for compiler *) datatype options = Options of { expected_modes : (string * mode list) option, proposed_modes : (string * mode list) list, proposed_names : ((string * mode) * string) list, show_steps : bool, show_proof_trace : bool, show_intermediate_results : bool, show_mode_inference : bool, show_modes : bool, show_compilation : bool, show_caught_failures : bool, show_invalid_clauses : bool, skip_proof : bool, no_topmost_reordering : bool, function_flattening : bool, fail_safe_function_flattening : bool, specialise : bool, no_higher_order_predicate : string list, inductify : bool, detect_switches : bool, smart_depth_limiting : bool, compilation : compilation }; val expected_modes : options -> (string * mode list) option val proposed_modes : options -> string -> mode list option val proposed_names : options -> string -> mode -> string option val show_steps : options -> bool val show_proof_trace : options -> bool val show_intermediate_results : options -> bool val show_mode_inference : options -> bool val show_modes : options -> bool val show_compilation : options -> bool val show_caught_failures : options -> bool val show_invalid_clauses : options -> bool val skip_proof : options -> bool val no_topmost_reordering : options -> bool val function_flattening : options -> bool val fail_safe_function_flattening : options -> bool val specialise : options -> bool val no_higher_order_predicate : options -> string list val is_inductify : options -> bool val detect_switches : options -> bool val smart_depth_limiting : options -> bool val compilation : options -> compilation val default_options : options val bool_options : string list val print_step : options -> string -> unit (* conversions *) val imp_prems_conv : conv -> conv (* simple transformations *) val split_conjuncts_in_assms : Proof.context -> thm -> thm val dest_conjunct_prem : thm -> thm list val expand_tuples : theory -> thm -> thm val case_betapply : theory -> term -> term val eta_contract_ho_arguments : theory -> thm -> thm val remove_equalities : theory -> thm -> thm val remove_pointless_clauses : thm -> thm list val peephole_optimisation : theory -> thm -> thm option (* auxillary *) val unify_consts : theory -> term list -> term list -> (term list * term list) val mk_casesrule : Proof.context -> term -> thm list -> term val preprocess_intro : theory -> thm -> thm val define_quickcheck_predicate : term -> theory -> (((string * typ) * (string * typ) list) * thm) * theory end structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX = struct (* general functions *) fun comb_option f (SOME x1, SOME x2) = SOME (f (x1, x2)) | comb_option f (NONE, SOME x2) = SOME x2 | comb_option f (SOME x1, NONE) = SOME x1 | comb_option f (NONE, NONE) = NONE fun map2_optional f (x :: xs) (y :: ys) = f x (SOME y) :: (map2_optional f xs ys) | map2_optional f (x :: xs) [] = (f x NONE) :: (map2_optional f xs []) | map2_optional f [] [] = [] fun find_indices f xs = map_filter (fn (i, true) => SOME i | (_, false) => NONE) (map_index (apsnd f) xs) (* mode *) datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode (* equality of instantiatedness with respect to equivalences: Pair Input Input == Input and Pair Output Output == Output *) fun eq_mode (Fun (m1, m2), Fun (m3, m4)) = eq_mode (m1, m3) andalso eq_mode (m2, m4) | eq_mode (Pair (m1, m2), Pair (m3, m4)) = eq_mode (m1, m3) andalso eq_mode (m2, m4) | eq_mode (Pair (m1, m2), Input) = eq_mode (m1, Input) andalso eq_mode (m2, Input) | eq_mode (Pair (m1, m2), Output) = eq_mode (m1, Output) andalso eq_mode (m2, Output) | eq_mode (Input, Pair (m1, m2)) = eq_mode (Input, m1) andalso eq_mode (Input, m2) | eq_mode (Output, Pair (m1, m2)) = eq_mode (Output, m1) andalso eq_mode (Output, m2) | eq_mode (Input, Input) = true | eq_mode (Output, Output) = true | eq_mode (Bool, Bool) = true | eq_mode _ = false fun mode_ord (Input, Output) = LESS | mode_ord (Output, Input) = GREATER | mode_ord (Input, Input) = EQUAL | mode_ord (Output, Output) = EQUAL | mode_ord (Bool, Bool) = EQUAL | mode_ord (Pair (m1, m2), Pair (m3, m4)) = prod_ord mode_ord mode_ord ((m1, m2), (m3, m4)) | mode_ord (Fun (m1, m2), Fun (m3, m4)) = prod_ord mode_ord mode_ord ((m1, m2), (m3, m4)) fun list_fun_mode [] = Bool | list_fun_mode (m :: ms) = Fun (m, list_fun_mode ms) (* name: binder_modes? *) fun strip_fun_mode (Fun (mode, mode')) = mode :: strip_fun_mode mode' | strip_fun_mode Bool = [] | strip_fun_mode _ = raise Fail "Bad mode for strip_fun_mode" (* name: strip_fun_mode? *) fun dest_fun_mode (Fun (mode, mode')) = mode :: dest_fun_mode mode' | dest_fun_mode mode = [mode] fun dest_tuple_mode (Pair (mode, mode')) = mode :: dest_tuple_mode mode' | dest_tuple_mode _ = [] fun all_modes_of_typ' (T as Type ("fun", _)) = let val (S, U) = strip_type T in if U = HOLogic.boolT then fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) (map all_modes_of_typ' S) [Bool] else [Input, Output] end | all_modes_of_typ' (Type (\<^type_name>\Product_Type.prod\, [T1, T2])) = map_product (curry Pair) (all_modes_of_typ' T1) (all_modes_of_typ' T2) | all_modes_of_typ' _ = [Input, Output] fun all_modes_of_typ (T as Type ("fun", _)) = let val (S, U) = strip_type T in if U = \<^typ>\bool\ then fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) (map all_modes_of_typ' S) [Bool] else raise Fail "Invocation of all_modes_of_typ with a non-predicate type" end | all_modes_of_typ \<^typ>\bool\ = [Bool] | all_modes_of_typ _ = raise Fail "Invocation of all_modes_of_typ with a non-predicate type" fun all_smodes_of_typ (T as Type ("fun", _)) = let val (S, U) = strip_type T fun all_smodes (Type (\<^type_name>\Product_Type.prod\, [T1, T2])) = map_product (curry Pair) (all_smodes T1) (all_smodes T2) | all_smodes _ = [Input, Output] in if U = HOLogic.boolT then fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) (map all_smodes S) [Bool] else raise Fail "invalid type for predicate" end fun ho_arg_modes_of mode = let fun ho_arg_mode (m as Fun _) = [m] | ho_arg_mode (Pair (m1, m2)) = ho_arg_mode m1 @ ho_arg_mode m2 | ho_arg_mode _ = [] in maps ho_arg_mode (strip_fun_mode mode) end fun ho_args_of mode ts = let fun ho_arg (Fun _) (SOME t) = [t] | ho_arg (Fun _) NONE = raise Fail "mode and term do not match" | ho_arg (Pair (m1, m2)) (SOME (Const (\<^const_name>\Pair\, _) $ t1 $ t2)) = ho_arg m1 (SOME t1) @ ho_arg m2 (SOME t2) | ho_arg (Pair (m1, m2)) NONE = ho_arg m1 NONE @ ho_arg m2 NONE | ho_arg _ _ = [] in flat (map2_optional ho_arg (strip_fun_mode mode) ts) end fun ho_args_of_typ T ts = let fun ho_arg (T as Type ("fun", [_, _])) (SOME t) = if body_type T = \<^typ>\bool\ then [t] else [] | ho_arg (Type ("fun", [_, _])) NONE = raise Fail "mode and term do not match" | ho_arg (Type(\<^type_name>\Product_Type.prod\, [T1, T2])) (SOME (Const (\<^const_name>\Pair\, _) $ t1 $ t2)) = ho_arg T1 (SOME t1) @ ho_arg T2 (SOME t2) | ho_arg (Type(\<^type_name>\Product_Type.prod\, [T1, T2])) NONE = ho_arg T1 NONE @ ho_arg T2 NONE | ho_arg _ _ = [] in flat (map2_optional ho_arg (binder_types T) ts) end fun ho_argsT_of_typ Ts = let fun ho_arg (T as Type("fun", [_,_])) = if body_type T = \<^typ>\bool\ then [T] else [] | ho_arg (Type (\<^type_name>\Product_Type.prod\, [T1, T2])) = ho_arg T1 @ ho_arg T2 | ho_arg _ = [] in maps ho_arg Ts end (* temporary function should be replaced by unsplit_input or so? *) fun replace_ho_args mode hoargs ts = let fun replace (Fun _, _) (arg' :: hoargs') = (arg', hoargs') | replace (Pair (m1, m2), Const (\<^const_name>\Pair\, T) $ t1 $ t2) hoargs = let val (t1', hoargs') = replace (m1, t1) hoargs val (t2', hoargs'') = replace (m2, t2) hoargs' in (Const (\<^const_name>\Pair\, T) $ t1' $ t2', hoargs'') end | replace (_, t) hoargs = (t, hoargs) in fst (fold_map replace (strip_fun_mode mode ~~ ts) hoargs) end fun ho_argsT_of mode Ts = let fun ho_arg (Fun _) T = [T] | ho_arg (Pair (m1, m2)) (Type (\<^type_name>\Product_Type.prod\, [T1, T2])) = ho_arg m1 T1 @ ho_arg m2 T2 | ho_arg _ _ = [] in flat (map2 ho_arg (strip_fun_mode mode) Ts) end (* splits mode and maps function to higher-order argument types *) fun split_map_mode f mode ts = let fun split_arg_mode' (m as Fun _) t = f m t | split_arg_mode' (Pair (m1, m2)) (Const (\<^const_name>\Pair\, _) $ t1 $ t2) = let val (i1, o1) = split_arg_mode' m1 t1 val (i2, o2) = split_arg_mode' m2 t2 in (comb_option HOLogic.mk_prod (i1, i2), comb_option HOLogic.mk_prod (o1, o2)) end | split_arg_mode' m t = if eq_mode (m, Input) then (SOME t, NONE) else if eq_mode (m, Output) then (NONE, SOME t) else raise Fail "split_map_mode: mode and term do not match" in (apply2 (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) ts) end (* splits mode and maps function to higher-order argument types *) fun split_map_modeT f mode Ts = let fun split_arg_mode' (m as Fun _) T = f m T | split_arg_mode' (Pair (m1, m2)) (Type (\<^type_name>\Product_Type.prod\, [T1, T2])) = let val (i1, o1) = split_arg_mode' m1 T1 val (i2, o2) = split_arg_mode' m2 T2 in (comb_option HOLogic.mk_prodT (i1, i2), comb_option HOLogic.mk_prodT (o1, o2)) end | split_arg_mode' Input T = (SOME T, NONE) | split_arg_mode' Output T = (NONE, SOME T) | split_arg_mode' _ _ = raise Fail "split_modeT': mode and type do not match" in (apply2 (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts) end fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts fun fold_map_aterms_prodT comb f (Type (\<^type_name>\Product_Type.prod\, [T1, T2])) s = let val (x1, s') = fold_map_aterms_prodT comb f T1 s val (x2, s'') = fold_map_aterms_prodT comb f T2 s' in (comb x1 x2, s'') end | fold_map_aterms_prodT _ f T s = f T s fun map_filter_prod f (Const (\<^const_name>\Pair\, _) $ t1 $ t2) = comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2) | map_filter_prod f t = f t fun split_modeT mode Ts = let fun split_arg_mode (Fun _) _ = ([], []) | split_arg_mode (Pair (m1, m2)) (Type (\<^type_name>\Product_Type.prod\, [T1, T2])) = let val (i1, o1) = split_arg_mode m1 T1 val (i2, o2) = split_arg_mode m2 T2 in (i1 @ i2, o1 @ o2) end | split_arg_mode Input T = ([T], []) | split_arg_mode Output T = ([], [T]) | split_arg_mode _ _ = raise Fail "split_modeT: mode and type do not match" in (apply2 flat o split_list) (map2 split_arg_mode (strip_fun_mode mode) Ts) end fun string_of_mode mode = let fun string_of_mode1 Input = "i" | string_of_mode1 Output = "o" | string_of_mode1 Bool = "bool" | string_of_mode1 mode = "(" ^ (string_of_mode3 mode) ^ ")" and string_of_mode2 (Pair (m1, m2)) = string_of_mode3 m1 ^ " * " ^ string_of_mode2 m2 | string_of_mode2 mode = string_of_mode1 mode and string_of_mode3 (Fun (m1, m2)) = string_of_mode2 m1 ^ " => " ^ string_of_mode3 m2 | string_of_mode3 mode = string_of_mode2 mode in string_of_mode3 mode end fun ascii_string_of_mode mode' = let fun ascii_string_of_mode' Input = "i" | ascii_string_of_mode' Output = "o" | ascii_string_of_mode' Bool = "b" | ascii_string_of_mode' (Pair (m1, m2)) = "P" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2 | ascii_string_of_mode' (Fun (m1, m2)) = "F" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Fun m2 ^ "B" and ascii_string_of_mode'_Fun (Fun (m1, m2)) = ascii_string_of_mode' m1 ^ (if m2 = Bool then "" else "_" ^ ascii_string_of_mode'_Fun m2) | ascii_string_of_mode'_Fun Bool = "B" | ascii_string_of_mode'_Fun m = ascii_string_of_mode' m and ascii_string_of_mode'_Pair (Pair (m1, m2)) = ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2 | ascii_string_of_mode'_Pair m = ascii_string_of_mode' m in ascii_string_of_mode'_Fun mode' end (* premises *) datatype indprem = Prem of term | Negprem of term | Sidecond of term | Generator of (string * typ) fun dest_indprem (Prem t) = t | dest_indprem (Negprem t) = t | dest_indprem (Sidecond t) = t | dest_indprem (Generator _) = raise Fail "cannot destruct generator" fun map_indprem f (Prem t) = Prem (f t) | map_indprem f (Negprem t) = Negprem (f t) | map_indprem f (Sidecond t) = Sidecond (f t) | map_indprem f (Generator (v, T)) = Generator (dest_Free (f (Free (v, T)))) (* general syntactic functions *) fun is_equationlike_term (Const (\<^const_name>\Pure.eq\, _) $ _ $ _) = true | is_equationlike_term (Const (\<^const_name>\Trueprop\, _) $ (Const (\<^const_name>\HOL.eq\, _) $ _ $ _)) = true | is_equationlike_term _ = false val is_equationlike = is_equationlike_term o Thm.prop_of fun is_pred_equation_term (Const (\<^const_name>\Pure.eq\, _) $ u $ v) = (fastype_of u = \<^typ>\bool\) andalso (fastype_of v = \<^typ>\bool\) | is_pred_equation_term _ = false val is_pred_equation = is_pred_equation_term o Thm.prop_of fun is_intro_term constname t = the_default false (try (fn t => case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of Const (c, _) => c = constname | _ => false) t) fun is_intro constname t = is_intro_term constname (Thm.prop_of t) fun is_predT (T as Type("fun", [_, _])) = (body_type T = \<^typ>\bool\) | is_predT _ = false fun lookup_constr ctxt = let val tab = Ctr_Sugar.ctr_sugars_of ctxt |> maps (map_filter (try dest_Const) o #ctrs) |> map (fn (c, T) => ((c, (fst o dest_Type o body_type) T), BNF_Util.num_binder_types T)) in fn (c, T) => case body_type T of Type (Tname, _) => AList.lookup (op =) tab (c, Tname) | _ => NONE end; fun is_constrt ctxt = let val lookup_constr = lookup_constr ctxt fun check t = (case strip_comb t of (Var _, []) => true | (Free _, []) => true | (Const cT, ts) => (case lookup_constr cT of SOME i => length ts = i andalso forall check ts | _ => false) | _ => false) in check end fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t) fun strip_ex (Const (\<^const_name>\Ex\, _) $ Abs (x, T, t)) = let val (xTs, t') = strip_ex t in ((x, T) :: xTs, t') end | strip_ex t = ([], t) fun focus_ex t nctxt = let val ((xs, Ts), t') = apfst split_list (strip_ex t) val (xs', nctxt') = fold_map Name.variant xs nctxt; val ps' = xs' ~~ Ts; val vs = map Free ps'; val t'' = Term.subst_bounds (rev vs, t'); in ((ps', t''), nctxt') end val strip_intro_concl = strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of (* introduction rule combinators *) fun map_atoms f intro = let val (literals, head) = Logic.strip_horn intro fun appl t = (case t of (\<^term>\Not\ $ t') => HOLogic.mk_not (f t') | _ => f t) in Logic.list_implies (map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head) end fun fold_atoms f intro s = let val (literals, _) = Logic.strip_horn intro fun appl t s = (case t of (\<^term>\Not\ $ t') => f t' s | _ => f t s) in fold appl (map HOLogic.dest_Trueprop literals) s end fun fold_map_atoms f intro s = let val (literals, head) = Logic.strip_horn intro fun appl t s = (case t of (\<^term>\Not\ $ t') => apfst HOLogic.mk_not (f t' s) | _ => f t s) val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s in (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s') end; fun map_filter_premises f intro = let val (premises, head) = Logic.strip_horn intro in Logic.list_implies (map_filter f premises, head) end fun maps_premises f intro = let val (premises, head) = Logic.strip_horn intro in Logic.list_implies (maps f premises, head) end fun map_concl f intro = let val (premises, head) = Logic.strip_horn intro in Logic.list_implies (premises, f head) end (* combinators to apply a function to all basic parts of nested products *) fun map_products f (Const (\<^const_name>\Pair\, T) $ t1 $ t2) = Const (\<^const_name>\Pair\, T) $ map_products f t1 $ map_products f t2 | map_products f t = f t (* split theorems of case expressions *) fun prepare_split_thm ctxt split_thm = (split_thm RS @{thm iffD2}) |> Local_Defs.unfold0 ctxt [@{thm atomize_conjL[symmetric]}, @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}] fun find_split_thm thy (Const (name, _)) = Option.map #split (Ctr_Sugar.ctr_sugar_of_case (Proof_Context.init_global thy) name) | find_split_thm _ _ = NONE (* lifting term operations to theorems *) fun map_term thy f th = Skip_Proof.make_thm thy (f (Thm.prop_of th)) (* fun equals_conv lhs_cv rhs_cv ct = case Thm.term_of ct of Const (@{const_name Pure.eq}, _) $ _ $ _ => Conv.arg_conv cv ct | _ => error "equals_conv" *) (* Different compilations *) datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq | Pos_Generator_DSeq | Neg_Generator_DSeq | Pos_Generator_CPS | Neg_Generator_CPS fun negative_compilation_of Pos_Random_DSeq = Neg_Random_DSeq | negative_compilation_of Neg_Random_DSeq = Pos_Random_DSeq | negative_compilation_of New_Pos_Random_DSeq = New_Neg_Random_DSeq | negative_compilation_of New_Neg_Random_DSeq = New_Pos_Random_DSeq | negative_compilation_of Pos_Generator_DSeq = Neg_Generator_DSeq | negative_compilation_of Neg_Generator_DSeq = Pos_Generator_DSeq | negative_compilation_of Pos_Generator_CPS = Neg_Generator_CPS | negative_compilation_of Neg_Generator_CPS = Pos_Generator_CPS | negative_compilation_of c = c fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq | compilation_for_polarity false New_Pos_Random_DSeq = New_Neg_Random_DSeq | compilation_for_polarity _ c = c fun is_depth_limited_compilation c = (c = New_Pos_Random_DSeq) orelse (c = New_Neg_Random_DSeq) orelse (c = Pos_Generator_DSeq) orelse (c = Pos_Generator_DSeq) fun string_of_compilation c = (case c of Pred => "" | Random => "random" | Depth_Limited => "depth limited" | Depth_Limited_Random => "depth limited random" | DSeq => "dseq" | Annotated => "annotated" | Pos_Random_DSeq => "pos_random dseq" | Neg_Random_DSeq => "neg_random_dseq" | New_Pos_Random_DSeq => "new_pos_random dseq" | New_Neg_Random_DSeq => "new_neg_random_dseq" | Pos_Generator_DSeq => "pos_generator_dseq" | Neg_Generator_DSeq => "neg_generator_dseq" | Pos_Generator_CPS => "pos_generator_cps" | Neg_Generator_CPS => "neg_generator_cps") val compilation_names = [("pred", Pred), ("random", Random), ("depth_limited", Depth_Limited), ("depth_limited_random", Depth_Limited_Random), (*("annotated", Annotated),*) ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq), ("new_random_dseq", New_Pos_Random_DSeq), ("generator_dseq", Pos_Generator_DSeq), ("generator_cps", Pos_Generator_CPS)] val non_random_compilations = [Pred, Depth_Limited, DSeq, Annotated] val random_compilations = [Random, Depth_Limited_Random, Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq, Pos_Generator_CPS, Neg_Generator_CPS] (* datastructures and setup for generic compilation *) datatype compilation_funs = CompilationFuns of { mk_monadT : typ -> typ, dest_monadT : typ -> typ, mk_empty : typ -> term, mk_single : term -> term, mk_bind : term * term -> term, mk_plus : term * term -> term, mk_if : term -> term, mk_iterate_upto : typ -> term * term * term -> term, mk_not : term -> term, mk_map : typ -> typ -> term -> term -> term } fun mk_monadT (CompilationFuns funs) = #mk_monadT funs fun dest_monadT (CompilationFuns funs) = #dest_monadT funs fun mk_empty (CompilationFuns funs) = #mk_empty funs fun mk_single (CompilationFuns funs) = #mk_single funs fun mk_bind (CompilationFuns funs) = #mk_bind funs fun mk_plus (CompilationFuns funs) = #mk_plus funs fun mk_if (CompilationFuns funs) = #mk_if funs fun mk_iterate_upto (CompilationFuns funs) = #mk_iterate_upto funs fun mk_not (CompilationFuns funs) = #mk_not funs fun mk_map (CompilationFuns funs) = #mk_map funs (** function types and names of different compilations **) fun funT_of compfuns mode T = let val Ts = binder_types T val (inTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts in inTs ---> (mk_monadT compfuns (HOLogic.mk_tupleT outTs)) end (* Different options for compiler *) datatype options = Options of { expected_modes : (string * mode list) option, proposed_modes : (string * mode list) list, proposed_names : ((string * mode) * string) list, show_steps : bool, show_proof_trace : bool, show_intermediate_results : bool, show_mode_inference : bool, show_modes : bool, show_compilation : bool, show_caught_failures : bool, show_invalid_clauses : bool, skip_proof : bool, no_topmost_reordering : bool, function_flattening : bool, specialise : bool, fail_safe_function_flattening : bool, no_higher_order_predicate : string list, inductify : bool, detect_switches : bool, smart_depth_limiting : bool, compilation : compilation } fun expected_modes (Options opt) = #expected_modes opt fun proposed_modes (Options opt) = AList.lookup (op =) (#proposed_modes opt) fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode) (#proposed_names opt) (name, mode) fun show_steps (Options opt) = #show_steps opt fun show_intermediate_results (Options opt) = #show_intermediate_results opt fun show_proof_trace (Options opt) = #show_proof_trace opt fun show_modes (Options opt) = #show_modes opt fun show_mode_inference (Options opt) = #show_mode_inference opt fun show_compilation (Options opt) = #show_compilation opt fun show_caught_failures (Options opt) = #show_caught_failures opt fun show_invalid_clauses (Options opt) = #show_invalid_clauses opt fun skip_proof (Options opt) = #skip_proof opt fun function_flattening (Options opt) = #function_flattening opt fun fail_safe_function_flattening (Options opt) = #fail_safe_function_flattening opt fun specialise (Options opt) = #specialise opt fun no_topmost_reordering (Options opt) = #no_topmost_reordering opt fun no_higher_order_predicate (Options opt) = #no_higher_order_predicate opt fun is_inductify (Options opt) = #inductify opt fun compilation (Options opt) = #compilation opt fun detect_switches (Options opt) = #detect_switches opt fun smart_depth_limiting (Options opt) = #smart_depth_limiting opt val default_options = Options { expected_modes = NONE, proposed_modes = [], proposed_names = [], show_steps = false, show_intermediate_results = false, show_proof_trace = false, show_modes = false, show_mode_inference = false, show_compilation = false, show_caught_failures = false, show_invalid_clauses = false, skip_proof = true, no_topmost_reordering = false, function_flattening = false, specialise = false, fail_safe_function_flattening = false, no_higher_order_predicate = [], inductify = false, detect_switches = true, smart_depth_limiting = false, compilation = Pred } val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes", "show_mode_inference", "show_compilation", "show_invalid_clauses", "skip_proof", "inductify", "no_function_flattening", "detect_switches", "specialise", "no_topmost_reordering", "smart_depth_limiting"] fun print_step options s = if show_steps options then tracing s else () (* simple transformations *) (** tuple processing **) fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt) | rewrite_args (arg::args) (pats, intro_t, ctxt) = (case HOLogic.strip_tupleT (fastype_of arg) of (_ :: _ :: _) => let fun rewrite_arg' (Const (\<^const_name>\Pair\, _) $ _ $ t2, Type (\<^type_name>\Product_Type.prod\, [_, T2])) (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt)) | rewrite_arg' (t, Type (\<^type_name>\Product_Type.prod\, [T1, T2])) (args, (pats, intro_t, ctxt)) = let val thy = Proof_Context.theory_of ctxt val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2))) val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t val args' = map (Pattern.rewrite_term thy [pat] []) args in rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt')) end | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt)) val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg) (args, (pats, intro_t, ctxt)) in rewrite_args args' (pats, intro_t', ctxt') end | _ => rewrite_args args (pats, intro_t, ctxt)) fun rewrite_prem atom = let val (_, args) = strip_comb atom in rewrite_args args end fun split_conjuncts_in_assms ctxt th = let val ((_, [fixed_th]), ctxt') = Variable.import false [th] ctxt fun split_conjs i nprems th = if i > nprems then th else (case try (op RSN) (@{thm conjI}, (i, th)) of SOME th' => split_conjs i (nprems + 1) th' | NONE => split_conjs (i + 1) nprems th) in singleton (Variable.export ctxt' ctxt) (split_conjs 1 (Thm.nprems_of fixed_th) fixed_th) end fun dest_conjunct_prem th = (case HOLogic.dest_Trueprop (Thm.prop_of th) of (Const (\<^const_name>\HOL.conj\, _) $ _ $ _) => dest_conjunct_prem (th RS @{thm conjunct1}) @ dest_conjunct_prem (th RS @{thm conjunct2}) | _ => [th]) fun expand_tuples thy intro = let val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt val intro_t = Thm.prop_of intro' val concl = Logic.strip_imp_concl intro_t val (_, args) = strip_comb (HOLogic.dest_Trueprop concl) val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1) val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2) fun rewrite_pat (ct1, ct2) = (ct1, Thm.cterm_of ctxt3 (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2))) val t_insts' = map rewrite_pat t_insts val intro'' = Thm.instantiate (T_insts, t_insts') intro val [intro'''] = Variable.export ctxt3 ctxt [intro''] val intro'''' = Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.inject}]) intro''' (* splitting conjunctions introduced by prod.inject*) val intro''''' = split_conjuncts_in_assms ctxt intro'''' in intro''''' end (** making case distributivity rules **) (*** this should be part of the datatype package ***) fun datatype_name_of_case_name thy = Ctr_Sugar.ctr_sugar_of_case (Proof_Context.init_global thy) #> the #> #ctrs #> hd #> fastype_of #> body_type #> dest_Type #> fst fun make_case_comb thy Tcon = let val ctxt = Proof_Context.init_global thy val SOME {casex, ...} = Ctr_Sugar.ctr_sugar_of ctxt Tcon val casex' = Type.legacy_freeze casex val Ts = BNF_Util.binder_fun_types (fastype_of casex') in list_comb (casex', map_index (fn (j, T) => Free ("f" ^ string_of_int j, T)) Ts) end fun make_case_distrib thy Tcon = let val comb = make_case_comb thy Tcon; val Type ("fun", [T, T']) = fastype_of comb; val (Const (case_name, _), fs) = strip_comb comb val used = Term.add_tfree_names comb [] val U = TFree (singleton (Name.variant_list used) "'t", \<^sort>\type\) val x = Free ("x", T) val f = Free ("f", T' --> U) fun apply_f f' = let val Ts = binder_types (fastype_of f') val bs = map Bound ((length Ts - 1) downto 0) in fold_rev absdummy Ts (f $ (list_comb (f', bs))) end val fs' = map apply_f fs val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U) in HOLogic.mk_eq (f $ (comb $ x), list_comb (case_c', fs') $ x) end fun case_rewrite thy Tcon = (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop) (make_case_distrib thy Tcon) fun instantiated_case_rewrite thy Tcon = let val th = case_rewrite thy Tcon val ctxt = Proof_Context.init_global thy val f = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th))))) val Type ("fun", [uninst_T, uninst_T']) = fastype_of f val ([yname], ctxt') = Variable.add_fixes ["y"] ctxt val T' = TFree ("'t'", \<^sort>\type\) val U = TFree ("'u", \<^sort>\type\) val y = Free (yname, U) val f' = absdummy (U --> T') (Bound 0 $ y) val th' = Thm.instantiate ([(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')), (dest_TVar uninst_T', Thm.ctyp_of ctxt' T')], [((fst (dest_Var f), (U --> T') --> T'), Thm.cterm_of ctxt' f')]) th val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th'] in th' end fun case_betapply thy t = let val case_name = fst (dest_Const (fst (strip_comb t))) val Tcon = datatype_name_of_case_name thy case_name val th = instantiated_case_rewrite thy Tcon in Raw_Simplifier.rewrite_term thy [th RS @{thm eq_reflection}] [] t end (*** conversions ***) fun imp_prems_conv cv ct = (case Thm.term_of ct of Const (\<^const_name>\Pure.imp\, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct | _ => Conv.all_conv ct) (** eta contract higher-order arguments **) fun eta_contract_ho_arguments thy intro = let fun f atom = list_comb (apsnd ((map o map_products) Envir.eta_contract) (strip_comb atom)) in map_term thy (map_concl f o map_atoms f) intro end (** remove equalities **) fun remove_equalities thy intro = let fun remove_eqs intro_t = let val (prems, concl) = Logic.strip_horn intro_t fun remove_eq (prems, concl) = let fun removable_eq prem = (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) prem of SOME (lhs, rhs) => (case lhs of Var _ => true | _ => (case rhs of Var _ => true | _ => false)) | NONE => false) in (case find_first removable_eq prems of NONE => (prems, concl) | SOME eq => let val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) val prems' = remove (op =) eq prems val subst = (case lhs of (v as Var _) => (fn t => if t = v then rhs else t) | _ => (case rhs of (v as Var _) => (fn t => if t = v then lhs else t))) in remove_eq (map (map_aterms subst) prems', map_aterms subst concl) end) end in Logic.list_implies (remove_eq (prems, concl)) end in map_term thy remove_eqs intro end (* Some last processing *) fun remove_pointless_clauses intro = if Logic.strip_imp_prems (Thm.prop_of intro) = [\<^prop>\False\] then [] else [intro] (* some peephole optimisations *) fun peephole_optimisation thy intro = let val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) val process = rewrite_rule ctxt (Named_Theorems.get ctxt \<^named_theorems>\code_pred_simp\) fun process_False intro_t = if member (op =) (Logic.strip_imp_prems intro_t) \<^prop>\False\ then NONE else SOME intro_t fun process_True intro_t = map_filter_premises (fn p => if p = \<^prop>\True\ then NONE else SOME p) intro_t in Option.map (Skip_Proof.make_thm thy) (process_False (process_True (Thm.prop_of (process intro)))) end (* importing introduction rules *) fun import_intros inp_pred [] ctxt = let val (outp_pred, ctxt') = yield_singleton (Variable.import_terms true) inp_pred ctxt val T = fastype_of outp_pred val paramTs = ho_argsT_of_typ (binder_types T) val (param_names, _) = Variable.variant_fixes (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt' val params = map2 (curry Free) param_names paramTs in (((outp_pred, params), []), ctxt') end | import_intros inp_pred (th :: ths) ctxt = let val ((_, [th']), ctxt') = Variable.import true [th] ctxt val thy = Proof_Context.theory_of ctxt' val (pred, args) = strip_intro_concl th' val T = fastype_of pred val ho_args = ho_args_of_typ T args fun subst_of (pred', pred) = let val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty handle Type.TYPE_MATCH => error ("Type mismatch of predicate " ^ fst (dest_Const pred) ^ " (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^ " and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^ " in " ^ Thm.string_of_thm ctxt' th) in Vartab.fold (fn (xi, (S, T)) => Term_Subst.TVars.add ((xi, S), T)) subst Term_Subst.TVars.empty end fun instantiate_typ th = let val (pred', _) = strip_intro_concl th val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then raise Fail "Trying to instantiate another predicate" else () val instT = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T)) (subst_of (pred', pred)) []; in Thm.instantiate (instT, []) th end fun instantiate_ho_args th = let val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th val ho_args' = map dest_Var (ho_args_of_typ T args') in Thm.instantiate ([], ho_args' ~~ map (Thm.cterm_of ctxt') ho_args) th end val outp_pred = Term_Subst.instantiate (subst_of (inp_pred, pred), Term_Subst.Vars.empty) inp_pred val ((_, ths'), ctxt1) = Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt' in (((outp_pred, ho_args), th' :: ths'), ctxt1) end (* generation of case rules from user-given introduction rules *) fun mk_args2 (Type (\<^type_name>\Product_Type.prod\, [T1, T2])) st = let val (t1, st') = mk_args2 T1 st val (t2, st'') = mk_args2 T2 st' in (HOLogic.mk_prod (t1, t2), st'') end (*| mk_args2 (T as Type ("fun", _)) (params, ctxt) = let val (S, U) = strip_type T in if U = HOLogic.boolT then (hd params, (tl params, ctxt)) else let val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt in (Free (x, T), (params, ctxt')) end end*) | mk_args2 T (params, ctxt) = let val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt in (Free (x, T), (params, ctxt')) end fun mk_casesrule ctxt pred introrules = let (* TODO: can be simplified if parameters are not treated specially ? *) val (((pred, params), intros_th), ctxt1) = import_intros pred introrules ctxt (* TODO: distinct required ? -- test case with more than one parameter! *) val params = distinct (op aconv) params val intros = map Thm.prop_of intros_th val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1 val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT)) val argsT = binder_types (fastype_of pred) (* TODO: can be simplified if parameters are not treated specially ? <-- see uncommented code! *) val (argvs, _) = fold_map mk_args2 argsT (params, ctxt2) fun mk_case intro = let val (_, args) = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl) intro val prems = Logic.strip_imp_prems intro val eqprems = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args val frees = map Free (fold Term.add_frees (args @ prems) []) in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs)) val cases = map mk_case intros in Logic.list_implies (assm :: cases, prop) end; (* unifying constants to have the same type variables *) fun unify_consts thy cs intr_ts = let val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I); fun varify (t, (i, ts)) = - let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t)) + let + val t' = map_types (Logic.incr_tvar (i + 1)) + (#2 (Type.varify_global Term_Subst.TFrees.empty t)) in (maxidx_of_term t', t' :: ts) end val (i, cs') = List.foldr varify (~1, []) cs val (i', intr_ts') = List.foldr varify (i, []) intr_ts val rec_consts = fold add_term_consts_2 cs' [] val intr_consts = fold add_term_consts_2 intr_ts' [] fun unify (cname, cT) = let val consts = map snd (filter (fn c => fst c = cname) intr_consts) in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end val (env, _) = fold unify rec_consts (Vartab.empty, i') val subst = map_types (Envir.norm_type env) in (map subst cs', map subst intr_ts') end handle Type.TUNIFY => (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts)) (* preprocessing rules *) fun preprocess_equality thy rule = Conv.fconv_rule (imp_prems_conv (HOLogic.Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq}))))) (Thm.transfer thy rule) fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy (* defining a quickcheck predicate *) fun strip_imp_prems (Const(\<^const_name>\HOL.implies\, _) $ A $ B) = A :: strip_imp_prems B | strip_imp_prems _ = []; fun strip_imp_concl (Const(\<^const_name>\HOL.implies\, _) $ _ $ B) = strip_imp_concl B | strip_imp_concl A = A; fun strip_horn A = (strip_imp_prems A, strip_imp_concl A) fun define_quickcheck_predicate t thy = let val (vs, t') = strip_abs t val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs (* FIXME proper context!? *) val t'' = subst_bounds (map Free (rev vs'), t') val (prems, concl) = strip_horn t'' val constname = "quickcheck" val full_constname = Sign.full_bname thy constname val constT = map snd vs' ---> \<^typ>\bool\ val thy1 = Sign.add_consts [(Binding.name constname, constT, NoSyn)] thy val const = Const (full_constname, constT) val t = Logic.list_implies (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), HOLogic.mk_Trueprop (list_comb (const, map Free vs'))) val intro = Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t (fn {context = ctxt, ...} => ALLGOALS (Skip_Proof.cheat_tac ctxt)) in ((((full_constname, constT), vs'), intro), thy1) end end diff --git a/src/HOL/Tools/choice_specification.ML b/src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML +++ b/src/HOL/Tools/choice_specification.ML @@ -1,206 +1,206 @@ (* Title: HOL/Tools/choice_specification.ML Author: Sebastian Skalberg, TU Muenchen Package for defining constants by specification. *) signature CHOICE_SPECIFICATION = sig val close_form : term -> term val add_specification: (bstring * xstring * bool) list -> theory * thm -> theory * thm end structure Choice_Specification: CHOICE_SPECIFICATION = struct local fun mk_definitional [] arg = arg | mk_definitional ((thname, cname, covld) :: cos) (thy, thm) = (case HOLogic.dest_Trueprop (Thm.concl_of thm) of Const (\<^const_name>\Ex\, _) $ P => let val ctype = domain_type (type_of P) val cname_full = Sign.intern_const thy cname val cdefname = if thname = "" then Thm.def_name (Long_Name.base_name cname) else thname val def_eq = Logic.mk_equals (Const (cname_full, ctype), HOLogic.choice_const ctype $ P) val (thms, thy') = Global_Theory.add_defs covld [((Binding.name cdefname, def_eq), [])] thy val thm' = [thm,hd thms] MRS @{thm exE_some} in mk_definitional cos (thy',thm') end | _ => raise THM ("Bad specification theorem", 0, [thm])) in fun add_specification cos = mk_definitional cos #> apsnd Drule.export_without_context end (* Collect all intances of constants in term *) fun collect_consts (t $ u, tms) = collect_consts (u, collect_consts (t, tms)) | collect_consts (Abs (_, _, t), tms) = collect_consts (t, tms) | collect_consts (tm as Const _, tms) = insert (op aconv) tm tms | collect_consts (_, tms) = tms (* Complementing Type.varify_global... *) fun unvarify_global t fmap = let val fmap' = map Library.swap fmap fun unthaw (f as (a, S)) = (case AList.lookup (op =) fmap' a of NONE => TVar f | SOME (b, _) => TFree (b, S)) in map_types (map_type_tvar unthaw) t end (* The syntactic meddling needed to setup add_specification for work *) fun close_form t = fold_rev (fn (s, T) => fn t => HOLogic.mk_all (s, T, t)) (map dest_Free (Misc_Legacy.term_frees t)) t fun zip3 [] [] [] = [] | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs | zip3 _ _ _ = raise Fail "Choice_Specification.process_spec internal error" fun myfoldr f [x] = x | myfoldr f (x::xs) = f (x,myfoldr f xs) | myfoldr f [] = raise Fail "Choice_Specification.process_spec internal error" fun process_spec cos alt_props thy = let val ctxt = Proof_Context.init_global thy val rew_imps = alt_props |> map (Object_Logic.atomize ctxt o Thm.cterm_of ctxt o Syntax.read_prop_global thy o snd) val props' = rew_imps |> map (HOLogic.dest_Trueprop o Thm.term_of o snd o Thm.dest_equals o Thm.cprop_of) fun proc_single prop = let val frees = Misc_Legacy.term_frees prop val _ = forall (fn v => Sign.of_sort thy (type_of v, \<^sort>\type\)) frees orelse error "Specificaton: Only free variables of sort 'type' allowed" val prop_closed = close_form prop in (prop_closed, frees) end val props'' = map proc_single props' val frees = map snd props'' val prop = myfoldr HOLogic.mk_conj (map fst props'') - val (vmap, prop_thawed) = Type.varify_global [] prop + val (vmap, prop_thawed) = Type.varify_global Term_Subst.TFrees.empty prop val thawed_prop_consts = collect_consts (prop_thawed, []) val (altcos, overloaded) = split_list cos val (names, sconsts) = split_list altcos val consts = map (Syntax.read_term_global thy) sconsts val _ = not (Library.exists (not o Term.is_Const) consts) orelse error "Specification: Non-constant found as parameter" fun proc_const c = let - val (_, c') = Type.varify_global [] c + val (_, c') = Type.varify_global Term_Subst.TFrees.empty c val (cname,ctyp) = dest_Const c' in (case filter (fn t => let val (name, typ) = dest_Const t in name = cname andalso Sign.typ_equiv thy (typ, ctyp) end) thawed_prop_consts of [] => error ("Specification: No suitable instances of constant \"" ^ Syntax.string_of_term_global thy c ^ "\" found") | [cf] => unvarify_global cf vmap | _ => error ("Specification: Several variations of \"" ^ Syntax.string_of_term_global thy c ^ "\" found (try applying explicit type constraints)")) end val proc_consts = map proc_const consts fun mk_exist c prop = let val T = type_of c val cname = Long_Name.base_name (fst (dest_Const c)) val vname = if Symbol_Pos.is_identifier cname then cname else "x" in HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c, prop)) end val ex_prop = fold_rev mk_exist proc_consts prop val cnames = map (fst o dest_Const) proc_consts fun post_process (arg as (thy,thm)) = let fun inst_all thy v thm = let val cv = Thm.global_cterm_of thy v val cT = Thm.ctyp_of_cterm cv val spec' = Thm.instantiate' [SOME cT] [NONE, SOME cv] spec in thm RS spec' end fun remove_alls frees (thm, thy) = (fold (inst_all thy) frees thm, thy) fun process_single ((name, atts), rew_imp, frees) args = let fun undo_imps thm = Thm.equal_elim (Thm.symmetric rew_imp) thm fun add_final (thm, thy) = if name = "" then (thm, thy) else (writeln (" " ^ name ^ ": " ^ Thm.string_of_thm_global thy thm); Global_Theory.store_thm (Binding.name name, thm) thy) in swap args |> remove_alls frees |> apfst undo_imps |> apfst Drule.export_without_context |-> Thm.theory_attributes (map (Attrib.attribute_cmd_global thy) (@{attributes [nitpick_choice_spec]} @ atts)) |> add_final |> swap end fun process_all [proc_arg] args = process_single proc_arg args | process_all (proc_arg::rest) (thy,thm) = let val single_th = thm RS conjunct1 val rest_th = thm RS conjunct2 val (thy', _) = process_single proc_arg (thy, single_th) in process_all rest (thy', rest_th) end | process_all [] _ = raise Fail "Choice_Specification.process_spec internal error" val alt_names = map fst alt_props val _ = if exists (fn (name, _) => name <> "") alt_names then writeln "specification" else () in arg |> apsnd (Thm.unvarify_global thy) |> process_all (zip3 alt_names rew_imps frees) end fun after_qed [[thm]] = Proof_Context.background_theory (fn thy => #1 (post_process (add_specification (zip3 names cnames overloaded) (thy, thm)))); in thy |> Proof_Context.init_global |> Variable.declare_term ex_prop |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]] end (* outer syntax *) val opt_name = Scan.optional (Parse.name --| \<^keyword>\:\) "" val opt_overloaded = Parse.opt_keyword "overloaded" val _ = Outer_Syntax.command \<^command_keyword>\specification\ "define constants by specification" (\<^keyword>\(\ |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| \<^keyword>\)\ -- Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop) >> (fn (cos, alt_props) => Toplevel.theory_to_proof (process_spec cos alt_props))) end diff --git a/src/Pure/Proof/proof_checker.ML b/src/Pure/Proof/proof_checker.ML --- a/src/Pure/Proof/proof_checker.ML +++ b/src/Pure/Proof/proof_checker.ML @@ -1,152 +1,152 @@ (* Title: Pure/Proof/proof_checker.ML Author: Stefan Berghofer, TU Muenchen Simple proof checker based only on the core inference rules of Isabelle/Pure. *) signature PROOF_CHECKER = sig val thm_of_proof : theory -> Proofterm.proof -> thm end; structure Proof_Checker : PROOF_CHECKER = struct (***** construct a theorem out of a proof term *****) fun lookup_thm thy = let val tab = Symtab.build (Global_Theory.all_thms_of thy true |> fold_rev Symtab.update) in fn s => (case Symtab.lookup tab s of NONE => error ("Unknown theorem " ^ quote s) | SOME thm => thm) end; val beta_eta_convert = Conv.fconv_rule Drule.beta_eta_conversion; (* equality modulo renaming of type variables *) fun is_equal t t' = let val atoms = fold_types (fold_atyps (insert (op =))) t []; val atoms' = fold_types (fold_atyps (insert (op =))) t' [] in length atoms = length atoms' andalso map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t' end; fun pretty_prf thy vs Hs prf = let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |> Proofterm.prf_subst_pbounds (map (Hyp o Thm.prop_of) Hs) in (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf', Syntax.pretty_term_global thy (Proofterm.prop_of prf')) end; fun pretty_term thy vs _ t = let val t' = subst_bounds (map Free vs, t) in (Syntax.pretty_term_global thy t', Syntax.pretty_typ_global thy (fastype_of t')) end; fun appl_error thy prt vs Hs s f a = let val (pp_f, pp_fT) = pretty_prf thy vs Hs f; val (pp_a, pp_aT) = prt thy vs Hs a in error (cat_lines [s, "", Pretty.string_of (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, pp_f, Pretty.str " ::", Pretty.brk 1, pp_fT]), Pretty.string_of (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, pp_a, Pretty.str " ::", Pretty.brk 1, pp_aT]), ""]) end; fun thm_of_proof thy = let val lookup = lookup_thm thy in fn prf => let val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees prf Name.context; fun thm_of_atom thm Ts = let val tvars = rev (Term.add_tvars (Thm.full_prop_of thm) []); - val (fmap, thm') = Thm.varifyT_global' [] thm; + val (fmap, thm') = Thm.varifyT_global' Term_Subst.TFrees.empty thm; val ctye = (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts); in Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm')) end; fun thm_of _ _ (PThm ({name, prop = prop', types = SOME Ts, ...}, _)) = let val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name)); val prop = Thm.prop_of thm; val _ = if is_equal prop prop' then () else error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^ Syntax.string_of_term_global thy prop ^ "\n\n" ^ Syntax.string_of_term_global thy prop'); in thm_of_atom thm Ts end | thm_of _ _ (PAxm (name, _, SOME Ts)) = thm_of_atom (Thm.axiom thy name) Ts | thm_of _ Hs (PBound i) = nth Hs i | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) = let val (x, names') = Name.variant s names; val thm = thm_of ((x, T) :: vs, names') Hs prf in Thm.forall_intr (Thm.global_cterm_of thy (Free (x, T))) thm end | thm_of (vs, names) Hs (prf % SOME t) = let val thm = thm_of (vs, names) Hs prf; val ct = Thm.global_cterm_of thy (Term.subst_bounds (map Free vs, t)); in Thm.forall_elim ct thm handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t end | thm_of (vs, names) Hs (AbsP (_, SOME t, prf)) = let val ct = Thm.global_cterm_of thy (Term.subst_bounds (map Free vs, t)); val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf; in Thm.implies_intr ct thm end | thm_of vars Hs (prf %% prf') = let val thm = beta_eta_convert (thm_of vars Hs prf); val thm' = beta_eta_convert (thm_of vars Hs prf'); in Thm.implies_elim thm thm' handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf' end | thm_of _ _ (Hyp t) = Thm.assume (Thm.global_cterm_of thy t) | thm_of _ _ (PClass (T, c)) = if Sign.of_sort thy (T, [c]) then Thm.of_class (Thm.global_ctyp_of thy T, c) else error ("thm_of_proof: bad PClass proof " ^ Syntax.string_of_term_global thy (Logic.mk_of_class (T, c))) | thm_of _ _ _ = error "thm_of_proof: partial proof term"; in beta_eta_convert (thm_of ([], prf_names) [] prf) end end; end; diff --git a/src/Pure/proofterm.ML b/src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML +++ b/src/Pure/proofterm.ML @@ -1,2340 +1,2341 @@ (* Title: Pure/proofterm.ML Author: Stefan Berghofer, TU Muenchen LF style proof terms. *) infix 8 % %% %>; signature PROOFTERM = sig type thm_header = {serial: serial, pos: Position.T list, theory_name: string, name: string, prop: term, types: typ list option} type thm_body type thm_node datatype proof = MinProof | PBound of int | Abst of string * typ option * proof | AbsP of string * term option * proof | % of proof * term option | %% of proof * proof | Hyp of term | PAxm of string * term * typ list option | PClass of typ * class | Oracle of string * term * typ list option | PThm of thm_header * thm_body and proof_body = PBody of {oracles: ((string * Position.T) * term option) Ord_List.T, thms: (serial * thm_node) Ord_List.T, proof: proof} type oracle = (string * Position.T) * term option type thm = serial * thm_node exception MIN_PROOF of unit val proof_of: proof_body -> proof val join_proof: proof_body future -> proof val map_proof_of: (proof -> proof) -> proof_body -> proof_body val thm_header: serial -> Position.T list -> string -> string -> term -> typ list option -> thm_header val thm_body: proof_body -> thm_body val thm_body_proof_raw: thm_body -> proof val thm_body_proof_open: thm_body -> proof val thm_node_theory_name: thm_node -> string val thm_node_name: thm_node -> string val thm_node_prop: thm_node -> term val thm_node_body: thm_node -> proof_body future val thm_node_thms: thm_node -> thm list val join_thms: thm list -> proof_body list val make_thm: thm_header -> thm_body -> thm val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a val fold_body_thms: ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) -> proof_body list -> 'a -> 'a val oracle_ord: oracle ord val thm_ord: thm ord val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T val unions_thms: thm Ord_List.T list -> thm Ord_List.T val no_proof_body: proof -> proof_body val no_thm_names: proof -> proof val no_thm_proofs: proof -> proof val no_body_proofs: proof -> proof val encode: Consts.T -> proof XML.Encode.T val encode_body: Consts.T -> proof_body XML.Encode.T val encode_standard_term: Consts.T -> term XML.Encode.T val encode_standard_proof: Consts.T -> proof XML.Encode.T val decode: Consts.T -> proof XML.Decode.T val decode_body: Consts.T -> proof_body XML.Decode.T val %> : proof * term -> proof (*primitive operations*) val proofs: int Unsynchronized.ref val proofs_enabled: unit -> bool val atomic_proof: proof -> bool val compact_proof: proof -> bool val proof_combt: proof * term list -> proof val proof_combt': proof * term option list -> proof val proof_combP: proof * proof list -> proof val strip_combt: proof -> proof * term option list val strip_combP: proof -> proof * proof list val strip_thm_body: proof_body -> proof_body val map_proof_same: term Same.operation -> typ Same.operation -> (typ * class -> proof) -> proof Same.operation val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation val map_proof_types_same: typ Same.operation -> proof Same.operation val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof val map_proof_types: (typ -> typ) -> proof -> proof val fold_proof_terms: (term -> 'a -> 'a) -> proof -> 'a -> 'a val fold_proof_terms_types: (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a val maxidx_proof: proof -> int -> int val size_of_proof: proof -> int val change_types: typ list option -> proof -> proof val prf_abstract_over: term -> proof -> proof val prf_incr_bv: int -> int -> int -> int -> proof -> proof val incr_pboundvars: int -> int -> proof -> proof val prf_loose_bvar1: proof -> int -> bool val prf_loose_Pbvar1: proof -> int -> bool val prf_add_loose_bnos: int -> int -> proof -> int list * int list -> int list * int list val norm_proof: Envir.env -> proof -> proof val norm_proof': Envir.env -> proof -> proof val prf_subst_bounds: term list -> proof -> proof val prf_subst_pbounds: proof list -> proof -> proof val freeze_thaw_prf: proof -> proof * (proof -> proof) (*proof terms for specific inference rules*) val trivial_proof: proof val implies_intr_proof: term -> proof -> proof val implies_intr_proof': term -> proof -> proof val forall_intr_proof: string * term -> typ option -> proof -> proof val forall_intr_proof': term -> proof -> proof - val varify_proof: term -> (string * sort) list -> proof -> proof + val varify_proof: term -> Term_Subst.TFrees.set -> proof -> proof val legacy_freezeT: term -> proof -> proof val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof val permute_prems_proof: term list -> int -> int -> proof -> proof val generalize_proof: Symtab.set * Symtab.set -> int -> term -> proof -> proof val instantiate: typ Term_Subst.TVars.table * term Term_Subst.Vars.table -> proof -> proof val lift_proof: term -> int -> term -> proof -> proof val incr_indexes: int -> proof -> proof val assumption_proof: term list -> term -> int -> proof -> proof val bicompose_proof: bool -> term list -> term list -> term option -> term list -> int -> int -> proof -> proof -> proof val equality_axms: (string * term) list val reflexive_axm: proof val symmetric_axm: proof val transitive_axm: proof val equal_intr_axm: proof val equal_elim_axm: proof val abstract_rule_axm: proof val combination_axm: proof val reflexive_proof: proof val symmetric_proof: proof -> proof val transitive_proof: typ -> term -> proof -> proof -> proof val equal_intr_proof: term -> term -> proof -> proof -> proof val equal_elim_proof: term -> term -> proof -> proof -> proof val abstract_rule_proof: string * term -> proof -> proof val combination_proof: term -> term -> term -> term -> proof -> proof -> proof val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list -> sort list -> proof -> proof val of_sort_proof: Sorts.algebra -> (class * class -> proof) -> (string * class list list * class -> proof) -> (typ * class -> proof) -> typ * sort -> proof list val axm_proof: string -> term -> proof val oracle_proof: string -> term -> proof val shrink_proof: proof -> proof (*rewriting on proof terms*) val add_prf_rrule: proof * proof -> theory -> theory val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) -> theory -> theory val set_preproc: (theory -> proof -> proof) -> theory -> theory val apply_preproc: theory -> proof -> proof val forall_intr_variables_term: term -> term val forall_intr_variables: term -> proof -> proof val no_skel: proof val normal_skel: proof val rewrite_proof: theory -> (proof * proof) list * (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof val rewrite_proof_notypes: (proof * proof) list * (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof val rew_proof: theory -> proof -> proof val reconstruct_proof: theory -> term -> proof -> proof val prop_of': term list -> proof -> term val prop_of: proof -> term val expand_name_empty: thm_header -> string option val expand_proof: theory -> (thm_header -> string option) -> proof -> proof val standard_vars: Name.context -> term * proof option -> term * proof option val standard_vars_term: Name.context -> term -> term val add_standard_vars: proof -> (string * typ) list -> (string * typ) list val add_standard_vars_term: term -> (string * typ) list -> (string * typ) list val export_enabled: unit -> bool val export_standard_enabled: unit -> bool val export_proof_boxes_required: theory -> bool val export_proof_boxes: proof_body list -> unit val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body val thm_proof: theory -> (class * class -> proof) -> (string * class list list * class -> proof) -> string * Position.T -> sort list -> term list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof val unconstrain_thm_proof: theory -> (class * class -> proof) -> (string * class list list * class -> proof) -> sort list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof val get_identity: sort list -> term list -> term -> proof -> {serial: serial, theory_name: string, name: string} option val get_approximative_name: sort list -> term list -> term -> proof -> string type thm_id = {serial: serial, theory_name: string} val make_thm_id: serial * string -> thm_id val thm_header_id: thm_header -> thm_id val thm_id: thm -> thm_id val get_id: sort list -> term list -> term -> proof -> thm_id option val this_id: thm_id option -> thm_id -> bool val proof_boxes: {excluded: thm_id -> bool, included: thm_id -> bool} -> proof list -> (thm_header * proof) list (*exception MIN_PROOF*) end structure Proofterm : PROOFTERM = struct (** datatype proof **) type thm_header = {serial: serial, pos: Position.T list, theory_name: string, name: string, prop: term, types: typ list option}; datatype proof = MinProof | PBound of int | Abst of string * typ option * proof | AbsP of string * term option * proof | op % of proof * term option | op %% of proof * proof | Hyp of term | PAxm of string * term * typ list option | PClass of typ * class | Oracle of string * term * typ list option | PThm of thm_header * thm_body and proof_body = PBody of {oracles: ((string * Position.T) * term option) Ord_List.T, thms: (serial * thm_node) Ord_List.T, proof: proof} and thm_body = Thm_Body of {open_proof: proof -> proof, body: proof_body future} and thm_node = Thm_Node of {theory_name: string, name: string, prop: term, body: proof_body future, export: unit lazy, consolidate: unit lazy}; type oracle = (string * Position.T) * term option; val oracle_ord: oracle ord = prod_ord (prod_ord fast_string_ord Position.ord) (option_ord Term_Ord.fast_term_ord); type thm = serial * thm_node; val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i); exception MIN_PROOF of unit; fun proof_of (PBody {proof, ...}) = proof; val join_proof = Future.join #> proof_of; fun map_proof_of f (PBody {oracles, thms, proof}) = PBody {oracles = oracles, thms = thms, proof = f proof}; fun thm_header serial pos theory_name name prop types : thm_header = {serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types}; fun thm_body body = Thm_Body {open_proof = I, body = Future.value body}; fun thm_body_proof_raw (Thm_Body {body, ...}) = join_proof body; fun thm_body_proof_open (Thm_Body {open_proof, body, ...}) = open_proof (join_proof body); fun rep_thm_node (Thm_Node args) = args; val thm_node_theory_name = #theory_name o rep_thm_node; val thm_node_name = #name o rep_thm_node; val thm_node_prop = #prop o rep_thm_node; val thm_node_body = #body o rep_thm_node; val thm_node_thms = thm_node_body #> Future.join #> (fn PBody {thms, ...} => thms); val thm_node_export = #export o rep_thm_node; val thm_node_consolidate = #consolidate o rep_thm_node; fun join_thms (thms: thm list) = Future.joins (map (thm_node_body o #2) thms); val consolidate_bodies = maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms) #> Lazy.consolidate #> map Lazy.force #> ignore; fun make_thm_node theory_name name prop body export = let val consolidate = Lazy.lazy_name "Proofterm.make_thm_node" (fn () => let val PBody {thms, ...} = Future.join body in consolidate_bodies (join_thms thms) end); in Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body, export = export, consolidate = consolidate} end; val no_export = Lazy.value (); fun make_thm ({serial, theory_name, name, prop, ...}: thm_header) (Thm_Body {body, ...}) = (serial, make_thm_node theory_name name prop body no_export); (* proof atoms *) fun fold_proof_atoms all f = let fun app (Abst (_, _, prf)) = app prf | app (AbsP (_, _, prf)) = app prf | app (prf % _) = app prf | app (prf1 %% prf2) = app prf1 #> app prf2 | app (prf as PThm ({serial = i, ...}, Thm_Body {body, ...})) = (fn (x, seen) => if Inttab.defined seen i then (x, seen) else let val (x', seen') = (if all then app (join_proof body) else I) (x, Inttab.update (i, ()) seen) in (f prf x', seen') end) | app prf = (fn (x, seen) => (f prf x, seen)); in fn prfs => fn x => #1 (fold app prfs (x, Inttab.empty)) end; fun fold_body_thms f = let fun app (PBody {thms, ...}) = tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) => if Inttab.defined seen i then (x, seen) else let val name = thm_node_name thm_node; val prop = thm_node_prop thm_node; val body = Future.join (thm_node_body thm_node); val (x', seen') = app body (x, Inttab.update (i, ()) seen); in (f {serial = i, name = name, prop = prop, body = body} x', seen') end); in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end; (* proof body *) val unions_oracles = Ord_List.unions oracle_ord; val unions_thms = Ord_List.unions thm_ord; fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof}; val no_thm_body = thm_body (no_proof_body MinProof); fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf) | no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf) | no_thm_names (prf % t) = no_thm_names prf % t | no_thm_names (prf1 %% prf2) = no_thm_names prf1 %% no_thm_names prf2 | no_thm_names (PThm ({serial, pos, theory_name, name = _, prop, types}, thm_body)) = PThm (thm_header serial pos theory_name "" prop types, thm_body) | no_thm_names a = a; fun no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf) | no_thm_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_thm_proofs prf) | no_thm_proofs (prf % t) = no_thm_proofs prf % t | no_thm_proofs (prf1 %% prf2) = no_thm_proofs prf1 %% no_thm_proofs prf2 | no_thm_proofs (PThm (header, _)) = PThm (header, no_thm_body) | no_thm_proofs a = a; fun no_body_proofs (Abst (x, T, prf)) = Abst (x, T, no_body_proofs prf) | no_body_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_body_proofs prf) | no_body_proofs (prf % t) = no_body_proofs prf % t | no_body_proofs (prf1 %% prf2) = no_body_proofs prf1 %% no_body_proofs prf2 | no_body_proofs (PThm (header, Thm_Body {open_proof, body})) = let val body' = Future.value (no_proof_body (join_proof body)); val thm_body' = Thm_Body {open_proof = open_proof, body = body'}; in PThm (header, thm_body') end | no_body_proofs a = a; (** XML data representation **) (* encode *) local open XML.Encode Term_XML.Encode; fun proof consts prf = prf |> variant [fn MinProof => ([], []), fn PBound a => ([], int a), fn Abst (a, b, c) => ([a], pair (option typ) (proof consts) (b, c)), fn AbsP (a, b, c) => ([a], pair (option (term consts)) (proof consts) (b, c)), fn a % b => ([], pair (proof consts) (option (term consts)) (a, b)), fn a %% b => ([], pair (proof consts) (proof consts) (a, b)), fn Hyp a => ([], term consts a), fn PAxm (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)), fn PClass (a, b) => ([b], typ a), fn Oracle (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)), fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) => ([int_atom serial, theory_name, name], pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) (map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))] and proof_body consts (PBody {oracles, thms, proof = prf}) = triple (list (pair (pair string (properties o Position.properties_of)) (option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf) and thm consts (a, thm_node) = pair int (pair string (pair string (pair (term consts) (proof_body consts)))) (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node, (Future.join (thm_node_body thm_node)))))); fun standard_term consts t = t |> variant [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))), fn Free (a, _) => ([a], []), fn Var (a, _) => (indexname a, []), fn Bound a => ([], int a), fn Abs (a, b, c) => ([a], pair typ (standard_term consts) (b, c)), fn op $ a => ([], pair (standard_term consts) (standard_term consts) a)]; fun standard_proof consts prf = prf |> variant [fn MinProof => ([], []), fn PBound a => ([], int a), fn Abst (a, SOME b, c) => ([a], pair typ (standard_proof consts) (b, c)), fn AbsP (a, SOME b, c) => ([a], pair (standard_term consts) (standard_proof consts) (b, c)), fn a % SOME b => ([], pair (standard_proof consts) (standard_term consts) (a, b)), fn a %% b => ([], pair (standard_proof consts) (standard_proof consts) (a, b)), fn Hyp a => ([], standard_term consts a), fn PAxm (name, _, SOME Ts) => ([name], list typ Ts), fn PClass (T, c) => ([c], typ T), fn Oracle (name, prop, SOME Ts) => ([name], pair (standard_term consts) (list typ) (prop, Ts)), fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) => ([int_atom serial, theory_name, name], list typ Ts)]; in val encode = proof; val encode_body = proof_body; val encode_standard_term = standard_term; val encode_standard_proof = standard_proof; end; (* decode *) local open XML.Decode Term_XML.Decode; fun proof consts prf = prf |> variant [fn ([], []) => MinProof, fn ([], a) => PBound (int a), fn ([a], b) => let val (c, d) = pair (option typ) (proof consts) b in Abst (a, c, d) end, fn ([a], b) => let val (c, d) = pair (option (term consts)) (proof consts) b in AbsP (a, c, d) end, fn ([], a) => op % (pair (proof consts) (option (term consts)) a), fn ([], a) => op %% (pair (proof consts) (proof consts) a), fn ([], a) => Hyp (term consts a), fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in PAxm (a, c, d) end, fn ([b], a) => PClass (typ a, b), fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in Oracle (a, c, d) end, fn ([a, b, c], d) => let val ((e, (f, (g, h)))) = pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) d; val header = thm_header (int_atom a) (map Position.of_properties e) b c f g; in PThm (header, thm_body h) end] and proof_body consts x = let val (a, b, c) = triple (list (pair (pair string (Position.of_properties o properties)) (option (term consts)))) (list (thm consts)) (proof consts) x; in PBody {oracles = a, thms = b, proof = c} end and thm consts x = let val (a, (b, (c, (d, e)))) = pair int (pair string (pair string (pair (term consts) (proof_body consts)))) x in (a, make_thm_node b c d (Future.value e) no_export) end; in val decode = proof; val decode_body = proof_body; end; (** proof objects with different levels of detail **) val proofs = Unsynchronized.ref 2; fun proofs_enabled () = ! proofs >= 2; fun atomic_proof prf = (case prf of Abst _ => false | AbsP _ => false | op % _ => false | op %% _ => false | MinProof => false | _ => true); fun compact_proof (prf % _) = compact_proof prf | compact_proof (prf1 %% prf2) = atomic_proof prf2 andalso compact_proof prf1 | compact_proof prf = atomic_proof prf; fun (prf %> t) = prf % SOME t; val proof_combt = Library.foldl (op %>); val proof_combt' = Library.foldl (op %); val proof_combP = Library.foldl (op %%); fun strip_combt prf = let fun stripc (prf % t, ts) = stripc (prf, t::ts) | stripc x = x in stripc (prf, []) end; fun strip_combP prf = let fun stripc (prf %% prf', prfs) = stripc (prf, prf'::prfs) | stripc x = x in stripc (prf, []) end; fun strip_thm_body (body as PBody {proof, ...}) = (case fst (strip_combt (fst (strip_combP proof))) of PThm (_, Thm_Body {body = body', ...}) => Future.join body' | _ => body); val mk_Abst = fold_rev (fn (x, _: typ) => fn prf => Abst (x, NONE, prf)); val mk_AbsP = fold_rev (fn _: term => fn prf => AbsP ("H", NONE, prf)); fun map_proof_same term typ ofclass = let val typs = Same.map typ; fun proof (Abst (s, T, prf)) = (Abst (s, Same.map_option typ T, Same.commit proof prf) handle Same.SAME => Abst (s, T, proof prf)) | proof (AbsP (s, t, prf)) = (AbsP (s, Same.map_option term t, Same.commit proof prf) handle Same.SAME => AbsP (s, t, proof prf)) | proof (prf % t) = (proof prf % Same.commit (Same.map_option term) t handle Same.SAME => prf % Same.map_option term t) | proof (prf1 %% prf2) = (proof prf1 %% Same.commit proof prf2 handle Same.SAME => prf1 %% proof prf2) | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts)) | proof (PClass T_c) = ofclass T_c | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts)) | proof (PThm ({serial, pos, theory_name, name, prop, types = SOME Ts}, thm_body)) = PThm (thm_header serial pos theory_name name prop (SOME (typs Ts)), thm_body) | proof _ = raise Same.SAME; in proof end; fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => PClass (typ T, c)); fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ; fun same eq f x = let val x' = f x in if eq (x, x') then raise Same.SAME else x' end; fun map_proof_terms f g = Same.commit (map_proof_terms_same (same (op =) f) (same (op =) g)); fun map_proof_types f = Same.commit (map_proof_types_same (same (op =) f)); fun fold_proof_terms f (Abst (_, _, prf)) = fold_proof_terms f prf | fold_proof_terms f (AbsP (_, SOME t, prf)) = f t #> fold_proof_terms f prf | fold_proof_terms f (AbsP (_, NONE, prf)) = fold_proof_terms f prf | fold_proof_terms f (prf % SOME t) = fold_proof_terms f prf #> f t | fold_proof_terms f (prf % NONE) = fold_proof_terms f prf | fold_proof_terms f (prf1 %% prf2) = fold_proof_terms f prf1 #> fold_proof_terms f prf2 | fold_proof_terms _ _ = I; fun fold_proof_terms_types f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms_types f g prf | fold_proof_terms_types f g (Abst (_, NONE, prf)) = fold_proof_terms_types f g prf | fold_proof_terms_types f g (AbsP (_, SOME t, prf)) = f t #> fold_proof_terms_types f g prf | fold_proof_terms_types f g (AbsP (_, NONE, prf)) = fold_proof_terms_types f g prf | fold_proof_terms_types f g (prf % SOME t) = fold_proof_terms_types f g prf #> f t | fold_proof_terms_types f g (prf % NONE) = fold_proof_terms_types f g prf | fold_proof_terms_types f g (prf1 %% prf2) = fold_proof_terms_types f g prf1 #> fold_proof_terms_types f g prf2 | fold_proof_terms_types _ g (PAxm (_, _, SOME Ts)) = fold g Ts | fold_proof_terms_types _ g (PClass (T, _)) = g T | fold_proof_terms_types _ g (Oracle (_, _, SOME Ts)) = fold g Ts | fold_proof_terms_types _ g (PThm ({types = SOME Ts, ...}, _)) = fold g Ts | fold_proof_terms_types _ _ _ = I; fun maxidx_proof prf = fold_proof_terms_types Term.maxidx_term Term.maxidx_typ prf; fun size_of_proof (Abst (_, _, prf)) = 1 + size_of_proof prf | size_of_proof (AbsP (_, _, prf)) = 1 + size_of_proof prf | size_of_proof (prf % _) = 1 + size_of_proof prf | size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2 | size_of_proof _ = 1; fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types) | change_types (SOME [T]) (PClass (_, c)) = PClass (T, c) | change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types) | change_types types (PThm ({serial, pos, theory_name, name, prop, types = _}, thm_body)) = PThm (thm_header serial pos theory_name name prop types, thm_body) | change_types _ prf = prf; (* utilities *) fun strip_abs (_::Ts) (Abs (_, _, t)) = strip_abs Ts t | strip_abs _ t = t; fun mk_abs Ts t = Library.foldl (fn (t', T) => Abs ("", T, t')) (t, Ts); (*Abstraction of a proof term over its occurrences of v, which must contain no loose bound variables. The resulting proof term is ready to become the body of an Abst.*) fun prf_abstract_over v = let fun abst' lev u = if v aconv u then Bound lev else (case u of Abs (a, T, t) => Abs (a, T, abst' (lev + 1) t) | f $ t => (abst' lev f $ absth' lev t handle Same.SAME => f $ abst' lev t) | _ => raise Same.SAME) and absth' lev t = (abst' lev t handle Same.SAME => t); fun abst lev (AbsP (a, t, prf)) = (AbsP (a, Same.map_option (abst' lev) t, absth lev prf) handle Same.SAME => AbsP (a, t, abst lev prf)) | abst lev (Abst (a, T, prf)) = Abst (a, T, abst (lev + 1) prf) | abst lev (prf1 %% prf2) = (abst lev prf1 %% absth lev prf2 handle Same.SAME => prf1 %% abst lev prf2) | abst lev (prf % t) = (abst lev prf % Option.map (absth' lev) t handle Same.SAME => prf % Same.map_option (abst' lev) t) | abst _ _ = raise Same.SAME and absth lev prf = (abst lev prf handle Same.SAME => prf); in absth 0 end; (*increments a proof term's non-local bound variables required when moving a proof term within abstractions inc is increment for bound variables lev is level at which a bound variable is considered 'loose'*) fun incr_bv' inct tlev t = incr_bv (inct, tlev, t); fun prf_incr_bv' incP _ Plev _ (PBound i) = if i >= Plev then PBound (i+incP) else raise Same.SAME | prf_incr_bv' incP inct Plev tlev (AbsP (a, t, body)) = (AbsP (a, Same.map_option (same (op =) (incr_bv' inct tlev)) t, prf_incr_bv incP inct (Plev+1) tlev body) handle Same.SAME => AbsP (a, t, prf_incr_bv' incP inct (Plev+1) tlev body)) | prf_incr_bv' incP inct Plev tlev (Abst (a, T, body)) = Abst (a, T, prf_incr_bv' incP inct Plev (tlev+1) body) | prf_incr_bv' incP inct Plev tlev (prf %% prf') = (prf_incr_bv' incP inct Plev tlev prf %% prf_incr_bv incP inct Plev tlev prf' handle Same.SAME => prf %% prf_incr_bv' incP inct Plev tlev prf') | prf_incr_bv' incP inct Plev tlev (prf % t) = (prf_incr_bv' incP inct Plev tlev prf % Option.map (incr_bv' inct tlev) t handle Same.SAME => prf % Same.map_option (same (op =) (incr_bv' inct tlev)) t) | prf_incr_bv' _ _ _ _ _ = raise Same.SAME and prf_incr_bv incP inct Plev tlev prf = (prf_incr_bv' incP inct Plev tlev prf handle Same.SAME => prf); fun incr_pboundvars 0 0 prf = prf | incr_pboundvars incP inct prf = prf_incr_bv incP inct 0 0 prf; fun prf_loose_bvar1 (prf1 %% prf2) k = prf_loose_bvar1 prf1 k orelse prf_loose_bvar1 prf2 k | prf_loose_bvar1 (prf % SOME t) k = prf_loose_bvar1 prf k orelse loose_bvar1 (t, k) | prf_loose_bvar1 (_ % NONE) _ = true | prf_loose_bvar1 (AbsP (_, SOME t, prf)) k = loose_bvar1 (t, k) orelse prf_loose_bvar1 prf k | prf_loose_bvar1 (AbsP (_, NONE, _)) _ = true | prf_loose_bvar1 (Abst (_, _, prf)) k = prf_loose_bvar1 prf (k+1) | prf_loose_bvar1 _ _ = false; fun prf_loose_Pbvar1 (PBound i) k = i = k | prf_loose_Pbvar1 (prf1 %% prf2) k = prf_loose_Pbvar1 prf1 k orelse prf_loose_Pbvar1 prf2 k | prf_loose_Pbvar1 (prf % _) k = prf_loose_Pbvar1 prf k | prf_loose_Pbvar1 (AbsP (_, _, prf)) k = prf_loose_Pbvar1 prf (k+1) | prf_loose_Pbvar1 (Abst (_, _, prf)) k = prf_loose_Pbvar1 prf k | prf_loose_Pbvar1 _ _ = false; fun prf_add_loose_bnos plev _ (PBound i) (is, js) = if i < plev then (is, js) else (insert (op =) (i-plev) is, js) | prf_add_loose_bnos plev tlev (prf1 %% prf2) p = prf_add_loose_bnos plev tlev prf2 (prf_add_loose_bnos plev tlev prf1 p) | prf_add_loose_bnos plev tlev (prf % opt) (is, js) = prf_add_loose_bnos plev tlev prf (case opt of NONE => (is, insert (op =) ~1 js) | SOME t => (is, add_loose_bnos (t, tlev, js))) | prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) = prf_add_loose_bnos (plev+1) tlev prf (case opt of NONE => (is, insert (op =) ~1 js) | SOME t => (is, add_loose_bnos (t, tlev, js))) | prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p = prf_add_loose_bnos plev (tlev+1) prf p | prf_add_loose_bnos _ _ _ _ = ([], []); (* substitutions *) local fun conflicting_tvarsT envT = Term.fold_atyps (fn T => fn instT => (case T of TVar (v as (_, S)) => if Term_Subst.TVars.defined instT v orelse can (Type.lookup envT) v then instT else Term_Subst.TVars.update (v, Logic.dummy_tfree S) instT | _ => instT)); fun conflicting_tvars env = Term.fold_aterms (fn t => fn inst => (case t of Var (v as (_, T)) => if Term_Subst.Vars.defined inst v orelse can (Envir.lookup env) v then inst else Term_Subst.Vars.update (v, Free ("dummy", T)) inst | _ => inst)); fun del_conflicting_tvars envT ty = Term_Subst.instantiateT (Term_Subst.TVars.build (conflicting_tvarsT envT ty)) ty; fun del_conflicting_vars env tm = let val instT = Term_Subst.TVars.build (tm |> Term.fold_types (conflicting_tvarsT (Envir.type_env env))); val inst = Term_Subst.Vars.build (tm |> conflicting_tvars env); in Term_Subst.instantiate (instT, inst) tm end; in fun norm_proof env = let val envT = Envir.type_env env; fun msg s = warning ("type conflict in norm_proof:\n" ^ s); fun htype f t = f env t handle TYPE (s, _, _) => (msg s; f env (del_conflicting_vars env t)); fun htypeT f T = f envT T handle TYPE (s, _, _) => (msg s; f envT (del_conflicting_tvars envT T)); fun htypeTs f Ts = f envT Ts handle TYPE (s, _, _) => (msg s; f envT (map (del_conflicting_tvars envT) Ts)); fun norm (Abst (s, T, prf)) = (Abst (s, Same.map_option (htypeT Envir.norm_type_same) T, Same.commit norm prf) handle Same.SAME => Abst (s, T, norm prf)) | norm (AbsP (s, t, prf)) = (AbsP (s, Same.map_option (htype Envir.norm_term_same) t, Same.commit norm prf) handle Same.SAME => AbsP (s, t, norm prf)) | norm (prf % t) = (norm prf % Option.map (htype Envir.norm_term) t handle Same.SAME => prf % Same.map_option (htype Envir.norm_term_same) t) | norm (prf1 %% prf2) = (norm prf1 %% Same.commit norm prf2 handle Same.SAME => prf1 %% norm prf2) | norm (PAxm (s, prop, Ts)) = PAxm (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts) | norm (PClass (T, c)) = PClass (htypeT Envir.norm_type_same T, c) | norm (Oracle (s, prop, Ts)) = Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts) | norm (PThm ({serial = i, pos = p, theory_name, name = a, prop = t, types = Ts}, thm_body)) = PThm (thm_header i p theory_name a t (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body) | norm _ = raise Same.SAME; in Same.commit norm end; end; (* remove some types in proof term (to save space) *) fun remove_types (Abs (s, _, t)) = Abs (s, dummyT, remove_types t) | remove_types (t $ u) = remove_types t $ remove_types u | remove_types (Const (s, _)) = Const (s, dummyT) | remove_types t = t; fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) = Envir.Envir {maxidx = maxidx, tenv = Vartab.map (K (apsnd remove_types)) tenv, tyenv = tyenv}; fun norm_proof' env prf = norm_proof (remove_types_env env) prf; (* substitution of bound variables *) fun prf_subst_bounds args prf = let val n = length args; fun subst' lev (Bound i) = (if i Bound (i-n)) (*loose: change it*) | subst' lev (Abs (a, T, body)) = Abs (a, T, subst' (lev+1) body) | subst' lev (f $ t) = (subst' lev f $ substh' lev t handle Same.SAME => f $ subst' lev t) | subst' _ _ = raise Same.SAME and substh' lev t = (subst' lev t handle Same.SAME => t); fun subst lev (AbsP (a, t, body)) = (AbsP (a, Same.map_option (subst' lev) t, substh lev body) handle Same.SAME => AbsP (a, t, subst lev body)) | subst lev (Abst (a, T, body)) = Abst (a, T, subst (lev+1) body) | subst lev (prf %% prf') = (subst lev prf %% substh lev prf' handle Same.SAME => prf %% subst lev prf') | subst lev (prf % t) = (subst lev prf % Option.map (substh' lev) t handle Same.SAME => prf % Same.map_option (subst' lev) t) | subst _ _ = raise Same.SAME and substh lev prf = (subst lev prf handle Same.SAME => prf); in (case args of [] => prf | _ => substh 0 prf) end; fun prf_subst_pbounds args prf = let val n = length args; fun subst (PBound i) Plev tlev = (if i < Plev then raise Same.SAME (*var is locally bound*) else incr_pboundvars Plev tlev (nth args (i-Plev)) handle General.Subscript => PBound (i-n) (*loose: change it*)) | subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev) | subst (Abst (a, T, body)) Plev tlev = Abst (a, T, subst body Plev (tlev+1)) | subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev handle Same.SAME => prf %% subst prf' Plev tlev) | subst (prf % t) Plev tlev = subst prf Plev tlev % t | subst _ _ _ = raise Same.SAME and substh prf Plev tlev = (subst prf Plev tlev handle Same.SAME => prf) in (case args of [] => prf | _ => substh prf 0 0) end; (* freezing and thawing of variables in proof terms *) local fun frzT names = map_type_tvar (fn (ixn, S) => TFree (the (AList.lookup (op =) names ixn), S)); fun thawT names = map_type_tfree (fn (a, S) => (case AList.lookup (op =) names a of NONE => TFree (a, S) | SOME ixn => TVar (ixn, S))); fun freeze names names' (t $ u) = freeze names names' t $ freeze names names' u | freeze names names' (Abs (s, T, t)) = Abs (s, frzT names' T, freeze names names' t) | freeze _ names' (Const (s, T)) = Const (s, frzT names' T) | freeze _ names' (Free (s, T)) = Free (s, frzT names' T) | freeze names names' (Var (ixn, T)) = Free (the (AList.lookup (op =) names ixn), frzT names' T) | freeze _ _ t = t; fun thaw names names' (t $ u) = thaw names names' t $ thaw names names' u | thaw names names' (Abs (s, T, t)) = Abs (s, thawT names' T, thaw names names' t) | thaw _ names' (Const (s, T)) = Const (s, thawT names' T) | thaw names names' (Free (s, T)) = let val T' = thawT names' T in (case AList.lookup (op =) names s of NONE => Free (s, T') | SOME ixn => Var (ixn, T')) end | thaw _ names' (Var (ixn, T)) = Var (ixn, thawT names' T) | thaw _ _ t = t; in fun freeze_thaw_prf prf = let val (fs, Tfs, vs, Tvs) = fold_proof_terms_types (fn t => fn (fs, Tfs, vs, Tvs) => (Term.add_free_names t fs, Term.add_tfree_names t Tfs, Term.add_var_names t vs, Term.add_tvar_names t Tvs)) (fn T => fn (fs, Tfs, vs, Tvs) => (fs, Term.add_tfree_namesT T Tfs, vs, Term.add_tvar_namesT T Tvs)) prf ([], [], [], []); val names = vs ~~ Name.variant_list fs (map fst vs); val names' = Tvs ~~ Name.variant_list Tfs (map fst Tvs); val rnames = map swap names; val rnames' = map swap names'; in (map_proof_terms (freeze names names') (frzT names') prf, map_proof_terms (thaw rnames rnames') (thawT rnames')) end; end; (** inference rules **) (* trivial implication *) val trivial_proof = AbsP ("H", NONE, PBound 0); (* implication introduction *) fun gen_implies_intr_proof f h prf = let fun abshyp i (Hyp t) = if h aconv t then PBound i else raise Same.SAME | abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf) | abshyp i (AbsP (s, t, prf)) = AbsP (s, t, abshyp (i + 1) prf) | abshyp i (prf % t) = abshyp i prf % t | abshyp i (prf1 %% prf2) = (abshyp i prf1 %% abshyph i prf2 handle Same.SAME => prf1 %% abshyp i prf2) | abshyp _ _ = raise Same.SAME and abshyph i prf = (abshyp i prf handle Same.SAME => prf); in AbsP ("H", f h, abshyph 0 prf) end; val implies_intr_proof = gen_implies_intr_proof (K NONE); val implies_intr_proof' = gen_implies_intr_proof SOME; (* forall introduction *) fun forall_intr_proof (a, v) opt_T prf = Abst (a, opt_T, prf_abstract_over v prf); fun forall_intr_proof' v prf = let val (a, T) = (case v of Var ((a, _), T) => (a, T) | Free (a, T) => (a, T)) in forall_intr_proof (a, v) (SOME T) prf end; (* varify *) fun varify_proof t fixed prf = let - val fs = Term.fold_types (Term.fold_atyps - (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t []; + val fs = + (t, []) |-> (Term.fold_types o Term.fold_atyps) + (fn TFree v => if Term_Subst.TFrees.defined fixed v then I else insert (op =) v | _ => I); val used = Name.context |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t; val fmap = fs ~~ #1 (fold_map Name.variant (map fst fs) used); fun thaw (a, S) = (case AList.lookup (op =) fmap (a, S) of NONE => TFree (a, S) | SOME b => TVar ((b, 0), S)); in map_proof_terms (map_types (map_type_tfree thaw)) (map_type_tfree thaw) prf end; local fun new_name ix (pairs, used) = let val v = singleton (Name.variant_list used) (string_of_indexname ix) in ((ix, v) :: pairs, v :: used) end; fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of NONE => TVar (ix, sort) | SOME name => TFree (name, sort)); in fun legacy_freezeT t prf = let val used = Term.add_tfree_names t []; val (alist, _) = fold_rev new_name (map #1 (Term.add_tvars t [])) ([], used); in (case alist of [] => prf (*nothing to do!*) | _ => let val frzT = map_type_tvar (freeze_one alist) in map_proof_terms (map_types frzT) frzT prf end) end; end; (* rotate assumptions *) fun rotate_proof Bs Bi' params asms m prf = let val i = length asms; val j = length Bs; in mk_AbsP (Bs @ [Bi']) (proof_combP (prf, map PBound (j downto 1) @ [mk_Abst params (mk_AbsP asms (proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)), map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))])) end; (* permute premises *) fun permute_prems_proof prems' j k prf = let val n = length prems' in mk_AbsP prems' (proof_combP (prf, map PBound ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k)))) end; (* generalization *) fun generalize_proof (tfrees, frees) idx prop prf = let val gen = if Symtab.is_empty frees then [] else fold_aterms (fn Free (x, T) => Symtab.defined frees x ? insert (op =) (x, T) | _ => I) (Term_Subst.generalize (tfrees, Symtab.empty) idx prop) []; in prf |> Same.commit (map_proof_terms_same (Term_Subst.generalize_same (tfrees, Symtab.empty) idx) (Term_Subst.generalizeT_same tfrees idx)) |> fold (fn (x, T) => forall_intr_proof (x, Free (x, T)) NONE) gen |> fold_rev (fn (x, T) => fn prf' => prf' %> Var (Name.clean_index (x, idx), T)) gen end; (* instantiation *) fun instantiate (instT, inst) = Same.commit (map_proof_terms_same (Term_Subst.instantiate_same (instT, Term_Subst.Vars.map (K remove_types) inst)) (Term_Subst.instantiateT_same instT)); (* lifting *) fun lift_proof Bi inc prop prf = let fun lift'' Us Ts t = strip_abs Ts (Logic.incr_indexes ([], Us, inc) (mk_abs Ts t)); fun lift' Us Ts (Abst (s, T, prf)) = (Abst (s, Same.map_option (Logic.incr_tvar_same inc) T, lifth' Us (dummyT::Ts) prf) handle Same.SAME => Abst (s, T, lift' Us (dummyT::Ts) prf)) | lift' Us Ts (AbsP (s, t, prf)) = (AbsP (s, Same.map_option (same (op =) (lift'' Us Ts)) t, lifth' Us Ts prf) handle Same.SAME => AbsP (s, t, lift' Us Ts prf)) | lift' Us Ts (prf % t) = (lift' Us Ts prf % Option.map (lift'' Us Ts) t handle Same.SAME => prf % Same.map_option (same (op =) (lift'' Us Ts)) t) | lift' Us Ts (prf1 %% prf2) = (lift' Us Ts prf1 %% lifth' Us Ts prf2 handle Same.SAME => prf1 %% lift' Us Ts prf2) | lift' _ _ (PAxm (s, prop, Ts)) = PAxm (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts) | lift' _ _ (PClass (T, c)) = PClass (Logic.incr_tvar_same inc T, c) | lift' _ _ (Oracle (s, prop, Ts)) = Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts) | lift' _ _ (PThm ({serial = i, pos = p, theory_name, name = s, prop, types = Ts}, thm_body)) = PThm (thm_header i p theory_name s prop ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts), thm_body) | lift' _ _ _ = raise Same.SAME and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf); val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop); val k = length ps; fun mk_app b (i, j, prf) = if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j); fun lift Us bs i j (Const ("Pure.imp", _) $ A $ B) = AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B) | lift Us bs i j (Const ("Pure.all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t) | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf, map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k)))) (i + k - 1 downto i)); in mk_AbsP ps (lift [] [] 0 0 Bi) end; fun incr_indexes i = Same.commit (map_proof_terms_same (Logic.incr_indexes_same ([], [], i)) (Logic.incr_tvar_same i)); (* proof by assumption *) fun mk_asm_prf t i m = let fun imp_prf _ i 0 = PBound i | imp_prf (Const ("Pure.imp", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1)) | imp_prf _ i _ = PBound i; fun all_prf (Const ("Pure.all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t) | all_prf t = imp_prf t (~i) m in all_prf t end; fun assumption_proof Bs Bi n prf = mk_AbsP Bs (proof_combP (prf, map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi n ~1])); (* composition of object rule with proof state *) fun flatten_params_proof i j n (Const ("Pure.imp", _) $ A $ B, k) = AbsP ("H", NONE (*A*), flatten_params_proof (i+1) j n (B, k)) | flatten_params_proof i j n (Const ("Pure.all", _) $ Abs (a, T, t), k) = Abst (a, NONE (*T*), flatten_params_proof i (j+1) n (t, k)) | flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i), map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0))); fun bicompose_proof flatten Bs As A oldAs n m rprf sprf = let val lb = length Bs; val la = length As; in mk_AbsP (Bs @ As) (proof_combP (sprf, map PBound (lb + la - 1 downto la)) %% proof_combP (rprf, (if n>0 then [mk_asm_prf (the A) n m] else []) @ map (if flatten then flatten_params_proof 0 0 n else PBound o snd) (oldAs ~~ (la - 1 downto 0)))) end; (** type classes **) fun strip_shyps_proof algebra present witnessed extra prf = let val replacements = present @ witnessed @ map (`Logic.dummy_tfree) extra; fun get_replacement S = replacements |> get_first (fn (T', S') => if Sorts.sort_le algebra (S', S) then SOME T' else NONE); fun replace T = if exists (fn (T', _) => T' = T) present then raise Same.SAME else (case get_replacement (Type.sort_of_atyp T) of SOME T' => T' | NONE => raise Fail "strip_shyps_proof: bad type variable in proof term"); in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end; fun of_sort_proof algebra classrel_proof arity_proof hyps = Sorts.of_sort_derivation algebra {class_relation = fn _ => fn _ => fn (prf, c1) => fn c2 => if c1 = c2 then prf else classrel_proof (c1, c2) %% prf, type_constructor = fn (a, _) => fn dom => fn c => let val Ss = map (map snd) dom and prfs = maps (map fst) dom in proof_combP (arity_proof (a, Ss, c), prfs) end, type_variable = fn typ => map (fn c => (hyps (typ, c), c)) (Type.sort_of_atyp typ)}; (** axioms and theorems **) val add_type_variables = (fold_types o fold_atyps) (insert (op =)); fun type_variables_of t = rev (add_type_variables t []); val add_variables = fold_aterms (fn a => (is_Var a orelse is_Free a) ? insert (op =) a); fun variables_of t = rev (add_variables t []); fun test_args _ [] = true | test_args is (Bound i :: ts) = not (member (op =) is i) andalso test_args (i :: is) ts | test_args _ _ = false; fun is_fun (Type ("fun", _)) = true | is_fun (TVar _) = true | is_fun _ = false; fun vars_of t = map Var (rev (Term.add_vars t [])); fun add_funvars Ts (vs, t) = if is_fun (fastype_of1 (Ts, t)) then union (op =) vs (map_filter (fn Var (ixn, T) => if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t)) else vs; fun add_npvars q p Ts (vs, Const ("Pure.imp", _) $ t $ u) = add_npvars q p Ts (add_npvars q (not p) Ts (vs, t), u) | add_npvars q p Ts (vs, Const ("Pure.all", Type (_, [Type (_, [T, _]), _])) $ t) = add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t) | add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t) | add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t) and add_npvars' Ts (vs, t) = (case strip_comb t of (Var (ixn, _), ts) => if test_args [] ts then vs else Library.foldl (add_npvars' Ts) (AList.update (op =) (ixn, Library.foldl (add_funvars Ts) ((these ooo AList.lookup) (op =) vs ixn, ts)) vs, ts) | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts) | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts)); fun prop_vars (Const ("Pure.imp", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q) | prop_vars (Const ("Pure.all", _) $ Abs (_, _, t)) = prop_vars t | prop_vars t = (case strip_comb t of (Var (ixn, _), _) => [ixn] | _ => []); fun is_proj t = let fun is_p i t = (case strip_comb t of (Bound _, []) => false | (Bound j, ts) => j >= i orelse exists (is_p i) ts | (Abs (_, _, u), _) => is_p (i+1) u | (_, ts) => exists (is_p i) ts) in (case strip_abs_body t of Bound _ => true | t' => is_p 0 t') end; fun prop_args prop = let val needed_vars = union (op =) (Library.foldl (uncurry (union (op =))) ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop)))) (prop_vars prop); in variables_of prop |> map (fn var as Var (ixn, _) => if member (op =) needed_vars ixn then SOME var else NONE | free => SOME free) end; fun const_proof mk name prop = let val args = prop_args prop; val ({outer_constraints, ...}, prop1) = Logic.unconstrainT [] prop; val head = mk (name, prop1, NONE); in proof_combP (proof_combt' (head, args), map PClass outer_constraints) end; val axm_proof = const_proof PAxm; val oracle_proof = const_proof Oracle; val shrink_proof = let fun shrink ls lev (prf as Abst (a, T, body)) = let val (b, is, ch, body') = shrink ls (lev+1) body in (b, is, ch, if ch then Abst (a, T, body') else prf) end | shrink ls lev (prf as AbsP (a, t, body)) = let val (b, is, ch, body') = shrink (lev::ls) lev body in (b orelse member (op =) is 0, map_filter (fn 0 => NONE | i => SOME (i-1)) is, ch, if ch then AbsP (a, t, body') else prf) end | shrink ls lev prf = let val (is, ch, _, prf') = shrink' ls lev [] [] prf in (false, is, ch, prf') end and shrink' ls lev ts prfs (prf as prf1 %% prf2) = let val p as (_, is', ch', prf') = shrink ls lev prf2; val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1 in (union (op =) is is', ch orelse ch', ts', if ch orelse ch' then prf'' %% prf' else prf) end | shrink' ls lev ts prfs (prf as prf1 % t) = let val (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1 in (is, ch orelse ch', ts', if ch orelse ch' then prf' % t' else prf) end | shrink' ls lev ts prfs (prf as PBound i) = (if exists (fn SOME (Bound j) => lev-j <= nth ls i | _ => true) ts orelse has_duplicates (op =) (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts)) orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf) | shrink' _ _ ts _ (Hyp t) = ([], false, map (pair false) ts, Hyp t) | shrink' _ _ ts _ (prf as MinProof) = ([], false, map (pair false) ts, prf) | shrink' _ _ ts _ (prf as PClass _) = ([], false, map (pair false) ts, prf) | shrink' _ _ ts prfs prf = let val prop = (case prf of PAxm (_, prop, _) => prop | Oracle (_, prop, _) => prop | PThm ({prop, ...}, _) => prop | _ => raise Fail "shrink: proof not in normal form"); val vs = vars_of prop; val (ts', ts'') = chop (length vs) ts; val insts = take (length ts') (map (fst o dest_Var) vs) ~~ ts'; val nvs = Library.foldl (fn (ixns', (ixn, ixns)) => insert (op =) ixn (case AList.lookup (op =) insts ixn of SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns' | _ => union (op =) ixns ixns')) (needed prop ts'' prfs, add_npvars false true [] ([], prop)); val insts' = map (fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE) | (_, x) => (false, x)) insts in ([], false, insts' @ map (pair false) ts'', prf) end and needed (Const ("Pure.imp", _) $ t $ u) ts ((b, _, _, _)::prfs) = union (op =) (if b then map (fst o dest_Var) (vars_of t) else []) (needed u ts prfs) | needed (Var (ixn, _)) (_::_) _ = [ixn] | needed _ _ _ = []; in fn prf => #4 (shrink [] 0 prf) end; (** axioms for equality **) val aT = TFree ("'a", []); val bT = TFree ("'b", []); val x = Free ("x", aT); val y = Free ("y", aT); val z = Free ("z", aT); val A = Free ("A", propT); val B = Free ("B", propT); val f = Free ("f", aT --> bT); val g = Free ("g", aT --> bT); val equality_axms = [("reflexive", Logic.mk_equals (x, x)), ("symmetric", Logic.mk_implies (Logic.mk_equals (x, y), Logic.mk_equals (y, x))), ("transitive", Logic.list_implies ([Logic.mk_equals (x, y), Logic.mk_equals (y, z)], Logic.mk_equals (x, z))), ("equal_intr", Logic.list_implies ([Logic.mk_implies (A, B), Logic.mk_implies (B, A)], Logic.mk_equals (A, B))), ("equal_elim", Logic.list_implies ([Logic.mk_equals (A, B), A], B)), ("abstract_rule", Logic.mk_implies (Logic.all x (Logic.mk_equals (f $ x, g $ x)), Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))), ("combination", Logic.list_implies ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f $ x, g $ y)))]; val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm, equal_elim_axm, abstract_rule_axm, combination_axm] = map (fn (s, t) => PAxm ("Pure." ^ s, Logic.varify_global t, NONE)) equality_axms; val reflexive_proof = reflexive_axm % NONE; val is_reflexive_proof = fn PAxm ("Pure.reflexive", _, _) % _ => true | _ => false; fun symmetric_proof prf = if is_reflexive_proof prf then prf else symmetric_axm % NONE % NONE %% prf; fun transitive_proof U u prf1 prf2 = if is_reflexive_proof prf1 then prf2 else if is_reflexive_proof prf2 then prf1 else if U = propT then transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2 else transitive_axm % NONE % NONE % NONE %% prf1 %% prf2; fun equal_intr_proof A B prf1 prf2 = equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2; fun equal_elim_proof A B prf1 prf2 = equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2; fun abstract_rule_proof (a, x) prf = abstract_rule_axm % NONE % NONE %% forall_intr_proof (a, x) NONE prf; fun check_comb (PAxm ("Pure.combination", _, _) % f % _ % _ % _ %% prf %% _) = is_some f orelse check_comb prf | check_comb (PAxm ("Pure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) = check_comb prf1 andalso check_comb prf2 | check_comb (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf) = check_comb prf | check_comb _ = false; fun combination_proof f g t u prf1 prf2 = let val f = Envir.beta_norm f; val g = Envir.beta_norm g; val prf = if check_comb prf1 then combination_axm % NONE % NONE else (case prf1 of PAxm ("Pure.reflexive", _, _) % _ => combination_axm %> remove_types f % NONE | _ => combination_axm %> remove_types f %> remove_types g) in prf % (case head_of f of Abs _ => SOME (remove_types t) | Var _ => SOME (remove_types t) | _ => NONE) % (case head_of g of Abs _ => SOME (remove_types u) | Var _ => SOME (remove_types u) | _ => NONE) %% prf1 %% prf2 end; (** rewriting on proof terms **) (* simple first order matching functions for terms and proofs (see pattern.ML) *) exception PMatch; fun flt (i: int) = filter (fn n => n < i); fun fomatch Ts tymatch j instsp p = let fun mtch (instsp as (tyinsts, insts)) = fn (Var (ixn, T), t) => if j>0 andalso not (null (flt j (loose_bnos t))) then raise PMatch else (tymatch (tyinsts, fn () => (T, fastype_of1 (Ts, t))), (ixn, t) :: insts) | (Free (a, T), Free (b, U)) => if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch | (Const (a, T), Const (b, U)) => if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch | (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u) | (Bound i, Bound j) => if i=j then instsp else raise PMatch | _ => raise PMatch in mtch instsp (apply2 Envir.beta_eta_contract p) end; fun match_proof Ts tymatch = let fun optmatch _ inst (NONE, _) = inst | optmatch _ _ (SOME _, NONE) = raise PMatch | optmatch mtch inst (SOME x, SOME y) = mtch inst (x, y) fun matcht Ts j (pinst, tinst) (t, u) = (pinst, fomatch Ts tymatch j tinst (t, Envir.beta_norm u)); fun matchT (pinst, (tyinsts, insts)) p = (pinst, (tymatch (tyinsts, K p), insts)); fun matchTs inst (Ts, Us) = Library.foldl (uncurry matchT) (inst, Ts ~~ Us); fun mtch Ts i j (pinst, tinst) (Hyp (Var (ixn, _)), prf) = if i = 0 andalso j = 0 then ((ixn, prf) :: pinst, tinst) else (case apfst (flt i) (apsnd (flt j) (prf_add_loose_bnos 0 0 prf ([], []))) of ([], []) => ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst) | ([], _) => if j = 0 then ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst) else raise PMatch | _ => raise PMatch) | mtch Ts i j inst (prf1 % opt1, prf2 % opt2) = optmatch (matcht Ts j) (mtch Ts i j inst (prf1, prf2)) (opt1, opt2) | mtch Ts i j inst (prf1 %% prf2, prf1' %% prf2') = mtch Ts i j (mtch Ts i j inst (prf1, prf1')) (prf2, prf2') | mtch Ts i j inst (Abst (_, opT, prf1), Abst (_, opU, prf2)) = mtch (the_default dummyT opU :: Ts) i (j+1) (optmatch matchT inst (opT, opU)) (prf1, prf2) | mtch Ts i j inst (prf1, Abst (_, opU, prf2)) = mtch (the_default dummyT opU :: Ts) i (j+1) inst (incr_pboundvars 0 1 prf1 %> Bound 0, prf2) | mtch Ts i j inst (AbsP (_, opt, prf1), AbsP (_, opu, prf2)) = mtch Ts (i+1) j (optmatch (matcht Ts j) inst (opt, opu)) (prf1, prf2) | mtch Ts i j inst (prf1, AbsP (_, _, prf2)) = mtch Ts (i+1) j inst (incr_pboundvars 1 0 prf1 %% PBound 0, prf2) | mtch Ts i j inst (PAxm (s1, _, opTs), PAxm (s2, _, opUs)) = if s1 = s2 then optmatch matchTs inst (opTs, opUs) else raise PMatch | mtch Ts i j inst (PClass (T1, c1), PClass (T2, c2)) = if c1 = c2 then matchT inst (T1, T2) else raise PMatch | mtch Ts i j inst (PThm ({name = name1, prop = prop1, types = types1, ...}, _), PThm ({name = name2, prop = prop2, types = types2, ...}, _)) = if name1 = name2 andalso prop1 = prop2 then optmatch matchTs inst (types1, types2) else raise PMatch | mtch _ _ _ inst (PBound i, PBound j) = if i = j then inst else raise PMatch | mtch _ _ _ _ _ = raise PMatch in mtch Ts 0 0 end; fun prf_subst (pinst, (tyinsts, insts)) = let val substT = Envir.subst_type_same tyinsts; val substTs = Same.map substT; fun subst' lev (Var (xi, _)) = (case AList.lookup (op =) insts xi of NONE => raise Same.SAME | SOME u => incr_boundvars lev u) | subst' _ (Const (s, T)) = Const (s, substT T) | subst' _ (Free (s, T)) = Free (s, substT T) | subst' lev (Abs (a, T, body)) = (Abs (a, substT T, Same.commit (subst' (lev + 1)) body) handle Same.SAME => Abs (a, T, subst' (lev + 1) body)) | subst' lev (f $ t) = (subst' lev f $ Same.commit (subst' lev) t handle Same.SAME => f $ subst' lev t) | subst' _ _ = raise Same.SAME; fun subst plev tlev (AbsP (a, t, body)) = (AbsP (a, Same.map_option (subst' tlev) t, Same.commit (subst (plev + 1) tlev) body) handle Same.SAME => AbsP (a, t, subst (plev + 1) tlev body)) | subst plev tlev (Abst (a, T, body)) = (Abst (a, Same.map_option substT T, Same.commit (subst plev (tlev + 1)) body) handle Same.SAME => Abst (a, T, subst plev (tlev + 1) body)) | subst plev tlev (prf %% prf') = (subst plev tlev prf %% Same.commit (subst plev tlev) prf' handle Same.SAME => prf %% subst plev tlev prf') | subst plev tlev (prf % t) = (subst plev tlev prf % Same.commit (Same.map_option (subst' tlev)) t handle Same.SAME => prf % Same.map_option (subst' tlev) t) | subst plev tlev (Hyp (Var (xi, _))) = (case AList.lookup (op =) pinst xi of NONE => raise Same.SAME | SOME prf' => incr_pboundvars plev tlev prf') | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts) | subst _ _ (PClass (T, c)) = PClass (substT T, c) | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts) | subst _ _ (PThm ({serial = i, pos = p, theory_name, name = id, prop, types}, thm_body)) = PThm (thm_header i p theory_name id prop (Same.map_option substTs types), thm_body) | subst _ _ _ = raise Same.SAME; in fn t => subst 0 0 t handle Same.SAME => t end; (*A fast unification filter: true unless the two terms cannot be unified. Terms must be NORMAL. Treats all Vars as distinct. *) fun could_unify prf1 prf2 = let fun matchrands (prf1 %% prf2) (prf1' %% prf2') = could_unify prf2 prf2' andalso matchrands prf1 prf1' | matchrands (prf % SOME t) (prf' % SOME t') = Term.could_unify (t, t') andalso matchrands prf prf' | matchrands (prf % _) (prf' % _) = matchrands prf prf' | matchrands _ _ = true fun head_of (prf %% _) = head_of prf | head_of (prf % _) = head_of prf | head_of prf = prf in case (head_of prf1, head_of prf2) of (_, Hyp (Var _)) => true | (Hyp (Var _), _) => true | (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2 | (PClass (_, c), PClass (_, d)) => c = d andalso matchrands prf1 prf2 | (PThm ({name = a, prop = propa, ...}, _), PThm ({name = b, prop = propb, ...}, _)) => a = b andalso propa = propb andalso matchrands prf1 prf2 | (PBound i, PBound j) => i = j andalso matchrands prf1 prf2 | (AbsP _, _) => true (*because of possible eta equality*) | (Abst _, _) => true | (_, AbsP _) => true | (_, Abst _) => true | _ => false end; (* rewrite proof *) val no_skel = PBound 0; val normal_skel = Hyp (Var ((Name.uu, 0), propT)); fun rewrite_prf tymatch (rules, procs) prf = let fun rew _ _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel) | rew _ _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel) | rew Ts hs prf = (case get_first (fn r => r Ts hs prf) procs of NONE => get_first (fn (prf1, prf2) => SOME (prf_subst (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2) handle PMatch => NONE) (filter (could_unify prf o fst) rules) | some => some); fun rew0 Ts hs (prf as AbsP (_, _, prf' %% PBound 0)) = if prf_loose_Pbvar1 prf' 0 then rew Ts hs prf else let val prf'' = incr_pboundvars (~1) 0 prf' in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end | rew0 Ts hs (prf as Abst (_, _, prf' % SOME (Bound 0))) = if prf_loose_bvar1 prf' 0 then rew Ts hs prf else let val prf'' = incr_pboundvars 0 (~1) prf' in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end | rew0 Ts hs prf = rew Ts hs prf; fun rew1 _ _ (Hyp (Var _)) _ = NONE | rew1 Ts hs skel prf = (case rew2 Ts hs skel prf of SOME prf1 => (case rew0 Ts hs prf1 of SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2)) | NONE => SOME prf1) | NONE => (case rew0 Ts hs prf of SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1)) | NONE => NONE)) and rew2 Ts hs skel (prf % SOME t) = (case prf of Abst (_, _, body) => let val prf' = prf_subst_bounds [t] body in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end | _ => (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of SOME prf' => SOME (prf' % SOME t) | NONE => NONE)) | rew2 Ts hs skel (prf % NONE) = Option.map (fn prf' => prf' % NONE) (rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf) | rew2 Ts hs skel (prf1 %% prf2) = (case prf1 of AbsP (_, _, body) => let val prf' = prf_subst_pbounds [prf2] body in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end | _ => let val (skel1, skel2) = (case skel of skel1 %% skel2 => (skel1, skel2) | _ => (no_skel, no_skel)) in (case rew1 Ts hs skel1 prf1 of SOME prf1' => (case rew1 Ts hs skel2 prf2 of SOME prf2' => SOME (prf1' %% prf2') | NONE => SOME (prf1' %% prf2)) | NONE => (case rew1 Ts hs skel2 prf2 of SOME prf2' => SOME (prf1 %% prf2') | NONE => NONE)) end) | rew2 Ts hs skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts) hs (case skel of Abst (_, _, skel') => skel' | _ => no_skel) prf of SOME prf' => SOME (Abst (s, T, prf')) | NONE => NONE) | rew2 Ts hs skel (AbsP (s, t, prf)) = (case rew1 Ts (t :: hs) (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of SOME prf' => SOME (AbsP (s, t, prf')) | NONE => NONE) | rew2 _ _ _ _ = NONE; in the_default prf (rew1 [] [] no_skel prf) end; fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) => Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch); fun rewrite_proof_notypes rews = rewrite_prf fst rews; (* theory data *) structure Data = Theory_Data ( type T = ((stamp * (proof * proof)) list * (stamp * (typ list -> term option list -> proof -> (proof * proof) option)) list) * (theory -> proof -> proof) option; val empty = (([], []), NONE); val extend = I; fun merge (((rules1, procs1), preproc1), ((rules2, procs2), preproc2)) : T = ((AList.merge (op =) (K true) (rules1, rules2), AList.merge (op =) (K true) (procs1, procs2)), merge_options (preproc1, preproc2)); ); fun get_rew_data thy = let val (rules, procs) = #1 (Data.get thy) in (map #2 rules, map #2 procs) end; fun rew_proof thy = rewrite_prf fst (get_rew_data thy); fun add_prf_rrule r = (Data.map o apfst o apfst) (cons (stamp (), r)); fun add_prf_rproc p = (Data.map o apfst o apsnd) (cons (stamp (), p)); fun set_preproc f = (Data.map o apsnd) (K (SOME f)); fun apply_preproc thy = (case #2 (Data.get thy) of NONE => I | SOME f => f thy); (** reconstruction of partial proof terms **) fun forall_intr_variables_term prop = fold_rev Logic.all (variables_of prop) prop; fun forall_intr_variables prop prf = fold_rev forall_intr_proof' (variables_of prop) prf; local fun app_types shift prop Ts prf = let val inst = type_variables_of prop ~~ Ts; fun subst_same A = (case AList.lookup (op =) inst A of SOME T => T | NONE => raise Same.SAME); val subst_type_same = Term_Subst.map_atypsT_same (fn TVar ((a, i), S) => subst_same (TVar ((a, i - shift), S)) | A => subst_same A); in Same.commit (map_proof_types_same subst_type_same) prf end; fun guess_name (PThm ({name, ...}, _)) = name | guess_name (prf %% Hyp _) = guess_name prf | guess_name (prf %% PClass _) = guess_name prf | guess_name (prf % NONE) = guess_name prf | guess_name (prf % SOME (Var _)) = guess_name prf | guess_name _ = ""; (* generate constraints for proof term *) fun mk_var env Ts T = let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T) in (list_comb (v, map Bound (length Ts - 1 downto 0)), env') end; fun mk_tvar S (Envir.Envir {maxidx, tenv, tyenv}) = (TVar (("'t", maxidx + 1), S), Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}); val mk_abs = fold (fn T => fn u => Abs ("", T, u)); fun unifyT thy env T U = let val Envir.Envir {maxidx, tenv, tyenv} = env; val (tyenv', maxidx') = Sign.typ_unify thy (T, U) (tyenv, maxidx); in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end; fun chaseT env (T as TVar v) = (case Type.lookup (Envir.type_env env) v of NONE => T | SOME T' => chaseT env T') | chaseT _ T = T; fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) _ vTs (t as Const (s, T)) = if T = dummyT then (case Sign.const_type thy s of NONE => error ("reconstruct_proof: No such constant: " ^ quote s) | SOME T => let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T) in (Const (s, T'), T', vTs, Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}) end) else (t, T, vTs, env) | infer_type _ env _ vTs (t as Free (s, T)) = if T = dummyT then (case Symtab.lookup vTs s of NONE => let val (T, env') = mk_tvar [] env in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end | SOME T => (Free (s, T), T, vTs, env)) else (t, T, vTs, env) | infer_type _ _ _ _ (Var _) = error "reconstruct_proof: internal error" | infer_type thy env Ts vTs (Abs (s, T, t)) = let val (T', env') = if T = dummyT then mk_tvar [] env else (T, env); val (t', U, vTs', env'') = infer_type thy env' (T' :: Ts) vTs t in (Abs (s, T', t'), T' --> U, vTs', env'') end | infer_type thy env Ts vTs (t $ u) = let val (t', T, vTs1, env1) = infer_type thy env Ts vTs t; val (u', U, vTs2, env2) = infer_type thy env1 Ts vTs1 u; in (case chaseT env2 T of Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U') | _ => let val (V, env3) = mk_tvar [] env2 in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end) end | infer_type _ env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env) handle General.Subscript => error ("infer_type: bad variable index " ^ string_of_int i)); fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^ Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u); fun decompose thy Ts (p as (t, u)) env = let fun rigrig (a, T) (b, U) uT ts us = if a <> b then cantunify thy p else apfst flat (fold_map (decompose thy Ts) (ts ~~ us) (uT env T U)) in case apply2 (strip_comb o Envir.head_norm env) p of ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us | ((Bound i, ts), (Bound j, us)) => rigrig (i, dummyT) (j, dummyT) (K o K) ts us | ((Abs (_, T, t), []), (Abs (_, U, u), [])) => decompose thy (T::Ts) (t, u) (unifyT thy env T U) | ((Abs (_, T, t), []), _) => decompose thy (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env | (_, (Abs (_, T, u), [])) => decompose thy (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env | _ => ([(mk_abs Ts t, mk_abs Ts u)], env) end; fun make_constraints_cprf thy env cprf = let fun add_cnstrt Ts prop prf cs env vTs (t, u) = let val t' = mk_abs Ts t; val u' = mk_abs Ts u in (prop, prf, cs, Pattern.unify (Context.Theory thy) (t', u') env, vTs) handle Pattern.Pattern => let val (cs', env') = decompose thy [] (t', u') env in (prop, prf, cs @ cs', env', vTs) end | Pattern.Unif => cantunify thy (Envir.norm_term env t', Envir.norm_term env u') end; fun mk_cnstrts_atom env vTs prop opTs prf = let val prop_types = type_variables_of prop; val (Ts, env') = (case opTs of NONE => fold_map (mk_tvar o Type.sort_of_atyp) prop_types env | SOME Ts => (Ts, env)); val prop' = subst_atomic_types (prop_types ~~ Ts) (forall_intr_variables_term prop) handle ListPair.UnequalLengths => error ("Wrong number of type arguments for " ^ quote (guess_name prf)) in (prop', change_types (SOME Ts) prf, [], env', vTs) end; fun head_norm (prop, prf, cnstrts, env, vTs) = (Envir.head_norm env prop, prf, cnstrts, env, vTs); fun mk_cnstrts env _ Hs vTs (PBound i) = ((nth Hs i, PBound i, [], env, vTs) handle General.Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i)) | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) = let val (T, env') = (case opT of NONE => mk_tvar [] env | SOME T => (T, env)); val (t, prf, cnstrts, env'', vTs') = mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf; in (Const ("Pure.all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf), cnstrts, env'', vTs') end | mk_cnstrts env Ts Hs vTs (AbsP (s, SOME t, cprf)) = let val (t', _, vTs', env') = infer_type thy env Ts vTs t; val (u, prf, cnstrts, env'', vTs'') = mk_cnstrts env' Ts (t'::Hs) vTs' cprf; in (Logic.mk_implies (t', u), AbsP (s, SOME t', prf), cnstrts, env'', vTs'') end | mk_cnstrts env Ts Hs vTs (AbsP (s, NONE, cprf)) = let val (t, env') = mk_var env Ts propT; val (u, prf, cnstrts, env'', vTs') = mk_cnstrts env' Ts (t::Hs) vTs cprf; in (Logic.mk_implies (t, u), AbsP (s, SOME t, prf), cnstrts, env'', vTs') end | mk_cnstrts env Ts Hs vTs (cprf1 %% cprf2) = let val (u, prf2, cnstrts, env', vTs') = mk_cnstrts env Ts Hs vTs cprf2 in (case head_norm (mk_cnstrts env' Ts Hs vTs' cprf1) of (Const ("Pure.imp", _) $ u' $ t', prf1, cnstrts', env'', vTs'') => add_cnstrt Ts t' (prf1 %% prf2) (cnstrts' @ cnstrts) env'' vTs'' (u, u') | (t, prf1, cnstrts', env'', vTs'') => let val (v, env''') = mk_var env'' Ts propT in add_cnstrt Ts v (prf1 %% prf2) (cnstrts' @ cnstrts) env''' vTs'' (t, Logic.mk_implies (u, v)) end) end | mk_cnstrts env Ts Hs vTs (cprf % SOME t) = let val (t', U, vTs1, env1) = infer_type thy env Ts vTs t in (case head_norm (mk_cnstrts env1 Ts Hs vTs1 cprf) of (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, prf, cnstrts, env2, vTs2) => let val env3 = unifyT thy env2 T U in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2) end | (u, prf, cnstrts, env2, vTs2) => let val (v, env3) = mk_var env2 Ts (U --> propT); in add_cnstrt Ts (v $ t') (prf % SOME t') cnstrts env3 vTs2 (u, Const ("Pure.all", (U --> propT) --> propT) $ v) end) end | mk_cnstrts env Ts Hs vTs (cprf % NONE) = (case head_norm (mk_cnstrts env Ts Hs vTs cprf) of (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, prf, cnstrts, env', vTs') => let val (t, env'') = mk_var env' Ts T in (betapply (f, t), prf % SOME t, cnstrts, env'', vTs') end | (u, prf, cnstrts, env', vTs') => let val (T, env1) = mk_tvar [] env'; val (v, env2) = mk_var env1 Ts (T --> propT); val (t, env3) = mk_var env2 Ts T in add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs' (u, Const ("Pure.all", (T --> propT) --> propT) $ v) end) | mk_cnstrts env _ _ vTs (prf as PThm ({prop, types = opTs, ...}, _)) = mk_cnstrts_atom env vTs prop opTs prf | mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) = mk_cnstrts_atom env vTs prop opTs prf | mk_cnstrts env _ _ vTs (prf as PClass (T, c)) = mk_cnstrts_atom env vTs (Logic.mk_of_class (T, c)) NONE prf | mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) = mk_cnstrts_atom env vTs prop opTs prf | mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs) | mk_cnstrts _ _ _ _ MinProof = raise MIN_PROOF () in mk_cnstrts env [] [] Symtab.empty cprf end; (* update list of free variables of constraints *) fun upd_constrs env cs = let val tenv = Envir.term_env env; val tyenv = Envir.type_env env; val dom = [] |> Vartab.fold (cons o #1) tenv |> Vartab.fold (cons o #1) tyenv; val vran = [] |> Vartab.fold (Term.add_var_names o #2 o #2) tenv |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) tyenv; fun check_cs [] = [] | check_cs ((u, p, vs) :: ps) = let val vs' = subtract (op =) dom vs in if vs = vs' then (u, p, vs) :: check_cs ps else (true, p, fold (insert op =) vs' vran) :: check_cs ps end; in check_cs cs end; (* solution of constraints *) fun solve _ [] bigenv = bigenv | solve thy cs bigenv = let fun search _ [] = error ("Unsolvable constraints:\n" ^ Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => Syntax.pretty_flexpair (Syntax.init_pretty_global thy) (apply2 (Envir.norm_term bigenv) p)) cs))) | search env ((u, p as (t1, t2), vs)::ps) = if u then let val tn1 = Envir.norm_term bigenv t1; val tn2 = Envir.norm_term bigenv t2 in if Pattern.pattern tn1 andalso Pattern.pattern tn2 then (Pattern.unify (Context.Theory thy) (tn1, tn2) env, ps) handle Pattern.Unif => cantunify thy (tn1, tn2) else let val (cs', env') = decompose thy [] (tn1, tn2) env in if cs' = [(tn1, tn2)] then apsnd (cons (false, (tn1, tn2), vs)) (search env ps) else search env' (map (fn q => (true, q, vs)) cs' @ ps) end end else apsnd (cons (false, p, vs)) (search env ps); val Envir.Envir {maxidx, ...} = bigenv; val (env, cs') = search (Envir.empty maxidx) cs; in solve thy (upd_constrs env cs') (Envir.merge (bigenv, env)) end; in (* reconstruction of proofs *) fun reconstruct_proof thy prop cprf = let val (cprf' % SOME prop', thawf) = freeze_thaw_prf (cprf % SOME prop); val (t, prf, cs, env, _) = make_constraints_cprf thy (Envir.empty (maxidx_proof cprf ~1)) cprf'; val cs' = map (apply2 (Envir.norm_term env)) ((t, prop') :: cs) |> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) []))); val env' = solve thy cs' env; in thawf (norm_proof env' prf) end handle MIN_PROOF () => MinProof; fun prop_of_atom prop Ts = subst_atomic_types (type_variables_of prop ~~ Ts) (forall_intr_variables_term prop); val head_norm = Envir.head_norm Envir.init; fun prop_of0 Hs (PBound i) = nth Hs i | prop_of0 Hs (Abst (s, SOME T, prf)) = Logic.all_const T $ (Abs (s, T, prop_of0 Hs prf)) | prop_of0 Hs (AbsP (_, SOME t, prf)) = Logic.mk_implies (t, prop_of0 (t :: Hs) prf) | prop_of0 Hs (prf % SOME t) = (case head_norm (prop_of0 Hs prf) of Const ("Pure.all", _) $ f => f $ t | _ => error "prop_of: all expected") | prop_of0 Hs (prf1 %% _) = (case head_norm (prop_of0 Hs prf1) of Const ("Pure.imp", _) $ _ $ Q => Q | _ => error "prop_of: ==> expected") | prop_of0 _ (Hyp t) = t | prop_of0 _ (PThm ({prop, types = SOME Ts, ...}, _)) = prop_of_atom prop Ts | prop_of0 _ (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts | prop_of0 _ (PClass (T, c)) = Logic.mk_of_class (T, c) | prop_of0 _ (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts | prop_of0 _ _ = error "prop_of: partial proof object"; val prop_of' = Envir.beta_eta_contract oo prop_of0; val prop_of = prop_of' []; (* expand and reconstruct subproofs *) fun expand_name_empty (header: thm_header) = if #name header = "" then SOME "" else NONE; fun expand_proof thy expand_name prf = let fun expand seen maxidx (AbsP (s, t, prf)) = let val (seen', maxidx', prf') = expand seen maxidx prf in (seen', maxidx', AbsP (s, t, prf')) end | expand seen maxidx (Abst (s, T, prf)) = let val (seen', maxidx', prf') = expand seen maxidx prf in (seen', maxidx', Abst (s, T, prf')) end | expand seen maxidx (prf1 %% prf2) = let val (seen', maxidx', prf1') = expand seen maxidx prf1; val (seen'', maxidx'', prf2') = expand seen' maxidx' prf2; in (seen'', maxidx'', prf1' %% prf2') end | expand seen maxidx (prf % t) = let val (seen', maxidx', prf') = expand seen maxidx prf in (seen', maxidx', prf' % t) end | expand seen maxidx (prf as PThm (header, thm_body)) = let val {serial, pos, theory_name, name, prop, types} = header in (case expand_name header of SOME name' => if name' = "" andalso is_some types then let val (seen', maxidx', prf') = (case Inttab.lookup seen serial of NONE => let val prf1 = thm_body_proof_open thm_body |> reconstruct_proof thy prop |> forall_intr_variables prop; val (seen1, maxidx1, prf2) = expand_init seen prf1 val seen2 = seen1 |> Inttab.update (serial, (maxidx1, prf2)); in (seen2, maxidx1, prf2) end | SOME (maxidx1, prf1) => (seen, maxidx1, prf1)); val prf'' = prf' |> incr_indexes (maxidx + 1) |> app_types (maxidx + 1) prop (the types); in (seen', maxidx' + maxidx + 1, prf'') end else if name' <> name then (seen, maxidx, PThm (thm_header serial pos theory_name name' prop types, thm_body)) else (seen, maxidx, prf) | NONE => (seen, maxidx, prf)) end | expand seen maxidx prf = (seen, maxidx, prf) and expand_init seen prf = expand seen (maxidx_proof prf ~1) prf; in #3 (expand_init Inttab.empty prf) end; end; (** promises **) fun fulfill_norm_proof thy ps body0 = let val _ = consolidate_bodies (map #2 ps @ [body0]); val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0; val oracles = unions_oracles (fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]); val thms = unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]); val proof = rew_proof thy proof0; in PBody {oracles = oracles, thms = thms, proof = proof} end; fun fulfill_proof_future thy promises (postproc: proof_body -> proof_body) body = let fun fulfill () = postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)); in if null promises then Future.map postproc body else if Future.is_finished body andalso length promises = 1 then Future.map (fn _ => fulfill ()) (snd (hd promises)) else (singleton o Future.forks) {name = "Proofterm.fulfill_proof_future", group = NONE, deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 1, interrupts = true} fulfill end; (** theorems **) (* standardization of variables for export: only frees and named bounds *) local val declare_names_term = Term.declare_term_frees; val declare_names_term' = fn SOME t => declare_names_term t | NONE => I; val declare_names_proof = fold_proof_terms declare_names_term; fun variant names bs x = #1 (Name.variant x (fold Name.declare bs names)); fun variant_term bs (Abs (x, T, t)) = let val x' = variant (declare_names_term t Name.context) bs x; val t' = variant_term (x' :: bs) t; in Abs (x', T, t') end | variant_term bs (t $ u) = variant_term bs t $ variant_term bs u | variant_term _ t = t; fun variant_proof bs (Abst (x, T, prf)) = let val x' = variant (declare_names_proof prf Name.context) bs x; val prf' = variant_proof (x' :: bs) prf; in Abst (x', T, prf') end | variant_proof bs (AbsP (x, t, prf)) = let val x' = variant (declare_names_term' t (declare_names_proof prf Name.context)) bs x; val t' = Option.map (variant_term bs) t; val prf' = variant_proof (x' :: bs) prf; in AbsP (x', t', prf') end | variant_proof bs (prf % t) = variant_proof bs prf % Option.map (variant_term bs) t | variant_proof bs (prf1 %% prf2) = variant_proof bs prf1 %% variant_proof bs prf2 | variant_proof bs (Hyp t) = Hyp (variant_term bs t) | variant_proof _ prf = prf; val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I); fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t; val used_frees_proof = fold_proof_terms_types used_frees_term used_frees_type; val unvarifyT = Term.map_atyps (fn TVar ((a, _), S) => TFree (a, S) | T => T); val unvarify = Term.map_aterms (fn Var ((x, _), T) => Free (x, T) | t => t) #> map_types unvarifyT; val unvarify_proof = map_proof_terms unvarify unvarifyT; fun hidden_types prop proof = let val visible = (fold_types o fold_atyps) (insert (op =)) prop []; val add_hiddenT = fold_atyps (fn T => not (member (op =) visible T) ? insert (op =) T); in rev (fold_proof_terms_types (fold_types add_hiddenT) add_hiddenT proof []) end; fun standard_hidden_types term proof = let val hidden = hidden_types term proof; val idx = Term.maxidx_term term (maxidx_proof proof ~1) + 1; fun smash T = if member (op =) hidden T then (case Type.sort_of_atyp T of [] => dummyT | S => TVar (("'", idx), S)) else T; val smashT = map_atyps smash; in map_proof_terms (map_types smashT) smashT proof end; fun standard_hidden_terms term proof = let fun add_unless excluded x = ((is_Free x orelse is_Var x) andalso not (member (op =) excluded x)) ? insert (op =) x; val visible = fold_aterms (add_unless []) term []; val hidden = fold_proof_terms (fold_aterms (add_unless visible)) proof []; val dummy_term = Term.map_aterms (fn x => if member (op =) hidden x then Term.dummy_pattern (Term.fastype_of x) else x); in proof |> not (null hidden) ? map_proof_terms dummy_term I end; in fun standard_vars used (term, opt_proof) = let val proofs = opt_proof |> Option.map (standard_hidden_types term #> standard_hidden_terms term) |> the_list; val proof_terms = rev (fold (fold_proof_terms_types cons (cons o Logic.mk_type)) proofs []); val used_frees = used |> used_frees_term term |> fold used_frees_proof proofs; val inst = Term_Subst.zero_var_indexes_inst used_frees (term :: proof_terms); val term' = term |> Term_Subst.instantiate inst |> unvarify |> variant_term []; val proofs' = proofs |> map (instantiate inst #> unvarify_proof #> variant_proof []); in (term', try hd proofs') end; fun standard_vars_term used t = #1 (standard_vars used (t, NONE)); val add_standard_vars_term = fold_aterms (fn Free (x, T) => (fn env => (case AList.lookup (op =) env x of NONE => (x, T) :: env | SOME T' => if T = T' then env else raise TYPE ("standard_vars_env: type conflict for variable " ^ quote x, [T, T'], []))) | _ => I); val add_standard_vars = fold_proof_terms add_standard_vars_term; end; (* PThm nodes *) fun prune_body body = if Options.default_bool "prune_proofs" then (Future.map o map_proof_of) (K MinProof) body else body; fun export_enabled () = Options.default_bool "export_proofs"; fun export_standard_enabled () = Options.default_bool "export_standard_proofs"; fun export_proof_boxes_required thy = Context.theory_name thy = Context.PureN orelse (export_enabled () andalso not (export_standard_enabled ())); fun export_proof_boxes bodies = let fun export_thm (i, thm_node) boxes = if Inttab.defined boxes i then boxes else boxes |> Inttab.update (i, thm_node_export thm_node) |> fold export_thm (thm_node_thms thm_node); fun export_body (PBody {thms, ...}) = fold export_thm thms; val exports = Inttab.build (fold export_body bodies) |> Inttab.dest; in List.app (Lazy.force o #2) exports end; local fun unconstrainT_proof algebra classrel_proof arity_proof (ucontext: Logic.unconstrain_context) = let fun hyp_map hyp = (case AList.lookup (op =) (#constraints ucontext) hyp of SOME t => Hyp t | NONE => raise Fail "unconstrainT_proof: missing constraint"); val typ = Term_Subst.map_atypsT_same (Type.strip_sorts o #atyp_map ucontext); fun ofclass (ty, c) = let val ty' = Term.map_atyps (#atyp_map ucontext) ty; in the_single (of_sort_proof algebra classrel_proof arity_proof hyp_map (ty', [c])) end; in Same.commit (map_proof_same (Term_Subst.map_types_same typ) typ ofclass) #> fold_rev (implies_intr_proof o snd) (#constraints ucontext) end; fun export_proof thy i prop prf0 = let val prf = prf0 |> reconstruct_proof thy prop |> apply_preproc thy; val (prop', SOME prf') = (prop, SOME prf) |> standard_vars Name.context; val args = [] |> add_standard_vars_term prop' |> add_standard_vars prf' |> rev; val typargs = [] |> Term.add_tfrees prop' |> fold_proof_terms Term.add_tfrees prf' |> rev; val consts = Sign.consts_of thy; val xml = (typargs, (args, (prop', no_thm_names prf'))) |> let open XML.Encode Term_XML.Encode; val encode_vars = list (pair string typ); val encode_term = encode_standard_term consts; val encode_proof = encode_standard_proof consts; in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end; in Export.export_params {theory = thy, binding = Path.binding0 (Path.make ["proofs", string_of_int i]), executable = false, compress = true, strict = false} xml end; fun prepare_thm_proof unconstrain thy classrel_proof arity_proof (name, pos) shyps hyps concl promises body = let val named = name <> ""; val prop = Logic.list_implies (hyps, concl); val args = prop_args prop; val (ucontext, prop1) = Logic.unconstrainT shyps prop; val PBody {oracles = oracles0, thms = thms0, proof = prf} = body; val body0 = Future.value (PBody {oracles = oracles0, thms = thms0, proof = if proofs_enabled () then fold_rev implies_intr_proof hyps prf else MinProof}); fun new_prf () = let val i = serial (); val unconstrainT = unconstrainT_proof (Sign.classes_of thy) classrel_proof arity_proof ucontext; val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy); in (i, fulfill_proof_future thy promises postproc body0) end; val (i, body') = (*somewhat non-deterministic proof boxes!*) if export_enabled () then new_prf () else (case strip_combt (fst (strip_combP prf)) of (PThm ({serial = ser, name = a, prop = prop', types = NONE, ...}, thm_body'), args') => if (a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then let val Thm_Body {body = body', ...} = thm_body'; val i = if a = "" andalso named then serial () else ser; in (i, body' |> ser <> i ? Future.map (map_proof_of (rew_proof thy))) end else new_prf () | _ => new_prf ()); val open_proof = not named ? rew_proof thy; val export = if export_enabled () then Lazy.lazy (fn () => join_proof body' |> open_proof |> export_proof thy i prop1 handle exn => if Exn.is_interrupt exn then raise Fail ("Interrupt: potential resource problems while exporting proof " ^ string_of_int i) else Exn.reraise exn) else no_export; val thm_body = prune_body body'; val theory_name = Context.theory_long_name thy; val thm = (i, make_thm_node theory_name name prop1 thm_body export); val header = thm_header i ([pos, Position.thread_data ()]) theory_name name prop1 NONE; val head = PThm (header, Thm_Body {open_proof = open_proof, body = thm_body}); val proof = if unconstrain then proof_combt' (head, (map o Option.map o Term.map_types) (#map_atyps ucontext) args) else proof_combP (proof_combt' (head, args), map PClass (#outer_constraints ucontext) @ map Hyp hyps); in (thm, proof) end; in fun thm_proof thy = prepare_thm_proof false thy; fun unconstrain_thm_proof thy classrel_proof arity_proof shyps concl promises body = prepare_thm_proof true thy classrel_proof arity_proof ("", Position.none) shyps [] concl promises body; end; (* PThm identity *) fun get_identity shyps hyps prop prf = let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in (case fst (strip_combt (fst (strip_combP prf))) of PThm ({serial, theory_name, name, prop = prop', ...}, _) => if prop = prop' then SOME {serial = serial, theory_name = theory_name, name = name} else NONE | _ => NONE) end; fun get_approximative_name shyps hyps prop prf = Option.map #name (get_identity shyps hyps prop prf) |> the_default ""; (* thm_id *) type thm_id = {serial: serial, theory_name: string}; fun make_thm_id (serial, theory_name) : thm_id = {serial = serial, theory_name = theory_name}; fun thm_header_id ({serial, theory_name, ...}: thm_header) = make_thm_id (serial, theory_name); fun thm_id (serial, thm_node) : thm_id = make_thm_id (serial, thm_node_theory_name thm_node); fun get_id shyps hyps prop prf : thm_id option = (case get_identity shyps hyps prop prf of NONE => NONE | SOME {name = "", ...} => NONE | SOME {serial, theory_name, ...} => SOME (make_thm_id (serial, theory_name))); fun this_id NONE _ = false | this_id (SOME (thm_id: thm_id)) (thm_id': thm_id) = #serial thm_id = #serial thm_id'; (* proof boxes: intermediate PThm nodes *) fun proof_boxes {included, excluded} proofs = let fun boxes_of (Abst (_, _, prf)) = boxes_of prf | boxes_of (AbsP (_, _, prf)) = boxes_of prf | boxes_of (prf % _) = boxes_of prf | boxes_of (prf1 %% prf2) = boxes_of prf1 #> boxes_of prf2 | boxes_of (PThm (header as {serial = i, ...}, thm_body)) = (fn boxes => let val thm_id = thm_header_id header in if Inttab.defined boxes i orelse (excluded thm_id andalso not (included thm_id)) then boxes else let val prf' = thm_body_proof_open thm_body; val boxes' = Inttab.update (i, (header, prf')) boxes; in boxes_of prf' boxes' end end) | boxes_of MinProof = raise MIN_PROOF () | boxes_of _ = I; in Inttab.fold_rev (cons o #2) (Inttab.build (fold boxes_of proofs)) [] end; end; structure Basic_Proofterm = struct datatype proof = datatype Proofterm.proof datatype proof_body = datatype Proofterm.proof_body val op %> = Proofterm.%> end; open Basic_Proofterm; diff --git a/src/Pure/thm.ML b/src/Pure/thm.ML --- a/src/Pure/thm.ML +++ b/src/Pure/thm.ML @@ -1,2373 +1,2373 @@ (* Title: Pure/thm.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Makarius The very core of Isabelle's Meta Logic: certified types and terms, derivations, theorems, inference rules (including lifting and resolution), oracles. *) infix 0 RS RSN; signature BASIC_THM = sig type ctyp type cterm exception CTERM of string * cterm list type thm type conv = cterm -> thm exception THM of string * int * thm list val RSN: thm * (int * thm) -> thm val RS: thm * thm -> thm end; signature THM = sig include BASIC_THM (*certified types*) val typ_of: ctyp -> typ val global_ctyp_of: theory -> typ -> ctyp val ctyp_of: Proof.context -> typ -> ctyp val dest_ctyp: ctyp -> ctyp list val dest_ctypN: int -> ctyp -> ctyp val dest_ctyp0: ctyp -> ctyp val dest_ctyp1: ctyp -> ctyp val make_ctyp: ctyp -> ctyp list -> ctyp (*certified terms*) val term_of: cterm -> term val typ_of_cterm: cterm -> typ val ctyp_of_cterm: cterm -> ctyp val maxidx_of_cterm: cterm -> int val global_cterm_of: theory -> term -> cterm val cterm_of: Proof.context -> term -> cterm val renamed_term: term -> cterm -> cterm val dest_comb: cterm -> cterm * cterm val dest_fun: cterm -> cterm val dest_arg: cterm -> cterm val dest_fun2: cterm -> cterm val dest_arg1: cterm -> cterm val dest_abs: string option -> cterm -> cterm * cterm val rename_tvar: indexname -> ctyp -> ctyp val var: indexname * ctyp -> cterm val apply: cterm -> cterm -> cterm val lambda_name: string * cterm -> cterm -> cterm val lambda: cterm -> cterm -> cterm val adjust_maxidx_cterm: int -> cterm -> cterm val incr_indexes_cterm: int -> cterm -> cterm val match: cterm * cterm -> ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list val first_order_match: cterm * cterm -> ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list (*theorems*) val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a val fold_atomic_ctyps: (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a val terms_of_tpairs: (term * term) list -> term list val full_prop_of: thm -> term val theory_id: thm -> Context.theory_id val theory_name: thm -> string val maxidx_of: thm -> int val maxidx_thm: thm -> int -> int val shyps_of: thm -> sort Ord_List.T val hyps_of: thm -> term list val prop_of: thm -> term val tpairs_of: thm -> (term * term) list val concl_of: thm -> term val prems_of: thm -> term list val nprems_of: thm -> int val no_prems: thm -> bool val major_prem_of: thm -> term val cprop_of: thm -> cterm val cprem_of: thm -> int -> cterm val cconcl_of: thm -> cterm val cprems_of: thm -> cterm list val chyps_of: thm -> cterm list exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option val theory_of_cterm: cterm -> theory val theory_of_thm: thm -> theory val trim_context_ctyp: ctyp -> ctyp val trim_context_cterm: cterm -> cterm val transfer_ctyp: theory -> ctyp -> ctyp val transfer_cterm: theory -> cterm -> cterm val transfer: theory -> thm -> thm val transfer': Proof.context -> thm -> thm val transfer'': Context.generic -> thm -> thm val join_transfer: theory -> thm -> thm val join_transfer_context: Proof.context * thm -> Proof.context * thm val renamed_prop: term -> thm -> thm val weaken: cterm -> thm -> thm val weaken_sorts: sort list -> cterm -> cterm val proof_bodies_of: thm list -> proof_body list val proof_body_of: thm -> proof_body val proof_of: thm -> proof val reconstruct_proof_of: thm -> Proofterm.proof val consolidate: thm list -> unit val expose_proofs: theory -> thm list -> unit val expose_proof: theory -> thm -> unit val future: thm future -> cterm -> thm val thm_deps: thm -> Proofterm.thm Ord_List.T val extra_shyps: thm -> sort list val strip_shyps: thm -> thm val derivation_closed: thm -> bool val derivation_name: thm -> string val derivation_id: thm -> Proofterm.thm_id option val raw_derivation_name: thm -> string val expand_name: thm -> Proofterm.thm_header -> string option val name_derivation: string * Position.T -> thm -> thm val close_derivation: Position.T -> thm -> thm val trim_context: thm -> thm val axiom: theory -> string -> thm val all_axioms_of: theory -> (string * thm) list val get_tags: thm -> Properties.T val map_tags: (Properties.T -> Properties.T) -> thm -> thm val norm_proof: thm -> thm val adjust_maxidx_thm: int -> thm -> thm (*type classes*) val the_classrel: theory -> class * class -> thm val the_arity: theory -> string * sort list * class -> thm val classrel_proof: theory -> class * class -> proof val arity_proof: theory -> string * sort list * class -> proof (*oracles*) val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory val oracle_space: theory -> Name_Space.T val pretty_oracle: Proof.context -> string -> Pretty.T val extern_oracles: bool -> Proof.context -> (Markup.T * xstring) list val check_oracle: Proof.context -> xstring * Position.T -> string (*inference rules*) val assume: cterm -> thm val implies_intr: cterm -> thm -> thm val implies_elim: thm -> thm -> thm val forall_intr: cterm -> thm -> thm val forall_elim: cterm -> thm -> thm val reflexive: cterm -> thm val symmetric: thm -> thm val transitive: thm -> thm -> thm val beta_conversion: bool -> conv val eta_conversion: conv val eta_long_conversion: conv val abstract_rule: string -> cterm -> thm -> thm val combination: thm -> thm -> thm val equal_intr: thm -> thm -> thm val equal_elim: thm -> thm -> thm val solve_constraints: thm -> thm val flexflex_rule: Proof.context option -> thm -> thm Seq.seq val generalize: Symtab.set * Symtab.set -> int -> thm -> thm val generalize_cterm: Symtab.set * Symtab.set -> int -> cterm -> cterm val generalize_ctyp: Symtab.set -> int -> ctyp -> ctyp val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> thm -> thm val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> cterm -> cterm val trivial: cterm -> thm val of_class: ctyp * class -> thm val unconstrainT: thm -> thm - val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm + val varifyT_global': Term_Subst.TFrees.set -> thm -> ((string * sort) * indexname) list * thm val varifyT_global: thm -> thm val legacy_freezeT: thm -> thm val plain_prop_of: thm -> term val dest_state: thm * int -> (term * term) list * term list * term * term val lift_rule: cterm -> thm -> thm val incr_indexes: int -> thm -> thm val assumption: Proof.context option -> int -> thm -> thm Seq.seq val eq_assumption: int -> thm -> thm val rotate_rule: int -> int -> thm -> thm val permute_prems: int -> int -> thm -> thm val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} -> bool * thm * int -> int -> thm -> thm Seq.seq val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq val thynames_of_arity: theory -> string * class -> string list val add_classrel: thm -> theory -> theory val add_arity: thm -> theory -> theory end; structure Thm: THM = struct (*** Certified terms and types ***) (** certified types **) datatype ctyp = Ctyp of {cert: Context.certificate, T: typ, maxidx: int, sorts: sort Ord_List.T}; fun typ_of (Ctyp {T, ...}) = T; fun global_ctyp_of thy raw_T = let val T = Sign.certify_typ thy raw_T; val maxidx = Term.maxidx_of_typ T; val sorts = Sorts.insert_typ T []; in Ctyp {cert = Context.Certificate thy, T = T, maxidx = maxidx, sorts = sorts} end; val ctyp_of = global_ctyp_of o Proof_Context.theory_of; fun dest_ctyp (Ctyp {cert, T = Type (_, Ts), maxidx, sorts}) = map (fn T => Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts}) Ts | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []); fun dest_ctypN n (Ctyp {cert, T, maxidx, sorts}) = let fun err () = raise TYPE ("dest_ctypN", [T], []) in (case T of Type (_, Ts) => Ctyp {cert = cert, T = nth Ts n handle General.Subscript => err (), maxidx = maxidx, sorts = sorts} | _ => err ()) end; val dest_ctyp0 = dest_ctypN 0; val dest_ctyp1 = dest_ctypN 1; fun join_certificate_ctyp (Ctyp {cert, ...}) cert0 = Context.join_certificate (cert0, cert); fun union_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sorts.union sorts0 sorts; fun maxidx_ctyp (Ctyp {maxidx, ...}) maxidx0 = Int.max (maxidx0, maxidx); fun make_ctyp (Ctyp {cert, T, maxidx = _, sorts = _}) cargs = let val As = map typ_of cargs; fun err () = raise TYPE ("make_ctyp", T :: As, []); in (case T of Type (a, args) => Ctyp { cert = fold join_certificate_ctyp cargs cert, maxidx = fold maxidx_ctyp cargs ~1, sorts = fold union_sorts_ctyp cargs [], T = if length args = length cargs then Type (a, As) else err ()} | _ => err ()) end; (** certified terms **) (*certified terms with checked typ, maxidx, and sorts*) datatype cterm = Cterm of {cert: Context.certificate, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T}; exception CTERM of string * cterm list; fun term_of (Cterm {t, ...}) = t; fun typ_of_cterm (Cterm {T, ...}) = T; fun ctyp_of_cterm (Cterm {cert, T, maxidx, sorts, ...}) = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts}; fun maxidx_of_cterm (Cterm {maxidx, ...}) = maxidx; fun global_cterm_of thy tm = let val (t, T, maxidx) = Sign.certify_term thy tm; val sorts = Sorts.insert_term t []; in Cterm {cert = Context.Certificate thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; val cterm_of = global_cterm_of o Proof_Context.theory_of; fun join_certificate0 (Cterm {cert = cert1, ...}, Cterm {cert = cert2, ...}) = Context.join_certificate (cert1, cert2); fun renamed_term t' (Cterm {cert, t, T, maxidx, sorts}) = if t aconv t' then Cterm {cert = cert, t = t', T = T, maxidx = maxidx, sorts = sorts} else raise TERM ("renamed_term: terms disagree", [t, t']); (* destructors *) fun dest_comb (Cterm {t = c $ a, T, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in (Cterm {t = c, T = A --> T, cert = cert, maxidx = maxidx, sorts = sorts}, Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts}) end | dest_comb ct = raise CTERM ("dest_comb", [ct]); fun dest_fun (Cterm {t = c $ _, T, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in Cterm {t = c, T = A --> T, cert = cert, maxidx = maxidx, sorts = sorts} end | dest_fun ct = raise CTERM ("dest_fun", [ct]); fun dest_arg (Cterm {t = c $ a, T = _, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end | dest_arg ct = raise CTERM ("dest_arg", [ct]); fun dest_fun2 (Cterm {t = c $ _ $ _, T, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0; val B = Term.argument_type_of c 1; in Cterm {t = c, T = A --> B --> T, cert = cert, maxidx = maxidx, sorts = sorts} end | dest_fun2 ct = raise CTERM ("dest_fun2", [ct]); fun dest_arg1 (Cterm {t = c $ a $ _, T = _, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]); fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), cert, maxidx, sorts}) = let val (y', t') = Term.dest_abs (the_default x a, T, t) in (Cterm {t = Free (y', T), T = T, cert = cert, maxidx = maxidx, sorts = sorts}, Cterm {t = t', T = U, cert = cert, maxidx = maxidx, sorts = sorts}) end | dest_abs _ ct = raise CTERM ("dest_abs", [ct]); (* constructors *) fun rename_tvar (a, i) (Ctyp {cert, T, maxidx, sorts}) = let val S = (case T of TFree (_, S) => S | TVar (_, S) => S | _ => raise TYPE ("rename_tvar: no variable", [T], [])); val _ = if i < 0 then raise TYPE ("rename_tvar: bad index", [TVar ((a, i), S)], []) else (); in Ctyp {cert = cert, T = TVar ((a, i), S), maxidx = Int.max (i, maxidx), sorts = sorts} end; fun var ((x, i), Ctyp {cert, T, maxidx, sorts}) = if i < 0 then raise TERM ("var: bad index", [Var ((x, i), T)]) else Cterm {cert = cert, t = Var ((x, i), T), T = T, maxidx = Int.max (i, maxidx), sorts = sorts}; fun apply (cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...}) (cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) = if T = dty then Cterm {cert = join_certificate0 (cf, cx), t = f $ x, T = rty, maxidx = Int.max (maxidx1, maxidx2), sorts = Sorts.union sorts1 sorts2} else raise CTERM ("apply: types don't agree", [cf, cx]) | apply cf cx = raise CTERM ("apply: first arg is not a function", [cf, cx]); fun lambda_name (x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...}) (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) = let val t = Term.lambda_name (x, t1) t2 in Cterm {cert = join_certificate0 (ct1, ct2), t = t, T = T1 --> T2, maxidx = Int.max (maxidx1, maxidx2), sorts = Sorts.union sorts1 sorts2} end; fun lambda t u = lambda_name ("", t) u; (* indexes *) fun adjust_maxidx_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) = if maxidx = i then ct else if maxidx < i then Cterm {maxidx = i, cert = cert, t = t, T = T, sorts = sorts} else Cterm {maxidx = Int.max (maxidx_of_term t, i), cert = cert, t = t, T = T, sorts = sorts}; fun incr_indexes_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) = if i < 0 then raise CTERM ("negative increment", [ct]) else if i = 0 then ct else Cterm {cert = cert, t = Logic.incr_indexes ([], [], i) t, T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts}; (*** Derivations and Theorems ***) (* sort constraints *) type constraint = {theory: theory, typ: typ, sort: sort}; local val constraint_ord : constraint ord = Context.theory_id_ord o apply2 (Context.theory_id o #theory) ||| Term_Ord.typ_ord o apply2 #typ ||| Term_Ord.sort_ord o apply2 #sort; val smash_atyps = map_atyps (fn TVar (_, S) => Term.aT S | TFree (_, S) => Term.aT S | T => T); in val union_constraints = Ord_List.union constraint_ord; fun insert_constraints thy (T, S) = let val ignored = S = [] orelse (case T of TFree (_, S') => S = S' | TVar (_, S') => S = S' | _ => false); in if ignored then I else Ord_List.insert constraint_ord {theory = thy, typ = smash_atyps T, sort = S} end; fun insert_constraints_env thy env = let val tyenv = Envir.type_env env; fun insert ([], _) = I | insert (S, T) = insert_constraints thy (Envir.norm_type tyenv T, S); in tyenv |> Vartab.fold (insert o #2) end; end; (* datatype thm *) datatype thm = Thm of deriv * (*derivation*) {cert: Context.certificate, (*background theory certificate*) tags: Properties.T, (*additional annotations/comments*) maxidx: int, (*maximum index of any Var or TVar*) constraints: constraint Ord_List.T, (*implicit proof obligations for sort constraints*) shyps: sort Ord_List.T, (*sort hypotheses*) hyps: term Ord_List.T, (*hypotheses*) tpairs: (term * term) list, (*flex-flex pairs*) prop: term} (*conclusion*) and deriv = Deriv of {promises: (serial * thm future) Ord_List.T, body: Proofterm.proof_body}; type conv = cterm -> thm; (*errors involving theorems*) exception THM of string * int * thm list; fun rep_thm (Thm (_, args)) = args; fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) = fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps; fun fold_atomic_ctyps f (th as Thm (_, {cert, maxidx, shyps, ...})) = let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps} in (fold_terms o fold_types o fold_atyps) (f o ctyp) th end; fun fold_atomic_cterms f (th as Thm (_, {cert, maxidx, shyps, ...})) = let fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps} in (fold_terms o fold_aterms) (fn t as Const (_, T) => f (cterm t T) | t as Free (_, T) => f (cterm t T) | t as Var (_, T) => f (cterm t T) | _ => I) th end; fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs []; fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u'; fun union_tpairs ts us = Library.merge eq_tpairs (ts, us); val maxidx_tpairs = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u); fun attach_tpairs tpairs prop = Logic.list_implies (map Logic.mk_equals tpairs, prop); fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop; val union_hyps = Ord_List.union Term_Ord.fast_term_ord; val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord; val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord; fun join_certificate1 (Cterm {cert = cert1, ...}, Thm (_, {cert = cert2, ...})) = Context.join_certificate (cert1, cert2); fun join_certificate2 (Thm (_, {cert = cert1, ...}), Thm (_, {cert = cert2, ...})) = Context.join_certificate (cert1, cert2); (* basic components *) val cert_of = #cert o rep_thm; val theory_id = Context.certificate_theory_id o cert_of; val theory_name = Context.theory_id_name o theory_id; val maxidx_of = #maxidx o rep_thm; fun maxidx_thm th i = Int.max (maxidx_of th, i); val shyps_of = #shyps o rep_thm; val hyps_of = #hyps o rep_thm; val prop_of = #prop o rep_thm; val tpairs_of = #tpairs o rep_thm; val concl_of = Logic.strip_imp_concl o prop_of; val prems_of = Logic.strip_imp_prems o prop_of; val nprems_of = Logic.count_prems o prop_of; fun no_prems th = nprems_of th = 0; fun major_prem_of th = (case prems_of th of prem :: _ => Logic.strip_assums_concl prem | [] => raise THM ("major_prem_of: rule with no premises", 0, [th])); fun cprop_of (Thm (_, {cert, maxidx, shyps, prop, ...})) = Cterm {cert = cert, maxidx = maxidx, T = propT, t = prop, sorts = shyps}; fun cprem_of (th as Thm (_, {cert, maxidx, shyps, prop, ...})) i = Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])}; fun cconcl_of (th as Thm (_, {cert, maxidx, shyps, ...})) = Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = concl_of th}; fun cprems_of (th as Thm (_, {cert, maxidx, shyps, ...})) = map (fn t => Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = t}) (prems_of th); fun chyps_of (Thm (_, {cert, shyps, hyps, ...})) = map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps; (* implicit theory context *) exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option; fun theory_of_cterm (ct as Cterm {cert, ...}) = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct], [], NONE); fun theory_of_thm th = Context.certificate_theory (cert_of th) handle ERROR msg => raise CONTEXT (msg, [], [], [th], NONE); fun trim_context_ctyp cT = (case cT of Ctyp {cert = Context.Certificate_Id _, ...} => cT | Ctyp {cert = Context.Certificate thy, T, maxidx, sorts} => Ctyp {cert = Context.Certificate_Id (Context.theory_id thy), T = T, maxidx = maxidx, sorts = sorts}); fun trim_context_cterm ct = (case ct of Cterm {cert = Context.Certificate_Id _, ...} => ct | Cterm {cert = Context.Certificate thy, t, T, maxidx, sorts} => Cterm {cert = Context.Certificate_Id (Context.theory_id thy), t = t, T = T, maxidx = maxidx, sorts = sorts}); fun trim_context_thm th = (case th of Thm (_, {constraints = _ :: _, ...}) => raise THM ("trim_context: pending sort constraints", 0, [th]) | Thm (_, {cert = Context.Certificate_Id _, ...}) => th | Thm (der, {cert = Context.Certificate thy, tags, maxidx, constraints = [], shyps, hyps, tpairs, prop}) => Thm (der, {cert = Context.Certificate_Id (Context.theory_id thy), tags = tags, maxidx = maxidx, constraints = [], shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop})); fun transfer_ctyp thy' cT = let val Ctyp {cert, T, maxidx, sorts} = cT; val _ = Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse raise CONTEXT ("Cannot transfer: not a super theory", [cT], [], [], SOME (Context.Theory thy')); val cert' = Context.join_certificate (Context.Certificate thy', cert); in if Context.eq_certificate (cert, cert') then cT else Ctyp {cert = cert', T = T, maxidx = maxidx, sorts = sorts} end; fun transfer_cterm thy' ct = let val Cterm {cert, t, T, maxidx, sorts} = ct; val _ = Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse raise CONTEXT ("Cannot transfer: not a super theory", [], [ct], [], SOME (Context.Theory thy')); val cert' = Context.join_certificate (Context.Certificate thy', cert); in if Context.eq_certificate (cert, cert') then ct else Cterm {cert = cert', t = t, T = T, maxidx = maxidx, sorts = sorts} end; fun transfer thy' th = let val Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) = th; val _ = Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse raise CONTEXT ("Cannot transfer: not a super theory", [], [], [th], SOME (Context.Theory thy')); val cert' = Context.join_certificate (Context.Certificate thy', cert); in if Context.eq_certificate (cert, cert') then th else Thm (der, {cert = cert', tags = tags, maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}) end; val transfer' = transfer o Proof_Context.theory_of; val transfer'' = transfer o Context.theory_of; fun join_transfer thy th = (Context.subthy_id (theory_id th, Context.theory_id thy) ? transfer thy) th; fun join_transfer_context (ctxt, th) = if Context.subthy_id (theory_id th, Context.theory_id (Proof_Context.theory_of ctxt)) then (ctxt, transfer' ctxt th) else (Context.raw_transfer (theory_of_thm th) ctxt, th); (* matching *) local fun gen_match match (ct1 as Cterm {t = t1, sorts = sorts1, ...}, ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) = let val cert = join_certificate0 (ct1, ct2); val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct1, ct2], [], NONE); val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty); val sorts = Sorts.union sorts1 sorts2; fun mk_cTinst ((a, i), (S, T)) = (((a, i), S), Ctyp {T = T, cert = cert, maxidx = maxidx2, sorts = sorts}); fun mk_ctinst ((x, i), (U, t)) = let val T = Envir.subst_type Tinsts U in (((x, i), T), Cterm {t = t, T = T, cert = cert, maxidx = maxidx2, sorts = sorts}) end; in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end; in val match = gen_match Pattern.match; val first_order_match = gen_match Pattern.first_order_match; end; (*implicit alpha-conversion*) fun renamed_prop prop' (Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = if prop aconv prop' then Thm (der, {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop'}) else raise TERM ("renamed_prop: props disagree", [prop, prop']); fun make_context ths NONE cert = (Context.Theory (Context.certificate_theory cert) handle ERROR msg => raise CONTEXT (msg, [], [], ths, NONE)) | make_context ths (SOME ctxt) cert = let val thy_id = Context.certificate_theory_id cert; val thy_id' = Context.theory_id (Proof_Context.theory_of ctxt); in if Context.subthy_id (thy_id, thy_id') then Context.Proof ctxt else raise CONTEXT ("Bad context", [], [], ths, SOME (Context.Proof ctxt)) end; fun make_context_certificate ths opt_ctxt cert = let val context = make_context ths opt_ctxt cert; val cert' = Context.Certificate (Context.theory_of context); in (context, cert') end; (*explicit weakening: maps |- B to A |- B*) fun weaken raw_ct th = let val ct as Cterm {t = A, T, sorts, maxidx = maxidxA, ...} = adjust_maxidx_cterm ~1 raw_ct; val Thm (der, {tags, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; in if T <> propT then raise THM ("weaken: assumptions must have type prop", 0, []) else if maxidxA <> ~1 then raise THM ("weaken: assumptions may not contain schematic variables", maxidxA, []) else Thm (der, {cert = join_certificate1 (ct, th), tags = tags, maxidx = maxidx, constraints = constraints, shyps = Sorts.union sorts shyps, hyps = insert_hyps A hyps, tpairs = tpairs, prop = prop}) end; fun weaken_sorts raw_sorts ct = let val Cterm {cert, t, T, maxidx, sorts} = ct; val thy = theory_of_cterm ct; val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts); val sorts' = Sorts.union sorts more_sorts; in Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = sorts'} end; (** derivations and promised proofs **) fun make_deriv promises oracles thms proof = Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}}; val empty_deriv = make_deriv [] [] [] MinProof; (* inference rules *) val promise_ord: (serial * thm future) ord = fn ((i, _), (j, _)) => int_ord (j, i); fun bad_proofs i = error ("Illegal level of detail for proof objects: " ^ string_of_int i); fun deriv_rule2 f (Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = prf1}}) (Deriv {promises = ps2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) = let val ps = Ord_List.union promise_ord ps1 ps2; val oracles = Proofterm.unions_oracles [oracles1, oracles2]; val thms = Proofterm.unions_thms [thms1, thms2]; val prf = (case ! Proofterm.proofs of 2 => f prf1 prf2 | 1 => MinProof | 0 => MinProof | i => bad_proofs i); in make_deriv ps oracles thms prf end; fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv; fun deriv_rule0 make_prf = if ! Proofterm.proofs <= 1 then empty_deriv else deriv_rule1 I (make_deriv [] [] [] (make_prf ())); fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) = make_deriv promises oracles thms (f proof); (* fulfilled proofs *) fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises; fun join_promises [] = () | join_promises promises = join_promises_of (Future.joins (map snd promises)) and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms)); fun fulfill_body (th as Thm (Deriv {promises, body}, _)) = let val fulfilled_promises = map #1 promises ~~ map fulfill_body (Future.joins (map #2 promises)) in Proofterm.fulfill_norm_proof (theory_of_thm th) fulfilled_promises body end; fun proof_bodies_of thms = (join_promises_of thms; map fulfill_body thms); val proof_body_of = singleton proof_bodies_of; val proof_of = Proofterm.proof_of o proof_body_of; fun reconstruct_proof_of thm = Proofterm.reconstruct_proof (theory_of_thm thm) (prop_of thm) (proof_of thm); val consolidate = ignore o proof_bodies_of; fun expose_proofs thy thms = if Proofterm.export_proof_boxes_required thy then Proofterm.export_proof_boxes (proof_bodies_of (map (transfer thy) thms)) else (); fun expose_proof thy = expose_proofs thy o single; (* future rule *) fun future_result i orig_cert orig_shyps orig_prop thm = let fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]); val Thm (Deriv {promises, ...}, {cert, constraints, shyps, hyps, tpairs, prop, ...}) = thm; val _ = Context.eq_certificate (cert, orig_cert) orelse err "bad theory"; val _ = prop aconv orig_prop orelse err "bad prop"; val _ = null constraints orelse err "bad sort constraints"; val _ = null tpairs orelse err "bad flex-flex constraints"; val _ = null hyps orelse err "bad hyps"; val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps"; val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies"; val _ = join_promises promises; in thm end; fun future future_thm ct = let val Cterm {cert = cert, t = prop, T, maxidx, sorts} = ct; val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]); val _ = if Proofterm.proofs_enabled () then raise CTERM ("future: proof terms enabled", [ct]) else (); val i = serial (); val future = future_thm |> Future.map (future_result i cert sorts prop); in Thm (make_deriv [(i, future)] [] [] MinProof, {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = prop}) end; (** Axioms **) fun axiom thy name = (case Name_Space.lookup (Theory.axiom_table thy) name of SOME prop => let val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop); val cert = Context.Certificate thy; val maxidx = maxidx_of_term prop; val shyps = Sorts.insert_term prop []; in Thm (der, {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = shyps, hyps = [], tpairs = [], prop = prop}) end | NONE => raise THEORY ("No axiom " ^ quote name, [thy])); fun all_axioms_of thy = map (fn (name, _) => (name, axiom thy name)) (Theory.all_axioms_of thy); (* tags *) val get_tags = #tags o rep_thm; fun map_tags f (Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = Thm (der, {cert = cert, tags = f tags, maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}); (* technical adjustments *) fun norm_proof (th as Thm (der, args)) = Thm (deriv_rule1 (Proofterm.rew_proof (theory_of_thm th)) der, args); fun adjust_maxidx_thm i (th as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = if maxidx = i then th else if maxidx < i then Thm (der, {maxidx = i, cert = cert, tags = tags, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}) else Thm (der, {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), cert = cert, tags = tags, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}); (*** Theory data ***) (* type classes *) structure Aritytab = Table( type key = string * sort list * class; val ord = fast_string_ord o apply2 #1 ||| fast_string_ord o apply2 #3 ||| list_ord Term_Ord.sort_ord o apply2 #2; ); datatype classes = Classes of {classrels: thm Symreltab.table, arities: (thm * string * serial) Aritytab.table}; fun make_classes (classrels, arities) = Classes {classrels = classrels, arities = arities}; val empty_classes = make_classes (Symreltab.empty, Aritytab.empty); (*see Theory.at_begin hook for transitive closure of classrels and arity completion*) fun merge_classes (Classes {classrels = classrels1, arities = arities1}, Classes {classrels = classrels2, arities = arities2}) = let val classrels' = Symreltab.merge (K true) (classrels1, classrels2); val arities' = Aritytab.merge (K true) (arities1, arities2); in make_classes (classrels', arities') end; (* data *) structure Data = Theory_Data ( type T = unit Name_Space.table * (*oracles: authentic derivation names*) classes; (*type classes within the logic*) val empty : T = (Name_Space.empty_table Markup.oracleN, empty_classes); val extend = I; fun merge ((oracles1, sorts1), (oracles2, sorts2)) : T = (Name_Space.merge_tables (oracles1, oracles2), merge_classes (sorts1, sorts2)); ); val get_oracles = #1 o Data.get; val map_oracles = Data.map o apfst; val get_classes = (fn (_, Classes args) => args) o Data.get; val get_classrels = #classrels o get_classes; val get_arities = #arities o get_classes; fun map_classes f = (Data.map o apsnd) (fn Classes {classrels, arities} => make_classes (f (classrels, arities))); fun map_classrels f = map_classes (fn (classrels, arities) => (f classrels, arities)); fun map_arities f = map_classes (fn (classrels, arities) => (classrels, f arities)); (* type classes *) fun the_classrel thy (c1, c2) = (case Symreltab.lookup (get_classrels thy) (c1, c2) of SOME thm => transfer thy thm | NONE => error ("Unproven class relation " ^ Syntax.string_of_classrel (Proof_Context.init_global thy) [c1, c2])); fun the_arity thy (a, Ss, c) = (case Aritytab.lookup (get_arities thy) (a, Ss, c) of SOME (thm, _, _) => transfer thy thm | NONE => error ("Unproven type arity " ^ Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c]))); val classrel_proof = proof_of oo the_classrel; val arity_proof = proof_of oo the_arity; (* solve sort constraints by pro-forma proof *) local fun union_digest (oracles1, thms1) (oracles2, thms2) = (Proofterm.unions_oracles [oracles1, oracles2], Proofterm.unions_thms [thms1, thms2]); fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) = (oracles, thms); fun constraint_digest ({theory = thy, typ, sort, ...}: constraint) = Sorts.of_sort_derivation (Sign.classes_of thy) {class_relation = fn _ => fn _ => fn (digest, c1) => fn c2 => if c1 = c2 then ([], []) else union_digest digest (thm_digest (the_classrel thy (c1, c2))), type_constructor = fn (a, _) => fn dom => fn c => let val arity_digest = thm_digest (the_arity thy (a, (map o map) #2 dom, c)) in (fold o fold) (union_digest o #1) dom arity_digest end, type_variable = fn T => map (pair ([], [])) (Type.sort_of_atyp T)} (typ, sort); in fun solve_constraints (thm as Thm (_, {constraints = [], ...})) = thm | solve_constraints (thm as Thm (der, args)) = let val {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop} = args; val thy = Context.certificate_theory cert; val bad_thys = constraints |> map_filter (fn {theory = thy', ...} => if Context.eq_thy (thy, thy') then NONE else SOME thy'); val () = if null bad_thys then () else raise THEORY ("solve_constraints: bad theories for theorem\n" ^ Syntax.string_of_term_global thy (prop_of thm), thy :: bad_thys); val Deriv {promises, body = PBody {oracles, thms, proof}} = der; val (oracles', thms') = (oracles, thms) |> fold (fold union_digest o constraint_digest) constraints; val body' = PBody {oracles = oracles', thms = thms', proof = proof}; in Thm (Deriv {promises = promises, body = body'}, {constraints = [], cert = cert, tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}) end; end; (*Dangling sort constraints of a thm*) fun extra_shyps (th as Thm (_, {shyps, ...})) = Sorts.subtract (fold_terms Sorts.insert_term th []) shyps; (*Remove extra sorts that are witnessed by type signature information*) fun strip_shyps thm = (case thm of Thm (_, {shyps = [], ...}) => thm | Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) => let val thy = theory_of_thm thm; val algebra = Sign.classes_of thy; val minimize = Sorts.minimize_sort algebra; val le = Sorts.sort_le algebra; fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1)); fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)]; val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm []; val extra = fold (Sorts.remove_sort o #2) present shyps; val witnessed = Sign.witness_sorts thy present extra; val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize); val extra' = non_witnessed |> map_filter (fn (S, _) => if non_witnessed |> exists (fn (S', _) => lt (S', S)) then NONE else SOME S) |> Sorts.make; val constrs' = non_witnessed |> maps (fn (S1, S2) => let val S0 = the (find_first (fn S => le (S, S1)) extra') in rel (S0, S1) @ rel (S1, S2) end); val constraints' = fold (insert_constraints thy) (witnessed @ constrs') constraints; val shyps' = fold (Sorts.insert_sort o #2) present extra'; in Thm (deriv_rule_unconditional (Proofterm.strip_shyps_proof algebra present witnessed extra') der, {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints', shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}) end) |> solve_constraints; (*** Closed theorems with official name ***) (*non-deterministic, depends on unknown promises*) fun derivation_closed (Thm (Deriv {body, ...}, _)) = Proofterm.compact_proof (Proofterm.proof_of body); (*non-deterministic, depends on unknown promises*) fun raw_derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = Proofterm.get_approximative_name shyps hyps prop (Proofterm.proof_of body); fun expand_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = let val self_id = (case Proofterm.get_identity shyps hyps prop (Proofterm.proof_of body) of NONE => K false | SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header); fun expand header = if self_id header orelse #name header = "" then SOME "" else NONE; in expand end; (*deterministic name of finished proof*) fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) = Proofterm.get_approximative_name shyps hyps prop (proof_of thm); (*identified PThm node*) fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) = Proofterm.get_id shyps hyps prop (proof_of thm); (*dependencies of PThm node*) fun thm_deps (thm as Thm (Deriv {promises = [], body = PBody {thms, ...}, ...}, _)) = (case (derivation_id thm, thms) of (SOME {serial = i, ...}, [(j, thm_node)]) => if i = j then Proofterm.thm_node_thms thm_node else thms | _ => thms) | thm_deps thm = raise THM ("thm_deps: bad promises", 0, [thm]); fun name_derivation name_pos = strip_shyps #> (fn thm as Thm (der, args) => let val thy = theory_of_thm thm; val Deriv {promises, body} = der; val {shyps, hyps, prop, tpairs, ...} = args; val _ = null tpairs orelse raise THM ("name_derivation: bad flex-flex constraints", 0, [thm]); val ps = map (apsnd (Future.map fulfill_body)) promises; val (pthm, proof) = Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy) name_pos shyps hyps prop ps body; val der' = make_deriv [] [] [pthm] proof; in Thm (der', args) end); fun close_derivation pos = solve_constraints #> (fn thm => if not (null (tpairs_of thm)) orelse derivation_closed thm then thm else name_derivation ("", pos) thm); val trim_context = solve_constraints #> trim_context_thm; (*** Oracles ***) fun add_oracle (b, oracle_fn) thy = let val (name, oracles') = Name_Space.define (Context.Theory thy) true (b, ()) (get_oracles thy); val thy' = map_oracles (K oracles') thy; fun invoke_oracle arg = let val Cterm {cert = cert2, t = prop, T, maxidx, sorts} = oracle_fn arg in if T <> propT then raise THM ("Oracle's result must have type prop: " ^ name, 0, []) else let val (oracle, prf) = (case ! Proofterm.proofs of 2 => (((name, Position.thread_data ()), SOME prop), Proofterm.oracle_proof name prop) | 1 => (((name, Position.thread_data ()), SOME prop), MinProof) | 0 => (((name, Position.none), NONE), MinProof) | i => bad_proofs i); in Thm (make_deriv [] [oracle] [] prf, {cert = Context.join_certificate (Context.Certificate thy', cert2), tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = prop}) end end; in ((name, invoke_oracle), thy') end; val oracle_space = Name_Space.space_of_table o get_oracles; fun pretty_oracle ctxt = Name_Space.pretty ctxt (oracle_space (Proof_Context.theory_of ctxt)); fun extern_oracles verbose ctxt = map #1 (Name_Space.markup_table verbose ctxt (get_oracles (Proof_Context.theory_of ctxt))); fun check_oracle ctxt = Name_Space.check (Context.Proof ctxt) (get_oracles (Proof_Context.theory_of ctxt)) #> #1; (*** Meta rules ***) (** primitive rules **) (*The assumption rule A |- A*) fun assume raw_ct = let val Cterm {cert, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in if T <> propT then raise THM ("assume: prop", 0, []) else if maxidx <> ~1 then raise THM ("assume: variables", maxidx, []) else Thm (deriv_rule0 (fn () => Proofterm.Hyp prop), {cert = cert, tags = [], maxidx = ~1, constraints = [], shyps = sorts, hyps = [prop], tpairs = [], prop = prop}) end; (*Implication introduction [A] : B ------- A \ B *) fun implies_intr (ct as Cterm {t = A, T, maxidx = maxidx1, sorts, ...}) (th as Thm (der, {maxidx = maxidx2, hyps, constraints, shyps, tpairs, prop, ...})) = if T <> propT then raise THM ("implies_intr: assumptions must have type prop", 0, [th]) else Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der, {cert = join_certificate1 (ct, th), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = constraints, shyps = Sorts.union sorts shyps, hyps = remove_hyps A hyps, tpairs = tpairs, prop = Logic.mk_implies (A, prop)}); (*Implication elimination A \ B A ------------ B *) fun implies_elim thAB thA = let val Thm (derA, {maxidx = maxidx1, hyps = hypsA, constraints = constraintsA, shyps = shypsA, tpairs = tpairsA, prop = propA, ...}) = thA and Thm (der, {maxidx = maxidx2, hyps, constraints, shyps, tpairs, prop, ...}) = thAB; fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]); in (case prop of Const ("Pure.imp", _) $ A $ B => if A aconv propA then Thm (deriv_rule2 (curry Proofterm.%%) der derA, {cert = join_certificate2 (thAB, thA), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraintsA constraints, shyps = Sorts.union shypsA shyps, hyps = union_hyps hypsA hyps, tpairs = union_tpairs tpairsA tpairs, prop = B}) else err () | _ => err ()) end; (*Forall introduction. The Free or Var x must not be free in the hypotheses. [x] : A ------ \x. A *) fun forall_intr (ct as Cterm {maxidx = maxidx1, t = x, T, sorts, ...}) (th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) = let fun result a = Thm (deriv_rule1 (Proofterm.forall_intr_proof (a, x) NONE) der, {cert = join_certificate1 (ct, th), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = constraints, shyps = Sorts.union sorts shyps, hyps = hyps, tpairs = tpairs, prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))}); fun check_occs a x ts = if exists (fn t => Logic.occs (x, t)) ts then raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th]) else (); in (case x of Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result a) | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result a) | _ => raise THM ("forall_intr: not a variable", 0, [th])) end; (*Forall elimination \x. A ------ A[t/x] *) fun forall_elim (ct as Cterm {t, T, maxidx = maxidx1, sorts, ...}) (th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) = (case prop of Const ("Pure.all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A => if T <> qary then raise THM ("forall_elim: type mismatch", 0, [th]) else Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der, {cert = join_certificate1 (ct, th), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = constraints, shyps = Sorts.union sorts shyps, hyps = hyps, tpairs = tpairs, prop = Term.betapply (A, t)}) | _ => raise THM ("forall_elim: not quantified", 0, [th])); (* Equality *) (*Reflexivity t \ t *) fun reflexive (Cterm {cert, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = Logic.mk_equals (t, t)}); (*Symmetry t \ u ------ u \ t *) fun symmetric (th as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) = (case prop of (eq as Const ("Pure.eq", _)) $ t $ u => Thm (deriv_rule1 Proofterm.symmetric_proof der, {cert = cert, tags = [], maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = eq $ u $ t}) | _ => raise THM ("symmetric", 0, [th])); (*Transitivity t1 \ u u \ t2 ------------------ t1 \ t2 *) fun transitive th1 th2 = let val Thm (der1, {maxidx = maxidx1, hyps = hyps1, constraints = constraints1, shyps = shyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, hyps = hyps2, constraints = constraints2, shyps = shyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]); in case (prop1, prop2) of ((eq as Const ("Pure.eq", Type (_, [U, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) => if not (u aconv u') then err "middle term" else Thm (deriv_rule2 (Proofterm.transitive_proof U u) der1 der2, {cert = join_certificate2 (th1, th2), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = eq $ t1 $ t2}) | _ => err "premises" end; (*Beta-conversion (\x. t) u \ t[u/x] fully beta-reduces the term if full = true *) fun beta_conversion full (Cterm {cert, t, T = _, maxidx, sorts}) = let val t' = if full then Envir.beta_norm t else (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt) | _ => raise THM ("beta_conversion: not a redex", 0, [])); in Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = Logic.mk_equals (t, t')}) end; fun eta_conversion (Cterm {cert, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = Logic.mk_equals (t, Envir.eta_contract t)}); fun eta_long_conversion (Cterm {cert, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = Logic.mk_equals (t, Envir.eta_long [] t)}); (*The abstraction rule. The Free or Var x must not be free in the hypotheses. The bound variable will be named "a" (since x will be something like x320) t \ u -------------- \x. t \ \x. u *) fun abstract_rule a (Cterm {t = x, T, sorts, ...}) (th as Thm (der, {cert, maxidx, hyps, constraints, shyps, tpairs, prop, ...})) = let val (t, u) = Logic.dest_equals prop handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]); val result = Thm (deriv_rule1 (Proofterm.abstract_rule_proof (a, x)) der, {cert = cert, tags = [], maxidx = maxidx, constraints = constraints, shyps = Sorts.union sorts shyps, hyps = hyps, tpairs = tpairs, prop = Logic.mk_equals (Abs (a, T, abstract_over (x, t)), Abs (a, T, abstract_over (x, u)))}); fun check_occs a x ts = if exists (fn t => Logic.occs (x, t)) ts then raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 0, [th]) else (); in (case x of Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result) | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result) | _ => raise THM ("abstract_rule: not a variable", 0, [th])) end; (*The combination rule f \ g t \ u ------------- f t \ g u *) fun combination th1 th2 = let val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; fun chktypes fT tT = (case fT of Type ("fun", [T1, _]) => if T1 <> tT then raise THM ("combination: types", 0, [th1, th2]) else () | _ => raise THM ("combination: not function type", 0, [th1, th2])); in (case (prop1, prop2) of (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g, Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) => (chktypes fT tT; Thm (deriv_rule2 (Proofterm.combination_proof f g t u) der1 der2, {cert = join_certificate2 (th1, th2), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = Logic.mk_equals (f $ t, g $ u)})) | _ => raise THM ("combination: premises", 0, [th1, th2])) end; (*Equality introduction A \ B B \ A ---------------- A \ B *) fun equal_intr th1 th2 = let val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]); in (case (prop1, prop2) of (Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') => if A aconv A' andalso B aconv B' then Thm (deriv_rule2 (Proofterm.equal_intr_proof A B) der1 der2, {cert = join_certificate2 (th1, th2), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = Logic.mk_equals (A, B)}) else err "not equal" | _ => err "premises") end; (*The equal propositions rule A \ B A --------- B *) fun equal_elim th1 th2 = let val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]); in (case prop1 of Const ("Pure.eq", _) $ A $ B => if prop2 aconv A then Thm (deriv_rule2 (Proofterm.equal_elim_proof A B) der1 der2, {cert = join_certificate2 (th1, th2), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = B}) else err "not equal" | _ => err "major premise") end; (**** Derived rules ****) (*Smash unifies the list of term pairs leaving no flex-flex pairs. Instantiates the theorem and deletes trivial tpairs. Resulting sequence may contain multiple elements if the tpairs are not all flex-flex.*) fun flexflex_rule opt_ctxt = solve_constraints #> (fn th => let val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; val (context, cert') = make_context_certificate [th] opt_ctxt cert; in Unify.smash_unifiers context tpairs (Envir.empty maxidx) |> Seq.map (fn env => if Envir.is_empty env then th else let val tpairs' = tpairs |> map (apply2 (Envir.norm_term env)) (*remove trivial tpairs, of the form t \ t*) |> filter_out (op aconv); val der' = deriv_rule1 (Proofterm.norm_proof' env) der; val constraints' = insert_constraints_env (Context.certificate_theory cert') env constraints; val prop' = Envir.norm_term env prop; val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'); val shyps = Envir.insert_sorts env shyps; in Thm (der', {cert = cert', tags = [], maxidx = maxidx, constraints = constraints', shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'}) end) end); (*Generalization of fixed variables A -------------------- A[?'a/'a, ?x/x, ...] *) fun generalize (tfrees, frees) idx th = if Symtab.is_empty tfrees andalso Symtab.is_empty frees then th else let val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); val bad_type = if Symtab.is_empty tfrees then K false else Term.exists_subtype (fn TFree (a, _) => Symtab.defined tfrees a | _ => false); fun bad_term (Free (x, T)) = bad_type T orelse Symtab.defined frees x | bad_term (Var (_, T)) = bad_type T | bad_term (Const (_, T)) = bad_type T | bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t | bad_term (t $ u) = bad_term t orelse bad_term u | bad_term (Bound _) = false; val _ = exists bad_term hyps andalso raise THM ("generalize: variable free in assumptions", 0, [th]); val generalize = Term_Subst.generalize (tfrees, frees) idx; val prop' = generalize prop; val tpairs' = map (apply2 generalize) tpairs; val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); in Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop) der, {cert = cert, tags = [], maxidx = maxidx', constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'}) end; fun generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) = if Symtab.is_empty tfrees andalso Symtab.is_empty frees then ct else if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct]) else Cterm {cert = cert, sorts = sorts, T = Term_Subst.generalizeT tfrees idx T, t = Term_Subst.generalize (tfrees, frees) idx t, maxidx = Int.max (maxidx, idx)}; fun generalize_ctyp tfrees idx (cT as Ctyp {cert, T, maxidx, sorts}) = if Symtab.is_empty tfrees then cT else if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", []) else Ctyp {cert = cert, sorts = sorts, T = Term_Subst.generalizeT tfrees idx T, maxidx = Int.max (maxidx, idx)}; (*Instantiation of schematic variables A -------------------- A[t1/v1, ..., tn/vn] *) local fun add_cert cert_of (_, c) cert = Context.join_certificate (cert, cert_of c); val add_instT_cert = add_cert (fn Ctyp {cert, ...} => cert); val add_inst_cert = add_cert (fn Cterm {cert, ...} => cert); fun add_sorts sorts_of (_, c) sorts = Sorts.union (sorts_of c) sorts; val add_instT_sorts = add_sorts (fn Ctyp {sorts, ...} => sorts); val add_inst_sorts = add_sorts (fn Cterm {sorts, ...} => sorts); fun add_instT thy (v as (_, S), Ctyp {T = U, maxidx, ...}) = if Sign.of_sort thy (U, S) then Term_Subst.TVars.add (v, (U, maxidx)) else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy S, [U], []); fun add_inst thy (v as (_, T), Cterm {t = u, T = U, maxidx, ...}) = if T = U then Term_Subst.Vars.add (v, (u, maxidx)) else let fun pretty_typing t ty = Pretty.block [Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy ty]; val msg = Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict", Pretty.fbrk, pretty_typing (Var v) T, Pretty.fbrk, pretty_typing u U]) in raise TYPE (msg, [T, U], [Var v, u]) end; fun prep_insts (instT, inst) (cert, sorts) = let val cert' = cert |> fold add_instT_cert instT |> fold add_inst_cert inst; val thy' = Context.certificate_theory cert' handle ERROR msg => raise CONTEXT (msg, map #2 instT, map #2 inst, [], NONE); val sorts' = sorts |> fold add_instT_sorts instT |> fold add_inst_sorts inst; val instT' = Term_Subst.TVars.build (fold (add_instT thy') instT); val inst' = Term_Subst.Vars.build (fold (add_inst thy') inst); in ((instT', inst'), (cert', sorts')) end; in (*Left-to-right replacements: ctpairs = [..., (vi, ti), ...]. Instantiates distinct Vars by terms of same type. Does NOT normalize the resulting theorem!*) fun instantiate ([], []) th = th | instantiate (instT, inst) th = let val Thm (der, {cert, hyps, constraints, shyps, tpairs, prop, ...}) = th; val ((instT', inst'), (cert', shyps')) = prep_insts (instT, inst) (cert, shyps) handle CONTEXT (msg, cTs, cts, ths, context) => raise CONTEXT (msg, cTs, cts, th :: ths, context); val subst = Term_Subst.instantiate_maxidx (instT', inst'); val (prop', maxidx1) = subst prop ~1; val (tpairs', maxidx') = fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1; val thy' = Context.certificate_theory cert'; val constraints' = Term_Subst.TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S)) instT' constraints; in Thm (deriv_rule1 (fn d => Proofterm.instantiate (Term_Subst.TVars.map (K #1) instT', Term_Subst.Vars.map (K #1) inst') d) der, {cert = cert', tags = [], maxidx = maxidx', constraints = constraints', shyps = shyps', hyps = hyps, tpairs = tpairs', prop = prop'}) |> solve_constraints end handle TYPE (msg, _, _) => raise THM (msg, 0, [th]); fun instantiate_cterm ([], []) ct = ct | instantiate_cterm (instT, inst) ct = let val Cterm {cert, t, T, sorts, ...} = ct; val ((instT', inst'), (cert', sorts')) = prep_insts (instT, inst) (cert, sorts); val subst = Term_Subst.instantiate_maxidx (instT', inst'); val substT = Term_Subst.instantiateT_maxidx instT'; val (t', maxidx1) = subst t ~1; val (T', maxidx') = substT T maxidx1; in Cterm {cert = cert', t = t', T = T', sorts = sorts', maxidx = maxidx'} end handle TYPE (msg, _, _) => raise CTERM (msg, [ct]); end; (*The trivial implication A \ A, justified by assume and forall rules. A can contain Vars, not so for assume!*) fun trivial (Cterm {cert, t = A, T, maxidx, sorts}) = if T <> propT then raise THM ("trivial: the term must have type prop", 0, []) else Thm (deriv_rule0 (fn () => Proofterm.trivial_proof), {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = Logic.mk_implies (A, A)}); (*Axiom-scheme reflecting signature contents T :: c ------------------- OFCLASS(T, c_class) *) fun of_class (cT, raw_c) = let val Ctyp {cert, T, ...} = cT; val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [cT], [], [], NONE); val c = Sign.certify_class thy raw_c; val Cterm {t = prop, maxidx, sorts, ...} = global_cterm_of thy (Logic.mk_of_class (T, c)); in if Sign.of_sort thy (T, [c]) then Thm (deriv_rule0 (fn () => Proofterm.PClass (T, c)), {cert = cert, tags = [], maxidx = maxidx, constraints = insert_constraints thy (T, [c]) [], shyps = sorts, hyps = [], tpairs = [], prop = prop}) else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, []) end |> solve_constraints; (*Internalize sort constraints of type variables*) val unconstrainT = strip_shyps #> (fn thm as Thm (der, args) => let val Deriv {promises, body} = der; val {cert, shyps, hyps, tpairs, prop, ...} = args; val thy = theory_of_thm thm; fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]); val _ = null hyps orelse err "bad hyps"; val _ = null tpairs orelse err "bad flex-flex constraints"; val tfrees = rev (Term.add_tfree_names prop []); val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); val ps = map (apsnd (Future.map fulfill_body)) promises; val (pthm, proof) = Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy) shyps prop ps body; val der' = make_deriv [] [] [pthm] proof; val prop' = Proofterm.thm_node_prop (#2 pthm); in Thm (der', {cert = cert, tags = [], maxidx = maxidx_of_term prop', constraints = [], shyps = [[]], (*potentially redundant*) hyps = [], tpairs = [], prop = prop'}) end); (*Replace all TFrees not fixed or in the hyps by new TVars*) fun varifyT_global' fixed (Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) = let - val tfrees = fold Term.add_tfrees hyps fixed; + val tfrees = fold Term_Subst.add_tfrees hyps fixed; val prop1 = attach_tpairs tpairs prop; val (al, prop2) = Type.varify_global tfrees prop1; val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); in (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees) der, {cert = cert, tags = [], maxidx = Int.max (0, maxidx), constraints = constraints, shyps = shyps, hyps = hyps, tpairs = rev (map Logic.dest_equals ts), prop = prop3})) end; -val varifyT_global = #2 o varifyT_global' []; +val varifyT_global = #2 o varifyT_global' Term_Subst.TFrees.empty; (*Replace all TVars by TFrees that are often new*) fun legacy_freezeT (Thm (der, {cert, constraints, shyps, hyps, tpairs, prop, ...})) = let val prop1 = attach_tpairs tpairs prop; val prop2 = Type.legacy_freeze prop1; val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); in Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1) der, {cert = cert, tags = [], maxidx = maxidx_of_term prop2, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = rev (map Logic.dest_equals ts), prop = prop3}) end; fun plain_prop_of raw_thm = let val thm = strip_shyps raw_thm; fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]); in if not (null (hyps_of thm)) then err "theorem may not contain hypotheses" else if not (null (extra_shyps thm)) then err "theorem may not contain sort hypotheses" else if not (null (tpairs_of thm)) then err "theorem may not contain flex-flex pairs" else prop_of thm end; (*** Inference rules for tactics ***) (*Destruct proof state into constraints, other goals, goal(i), rest *) fun dest_state (state as Thm (_, {prop,tpairs,...}), i) = (case Logic.strip_prems(i, [], prop) of (B::rBs, C) => (tpairs, rev rBs, B, C) | _ => raise THM("dest_state", i, [state])) handle TERM _ => raise THM("dest_state", i, [state]); (*Prepare orule for resolution by lifting it over the parameters and assumptions of goal.*) fun lift_rule goal orule = let val Cterm {t = gprop, T, maxidx = gmax, sorts, ...} = goal; val inc = gmax + 1; val lift_abs = Logic.lift_abs inc gprop; val lift_all = Logic.lift_all inc gprop; val Thm (der, {maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = orule; val (As, B) = Logic.strip_horn prop; in if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, []) else Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop) der, {cert = join_certificate1 (goal, orule), tags = [], maxidx = maxidx + inc, constraints = constraints, shyps = Sorts.union shyps sorts, (*sic!*) hyps = hyps, tpairs = map (apply2 lift_abs) tpairs, prop = Logic.list_implies (map lift_all As, lift_all B)}) end; fun incr_indexes i (thm as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) = if i < 0 then raise THM ("negative increment", 0, [thm]) else if i = 0 then thm else Thm (deriv_rule1 (Proofterm.incr_indexes i) der, {cert = cert, tags = [], maxidx = maxidx + i, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = map (apply2 (Logic.incr_indexes ([], [], i))) tpairs, prop = Logic.incr_indexes ([], [], i) prop}); (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) fun assumption opt_ctxt i state = let val Thm (der, {cert, maxidx, constraints, shyps, hyps, ...}) = state; val (context, cert') = make_context_certificate [state] opt_ctxt cert; val (tpairs, Bs, Bi, C) = dest_state (state, i); fun newth n (env, tpairs) = let val normt = Envir.norm_term env; fun assumption_proof prf = Proofterm.assumption_proof (map normt Bs) (normt Bi) n prf; in Thm (deriv_rule1 (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof' env) der, {tags = [], maxidx = Envir.maxidx_of env, constraints = insert_constraints_env (Context.certificate_theory cert') env constraints, shyps = Envir.insert_sorts env shyps, hyps = hyps, tpairs = if Envir.is_empty env then tpairs else map (apply2 normt) tpairs, prop = if Envir.is_empty env then Logic.list_implies (Bs, C) (*avoid wasted normalizations*) else normt (Logic.list_implies (Bs, C)) (*normalize the new rule fully*), cert = cert'}) end; val (close, asms, concl) = Logic.assum_problems (~1, Bi); val concl' = close concl; fun addprfs [] _ = Seq.empty | addprfs (asm :: rest) n = Seq.make (fn () => Seq.pull (Seq.mapp (newth n) (if Term.could_unify (asm, concl) then (Unify.unifiers (context, Envir.empty maxidx, (close asm, concl') :: tpairs)) else Seq.empty) (addprfs rest (n + 1)))) in addprfs asms 1 end; (*Solve subgoal Bi of proof state B1...Bn/C by assumption. Checks if Bi's conclusion is alpha/eta-convertible to one of its assumptions*) fun eq_assumption i state = let val Thm (der, {cert, maxidx, constraints, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); val (_, asms, concl) = Logic.assum_problems (~1, Bi); in (case find_index (fn asm => Envir.aeconv (asm, concl)) asms of ~1 => raise THM ("eq_assumption", 0, [state]) | n => Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der, {cert = cert, tags = [], maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = Logic.list_implies (Bs, C)})) end; (*For rotate_tac: fast rotation of assumptions of subgoal i*) fun rotate_rule k i state = let val Thm (der, {cert, maxidx, constraints, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); val params = Term.strip_all_vars Bi; val rest = Term.strip_all_body Bi; val asms = Logic.strip_imp_prems rest val concl = Logic.strip_imp_concl rest; val n = length asms; val m = if k < 0 then n + k else k; val Bi' = if 0 = m orelse m = n then Bi else if 0 < m andalso m < n then let val (ps, qs) = chop m asms in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end else raise THM ("rotate_rule", k, [state]); in Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi' params asms m) der, {cert = cert, tags = [], maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = Logic.list_implies (Bs @ [Bi'], C)}) end; (*Rotates a rule's premises to the left by k, leaving the first j premises unchanged. Does nothing if k=0 or if k equals n-j, where n is the number of premises. Useful with eresolve_tac and underlies defer_tac*) fun permute_prems j k rl = let val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = rl; val prems = Logic.strip_imp_prems prop and concl = Logic.strip_imp_concl prop; val moved_prems = List.drop (prems, j) and fixed_prems = List.take (prems, j) handle General.Subscript => raise THM ("permute_prems: j", j, [rl]); val n_j = length moved_prems; val m = if k < 0 then n_j + k else k; val (prems', prop') = if 0 = m orelse m = n_j then (prems, prop) else if 0 < m andalso m < n_j then let val (ps, qs) = chop m moved_prems; val prems' = fixed_prems @ qs @ ps; in (prems', Logic.list_implies (prems', concl)) end else raise THM ("permute_prems: k", k, [rl]); in Thm (deriv_rule1 (Proofterm.permute_prems_proof prems' j m) der, {cert = cert, tags = [], maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop'}) end; (* strip_apply f B A strips off all assumptions/parameters from A introduced by lifting over B, and applies f to remaining part of A*) fun strip_apply f = let fun strip (Const ("Pure.imp", _) $ _ $ B1) (Const ("Pure.imp", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2) | strip ((c as Const ("Pure.all", _)) $ Abs (_, _, t1)) ( Const ("Pure.all", _) $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2) | strip _ A = f A in strip end; fun strip_lifted (Const ("Pure.imp", _) $ _ $ B1) (Const ("Pure.imp", _) $ _ $ B2) = strip_lifted B1 B2 | strip_lifted (Const ("Pure.all", _) $ Abs (_, _, t1)) (Const ("Pure.all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2 | strip_lifted _ A = A; (*Use the alist to rename all bound variables and some unknowns in a term dpairs = current disagreement pairs; tpairs = permanent ones (flexflex); Preserves unknowns in tpairs and on lhs of dpairs. *) fun rename_bvs [] _ _ _ _ = K I | rename_bvs al dpairs tpairs B As = let val add_var = fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I); val vids = [] |> fold (add_var o fst) dpairs |> fold (add_var o fst) tpairs |> fold (add_var o snd) tpairs; val vids' = fold (add_var o strip_lifted B) As []; (*unknowns appearing elsewhere be preserved!*) val al' = distinct ((op =) o apply2 fst) (filter_out (fn (x, y) => not (member (op =) vids' x) orelse member (op =) vids x orelse member (op =) vids y) al); val unchanged = filter_out (AList.defined (op =) al') vids'; fun del_clashing clash xs _ [] qs = if clash then del_clashing false xs xs qs [] else qs | del_clashing clash xs ys ((p as (x, y)) :: ps) qs = if member (op =) ys y then del_clashing true (x :: xs) (x :: ys) ps qs else del_clashing clash xs (y :: ys) ps (p :: qs); val al'' = del_clashing false unchanged unchanged al' []; fun rename (t as Var ((x, i), T)) = (case AList.lookup (op =) al'' x of SOME y => Var ((y, i), T) | NONE => t) | rename (Abs (x, T, t)) = Abs (the_default x (AList.lookup (op =) al x), T, rename t) | rename (f $ t) = rename f $ rename t | rename t = t; fun strip_ren f Ai = f rename B Ai in strip_ren end; (*Function to rename bounds/unknowns in the argument, lifted over B*) fun rename_bvars dpairs = rename_bvs (fold_rev Term.match_bvars dpairs []) dpairs; (*** RESOLUTION ***) (** Lifting optimizations **) (*strip off pairs of assumptions/parameters in parallel -- they are identical because of lifting*) fun strip_assums2 (Const("Pure.imp", _) $ _ $ B1, Const("Pure.imp", _) $ _ $ B2) = strip_assums2 (B1,B2) | strip_assums2 (Const("Pure.all",_)$Abs(a,T,t1), Const("Pure.all",_)$Abs(_,_,t2)) = let val (B1,B2) = strip_assums2 (t1,t2) in (Abs(a,T,B1), Abs(a,T,B2)) end | strip_assums2 BB = BB; (*Faster normalization: skip assumptions that were lifted over*) fun norm_term_skip env 0 t = Envir.norm_term env t | norm_term_skip env n (Const ("Pure.all", _) $ Abs (a, T, t)) = let val T' = Envir.norm_type (Envir.type_env env) T (*Must instantiate types of parameters because they are flattened; this could be a NEW parameter*) in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end | norm_term_skip env n (Const ("Pure.imp", _) $ A $ B) = Logic.mk_implies (A, norm_term_skip env (n - 1) B) | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??"; (*unify types of schematic variables (non-lifted case)*) fun unify_var_types context (th1, th2) env = let fun unify_vars (T :: Us) = fold (fn U => Pattern.unify_types context (T, U)) Us | unify_vars _ = I; val add_vars = full_prop_of #> fold_aterms (fn Var v => Vartab.insert_list (op =) v | _ => I); val vars = Vartab.build (add_vars th1 #> add_vars th2); in SOME (Vartab.fold (unify_vars o #2) vars env) end handle Pattern.Unif => NONE; (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) Unifies B with Bi, replacing subgoal i (1 <= i <= n) If match then forbid instantiations in proof state If lifted then shorten the dpair using strip_assums2. If eres_flg then simultaneously proves A1 by assumption. nsubgoal is the number of new subgoals (written m above). Curried so that resolution calls dest_state only once. *) local exception COMPOSE in fun bicompose_aux opt_ctxt {flatten, match, incremented} (state, (stpairs, Bs, Bi, C), lifted) (eres_flg, orule, nsubgoal) = let val Thm (sder, {maxidx=smax, constraints = constraints2, shyps = shyps2, hyps = hyps2, ...}) = state and Thm (rder, {maxidx=rmax, constraints = constraints1, shyps = shyps1, hyps = hyps1, tpairs=rtpairs, prop=rprop,...}) = orule (*How many hyps to skip over during normalization*) and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0) val (context, cert) = make_context_certificate [state, orule] opt_ctxt (join_certificate2 (state, orule)); (*Add new theorem with prop = "\Bs; As\ \ C" to thq*) fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) = let val normt = Envir.norm_term env; (*perform minimal copying here by examining env*) val (ntpairs, normp) = if Envir.is_empty env then (tpairs, (Bs @ As, C)) else let val ntps = map (apply2 normt) tpairs in if Envir.above env smax then (*no assignments in state; normalize the rule only*) if lifted then (ntps, (Bs @ map (norm_term_skip env nlift) As, C)) else (ntps, (Bs @ map normt As, C)) else if match then raise COMPOSE else (*normalize the new rule fully*) (ntps, (map normt (Bs @ As), normt C)) end val constraints' = union_constraints constraints1 constraints2 |> insert_constraints_env (Context.certificate_theory cert) env; fun bicompose_proof prf1 prf2 = Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1) prf1 prf2 val th = Thm (deriv_rule2 (if Envir.is_empty env then bicompose_proof else if Envir.above env smax then bicompose_proof o Proofterm.norm_proof' env else Proofterm.norm_proof' env oo bicompose_proof) rder' sder, {tags = [], maxidx = Envir.maxidx_of env, constraints = constraints', shyps = Envir.insert_sorts env (Sorts.union shyps1 shyps2), hyps = union_hyps hyps1 hyps2, tpairs = ntpairs, prop = Logic.list_implies normp, cert = cert}) in Seq.cons th thq end handle COMPOSE => thq; val (rAs,B) = Logic.strip_prems(nsubgoal, [], rprop) handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]); (*Modify assumptions, deleting n-th if n>0 for e-resolution*) fun newAs(As0, n, dpairs, tpairs) = let val (As1, rder') = if not lifted then (As0, rder) else let val rename = rename_bvars dpairs tpairs B As0 in (map (rename strip_apply) As0, deriv_rule1 (Proofterm.map_proof_terms (rename K) I) rder) end; in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n) handle TERM _ => raise THM("bicompose: 1st premise", 0, [orule]) end; val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); val dpairs = BBi :: (rtpairs@stpairs); (*elim-resolution: try each assumption in turn*) fun eres _ [] = raise THM ("bicompose: no premises", 0, [orule, state]) | eres env (A1 :: As) = let val A = SOME A1; val (close, asms, concl) = Logic.assum_problems (nlift + 1, A1); val concl' = close concl; fun tryasms [] _ = Seq.empty | tryasms (asm :: rest) n = if Term.could_unify (asm, concl) then let val asm' = close asm in (case Seq.pull (Unify.unifiers (context, env, (asm', concl') :: dpairs)) of NONE => tryasms rest (n + 1) | cell as SOME ((_, tpairs), _) => Seq.it_right (addth A (newAs (As, n, [BBi, (concl', asm')], tpairs))) (Seq.make (fn () => cell), Seq.make (fn () => Seq.pull (tryasms rest (n + 1))))) end else tryasms rest (n + 1); in tryasms asms 1 end; (*ordinary resolution*) fun res env = (case Seq.pull (Unify.unifiers (context, env, dpairs)) of NONE => Seq.empty | cell as SOME ((_, tpairs), _) => Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs))) (Seq.make (fn () => cell), Seq.empty)); val env0 = Envir.empty (Int.max (rmax, smax)); in (case if incremented then SOME env0 else unify_var_types context (state, orule) env0 of NONE => Seq.empty | SOME env => if eres_flg then eres env (rev rAs) else res env) end; end; fun bicompose opt_ctxt flags arg i state = bicompose_aux opt_ctxt flags (state, dest_state (state,i), false) arg; (*Quick test whether rule is resolvable with the subgoal with hyps Hs and conclusion B. If eres_flg then checks 1st premise of rule also*) fun could_bires (Hs, B, eres_flg, rule) = let fun could_reshyp (A1::_) = exists (fn H => Term.could_unify (A1, H)) Hs | could_reshyp [] = false; (*no premise -- illegal*) in Term.could_unify(concl_of rule, B) andalso (not eres_flg orelse could_reshyp (prems_of rule)) end; (*Bi-resolution of a state with a list of (flag,rule) pairs. Puts the rule above: rule/state. Renames vars in the rules. *) fun biresolution opt_ctxt match brules i state = let val (stpairs, Bs, Bi, C) = dest_state(state,i); val lift = lift_rule (cprem_of state i); val B = Logic.strip_assums_concl Bi; val Hs = Logic.strip_assums_hyp Bi; val compose = bicompose_aux opt_ctxt {flatten = true, match = match, incremented = true} (state, (stpairs, Bs, Bi, C), true); fun res [] = Seq.empty | res ((eres_flg, rule)::brules) = if Config.get_generic (make_context [state] opt_ctxt (cert_of state)) Pattern.unify_trace_failure orelse could_bires (Hs, B, eres_flg, rule) then Seq.make (*delay processing remainder till needed*) (fn()=> SOME(compose (eres_flg, lift rule, nprems_of rule), res brules)) else res brules in Seq.flat (res brules) end; (*Resolution: exactly one resolvent must be produced*) fun tha RSN (i, thb) = (case Seq.chop 2 (biresolution NONE false [(false, tha)] i thb) of ([th], _) => solve_constraints th | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb]) | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb])); (*Resolution: P \ Q, Q \ R gives P \ R*) fun tha RS thb = tha RSN (1,thb); (**** Type classes ****) fun standard_tvars thm = let val thy = theory_of_thm thm; val tvars = rev (Term.add_tvars (prop_of thm) []); val names = Name.invent Name.context Name.aT (length tvars); val tinst = map2 (fn (ai, S) => fn b => ((ai, S), global_ctyp_of thy (TVar ((b, 0), S)))) tvars names; in instantiate (tinst, []) thm end (* class relations *) val is_classrel = Symreltab.defined o get_classrels; fun complete_classrels thy = let fun complete (c, (_, (all_preds, all_succs))) (finished1, thy1) = let fun compl c1 c2 (finished2, thy2) = if is_classrel thy2 (c1, c2) then (finished2, thy2) else (false, thy2 |> (map_classrels o Symreltab.update) ((c1, c2), (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2)) |> standard_tvars |> close_derivation \<^here> |> tap (expose_proof thy2) |> trim_context)); val proven = is_classrel thy1; val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds []; val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs []; in fold_product compl preds succs (finished1, thy1) end; in (case Graph.fold complete (Sorts.classes_of (Sign.classes_of thy)) (true, thy) of (true, _) => NONE | (_, thy') => SOME thy') end; (* type arities *) fun thynames_of_arity thy (a, c) = (get_arities thy, []) |-> Aritytab.fold (fn ((a', _, c'), (_, name, ser)) => (a = a' andalso c = c') ? cons (name, ser)) |> sort (int_ord o apply2 #2) |> map #1; fun insert_arity_completions thy ((t, Ss, c), (th, thy_name, ser)) (finished, arities) = let val completions = Sign.super_classes thy c |> map_filter (fn c1 => if Aritytab.defined arities (t, Ss, c1) then NONE else let val th1 = (th RS the_classrel thy (c, c1)) |> standard_tvars |> close_derivation \<^here> |> tap (expose_proof thy) |> trim_context; in SOME ((t, Ss, c1), (th1, thy_name, ser)) end); val finished' = finished andalso null completions; val arities' = fold Aritytab.update completions arities; in (finished', arities') end; fun complete_arities thy = let val arities = get_arities thy; val (finished, arities') = Aritytab.fold (insert_arity_completions thy) arities (true, get_arities thy); in if finished then NONE else SOME (map_arities (K arities') thy) end; val _ = Theory.setup (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities); (* primitive rules *) fun add_classrel raw_th thy = let val th = strip_shyps (transfer thy raw_th); val th' = th |> unconstrainT |> tap (expose_proof thy) |> trim_context; val prop = plain_prop_of th; val (c1, c2) = Logic.dest_classrel prop; in thy |> Sign.primitive_classrel (c1, c2) |> map_classrels (Symreltab.update ((c1, c2), th')) |> perhaps complete_classrels |> perhaps complete_arities end; fun add_arity raw_th thy = let val th = strip_shyps (transfer thy raw_th); val th' = th |> unconstrainT |> tap (expose_proof thy) |> trim_context; val prop = plain_prop_of th; val (t, Ss, c) = Logic.dest_arity prop; val ar = ((t, Ss, c), (th', Context.theory_name thy, serial ())); in thy |> Sign.primitive_arity (t, Ss, [c]) |> map_arities (Aritytab.update ar #> curry (insert_arity_completions thy ar) true #> #2) end; end; structure Basic_Thm: BASIC_THM = Thm; open Basic_Thm; diff --git a/src/Pure/type.ML b/src/Pure/type.ML --- a/src/Pure/type.ML +++ b/src/Pure/type.ML @@ -1,713 +1,714 @@ (* Title: Pure/type.ML Author: Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel Type signatures and certified types, special treatment of type vars, matching and unification of types, extend and merge type signatures. *) signature TYPE = sig (*constraints*) val mark_polymorphic: typ -> typ val constraint: typ -> term -> term val constraint_type: Proof.context -> typ -> typ val strip_constraints: term -> term val appl_error: Proof.context -> term -> typ -> term -> typ -> string (*type signatures and certified types*) datatype decl = LogicalType of int | Abbreviation of string list * typ * bool | Nonterminal type tsig val eq_tsig: tsig * tsig -> bool val rep_tsig: tsig -> {classes: Name_Space.T * Sorts.algebra, default: sort, types: decl Name_Space.table, log_types: string list} val change_base: bool -> tsig -> tsig val change_ignore: tsig -> tsig val empty_tsig: tsig val class_space: tsig -> Name_Space.T val defaultS: tsig -> sort val logical_types: tsig -> string list val eq_sort: tsig -> sort * sort -> bool val subsort: tsig -> sort * sort -> bool val of_sort: tsig -> typ * sort -> bool val inter_sort: tsig -> sort * sort -> sort val cert_class: tsig -> class -> class val cert_sort: tsig -> sort -> sort val minimize_sort: tsig -> sort -> sort val witness_sorts: tsig -> (typ * sort) list -> sort list -> (typ * sort) list type mode val mode_default: mode val mode_syntax: mode val mode_abbrev: mode val get_mode: Proof.context -> mode val set_mode: mode -> Proof.context -> Proof.context val restore_mode: Proof.context -> Proof.context -> Proof.context val type_space: tsig -> Name_Space.T val type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig val check_decl: Context.generic -> tsig -> xstring * Position.T -> (string * Position.report list) * decl val the_decl: tsig -> string * Position.T -> decl val cert_typ_mode: mode -> tsig -> typ -> typ val cert_typ: tsig -> typ -> typ val arity_number: tsig -> string -> int val arity_sorts: Context.generic -> tsig -> string -> sort -> sort list (*special treatment of type vars*) val sort_of_atyp: typ -> sort val strip_sorts: typ -> typ val strip_sorts_dummy: typ -> typ val no_tvars: typ -> typ - val varify_global: (string * sort) list -> term -> ((string * sort) * indexname) list * term + val varify_global: Term_Subst.TFrees.set -> term -> ((string * sort) * indexname) list * term val legacy_freeze_thaw_type: typ -> typ * (typ -> typ) val legacy_freeze_type: typ -> typ val legacy_freeze_thaw: term -> term * (term -> term) val legacy_freeze: term -> term (*matching and unification*) exception TYPE_MATCH type tyenv = (sort * typ) Vartab.table val lookup: tyenv -> indexname * sort -> typ option val devar: tyenv -> typ -> typ val typ_match: tsig -> typ * typ -> tyenv -> tyenv val typ_instance: tsig -> typ * typ -> bool val raw_match: typ * typ -> tyenv -> tyenv val raw_matches: typ list * typ list -> tyenv -> tyenv val could_match: typ * typ -> bool val could_matches: typ list * typ list -> bool val raw_instance: typ * typ -> bool exception TUNIFY val unify: tsig -> typ * typ -> tyenv * int -> tyenv * int val raw_unify: typ * typ -> tyenv -> tyenv val raw_unifys: typ list * typ list -> tyenv -> tyenv val could_unify: typ * typ -> bool val could_unifys: typ list * typ list -> bool val unified: tyenv -> typ * typ -> bool (*extend and merge type signatures*) val add_class: Context.generic -> binding * class list -> tsig -> tsig val hide_class: bool -> string -> tsig -> tsig val set_defsort: sort -> tsig -> tsig val add_type: Context.generic -> binding * int -> tsig -> tsig val add_abbrev: Context.generic -> binding * string list * typ -> tsig -> tsig val add_nonterminal: Context.generic -> binding -> tsig -> tsig val hide_type: bool -> string -> tsig -> tsig val add_arity: Context.generic -> arity -> tsig -> tsig val add_classrel: Context.generic -> class * class -> tsig -> tsig val merge_tsig: Context.generic -> tsig * tsig -> tsig end; structure Type: TYPE = struct (** constraints **) (*indicate polymorphic Vars*) fun mark_polymorphic T = Type ("_polymorphic_", [T]); fun constraint T t = if T = dummyT then t else Const ("_type_constraint_", T --> T) $ t; fun constraint_type ctxt T = let fun err () = error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T); in (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ()) end; fun strip_constraints (Const ("_type_constraint_", _) $ t) = strip_constraints t | strip_constraints (t $ u) = strip_constraints t $ strip_constraints u | strip_constraints (Abs (x, T, t)) = Abs (x, T, strip_constraints t) | strip_constraints a = a; fun appl_error ctxt (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U = cat_lines ["Failed to meet type constraint:", "", Pretty.string_of (Pretty.block [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt u, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt U]), Pretty.string_of (Pretty.block [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt T])] | appl_error ctxt t T u U = cat_lines ["Type error in application: " ^ (case T of Type ("fun", _) => "incompatible operand type" | _ => "operator not of function type"), "", Pretty.string_of (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, Syntax.pretty_term ctxt t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt T]), Pretty.string_of (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, Syntax.pretty_term ctxt u, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt U])]; (** type signatures and certified types **) (* type declarations *) datatype decl = LogicalType of int | Abbreviation of string list * typ * bool | Nonterminal; (* type tsig *) datatype tsig = TSig of { classes: Name_Space.T * Sorts.algebra, (*order-sorted algebra of type classes*) default: sort, (*default sort on input*) types: decl Name_Space.table, (*declared types*) log_types: string list}; (*logical types sorted by number of arguments*) fun eq_tsig (TSig {classes = classes1, default = default1, types = types1, log_types = _}, TSig {classes = classes2, default = default2, types = types2, log_types = _}) = pointer_eq (classes1, classes2) andalso default1 = default2 andalso pointer_eq (types1, types2); fun rep_tsig (TSig comps) = comps; fun make_tsig (classes, default, types, log_types) = TSig {classes = classes, default = default, types = types, log_types = log_types}; fun change_base begin (TSig {classes, default, types, log_types}) = make_tsig (classes, default, Name_Space.change_base begin types, log_types); fun change_ignore (TSig {classes, default, types, log_types}) = make_tsig (classes, default, Name_Space.change_ignore types, log_types); fun build_tsig (classes, default, types) = let val log_types = Name_Space.fold_table (fn (c, LogicalType n) => cons (c, n) | _ => I) types [] |> Library.sort (int_ord o apply2 snd) |> map fst; in make_tsig (classes, default, types, log_types) end; fun map_tsig f (TSig {classes, default, types, log_types = _}) = build_tsig (f (classes, default, types)); val empty_tsig = build_tsig ((Name_Space.empty Markup.classN, Sorts.empty_algebra), [], Name_Space.empty_table Markup.type_nameN); (* classes and sorts *) val class_space = #1 o #classes o rep_tsig; fun defaultS (TSig {default, ...}) = default; fun logical_types (TSig {log_types, ...}) = log_types; fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq (#2 classes); fun subsort (TSig {classes, ...}) = Sorts.sort_le (#2 classes); fun of_sort (TSig {classes, ...}) = Sorts.of_sort (#2 classes); fun inter_sort (TSig {classes, ...}) = Sorts.inter_sort (#2 classes); fun cert_class (TSig {classes = (_, algebra), ...}) c = if can (Graph.get_entry (Sorts.classes_of algebra)) c then c else raise TYPE ("Undeclared class: " ^ quote c, [], []); val cert_sort = map o cert_class; fun minimize_sort (TSig {classes, ...}) = Sorts.minimize_sort (#2 classes); fun witness_sorts (TSig {classes, log_types, ...}) = Sorts.witness_sorts (#2 classes) log_types; (* certification mode *) datatype mode = Mode of {normalize: bool, logical: bool}; val mode_default = Mode {normalize = true, logical = true}; val mode_syntax = Mode {normalize = true, logical = false}; val mode_abbrev = Mode {normalize = false, logical = false}; structure Mode = Proof_Data ( type T = mode; fun init _ = mode_default; ); val get_mode = Mode.get; fun set_mode mode = Mode.map (K mode); fun restore_mode ctxt = set_mode (get_mode ctxt); (* types *) val type_space = Name_Space.space_of_table o #types o rep_tsig; fun type_alias naming binding name = map_tsig (fn (classes, default, types) => (classes, default, (Name_Space.alias_table naming binding name types))); fun undecl_type c = "Undeclared type constructor: " ^ quote c; fun lookup_type (TSig {types, ...}) = Name_Space.lookup types; fun check_decl context (TSig {types, ...}) (c, pos) = Name_Space.check_reports context types (c, [pos]); fun the_decl tsig (c, pos) = (case lookup_type tsig c of NONE => error (undecl_type c ^ Position.here pos) | SOME decl => decl); (* certified types *) fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t; local fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts) | inst_typ env (T as TFree (x, _)) = the_default T (AList.lookup (op =) env x) | inst_typ _ T = T; in fun cert_typ_mode (Mode {normalize, logical}) tsig ty = let fun err msg = raise TYPE (msg, [ty], []); val check_logical = if logical then fn c => err ("Illegal occurrence of syntactic type: " ^ quote c) else fn _ => (); fun cert (T as Type (c, Ts)) = let val Ts' = map cert Ts; fun nargs n = if length Ts <> n then err (bad_nargs c) else (); in (case the_decl tsig (c, Position.none) of LogicalType n => (nargs n; Type (c, Ts')) | Abbreviation (vs, U, syn) => (nargs (length vs); if syn then check_logical c else (); if normalize then inst_typ (vs ~~ Ts') U else Type (c, Ts')) | Nonterminal => (nargs 0; check_logical c; T)) end | cert (TFree (x, S)) = TFree (x, cert_sort tsig S) | cert (TVar (xi as (_, i), S)) = if i < 0 then err ("Malformed type variable: " ^ quote (Term.string_of_vname xi)) else TVar (xi, cert_sort tsig S); val ty' = cert ty; in if ty = ty' then ty else ty' end; (*avoid copying of already normal type*) val cert_typ = cert_typ_mode mode_default; end; (* type arities *) fun arity_number tsig a = (case lookup_type tsig a of SOME (LogicalType n) => n | _ => error (undecl_type a)); fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) [] | arity_sorts context (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S handle Sorts.CLASS_ERROR err => error (Sorts.class_error context err); (** special treatment of type vars **) (* sort_of_atyp *) fun sort_of_atyp (TFree (_, S)) = S | sort_of_atyp (TVar (_, S)) = S | sort_of_atyp T = raise TYPE ("sort_of_atyp", [T], []); (* strip_sorts *) val strip_sorts = map_atyps (fn TFree (x, _) => TFree (x, []) | TVar (xi, _) => TVar (xi, [])); val strip_sorts_dummy = map_atyps (fn TFree (x, _) => TFree (x, dummyS) | TVar (xi, _) => TVar (xi, dummyS)); (* no_tvars *) fun no_tvars T = (case Term.add_tvarsT T [] of [] => T | vs => raise TYPE ("Illegal schematic type variable(s): " ^ commas_quote (map (Term.string_of_vname o #1) (rev vs)), [T], [])); (* varify_global *) fun varify_global fixed t = let - val fs = Term.fold_types (Term.fold_atyps - (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t []; + val fs = + (t, []) |-> (Term.fold_types o Term.fold_atyps) + (fn TFree v => if Term_Subst.TFrees.defined fixed v then I else insert (op =) v | _ => I); val used = Name.context |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t; val fmap = fs ~~ map (rpair 0) (#1 (fold_map Name.variant (map fst fs) used)); fun thaw (f as (_, S)) = (case AList.lookup (op =) fmap f of NONE => TFree f | SOME xi => TVar (xi, S)); in (fmap, map_types (map_type_tfree thaw) t) end; (* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *) local fun new_name ix (pairs, used) = let val v = singleton (Name.variant_list used) (string_of_indexname ix) in ((ix, v) :: pairs, v :: used) end; fun freeze_one alist (ix, sort) = TFree (the (AList.lookup (op =) alist ix), sort) handle Option.Option => raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []); fun thaw_one alist (a, sort) = TVar (the (AList.lookup (op =) alist a), sort) handle Option.Option => TFree (a, sort); in fun legacy_freeze_thaw_type T = let val used = Term.add_tfree_namesT T []; val (alist, _) = fold_rev new_name (map #1 (Term.add_tvarsT T [])) ([], used); in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end; val legacy_freeze_type = #1 o legacy_freeze_thaw_type; fun legacy_freeze_thaw t = let val used = Term.add_tfree_names t []; val (alist, _) = fold_rev new_name (map #1 (Term.add_tvars t [])) ([], used); in (case alist of [] => (t, fn x => x) (*nothing to do!*) | _ => (map_types (map_type_tvar (freeze_one alist)) t, map_types (map_type_tfree (thaw_one (map swap alist))))) end; val legacy_freeze = #1 o legacy_freeze_thaw; end; (** matching and unification of types **) type tyenv = (sort * typ) Vartab.table; fun tvar_clash ixn S S' = raise TYPE ("Type variable has two distinct sorts", [TVar (ixn, S), TVar (ixn, S')], []); fun lookup tye (ixn, S) = (case Vartab.lookup tye ixn of NONE => NONE | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S'); (* matching *) exception TYPE_MATCH; fun typ_match tsig = let fun match (TVar (v, S), T) subs = (case lookup subs (v, S) of NONE => if of_sort tsig (T, S) then Vartab.update_new (v, (S, T)) subs else raise TYPE_MATCH | SOME U => if U = T then subs else raise TYPE_MATCH) | match (Type (a, Ts), Type (b, Us)) subs = if a <> b then raise TYPE_MATCH else matches (Ts, Us) subs | match (TFree x, TFree y) subs = if x = y then subs else raise TYPE_MATCH | match _ _ = raise TYPE_MATCH and matches (T :: Ts, U :: Us) subs = matches (Ts, Us) (match (T, U) subs) | matches _ subs = subs; in match end; fun typ_instance tsig (T, U) = (Vartab.build (typ_match tsig (U, T)); true) handle TYPE_MATCH => false; (*purely structural matching*) fun raw_match (TVar (v, S), T) subs = (case lookup subs (v, S) of NONE => Vartab.update_new (v, (S, T)) subs | SOME U => if U = T then subs else raise TYPE_MATCH) | raw_match (Type (a, Ts), Type (b, Us)) subs = if a <> b then raise TYPE_MATCH else raw_matches (Ts, Us) subs | raw_match (TFree x, TFree y) subs = if x = y then subs else raise TYPE_MATCH | raw_match _ _ = raise TYPE_MATCH and raw_matches (T :: Ts, U :: Us) subs = raw_matches (Ts, Us) (raw_match (T, U) subs) | raw_matches ([], []) subs = subs | raw_matches _ _ = raise TYPE_MATCH; (*fast matching filter*) fun could_match (Type (a, Ts), Type (b, Us)) = a = b andalso could_matches (Ts, Us) | could_match (TFree (a, _), TFree (b, _)) = a = b | could_match (TVar _, _) = true | could_match _ = false and could_matches (T :: Ts, U :: Us) = could_match (T, U) andalso could_matches (Ts, Us) | could_matches ([], []) = true | could_matches _ = false; fun raw_instance (T, U) = if could_match (U, T) then (Vartab.build (raw_match (U, T)); true) handle TYPE_MATCH => false else false; (* unification *) exception TUNIFY; (*occurs check*) fun occurs v tye = let fun occ (Type (_, Ts)) = exists occ Ts | occ (TFree _) = false | occ (TVar (w, S)) = Term.eq_ix (v, w) orelse (case lookup tye (w, S) of NONE => false | SOME U => occ U); in occ end; (*chase variable assignments; if devar returns a type var then it must be unassigned*) fun devar tye (T as TVar v) = (case lookup tye v of SOME U => devar tye U | NONE => T) | devar _ T = T; (*order-sorted unification*) fun unify (TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) = let val tyvar_count = Unsynchronized.ref maxidx; fun gen_tyvar S = TVar ((Name.aT, Unsynchronized.inc tyvar_count), S); fun mg_domain a S = Sorts.mg_domain classes a S handle Sorts.CLASS_ERROR _ => raise TUNIFY; fun meet (_, []) tye = tye | meet (TVar (xi, S'), S) tye = if Sorts.sort_le classes (S', S) then tye else Vartab.update_new (xi, (S', gen_tyvar (Sorts.inter_sort classes (S', S)))) tye | meet (TFree (_, S'), S) tye = if Sorts.sort_le classes (S', S) then tye else raise TUNIFY | meet (Type (a, Ts), S) tye = meets (Ts, mg_domain a S) tye and meets (T :: Ts, S :: Ss) tye = meets (Ts, Ss) (meet (devar tye T, S) tye) | meets _ tye = tye; fun unif (ty1, ty2) tye = (case (devar tye ty1, devar tye ty2) of (T as TVar (v, S1), U as TVar (w, S2)) => if Term.eq_ix (v, w) then if S1 = S2 then tye else tvar_clash v S1 S2 else if Sorts.sort_le classes (S1, S2) then Vartab.update_new (w, (S2, T)) tye else if Sorts.sort_le classes (S2, S1) then Vartab.update_new (v, (S1, U)) tye else let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in Vartab.update_new (v, (S1, S)) (Vartab.update_new (w, (S2, S)) tye) end | (TVar (v, S), T) => if occurs v tye T then raise TUNIFY else meet (T, S) (Vartab.update_new (v, (S, T)) tye) | (T, TVar (v, S)) => if occurs v tye T then raise TUNIFY else meet (T, S) (Vartab.update_new (v, (S, T)) tye) | (Type (a, Ts), Type (b, Us)) => if a <> b then raise TUNIFY else unifs (Ts, Us) tye | (T, U) => if T = U then tye else raise TUNIFY) and unifs (T :: Ts, U :: Us) tye = unifs (Ts, Us) (unif (T, U) tye) | unifs _ tye = tye; in (unif TU tyenv, ! tyvar_count) end; (*purely structural unification*) fun raw_unify (ty1, ty2) tye = (case (devar tye ty1, devar tye ty2) of (T as TVar (v, S1), TVar (w, S2)) => if Term.eq_ix (v, w) then if S1 = S2 then tye else tvar_clash v S1 S2 else Vartab.update_new (w, (S2, T)) tye | (TVar (v, S), T) => if occurs v tye T then raise TUNIFY else Vartab.update_new (v, (S, T)) tye | (T, TVar (v, S)) => if occurs v tye T then raise TUNIFY else Vartab.update_new (v, (S, T)) tye | (Type (a, Ts), Type (b, Us)) => if a <> b then raise TUNIFY else raw_unifys (Ts, Us) tye | (T, U) => if T = U then tye else raise TUNIFY) and raw_unifys (T :: Ts, U :: Us) tye = raw_unifys (Ts, Us) (raw_unify (T, U) tye) | raw_unifys ([], []) tye = tye | raw_unifys _ _ = raise TUNIFY; (*fast unification filter*) fun could_unify (Type (a, Ts), Type (b, Us)) = a = b andalso could_unifys (Ts, Us) | could_unify (TFree (a, _), TFree (b, _)) = a = b | could_unify (TVar _, _) = true | could_unify (_, TVar _) = true | could_unify _ = false and could_unifys (T :: Ts, U :: Us) = could_unify (T, U) andalso could_unifys (Ts, Us) | could_unifys ([], []) = true | could_unifys _ = false; (*equality with respect to a type environment*) fun unified tye = let fun unif (T, T') = (case (devar tye T, devar tye T') of (Type (s, Ts), Type (s', Ts')) => s = s' andalso unifs (Ts, Ts') | (U, U') => U = U') and unifs ([], []) = true | unifs (T :: Ts, T' :: Ts') = unif (T', T') andalso unifs (Ts, Ts') | unifs _ = false; in if Vartab.is_empty tye then op = else unif end; (** extend and merge type signatures **) (* classes *) fun add_class context (c, cs) tsig = tsig |> map_tsig (fn ((space, classes), default, types) => let val cs' = map (cert_class tsig) cs handle TYPE (msg, _, _) => error msg; val _ = Binding.check c; val (c', space') = space |> Name_Space.declare context true c; val classes' = classes |> Sorts.add_class context (c', cs'); in ((space', classes'), default, types) end); fun hide_class fully c = map_tsig (fn ((space, classes), default, types) => ((Name_Space.hide fully c space, classes), default, types)); (* arities *) fun add_arity context (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) => let val _ = (case lookup_type tsig t of SOME (LogicalType n) => if length Ss <> n then error (bad_nargs t) else () | SOME _ => error ("Logical type constructor expected: " ^ quote t) | NONE => error (undecl_type t)); val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S) handle TYPE (msg, _, _) => error msg; val classes' = classes |> Sorts.add_arities context ((t, map (fn c' => (c', Ss')) S')); in ((space, classes'), default, types) end); (* classrel *) fun add_classrel context rel tsig = tsig |> map_tsig (fn ((space, classes), default, types) => let val rel' = apply2 (cert_class tsig) rel handle TYPE (msg, _, _) => error msg; val classes' = classes |> Sorts.add_classrel context rel'; in ((space, classes'), default, types) end); (* default sort *) fun set_defsort S tsig = tsig |> map_tsig (fn (classes, _, types) => (classes, cert_sort tsig S handle TYPE (msg, _, _) => error msg, types)); (* types *) local fun new_decl context (c, decl) types = (Binding.check c; #2 (Name_Space.define context true (c, decl) types)); fun map_types f = map_tsig (fn (classes, default, types) => let val types' = f types; val _ = not (Name_Space.defined types' "dummy") orelse Name_Space.intern (Name_Space.space_of_table types') "dummy" = "dummy" orelse error "Illegal declaration of dummy type"; in (classes, default, types') end); fun syntactic tsig (Type (c, Ts)) = (case lookup_type tsig c of SOME Nonterminal => true | _ => false) orelse exists (syntactic tsig) Ts | syntactic _ _ = false; in fun add_type context (c, n) = if n < 0 then error ("Bad type constructor declaration " ^ Binding.print c) else map_types (new_decl context (c, LogicalType n)); fun add_abbrev context (a, vs, rhs) tsig = tsig |> map_types (fn types => let fun err msg = cat_error msg ("The error(s) above occurred in type abbreviation " ^ Binding.print a); val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs)) handle TYPE (msg, _, _) => err msg; val _ = (case duplicates (op =) vs of [] => [] | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups)); val _ = (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of [] => [] | extras => err ("Extra variables on rhs: " ^ commas_quote extras)); in types |> new_decl context (a, Abbreviation (vs, rhs', syntactic tsig rhs')) end); fun add_nonterminal context = map_types o new_decl context o rpair Nonterminal; end; fun hide_type fully c = map_tsig (fn (classes, default, types) => (classes, default, Name_Space.hide_table fully c types)); (* merge type signatures *) fun merge_tsig context (tsig1, tsig2) = let val (TSig {classes = (space1, classes1), default = default1, types = types1, log_types = _}) = tsig1; val (TSig {classes = (space2, classes2), default = default2, types = types2, log_types = _}) = tsig2; val space' = Name_Space.merge (space1, space2); val classes' = Sorts.merge_algebra context (classes1, classes2); val default' = Sorts.inter_sort classes' (default1, default2); val types' = Name_Space.merge_tables (types1, types2); in build_tsig ((space', classes'), default', types') end; end; diff --git a/src/Tools/IsaPlanner/rw_inst.ML b/src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML +++ b/src/Tools/IsaPlanner/rw_inst.ML @@ -1,243 +1,243 @@ (* Title: Tools/IsaPlanner/rw_inst.ML Author: Lucas Dixon, University of Edinburgh Rewriting using a conditional meta-equality theorem which supports schematic variable instantiation. *) signature RW_INST = sig val rw: Proof.context -> ((indexname * (sort * typ)) list * (* type var instantiations *) (indexname * (typ * term)) list) (* schematic var instantiations *) * (string * typ) list (* Fake named bounds + types *) * (string * typ) list (* names of bound + types *) * term -> (* outer term for instantiation *) thm -> (* rule with indexes lifted *) thm -> (* target thm *) thm (* rewritten theorem possibly with additional premises for rule conditions *) end; structure RW_Inst: RW_INST = struct (* Given (string,type) pairs capturing the free vars that need to be allified in the assumption, and a theorem with assumptions possibly containing the free vars, then we give back the assumptions allified as hidden hyps. Given: x th: A vs ==> B vs Results in: "B vs" [!!x. A x] *) fun allify_conditions ctxt Ts th = let fun allify (x, T) t = Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t)); val cTs = map (Thm.cterm_of ctxt o Free) Ts; val cterm_asms = map (Thm.cterm_of ctxt o fold_rev allify Ts) (Thm.prems_of th); val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms; in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end; (* Given a list of variables that were bound, and a that has been instantiated with free variable placeholders for the bound vars, it creates an abstracted version of the theorem, with local bound vars as lambda-params: Ts: ("x", ty) rule:: C :x ==> P :x = Q :x results in: ("!! x. C x", (%x. p x = %y. p y) [!! x. C x]) note: assumes rule is instantiated *) (* Note, we take abstraction in the order of last abstraction first *) fun mk_abstractedrule ctxt TsFake Ts rule = let (* now we change the names of temporary free vars that represent bound vars with binders outside the redex *) val ns = IsaND.variant_names ctxt (Thm.full_prop_of rule :: Thm.hyps_of rule) (map fst Ts); val (fromnames, tonames, Ts') = fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') => (Thm.cterm_of ctxt (Free(faken,ty)) :: rnf, Thm.cterm_of ctxt (Free(n2,ty)) :: rnt, (n2,ty) :: Ts'')) (TsFake ~~ Ts ~~ ns) ([], [], []); (* rename conflicting free's in the rule to avoid cconflicts with introduced vars from bounds outside in redex *) val rule' = rule |> Drule.forall_intr_list fromnames |> Drule.forall_elim_list tonames; (* make unconditional rule and prems *) val (uncond_rule, cprems) = allify_conditions ctxt (rev Ts') rule'; (* using these names create lambda-abstracted version of the rule *) val abstractions = rev (Ts' ~~ tonames); val abstract_rule = fold (fn ((n, ty), ct) => Thm.abstract_rule n ct) abstractions uncond_rule; in (cprems, abstract_rule) end; (* given names to avoid, and vars that need to be fixed, it gives unique new names to the vars so that they can be fixed as free variables *) (* make fixed unique free variable instantiations for non-ground vars *) (* Create a table of vars to be renamed after instantiation - ie other uninstantiated vars in the hyps of the rule ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) fun mk_renamings ctxt tgt rule_inst = let val rule_conds = Thm.prems_of rule_inst; val (_, cond_vs) = fold (fn t => fn (tyvs, vs) => (union (op =) (Misc_Legacy.term_tvars t) tyvs, union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs)) rule_conds ([], []); val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt); val vars_to_fix = union (op =) termvars cond_vs; val ys = IsaND.variant_names ctxt (tgt :: rule_conds) (map (fst o fst) vars_to_fix); in map2 (fn (xi, T) => fn y => ((xi, T), Free (y, T))) vars_to_fix ys end; (* make a new fresh typefree instantiation for the given tvar *) fun new_tfree (tv as (ix,sort)) (pairs, used) = let val v = singleton (Name.variant_list used) (string_of_indexname ix) in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end; (* make instantiations to fix type variables that are not already instantiated (in ignore_ixs) from the list of terms. *) fun mk_fixtvar_tyinsts ignore_insts ts = let val ignore_ixs = map fst ignore_insts; val (tvars, tfrees) = fold_rev (fn t => fn (varixs, tfrees) => (Misc_Legacy.add_term_tvars (t,varixs), Misc_Legacy.add_term_tfrees (t,tfrees))) ts ([], []); val unfixed_tvars = filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars; val (fixtyinsts, _) = fold_rev new_tfree unfixed_tvars ([], map fst tfrees) in (fixtyinsts, tfrees) end; (* cross-instantiate the instantiations - ie for each instantiation replace all occurrences in other instantiations - no loops are possible and thus only one-parsing of the instantiations is necessary. *) fun cross_inst insts = let fun instL (ix, (ty,t)) = map (fn (ix2,(ty2,t2)) => (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2))); fun cross_instL ([], l) = rev l | cross_instL ((ix, t) :: insts, l) = cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); in cross_instL (insts, []) end; (* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *) fun cross_inst_typs insts = let fun instL (ix, (srt,ty)) = map (fn (ix2,(srt2,ty2)) => (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2))); fun cross_instL ([], l) = rev l | cross_instL ((ix, t) :: insts, l) = cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); in cross_instL (insts, []) end; (* assume that rule and target_thm have distinct var names. THINK: efficient version with tables for vars for: target vars, introduced vars, and rule vars, for quicker instantiation? The outerterm defines which part of the target_thm was modified. Note: we take Ts in the upterm order, ie last abstraction first., and with an outeterm where the abstracted subterm has the arguments in the revered order, ie first abstraction first. FakeTs has abstractions using the fake name - ie the name distinct from all other abstractions. *) fun rw ctxt ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = let (* fix all non-instantiated tvars *) val (fixtyinsts, othertfrees) = (* FIXME proper context!? *) mk_fixtvar_tyinsts nonfixed_typinsts [Thm.prop_of rule, Thm.prop_of target_thm]; val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); (* certified instantiations for types *) val ctyp_insts = map (fn (ix, (s, ty)) => ((ix, s), Thm.ctyp_of ctxt ty)) typinsts; (* type instantiated versions *) val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm; val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule; val term_typ_inst = map (fn (ix,(_,ty)) => (ix,ty)) typinsts; (* type instanitated outer term *) val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm; val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) FakeTs; val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) Ts; (* type-instantiate the var instantiations *) val insts_tyinst = fold_rev (fn (ix, (ty, t)) => fn insts_tyinst => (ix, (Term.typ_subst_TVars term_typ_inst ty, Term.subst_TVars term_typ_inst t)) :: insts_tyinst) unprepinsts []; (* cross-instantiate *) val insts_tyinst_inst = cross_inst insts_tyinst; (* create certms of instantiations *) val cinsts_tyinst = map (fn (ix, (ty, t)) => ((ix, ty), Thm.cterm_of ctxt t)) insts_tyinst_inst; (* The instantiated rule *) val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst); (* Create a table of vars to be renamed after instantiation - ie other uninstantiated vars in the hyps the *instantiated* rule ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) val renamings = mk_renamings ctxt (Thm.prop_of tgt_th_tyinst) rule_inst; val cterm_renamings = map (fn (x, y) => apply2 (Thm.cterm_of ctxt) (Var x, y)) renamings; (* Create the specific version of the rule for this target application *) val outerterm_inst = outerterm_tyinst |> Term.subst_Vars (map (fn (ix, (ty, t)) => (ix, t)) insts_tyinst_inst) |> Term.subst_Vars (map (fn ((ix, ty), t) => (ix, t)) renamings); val couter_inst = Thm.reflexive (Thm.cterm_of ctxt outerterm_inst); val (cprems, abstract_rule_inst) = rule_inst |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings) |> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst; val specific_tgt_rule = Conv.fconv_rule Drule.beta_eta_conversion (Thm.combination couter_inst abstract_rule_inst); (* create an instantiated version of the target thm *) val tgt_th_inst = tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst) |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings); val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; in Conv.fconv_rule Drule.beta_eta_conversion tgt_th_inst |> Thm.equal_elim specific_tgt_rule |> Drule.implies_intr_list cprems |> Drule.forall_intr_list frees_of_fixed_vars |> Drule.forall_elim_list vars - |> Thm.varifyT_global' othertfrees + |> Thm.varifyT_global' (Term_Subst.TFrees.make_set othertfrees) |-> K Drule.zero_var_indexes end; end;