diff --git a/src/Pure/ML/ml_antiquotations.ML b/src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML +++ b/src/Pure/ML/ml_antiquotations.ML @@ -1,619 +1,619 @@ (* Title: Pure/ML/ml_antiquotations.ML Author: Makarius Miscellaneous ML antiquotations. *) signature ML_ANTIQUOTATIONS = sig val make_judgment: Proof.context -> term -> term val dest_judgment: Proof.context -> term -> term val make_ctyp: Proof.context -> typ -> ctyp val make_cterm: Proof.context -> term -> cterm type insts = ((indexname * sort) * typ) list * ((indexname * typ) * term) list type cinsts = ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list val instantiate_typ: insts -> typ -> typ val instantiate_ctyp: cinsts -> ctyp -> ctyp val instantiate_term: insts -> term -> term val instantiate_cterm: cinsts -> cterm -> cterm end; structure ML_Antiquotations: ML_ANTIQUOTATIONS = struct (* ML support *) val _ = Theory.setup (ML_Antiquotation.inline \<^binding>\undefined\ (Scan.succeed "(raise General.Match)") #> ML_Antiquotation.inline \<^binding>\assert\ (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> ML_Antiquotation.declaration_embedded \<^binding>\print\ (Scan.lift (Scan.optional Parse.embedded "Output.writeln")) (fn src => fn output => fn ctxt => let val struct_name = ML_Context.struct_name ctxt; val (_, pos) = Token.name_of_src src; val (a, ctxt') = ML_Context.variant "output" ctxt; val env = "val " ^ a ^ ": string -> unit =\n\ \ (" ^ output ^ ") o (fn s => s ^ Position.here (" ^ ML_Syntax.print_position pos ^ "));\n"; val body = "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))"; in (K (env, body), ctxt') end) #> ML_Antiquotation.value \<^binding>\rat\ (Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat -- Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) => "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b))) #> ML_Antiquotation.conditional \<^binding>\if_linux\ (fn _ => ML_System.platform_is_linux) #> ML_Antiquotation.conditional \<^binding>\if_macos\ (fn _ => ML_System.platform_is_macos) #> ML_Antiquotation.conditional \<^binding>\if_windows\ (fn _ => ML_System.platform_is_windows) #> ML_Antiquotation.conditional \<^binding>\if_unix\ (fn _ => ML_System.platform_is_unix)); (* formal entities *) val _ = Theory.setup (ML_Antiquotation.value_embedded \<^binding>\system_option\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #> ML_Antiquotation.value_embedded \<^binding>\theory\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (Theory.check {long = false} ctxt (name, pos); "Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name)) || Scan.succeed "Proof_Context.theory_of ML_context") #> ML_Antiquotation.value_embedded \<^binding>\theory_context\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (Theory.check {long = false} ctxt (name, pos); "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))) #> ML_Antiquotation.inline \<^binding>\context\ (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #> ML_Antiquotation.inline_embedded \<^binding>\typ\ (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> ML_Antiquotation.inline_embedded \<^binding>\term\ (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> ML_Antiquotation.inline_embedded \<^binding>\prop\ (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> ML_Antiquotation.value_embedded \<^binding>\ctyp\ (Args.typ >> (fn T => "Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #> ML_Antiquotation.value_embedded \<^binding>\cterm\ (Args.term >> (fn t => "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> ML_Antiquotation.value_embedded \<^binding>\cprop\ (Args.prop >> (fn t => "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> ML_Antiquotation.inline_embedded \<^binding>\oracle_name\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => ML_Syntax.print_string (Thm.check_oracle ctxt (name, pos))))); (* schematic variables *) val schematic_input = Args.context -- Scan.lift Parse.embedded_input >> (fn (ctxt, src) => (Proof_Context.set_mode Proof_Context.mode_schematic ctxt, (Syntax.implode_input src, Input.pos_of src))); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\tvar\ (schematic_input >> (fn (ctxt, (s, pos)) => (case Syntax.read_typ ctxt s of TVar v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_sort v | _ => error ("Schematic type variable expected" ^ Position.here pos)))) #> ML_Antiquotation.inline_embedded \<^binding>\var\ (schematic_input >> (fn (ctxt, (s, pos)) => (case Syntax.read_term ctxt s of Var v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_typ v | _ => error ("Schematic variable expected" ^ Position.here pos))))); (* type classes *) fun class syn = Args.context -- Scan.lift Parse.embedded_inner_syntax >> (fn (ctxt, s) => Proof_Context.read_class ctxt s |> syn ? Lexicon.mark_class |> ML_Syntax.print_string); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\class\ (class false) #> ML_Antiquotation.inline_embedded \<^binding>\class_syntax\ (class true) #> ML_Antiquotation.inline_embedded \<^binding>\sort\ (Args.context -- Scan.lift Parse.embedded_inner_syntax >> (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))); (* type constructors *) fun type_name kind check = Args.context -- Scan.lift (Parse.token Parse.embedded) >> (fn (ctxt, tok) => let val s = Token.inner_syntax_of tok; val (_, pos) = Input.source_content (Token.input_of tok); val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s; val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos); val res = (case try check (c, decl) of SOME res => res | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos)); in ML_Syntax.print_string res end); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\type_name\ (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #> ML_Antiquotation.inline_embedded \<^binding>\type_abbrev\ (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #> ML_Antiquotation.inline_embedded \<^binding>\nonterminal\ (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #> ML_Antiquotation.inline_embedded \<^binding>\type_syntax\ (type_name "type" (fn (c, _) => Lexicon.mark_type c))); (* constants *) fun const_name check = Args.context -- Scan.lift (Parse.token Parse.embedded) >> (fn (ctxt, tok) => let val s = Token.inner_syntax_of tok; val (_, pos) = Input.source_content (Token.input_of tok); val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s; val res = check (Proof_Context.consts_of ctxt, c) handle TYPE (msg, _, _) => error (msg ^ Position.here pos); in ML_Syntax.print_string res end); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\const_name\ (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #> ML_Antiquotation.inline_embedded \<^binding>\const_abbrev\ (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> ML_Antiquotation.inline_embedded \<^binding>\const_syntax\ (const_name (fn (_, c) => Lexicon.mark_const c)) #> ML_Antiquotation.inline_embedded \<^binding>\syntax_const\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, arg) => ML_Syntax.print_string (Proof_Context.check_syntax_const ctxt arg))) #> ML_Antiquotation.inline_embedded \<^binding>\const\ (Args.context -- Scan.lift (Parse.position Parse.embedded_inner_syntax) -- Scan.optional (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] >> (fn ((ctxt, (raw_c, pos)), Ts) => let val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt raw_c; val consts = Proof_Context.consts_of ctxt; val n = length (Consts.typargs consts (c, Consts.type_scheme consts c)); val _ = length Ts <> n andalso error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^ quote c ^ enclose "(" ")" (commas (replicate n "_")) ^ Position.here pos); val const = Const (c, Consts.instance consts (c, Ts)); in ML_Syntax.atomic (ML_Syntax.print_term const) end))); (* object-logic judgment *) fun make_judgment ctxt = let val const = Object_Logic.judgment_const ctxt in fn t => Const const $ t end; fun dest_judgment ctxt = let val is_judgment = Object_Logic.is_judgment ctxt; val drop_judgment = Object_Logic.drop_judgment ctxt; in fn t => if is_judgment t then drop_judgment t else raise TERM ("dest_judgment", [t]) end; val _ = Theory.setup (ML_Antiquotation.value \<^binding>\make_judgment\ (Scan.succeed "ML_Antiquotations.make_judgment ML_context") #> ML_Antiquotation.value \<^binding>\dest_judgment\ (Scan.succeed "ML_Antiquotations.dest_judgment ML_context")); (* type/term instantiations and constructors *) fun make_ctyp ctxt T = Thm.ctyp_of ctxt T |> Thm.trim_context_ctyp; fun make_cterm ctxt t = Thm.cterm_of ctxt t |> Thm.trim_context_cterm; type insts = ((indexname * sort) * typ) list * ((indexname * typ) * term) list type cinsts = ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list fun instantiate_typ (insts: insts) = Term_Subst.instantiateT (TVars.make (#1 insts)); fun instantiate_ctyp (cinsts: cinsts) = Thm.instantiate_ctyp (TVars.make (#1 cinsts)); fun instantiate_term (insts: insts) = let val instT = TVars.make (#1 insts); val instantiateT = Term_Subst.instantiateT instT; val inst = Vars.make ((map o apfst o apsnd) instantiateT (#2 insts)); - in Term_Subst.instantiate (instT, inst) end; + in Term_Subst.instantiate_beta (instT, inst) end; fun instantiate_cterm (cinsts: cinsts) = let val cinstT = TVars.make (#1 cinsts); val instantiateT = Term_Subst.instantiateT (TVars.map (K Thm.typ_of) cinstT); val cinst = Vars.make ((map o apfst o apsnd) instantiateT (#2 cinsts)); - in Thm.instantiate_cterm (cinstT, cinst) end; + in Thm.instantiate_beta_cterm (cinstT, cinst) end; local fun make_keywords ctxt = Thy_Header.get_keywords' ctxt |> Keyword.no_major_keywords |> Keyword.add_major_keywords ["typ", "term", "prop", "ctyp", "cterm", "cprop"]; val parse_inst_name = Parse.position (Parse.type_ident >> pair true || Parse.name >> pair false); val parse_inst = (parse_inst_name -- (Parse.$$$ "=" |-- Parse.!!! Parse.embedded_ml) || Scan.ahead parse_inst_name -- Parse.embedded_ml) >> (fn (((b, a), pos), ml) => (b, ((a, pos), ml))); val parse_insts = Parse.and_list1 parse_inst >> (List.partition #1 #> apply2 (map #2)); val ml = ML_Lex.tokenize_no_range; val ml_range = ML_Lex.tokenize_range; fun ml_parens x = ml "(" @ x @ ml ")"; fun ml_bracks x = ml "[" @ x @ ml "]"; fun ml_commas xs = flat (separate (ml ", ") xs); val ml_list = ml_bracks o ml_commas; fun ml_pair (x, y) = ml_parens (ml_commas [x, y]); val ml_list_pair = ml_list o ListPair.map ml_pair; fun get_tfree envT (a, pos) = (case AList.lookup (op =) envT a of SOME S => (a, S) | NONE => error ("No occurrence of type variable " ^ quote a ^ Position.here pos)); fun check_free ctxt env (x, pos) = (case AList.lookup (op =) env x of SOME T => (Context_Position.reports ctxt (map (pair pos) (Syntax_Phases.markup_free ctxt x)); (x, T)) | NONE => error ("No occurrence of variable " ^ quote x ^ Position.here pos)); fun make_instT (a, pos) T = (case try (Term.dest_TVar o Logic.dest_type) T of NONE => error ("Not a free type variable " ^ quote a ^ Position.here pos) | SOME v => ml (ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_sort v)); fun make_inst (a, pos) t = (case try Term.dest_Var t of NONE => error ("Not a free variable " ^ quote a ^ Position.here pos) | SOME v => ml (ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_typ v)); fun prepare_insts ctxt1 ctxt0 (instT, inst) t = let val envT = Term.add_tfrees t []; val env = Term.add_frees t []; val freesT = map (Logic.mk_type o TFree o get_tfree envT) instT; val frees = map (Free o check_free ctxt1 env) inst; val (t' :: varsT, vars) = Variable.export_terms ctxt1 ctxt0 (t :: freesT @ frees) |> chop (1 + length freesT); val ml_insts = (map2 make_instT instT varsT, map2 make_inst inst vars); in (ml_insts, t') end; fun prepare_ml range (kind, ml1, ml2) ml_val (ml_instT, ml_inst) ctxt = let val (ml_name, ctxt') = ML_Context.variant kind ctxt; val ml_env = ml ("val " ^ ml_name ^ " = ") @ ml ml1 @ ml_parens (ml ml_val) @ ml ";\n"; fun ml_body (ml_argsT, ml_args) = ml_parens (ml ml2 @ ml_pair (ml_list_pair (ml_instT, ml_argsT), ml_list_pair (ml_inst, ml_args)) @ ml_range range (ML_Context.struct_name ctxt ^ "." ^ ml_name)); in ((ml_env, ml_body), ctxt') end; fun prepare_type range (arg, s) insts ctxt = let val T = Syntax.read_typ ctxt s; val t = Logic.mk_type T; val ctxt1 = Proof_Context.augment t ctxt; val (ml_insts, T') = prepare_insts ctxt1 ctxt insts t ||> Logic.dest_type; in prepare_ml range arg (ML_Syntax.print_typ T') ml_insts ctxt end; fun prepare_term read range (arg, (s, fixes)) insts ctxt = let val ctxt' = #2 (Proof_Context.add_fixes_cmd fixes ctxt); val t = read ctxt' s; val ctxt1 = Proof_Context.augment t ctxt'; val (ml_insts, t') = prepare_insts ctxt1 ctxt insts t; in prepare_ml range arg (ML_Syntax.print_term t') ml_insts ctxt end; fun typ_ml kind = (kind, "", "ML_Antiquotations.instantiate_typ"); fun term_ml kind = (kind, "", "ML_Antiquotations.instantiate_term"); fun ctyp_ml kind = (kind, "ML_Antiquotations.make_ctyp ML_context", "ML_Antiquotations.instantiate_ctyp"); fun cterm_ml kind = (kind, "ML_Antiquotations.make_cterm ML_context", "ML_Antiquotations.instantiate_cterm"); fun parse_body range = (Parse.command_name "typ" >> typ_ml || Parse.command_name "ctyp" >> ctyp_ml) -- Parse.!!! Parse.typ >> prepare_type range || (Parse.command_name "term" >> term_ml || Parse.command_name "cterm" >> cterm_ml) -- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_term range || (Parse.command_name "prop" >> term_ml || Parse.command_name "cprop" >> cterm_ml) -- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_prop range; val _ = Theory.setup (ML_Context.add_antiquotation \<^binding>\instantiate\ true (fn range => fn src => fn ctxt => let val (insts, prepare_val) = src |> Parse.read_embedded_src ctxt (make_keywords ctxt) ((parse_insts --| Parse.$$$ "in") -- parse_body range); val (((ml_env, ml_body), decls), ctxt1) = ctxt |> prepare_val (apply2 (map #1) insts) ||>> ML_Context.expand_antiquotes_list (op @ (apply2 (map #2) insts)); fun decl' ctxt' = let val (ml_args_env, ml_args) = split_list (decls ctxt') in (ml_env @ flat ml_args_env, ml_body (chop (length (#1 insts)) ml_args)) end; in (decl', ctxt1) end)); in end; local val keywords = Keyword.add_minor_keywords ["for", "=>"] Keyword.empty_keywords; val parse_name = Parse.input Parse.name; val parse_args = Scan.repeat Parse.embedded_ml_underscore; val parse_for_args = Scan.optional (Parse.$$$ "for" |-- Parse.!!! parse_args) []; fun parse_body b = if b then Parse.$$$ "=>" |-- Parse.!!! Parse.embedded_input >> (ML_Lex.read_source #> single) else Scan.succeed []; fun is_dummy [Antiquote.Text tok] = ML_Lex.content_of tok = "_" | is_dummy _ = false; val ml = ML_Lex.tokenize_no_range; val ml_range = ML_Lex.tokenize_range; val ml_dummy = ml "_"; fun ml_enclose range x = ml "(" @ x @ ml_range range ")"; fun ml_parens x = ml "(" @ x @ ml ")"; fun ml_bracks x = ml "[" @ x @ ml "]"; fun ml_commas xs = flat (separate (ml ", ") xs); val ml_list = ml_bracks o ml_commas; val ml_string = ml o ML_Syntax.print_string; fun ml_pair (x, y) = ml_parens (ml_commas [x, y]); fun type_antiquotation binding {function} = ML_Context.add_antiquotation binding true (fn range => fn src => fn ctxt => let val ((s, type_args), fn_body) = src |> Parse.read_embedded_src ctxt keywords (parse_name -- parse_args -- parse_body function); val pos = Input.pos_of s; val Type (c, Ts) = Proof_Context.read_type_name {proper = true, strict = true} ctxt (Syntax.implode_input s); val n = length Ts; val _ = length type_args = n orelse error ("Type constructor " ^ quote (Proof_Context.markup_type ctxt c) ^ " takes " ^ string_of_int n ^ " argument(s)" ^ Position.here pos); val (decls1, ctxt1) = ML_Context.expand_antiquotes_list type_args ctxt; val (decls2, ctxt2) = ML_Context.expand_antiquotes_list fn_body ctxt1; fun decl' ctxt' = let val (ml_args_env, ml_args_body) = split_list (decls1 ctxt'); val (ml_fn_env, ml_fn_body) = split_list (decls2 ctxt'); val ml1 = ml_enclose range (ml "Term.Type " @ ml_pair (ml_string c, ml_list ml_args_body)); val ml2 = if function then ml_enclose range (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @ ml "| T => " @ ml_range range "raise" @ ml " Term.TYPE (" @ ml_string ("Type_fn " ^ quote c) @ ml ", [T], [])") else ml1; in (flat (ml_args_env @ ml_fn_env), ml2) end; in (decl', ctxt2) end); fun const_antiquotation binding {pattern, function} = ML_Context.add_antiquotation binding true (fn range => fn src => fn ctxt => let val (((s, type_args), term_args), fn_body) = src |> Parse.read_embedded_src ctxt keywords (parse_name -- parse_args -- parse_for_args -- parse_body function); val Const (c, T) = Proof_Context.read_const {proper = true, strict = true} ctxt (Syntax.implode_input s); val consts = Proof_Context.consts_of ctxt; val type_paths = Consts.type_arguments consts c; val type_params = map Term.dest_TVar (Consts.typargs consts (c, T)); val n = length type_params; val m = length (Term.binder_types T); fun err msg = error ("Constant " ^ quote (Proof_Context.markup_const ctxt c) ^ msg ^ Position.here (Input.pos_of s)); val _ = length type_args <> n andalso err (" takes " ^ string_of_int n ^ " type argument(s)"); val _ = length term_args > m andalso Term.is_Type (Term.body_type T) andalso err (" cannot have more than " ^ string_of_int m ^ " argument(s)"); val (decls1, ctxt1) = ML_Context.expand_antiquotes_list type_args ctxt; val (decls2, ctxt2) = ML_Context.expand_antiquotes_list term_args ctxt1; val (decls3, ctxt3) = ML_Context.expand_antiquotes_list fn_body ctxt2; fun decl' ctxt' = let val (ml_args_env1, ml_args_body1) = split_list (decls1 ctxt'); val (ml_args_env2, ml_args_body2) = split_list (decls2 ctxt'); val (ml_fn_env, ml_fn_body) = split_list (decls3 ctxt'); val relevant = map is_dummy type_args ~~ type_paths; fun relevant_path is = not pattern orelse let val p = rev is in relevant |> exists (fn (u, q) => not u andalso is_prefix (op =) p q) end; val ml_typarg = the o AList.lookup (op =) (type_params ~~ ml_args_body1); fun ml_typ is (Type (d, Us)) = if relevant_path is then ml "Term.Type " @ ml_pair (ml_string d, ml_list (map_index (fn (i, U) => ml_typ (i :: is) U) Us)) else ml_dummy | ml_typ is (TVar arg) = if relevant_path is then ml_typarg arg else ml_dummy | ml_typ _ (TFree _) = raise Match; fun ml_app [] = ml "Term.Const " @ ml_pair (ml_string c, ml_typ [] T) | ml_app (u :: us) = ml "Term.$ " @ ml_pair (ml_app us, u); val ml_env = flat (ml_args_env1 @ ml_args_env2 @ ml_fn_env); val ml1 = ml_enclose range (ml_app (rev ml_args_body2)); val ml2 = if function then ml_enclose range (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @ ml "| t => " @ ml_range range "raise" @ ml " Term.TERM (" @ ml_string ("Const_fn " ^ quote c) @ ml ", [t])") else ml1; in (ml_env, ml2) end; in (decl', ctxt3) end); val _ = Theory.setup (type_antiquotation \<^binding>\Type\ {function = false} #> type_antiquotation \<^binding>\Type_fn\ {function = true} #> const_antiquotation \<^binding>\Const\ {pattern = false, function = false} #> const_antiquotation \<^binding>\Const_\ {pattern = true, function = false} #> const_antiquotation \<^binding>\Const_fn\ {pattern = true, function = true}); in end; (* special forms *) val _ = Theory.setup (ML_Antiquotation.special_form \<^binding>\try\ "() |> Basics.try" #> ML_Antiquotation.special_form \<^binding>\can\ "() |> Basics.can"); (* basic combinators *) local val parameter = Parse.position Parse.nat >> (fn (n, pos) => if n > 1 then n else error ("Bad parameter: " ^ string_of_int n ^ Position.here pos)); fun indices n = map string_of_int (1 upto n); fun empty n = replicate_string n " []"; fun dummy n = replicate_string n " _"; fun vars x n = implode (map (fn a => " " ^ x ^ a) (indices n)); fun cons n = implode (map (fn a => " (x" ^ a ^ " :: xs" ^ a ^ ")") (indices n)); val tuple = enclose "(" ")" o commas; fun tuple_empty n = tuple (replicate n "[]"); fun tuple_vars x n = tuple (map (fn a => x ^ a) (indices n)); fun tuple_cons n = "(" ^ tuple_vars "x" n ^ " :: xs)" fun cons_tuple n = tuple (map (fn a => "x" ^ a ^ " :: xs" ^ a) (indices n)); in val _ = Theory.setup (ML_Antiquotation.value \<^binding>\map\ (Scan.lift parameter >> (fn n => "fn f =>\n\ \ let\n\ \ fun map _" ^ empty n ^ " = []\n\ \ | map f" ^ cons n ^ " = f" ^ vars "x" n ^ " :: map f" ^ vars "xs" n ^ "\n\ \ | map _" ^ dummy n ^ " = raise ListPair.UnequalLengths\n" ^ " in map f end")) #> ML_Antiquotation.value \<^binding>\fold\ (Scan.lift parameter >> (fn n => "fn f =>\n\ \ let\n\ \ fun fold _" ^ empty n ^ " a = a\n\ \ | fold f" ^ cons n ^ " a = fold f" ^ vars "xs" n ^ " (f" ^ vars "x" n ^ " a)\n\ \ | fold _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ " in fold f end")) #> ML_Antiquotation.value \<^binding>\fold_map\ (Scan.lift parameter >> (fn n => "fn f =>\n\ \ let\n\ \ fun fold_map _" ^ empty n ^ " a = ([], a)\n\ \ | fold_map f" ^ cons n ^ " a =\n\ \ let\n\ \ val (x, a') = f" ^ vars "x" n ^ " a\n\ \ val (xs, a'') = fold_map f" ^ vars "xs" n ^ " a'\n\ \ in (x :: xs, a'') end\n\ \ | fold_map _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ " in fold_map f end")) #> ML_Antiquotation.value \<^binding>\split_list\ (Scan.lift parameter >> (fn n => "fn list =>\n\ \ let\n\ \ fun split_list [] =" ^ tuple_empty n ^ "\n\ \ | split_list" ^ tuple_cons n ^ " =\n\ \ let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\ \ in " ^ cons_tuple n ^ "end\n\ \ in split_list list end")) #> ML_Antiquotation.value \<^binding>\apply\ (Scan.lift (parameter -- Scan.option (Args.parens (Parse.position Parse.nat))) >> (fn (n, opt_index) => let val cond = (case opt_index of NONE => K true | SOME (index, index_pos) => if 1 <= index andalso index <= n then equal (string_of_int index) else error ("Bad index: " ^ string_of_int index ^ Position.here index_pos)); in "fn f => fn " ^ tuple_vars "x" n ^ " => " ^ tuple (map (fn a => (if cond a then "f x" else "x") ^ a) (indices n)) end))); end; (* outer syntax *) val _ = Theory.setup (ML_Antiquotation.value_embedded \<^binding>\keyword\ (Args.context -- Scan.lift (Parse.embedded_position || Parse.position (Parse.keyword_with (K true))) >> (fn (ctxt, (name, pos)) => if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name); "Parse.$$$ " ^ ML_Syntax.print_string name) else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #> ML_Antiquotation.value_embedded \<^binding>\command_keyword\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of SOME markup => (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)]; ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos)) | NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos))))); end; diff --git a/src/Pure/term.ML b/src/Pure/term.ML --- a/src/Pure/term.ML +++ b/src/Pure/term.ML @@ -1,1072 +1,1077 @@ (* Title: Pure/term.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Makarius Simply typed lambda-calculus: types, terms, and basic operations. *) infix 9 $; infixr 5 -->; infixr --->; infix aconv; signature BASIC_TERM = sig type indexname = string * int type class = string type sort = class list type arity = string * sort list * sort datatype typ = Type of string * typ list | TFree of string * sort | TVar of indexname * sort datatype term = Const of string * typ | Free of string * typ | Var of indexname * typ | Bound of int | Abs of string * typ * term | $ of term * term exception TYPE of string * typ list * term list exception TERM of string * term list val dummyS: sort val dummyT: typ val no_dummyT: typ -> typ val --> : typ * typ -> typ val ---> : typ list * typ -> typ val is_Type: typ -> bool val is_TFree: typ -> bool val is_TVar: typ -> bool val dest_Type: typ -> string * typ list val dest_TFree: typ -> string * sort val dest_TVar: typ -> indexname * sort val is_Bound: term -> bool val is_Const: term -> bool val is_Free: term -> bool val is_Var: term -> bool val dest_Const: term -> string * typ val dest_Free: term -> string * typ val dest_Var: term -> indexname * typ val dest_comb: term -> term * term val domain_type: typ -> typ val range_type: typ -> typ val dest_funT: typ -> typ * typ val binder_types: typ -> typ list val body_type: typ -> typ val strip_type: typ -> typ list * typ val type_of1: typ list * term -> typ val type_of: term -> typ val fastype_of1: typ list * term -> typ val fastype_of: term -> typ val strip_abs: term -> (string * typ) list * term val strip_abs_body: term -> term val strip_abs_vars: term -> (string * typ) list val strip_qnt_body: string -> term -> term val strip_qnt_vars: string -> term -> (string * typ) list val list_comb: term * term list -> term val strip_comb: term -> term * term list val head_of: term -> term val size_of_term: term -> int val size_of_typ: typ -> int val map_atyps: (typ -> typ) -> typ -> typ val map_aterms: (term -> term) -> term -> term val map_type_tvar: (indexname * sort -> typ) -> typ -> typ val map_type_tfree: (string * sort -> typ) -> typ -> typ val map_types: (typ -> typ) -> term -> term val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a val fold_atyps_sorts: (typ * sort -> 'a -> 'a) -> typ -> 'a -> 'a val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a val burrow_types: (typ list -> typ list) -> term list -> term list val aconv: term * term -> bool val propT: typ val strip_all_body: term -> term val strip_all_vars: term -> (string * typ) list val incr_bv: int * int * term -> term val incr_boundvars: int -> term -> term val add_loose_bnos: term * int * int list -> int list val loose_bnos: term -> int list val loose_bvar: term * int -> bool val loose_bvar1: term * int -> bool val subst_bounds: term list * term -> term val subst_bound: term * term -> term val betapply: term * term -> term val betapplys: term * term list -> term val subst_free: (term * term) list -> term -> term val abstract_over: term * term -> term val lambda: term -> term -> term val absfree: string * typ -> term -> term val absdummy: typ -> term -> term val subst_atomic: (term * term) list -> term -> term val typ_subst_atomic: (typ * typ) list -> typ -> typ val subst_atomic_types: (typ * typ) list -> term -> term val typ_subst_TVars: (indexname * typ) list -> typ -> typ val subst_TVars: (indexname * typ) list -> term -> term val subst_Vars: (indexname * term) list -> term -> term val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term val is_first_order: string list -> term -> bool val maxidx_of_typ: typ -> int val maxidx_of_typs: typ list -> int val maxidx_of_term: term -> int val fold_subtypes: (typ -> 'a -> 'a) -> typ -> 'a -> 'a val exists_subtype: (typ -> bool) -> typ -> bool val exists_type: (typ -> bool) -> term -> bool val exists_subterm: (term -> bool) -> term -> bool val exists_Const: (string * typ -> bool) -> term -> bool end; signature TERM = sig include BASIC_TERM val aT: sort -> typ val itselfT: typ -> typ val a_itselfT: typ val argument_type_of: term -> int -> typ val abs: string * typ -> term -> term + val args_of: term -> term list val add_tvar_namesT: typ -> indexname list -> indexname list val add_tvar_names: term -> indexname list -> indexname list val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list val add_var_names: term -> indexname list -> indexname list val add_vars: term -> (indexname * typ) list -> (indexname * typ) list val add_tfree_namesT: typ -> string list -> string list val add_tfree_names: term -> string list -> string list val add_tfreesT: typ -> (string * sort) list -> (string * sort) list val add_tfrees: term -> (string * sort) list -> (string * sort) list val add_free_names: term -> string list -> string list val add_frees: term -> (string * typ) list -> (string * typ) list val add_const_names: term -> string list -> string list val add_consts: term -> (string * typ) list -> (string * typ) list val hidden_polymorphism: term -> (indexname * sort) list val declare_typ_names: typ -> Name.context -> Name.context val declare_term_names: term -> Name.context -> Name.context val declare_term_frees: term -> Name.context -> Name.context val variant_frees: term -> (string * 'a) list -> (string * 'a) list val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list val eq_ix: indexname * indexname -> bool val eq_tvar: (indexname * sort) * (indexname * sort) -> bool val eq_var: (indexname * typ) * (indexname * typ) -> bool val aconv_untyped: term * term -> bool val could_unify: term * term -> bool val strip_abs_eta: int -> term -> (string * typ) list * term val match_bvars: (term * term) -> (string * string) list -> (string * string) list val map_abs_vars: (string -> string) -> term -> term val rename_abs: term -> term -> term -> term option val is_open: term -> bool val is_dependent: term -> bool val term_name: term -> string val dependent_lambda_name: string * term -> term -> term val lambda_name: string * term -> term -> term val close_schematic_term: term -> term val maxidx_typ: typ -> int -> int val maxidx_typs: typ list -> int -> int val maxidx_term: term -> int -> int val could_beta_contract: term -> bool val could_eta_contract: term -> bool val could_beta_eta_contract: term -> bool val used_free: string -> term -> bool exception USED_FREE of string * term val dest_abs_fresh: string -> term -> (string * typ) * term val dest_abs_global: term -> (string * typ) * term val dummy_pattern: typ -> term val dummy: term val dummy_prop: term val is_dummy_pattern: term -> bool val free_dummy_patterns: term -> Name.context -> term * Name.context val no_dummy_patterns: term -> term val replace_dummy_patterns: term -> int -> term * int val show_dummy_patterns: term -> term val string_of_vname: indexname -> string val string_of_vname': indexname -> string end; structure Term: TERM = struct (*Indexnames can be quickly renamed by adding an offset to the integer part, for resolution.*) type indexname = string * int; (*Types are classified by sorts.*) type class = string; type sort = class list; type arity = string * sort list * sort; (*The sorts attached to TFrees and TVars specify the sort of that variable.*) datatype typ = Type of string * typ list | TFree of string * sort | TVar of indexname * sort; (*Terms. Bound variables are indicated by depth number. Free variables, (scheme) variables and constants have names. An term is "closed" if every bound variable of level "lev" is enclosed by at least "lev" abstractions. It is possible to create meaningless terms containing loose bound vars or type mismatches. But such terms are not allowed in rules. *) datatype term = Const of string * typ | Free of string * typ | Var of indexname * typ | Bound of int | Abs of string*typ*term | op $ of term*term; (*Errors involving type mismatches*) exception TYPE of string * typ list * term list; (*Errors errors involving terms*) exception TERM of string * term list; (*Note variable naming conventions! a,b,c: string f,g,h: functions (including terms of function type) i,j,m,n: int t,u: term v,w: indexnames x,y: any A,B,C: term (denoting formulae) T,U: typ *) (** Types **) (*dummies for type-inference etc.*) val dummyS = [""]; val dummyT = Type ("dummy", []); fun no_dummyT typ = let fun check (T as Type ("dummy", _)) = raise TYPE ("Illegal occurrence of '_' dummy type", [T], []) | check (Type (_, Ts)) = List.app check Ts | check _ = (); in check typ; typ end; fun S --> T = Type("fun",[S,T]); (*handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)*) val op ---> = Library.foldr (op -->); (** Discriminators **) fun is_Type (Type _) = true | is_Type _ = false; fun is_TFree (TFree _) = true | is_TFree _ = false; fun is_TVar (TVar _) = true | is_TVar _ = false; (** Destructors **) fun dest_Type (Type x) = x | dest_Type T = raise TYPE ("dest_Type", [T], []); fun dest_TFree (TFree x) = x | dest_TFree T = raise TYPE ("dest_TFree", [T], []); fun dest_TVar (TVar x) = x | dest_TVar T = raise TYPE ("dest_TVar", [T], []); (** Discriminators **) fun is_Bound (Bound _) = true | is_Bound _ = false; fun is_Const (Const _) = true | is_Const _ = false; fun is_Free (Free _) = true | is_Free _ = false; fun is_Var (Var _) = true | is_Var _ = false; (** Destructors **) fun dest_Const (Const x) = x | dest_Const t = raise TERM("dest_Const", [t]); fun dest_Free (Free x) = x | dest_Free t = raise TERM("dest_Free", [t]); fun dest_Var (Var x) = x | dest_Var t = raise TERM("dest_Var", [t]); fun dest_comb (t1 $ t2) = (t1, t2) | dest_comb t = raise TERM("dest_comb", [t]); fun domain_type (Type ("fun", [T, _])) = T; fun range_type (Type ("fun", [_, U])) = U; fun dest_funT (Type ("fun", [T, U])) = (T, U) | dest_funT T = raise TYPE ("dest_funT", [T], []); (*maps [T1,...,Tn]--->T to the list [T1,T2,...,Tn]*) fun binder_types (Type ("fun", [T, U])) = T :: binder_types U | binder_types _ = []; (*maps [T1,...,Tn]--->T to T*) fun body_type (Type ("fun", [_, U])) = body_type U | body_type T = T; (*maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T)*) fun strip_type T = (binder_types T, body_type T); (*Compute the type of the term, checking that combinations are well-typed Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*) fun type_of1 (Ts, Const (_,T)) = T | type_of1 (Ts, Free (_,T)) = T | type_of1 (Ts, Bound i) = (nth Ts i handle General.Subscript => raise TYPE("type_of: bound variable", [], [Bound i])) | type_of1 (Ts, Var (_,T)) = T | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body) | type_of1 (Ts, f$u) = let val U = type_of1(Ts,u) and T = type_of1(Ts,f) in case T of Type("fun",[T1,T2]) => if T1=U then T2 else raise TYPE ("type_of: type mismatch in application", [T1,U], [f$u]) | _ => raise TYPE ("type_of: function type is expected in application", [T,U], [f$u]) end; fun type_of t : typ = type_of1 ([],t); (*Determine the type of a term, with minimal checking*) local fun fastype_of_term Ts (Abs (_, T, t)) = T --> fastype_of_term (T :: Ts) t | fastype_of_term Ts (t $ _) = range_type_of Ts t | fastype_of_term Ts a = fastype_of_atom Ts a and fastype_of_atom _ (Const (_, T)) = T | fastype_of_atom _ (Free (_, T)) = T | fastype_of_atom _ (Var (_, T)) = T | fastype_of_atom Ts (Bound i) = fastype_of_bound Ts i and fastype_of_bound (T :: Ts) i = if i = 0 then T else fastype_of_bound Ts (i - 1) | fastype_of_bound [] i = raise TERM ("fastype_of: Bound", [Bound i]) and range_type_of Ts (Abs (_, T, u)) = fastype_of_term (T :: Ts) u | range_type_of Ts (t $ u) = range_type_ofT (t $ u) (range_type_of Ts t) | range_type_of Ts a = range_type_ofT a (fastype_of_atom Ts a) and range_type_ofT _ (Type ("fun", [_, T])) = T | range_type_ofT t _ = raise TERM ("fastype_of: expected function type", [t]); in val fastype_of1 = uncurry fastype_of_term; val fastype_of = fastype_of_term []; end; (*Determine the argument type of a function*) fun argument_type_of tm k = let fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U | argT _ T = raise TYPE ("argument_type_of", [T], []); fun arg 0 _ (Abs (_, T, _)) = T | arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t | arg i Ts (t $ _) = arg (i + 1) Ts t | arg i Ts a = argT i (fastype_of1 (Ts, a)); in arg k [] tm end; fun abs (x, T) t = Abs (x, T, t); fun strip_abs (Abs (a, T, t)) = let val (a', t') = strip_abs t in ((a, T) :: a', t') end | strip_abs t = ([], t); (*maps (x1,...,xn)t to t*) fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t | strip_abs_body u = u; (*maps (x1,...,xn)t to [x1, ..., xn]*) fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t | strip_abs_vars u = [] : (string*typ) list; fun strip_qnt_body qnt = let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm | strip t = t in strip end; fun strip_qnt_vars qnt = let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else [] | strip t = [] : (string*typ) list in strip end; (*maps (f, [t1,...,tn]) to f(t1,...,tn)*) val list_comb : term * term list -> term = Library.foldl (op $); (*maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tail-recursive*) fun strip_comb u : term * term list = let fun stripc (f$t, ts) = stripc (f, t::ts) | stripc x = x in stripc(u,[]) end; +fun args_of u = + let fun args (f $ x) xs = args f (x :: xs) + | args _ xs = xs + in args u [] end; (*maps f(t1,...,tn) to f , which is never a combination*) fun head_of (f$t) = head_of f | head_of u = u; (*number of atoms and abstractions in a term*) fun size_of_term tm = let fun add_size (t $ u) n = add_size t (add_size u n) | add_size (Abs (_ ,_, t)) n = add_size t (n + 1) | add_size _ n = n + 1; in add_size tm 0 end; (*number of atoms and constructors in a type*) fun size_of_typ ty = let fun add_size (Type (_, tys)) n = fold add_size tys (n + 1) | add_size _ n = n + 1; in add_size ty 0 end; fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts) | map_atyps f T = f T; fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t) | map_aterms f t = f t; fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T); fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T); fun map_types f = let fun map_aux (Const (a, T)) = Const (a, f T) | map_aux (Free (a, T)) = Free (a, f T) | map_aux (Var (v, T)) = Var (v, f T) | map_aux (Bound i) = Bound i | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t) | map_aux (t $ u) = map_aux t $ map_aux u; in map_aux end; (* fold types and terms *) fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts | fold_atyps f T = f T; fun fold_atyps_sorts f = fold_atyps (fn T as TFree (_, S) => f (T, S) | T as TVar (_, S) => f (T, S)); fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u | fold_aterms f (Abs (_, _, t)) = fold_aterms f t | fold_aterms f a = f a; fun fold_term_types f (t as Const (_, T)) = f t T | fold_term_types f (t as Free (_, T)) = f t T | fold_term_types f (t as Var (_, T)) = f t T | fold_term_types f (Bound _) = I | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u; fun fold_types f = fold_term_types (K f); fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts) | replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts) | replace_types (Var (xi, _)) (T :: Ts) = (Var (xi, T), Ts) | replace_types (Bound i) Ts = (Bound i, Ts) | replace_types (Abs (x, _, b)) (T :: Ts) = let val (b', Ts') = replace_types b Ts in (Abs (x, T, b'), Ts') end | replace_types (t $ u) Ts = let val (t', Ts') = replace_types t Ts; val (u', Ts'') = replace_types u Ts'; in (t' $ u', Ts'') end; fun burrow_types f ts = let val Ts = rev ((fold o fold_types) cons ts []); val Ts' = f Ts; val (ts', []) = fold_map replace_types ts Ts'; in ts' end; (*collect variables*) val add_tvar_namesT = fold_atyps (fn TVar (xi, _) => insert (op =) xi | _ => I); val add_tvar_names = fold_types add_tvar_namesT; val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I); val add_tvars = fold_types add_tvarsT; val add_var_names = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I); val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I); val add_tfree_namesT = fold_atyps (fn TFree (a, _) => insert (op =) a | _ => I); val add_tfree_names = fold_types add_tfree_namesT; val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I); val add_tfrees = fold_types add_tfreesT; val add_free_names = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I); val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I); val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I); val add_consts = fold_aterms (fn Const c => insert (op =) c | _ => I); (*extra type variables in a term, not covered by its type*) fun hidden_polymorphism t = let val T = fastype_of t; val tvarsT = add_tvarsT T []; val extra_tvars = fold_types (fold_atyps (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t []; in extra_tvars end; (* renaming variables *) val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I); fun declare_term_names tm = fold_aterms (fn Const (a, _) => Name.declare (Long_Name.base_name a) | Free (a, _) => Name.declare a | _ => I) tm #> fold_types declare_typ_names tm; val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I); fun variant_frees t frees = fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees; fun rename_wrt_term t frees = rev (variant_frees t frees); (*reversed result!*) (** Comparing terms **) (* variables *) fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y; fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S'; fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T'; (* alpha equivalence *) fun tm1 aconv tm2 = pointer_eq (tm1, tm2) orelse (case (tm1, tm2) of (t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2 | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2 | (a1, a2) => a1 = a2); fun aconv_untyped (tm1, tm2) = pointer_eq (tm1, tm2) orelse (case (tm1, tm2) of (t1 $ u1, t2 $ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2) | (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2) | (Const (a, _), Const (b, _)) => a = b | (Free (x, _), Free (y, _)) => x = y | (Var (xi, _), Var (yj, _)) => xi = yj | (Bound i, Bound j) => i = j | _ => false); (*A fast unification filter: true unless the two terms cannot be unified. Terms must be NORMAL. Treats all Vars as distinct. *) fun could_unify (t, u) = let fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g | matchrands _ _ = true; in case (head_of t, head_of u) of (_, Var _) => true | (Var _, _) => true | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u | (Bound i, Bound j) => i = j andalso matchrands t u | (Abs _, _) => true (*because of possible eta equality*) | (_, Abs _) => true | _ => false end; (** Connectives of higher order logic **) fun aT S = TFree (Name.aT, S); fun itselfT ty = Type ("itself", [ty]); val a_itselfT = itselfT (TFree (Name.aT, [])); val propT : typ = Type ("prop",[]); (*maps \x1...xn. t to t*) fun strip_all_body (Const ("Pure.all", _) $ Abs (_, _, t)) = strip_all_body t | strip_all_body t = t; (*maps \x1...xn. t to [x1, ..., xn]*) fun strip_all_vars (Const ("Pure.all", _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t | strip_all_vars t = []; (*increments a term's non-local bound variables required when moving a term within abstractions inc is increment for bound variables lev is level at which a bound variable is considered 'loose'*) fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u | incr_bv (inc, lev, Abs(a,T,body)) = Abs(a, T, incr_bv(inc,lev+1,body)) | incr_bv (inc, lev, f$t) = incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) | incr_bv (inc, lev, u) = u; fun incr_boundvars 0 t = t | incr_boundvars inc t = incr_bv(inc,0,t); (*Scan a pair of terms; while they are similar, accumulate corresponding bound vars in "al"*) fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = match_bvs(s, t, if x="" orelse y="" then al else (x,y)::al) | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) | match_bvs(_,_,al) = al; (* strip abstractions created by parameters *) fun match_bvars (s,t) al = match_bvs(strip_abs_body s, strip_abs_body t, al); fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t) | map_abs_vars f t = t; fun rename_abs pat obj t = let val ren = match_bvs (pat, obj, []); fun ren_abs (Abs (x, T, b)) = Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b) | ren_abs (f $ t) = ren_abs f $ ren_abs t | ren_abs t = t in if null ren then NONE else SOME (ren_abs t) end; (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond. (Bound 0) is loose at level 0 *) fun add_loose_bnos (Bound i, lev, js) = if i= k | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k) | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1) | loose_bvar _ = false; fun loose_bvar1(Bound i,k) = i = k | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1) | loose_bvar1 _ = false; fun is_open t = loose_bvar (t, 0); fun is_dependent t = loose_bvar1 (t, 0); (*Substitute arguments for loose bound variables. Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi). Note that for ((\x y. c) a b), the bound vars in c are x=1 and y=0 and the appropriate call is subst_bounds([b,a], c) . Loose bound variables >=n are reduced by "n" to compensate for the disappearance of lambdas. *) fun subst_bounds (args: term list, t) : term = let val n = length args; fun subst (t as Bound i, lev) = (if i < lev then raise Same.SAME (*var is locally bound*) else incr_boundvars lev (nth args (i - lev)) handle General.Subscript => Bound (i - n)) (*loose: change it*) | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1)) | subst (f $ t, lev) = (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t) handle Same.SAME => f $ subst (t, lev)) | subst _ = raise Same.SAME; in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end; (*Special case: one argument*) fun subst_bound (arg, t) : term = let fun subst (Bound i, lev) = if i < lev then raise Same.SAME (*var is locally bound*) else if i = lev then incr_boundvars lev arg else Bound (i - 1) (*loose: change it*) | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1)) | subst (f $ t, lev) = (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t) handle Same.SAME => f $ subst (t, lev)) | subst _ = raise Same.SAME; in subst (t, 0) handle Same.SAME => t end; (*beta-reduce if possible, else form application*) fun betapply (Abs(_,_,t), u) = subst_bound (u,t) | betapply (f,u) = f$u; val betapplys = Library.foldl betapply; (*unfolding abstractions with substitution of bound variables and implicit eta-expansion*) fun strip_abs_eta k t = let val used = fold_aterms declare_term_frees t Name.context; fun strip_abs t (0, used) = (([], t), (0, used)) | strip_abs (Abs (v, T, t)) (k, used) = let val (v', used') = Name.variant v used; val t' = subst_bound (Free (v', T), t); val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used'); in (((v', T) :: vs, t''), (k', used'')) end | strip_abs t (k, used) = (([], t), (k, used)); fun expand_eta [] t _ = ([], t) | expand_eta (T::Ts) t used = let val (v, used') = Name.variant "" used; val (vs, t') = expand_eta Ts (t $ Free (v, T)) used'; in ((v, T) :: vs, t') end; val ((vs1, t'), (k', used')) = strip_abs t (k, used); val Ts = fst (chop k' (binder_types (fastype_of t'))); val (vs2, t'') = expand_eta Ts t' used'; in (vs1 @ vs2, t'') end; (*Substitute new for free occurrences of old in a term*) fun subst_free [] = I | subst_free pairs = let fun substf u = case AList.lookup (op aconv) pairs u of SOME u' => u' | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t) | t$u' => substf t $ substf u' | _ => u) in substf end; (*Abstraction of the term "body" over its occurrences of v, which must contain no loose bound variables. The resulting term is ready to become the body of an Abs.*) fun abstract_over (v, body) = let fun abs lev tm = if v aconv tm then Bound lev else (case tm of Abs (a, T, t) => Abs (a, T, abs (lev + 1) t) | t $ u => (abs lev t $ (abs lev u handle Same.SAME => u) handle Same.SAME => t $ abs lev u) | _ => raise Same.SAME); in abs 0 body handle Same.SAME => body end; fun term_name (Const (x, _)) = Long_Name.base_name x | term_name (Free (x, _)) = x | term_name (Var ((x, _), _)) = x | term_name _ = Name.uu; fun dependent_lambda_name (x, v) t = let val t' = abstract_over (v, t) in if is_dependent t' then Abs (if x = "" then term_name v else x, fastype_of v, t') else t end; fun lambda_name (x, v) t = Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t)); fun lambda v t = lambda_name ("", v) t; fun absfree (a, T) body = Abs (a, T, abstract_over (Free (a, T), body)); fun absdummy T body = Abs (Name.uu_, T, body); (*Replace the ATOMIC term ti by ui; inst = [(t1,u1), ..., (tn,un)]. A simultaneous substitution: [ (a,b), (b,a) ] swaps a and b. *) fun subst_atomic [] tm = tm | subst_atomic inst tm = let fun subst (Abs (a, T, body)) = Abs (a, T, subst body) | subst (t $ u) = subst t $ subst u | subst t = the_default t (AList.lookup (op aconv) inst t); in subst tm end; (*Replace the ATOMIC type Ti by Ui; inst = [(T1,U1), ..., (Tn,Un)].*) fun typ_subst_atomic [] ty = ty | typ_subst_atomic inst ty = let fun subst (Type (a, Ts)) = Type (a, map subst Ts) | subst T = the_default T (AList.lookup (op = : typ * typ -> bool) inst T); in subst ty end; fun subst_atomic_types [] tm = tm | subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm; fun typ_subst_TVars [] ty = ty | typ_subst_TVars inst ty = let fun subst (Type (a, Ts)) = Type (a, map subst Ts) | subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi) | subst T = T; in subst ty end; fun subst_TVars [] tm = tm | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm; fun subst_Vars [] tm = tm | subst_Vars inst tm = let fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi) | subst (Abs (a, T, t)) = Abs (a, T, subst t) | subst (t $ u) = subst t $ subst u | subst t = t; in subst tm end; fun subst_vars ([], []) tm = tm | subst_vars ([], inst) tm = subst_Vars inst tm | subst_vars (instT, inst) tm = let fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T) | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T) | subst (Var (xi, T)) = (case AList.lookup (op =) inst xi of NONE => Var (xi, typ_subst_TVars instT T) | SOME t => t) | subst (t as Bound _) = t | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t) | subst (t $ u) = subst t $ subst u; in subst tm end; fun close_schematic_term t = let val extra_types = map (fn v => Const ("Pure.type", itselfT (TVar v))) (hidden_polymorphism t); val extra_terms = map Var (add_vars t []); in fold lambda (extra_terms @ extra_types) t end; (** Identifying first-order terms **) (*Differs from proofterm/is_fun in its treatment of TVar*) fun is_funtype (Type ("fun", [_, _])) = true | is_funtype _ = false; (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*) fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts, t))); (*First order means in all terms of the form f(t1,...,tn) no argument has a function type. The supplied quantifiers are excluded: their argument always has a function type through a recursive call into its body.*) fun is_first_order quants = let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) = member (op =) quants q andalso (*it is a known quantifier*) not (is_funtype T) andalso first_order1 (T::Ts) body | first_order1 Ts t = case strip_comb t of (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts | (Abs _, ts) => false (*not in beta-normal form*) | _ => error "first_order: unexpected case" in first_order1 [] end; (* maximum index of typs and terms *) fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j) | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i | maxidx_typ (TFree _) i = i and maxidx_typs [] i = i | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i); fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j)) | maxidx_term (Const (_, T)) i = maxidx_typ T i | maxidx_term (Free (_, T)) i = maxidx_typ T i | maxidx_term (Bound _) i = i | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i) | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i); fun maxidx_of_typ T = maxidx_typ T ~1; fun maxidx_of_typs Ts = maxidx_typs Ts ~1; fun maxidx_of_term t = maxidx_term t ~1; (** misc syntax operations **) (* substructure *) fun fold_subtypes f = let fun iter ty = (case ty of Type (_, Ts) => f ty #> fold iter Ts | _ => f ty); in iter end; fun exists_subtype P = let fun ex ty = P ty orelse (case ty of Type (_, Ts) => exists ex Ts | _ => false); in ex end; fun exists_type P = let fun ex (Const (_, T)) = P T | ex (Free (_, T)) = P T | ex (Var (_, T)) = P T | ex (Bound _) = false | ex (Abs (_, T, t)) = P T orelse ex t | ex (t $ u) = ex t orelse ex u; in ex end; fun exists_subterm P = let fun ex tm = P tm orelse (case tm of t $ u => ex t orelse ex u | Abs (_, _, t) => ex t | _ => false); in ex end; fun exists_Const P = exists_subterm (fn Const c => P c | _ => false); (* contraction *) fun could_beta_contract (Abs _ $ _) = true | could_beta_contract (t $ u) = could_beta_contract t orelse could_beta_contract u | could_beta_contract (Abs (_, _, b)) = could_beta_contract b | could_beta_contract _ = false; fun could_eta_contract (Abs (_, _, _ $ Bound 0)) = true | could_eta_contract (Abs (_, _, b)) = could_eta_contract b | could_eta_contract (t $ u) = could_eta_contract t orelse could_eta_contract u | could_eta_contract _ = false; fun could_beta_eta_contract (Abs _ $ _) = true | could_beta_eta_contract (Abs (_, _, _ $ Bound 0)) = true | could_beta_eta_contract (Abs (_, _, b)) = could_beta_eta_contract b | could_beta_eta_contract (t $ u) = could_beta_eta_contract t orelse could_beta_eta_contract u | could_beta_eta_contract _ = false; (* dest abstraction *) (*ASSUMPTION: x is fresh wrt. the current context, but the check of used_free merely guards against gross mistakes*) fun used_free x = let fun used (Free (y, _)) = (x = y) | used (t $ u) = used t orelse used u | used (Abs (_, _, t)) = used t | used _ = false; in used end; exception USED_FREE of string * term; fun subst_abs v b = (v, subst_bound (Free v, b)); fun dest_abs_fresh x t = (case t of Abs (_, T, b) => if used_free x b then raise USED_FREE (x, t) else subst_abs (x, T) b | _ => raise TERM ("dest_abs", [t])); fun dest_abs_global t = (case t of Abs (x, T, b) => if used_free x b then let val used = Name.build_context (declare_term_frees b); val x' = #1 (Name.variant x used); in subst_abs (x', T) b end else subst_abs (x, T) b | _ => raise TERM ("dest_abs", [t])); (* dummy patterns *) fun dummy_pattern T = Const ("Pure.dummy_pattern", T); val dummy = dummy_pattern dummyT; val dummy_prop = dummy_pattern propT; fun is_dummy_pattern (Const ("Pure.dummy_pattern", _)) = true | is_dummy_pattern _ = false; fun no_dummy_patterns tm = if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]); fun free_dummy_patterns (Const ("Pure.dummy_pattern", T)) used = let val [x] = Name.invent used Name.uu 1 in (Free (Name.internal x, T), Name.declare x used) end | free_dummy_patterns (Abs (x, T, b)) used = let val (b', used') = free_dummy_patterns b used in (Abs (x, T, b'), used') end | free_dummy_patterns (t $ u) used = let val (t', used') = free_dummy_patterns t used; val (u', used'') = free_dummy_patterns u used'; in (t' $ u', used'') end | free_dummy_patterns a used = (a, used); fun replace_dummy Ts (Const ("Pure.dummy_pattern", T)) i = (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1) | replace_dummy Ts (Abs (x, T, t)) i = let val (t', i') = replace_dummy (T :: Ts) t i in (Abs (x, T, t'), i') end | replace_dummy Ts (t $ u) i = let val (t', i') = replace_dummy Ts t i; val (u', i'') = replace_dummy Ts u i'; in (t' $ u', i'') end | replace_dummy _ a i = (a, i); val replace_dummy_patterns = replace_dummy []; fun show_dummy_patterns (Var (("_dummy_", _), T)) = dummy_pattern T | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t) | show_dummy_patterns a = a; (* display variables *) fun string_of_vname (x, i) = let val idx = string_of_int i; val dot = (case rev (Symbol.explode x) of _ :: "\<^sub>" :: _ => false | c :: _ => Symbol.is_digit c | _ => true); in if dot then "?" ^ x ^ "." ^ idx else if i <> 0 then "?" ^ x ^ idx else "?" ^ x end; fun string_of_vname' (x, ~1) = x | string_of_vname' xi = string_of_vname xi; end; structure Basic_Term: BASIC_TERM = Term; open Basic_Term; diff --git a/src/Pure/term_subst.ML b/src/Pure/term_subst.ML --- a/src/Pure/term_subst.ML +++ b/src/Pure/term_subst.ML @@ -1,224 +1,282 @@ (* Title: Pure/term_subst.ML Author: Makarius Efficient type/term substitution. *) signature TERM_SUBST = sig val map_atypsT_same: typ Same.operation -> typ Same.operation val map_types_same: typ Same.operation -> term Same.operation val map_aterms_same: term Same.operation -> term Same.operation val generalizeT_same: Names.set -> int -> typ Same.operation val generalize_same: Names.set * Names.set -> int -> term Same.operation val generalizeT: Names.set -> int -> typ -> typ val generalize: Names.set * Names.set -> int -> term -> term val instantiateT_frees_same: typ TFrees.table -> typ Same.operation val instantiate_frees_same: typ TFrees.table * term Frees.table -> term Same.operation val instantiateT_frees: typ TFrees.table -> typ -> typ val instantiate_frees: typ TFrees.table * term Frees.table -> term -> term val instantiateT_maxidx: (typ * int) TVars.table -> typ -> int -> typ * int val instantiate_maxidx: (typ * int) TVars.table * (term * int) Vars.table -> term -> int -> term * int + val instantiate_beta_maxidx: (typ * int) TVars.table * (term * int) Vars.table -> + term -> int -> term * int val instantiateT_same: typ TVars.table -> typ Same.operation val instantiate_same: typ TVars.table * term Vars.table -> term Same.operation + val instantiate_beta_same: typ TVars.table * term Vars.table -> term Same.operation val instantiateT: typ TVars.table -> typ -> typ val instantiate: typ TVars.table * term Vars.table -> term -> term + val instantiate_beta: typ TVars.table * term Vars.table -> term -> term val zero_var_indexes_inst: Name.context -> term list -> typ TVars.table * term Vars.table val zero_var_indexes: term -> term val zero_var_indexes_list: term list -> term list end; structure Term_Subst: TERM_SUBST = struct (* generic mapping *) fun map_atypsT_same f = let fun typ (Type (a, Ts)) = Type (a, Same.map typ Ts) | typ T = f T; in typ end; fun map_types_same f = let fun term (Const (a, T)) = Const (a, f T) | term (Free (a, T)) = Free (a, f T) | term (Var (v, T)) = Var (v, f T) | term (Bound _) = raise Same.SAME | term (Abs (x, T, t)) = (Abs (x, f T, Same.commit term t) handle Same.SAME => Abs (x, T, term t)) | term (t $ u) = (term t $ Same.commit term u handle Same.SAME => t $ term u); in term end; fun map_aterms_same f = let fun term (Abs (x, T, t)) = Abs (x, T, term t) | term (t $ u) = (term t $ Same.commit term u handle Same.SAME => t $ term u) | term a = f a; in term end; (* generalization of fixed variables *) fun generalizeT_same tfrees idx ty = if Names.is_empty tfrees then raise Same.SAME else let fun gen (Type (a, Ts)) = Type (a, Same.map gen Ts) | gen (TFree (a, S)) = if Names.defined tfrees a then TVar ((a, idx), S) else raise Same.SAME | gen _ = raise Same.SAME; in gen ty end; fun generalize_same (tfrees, frees) idx tm = if Names.is_empty tfrees andalso Names.is_empty frees then raise Same.SAME else let val genT = generalizeT_same tfrees idx; fun gen (Free (x, T)) = if Names.defined frees x then Var (Name.clean_index (x, idx), Same.commit genT T) else Free (x, genT T) | gen (Var (xi, T)) = Var (xi, genT T) | gen (Const (c, T)) = Const (c, genT T) | gen (Bound _) = raise Same.SAME | gen (Abs (x, T, t)) = (Abs (x, genT T, Same.commit gen t) handle Same.SAME => Abs (x, T, gen t)) | gen (t $ u) = (gen t $ Same.commit gen u handle Same.SAME => t $ gen u); in gen tm end; fun generalizeT names i ty = Same.commit (generalizeT_same names i) ty; fun generalize names i tm = Same.commit (generalize_same names i) tm; (* instantiation of free variables (types before terms) *) fun instantiateT_frees_same instT ty = if TFrees.is_empty instT then raise Same.SAME else let fun subst (Type (a, Ts)) = Type (a, Same.map subst Ts) | subst (TFree v) = (case TFrees.lookup instT v of SOME T => T | NONE => raise Same.SAME) | subst _ = raise Same.SAME; in subst ty end; fun instantiate_frees_same (instT, inst) tm = if TFrees.is_empty instT andalso Frees.is_empty inst then raise Same.SAME else let val substT = instantiateT_frees_same instT; fun subst (Const (c, T)) = Const (c, substT T) | subst (Free (x, T)) = let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in (case Frees.lookup inst (x, T') of SOME t => t | NONE => if same then raise Same.SAME else Free (x, T')) end | subst (Var (xi, T)) = Var (xi, substT T) | subst (Bound _) = raise Same.SAME | subst (Abs (x, T, t)) = (Abs (x, substT T, Same.commit subst t) handle Same.SAME => Abs (x, T, subst t)) | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u); in subst tm end; fun instantiateT_frees instT ty = Same.commit (instantiateT_frees_same instT) ty; fun instantiate_frees inst tm = Same.commit (instantiate_frees_same inst) tm; (* instantiation of schematic variables (types before terms) -- recomputes maxidx *) local fun no_indexesT instT = TVars.map (fn _ => rpair ~1) instT; fun no_indexes inst = Vars.map (fn _ => rpair ~1) inst; fun instT_same maxidx instT ty = let fun maxify i = if i > ! maxidx then maxidx := i else (); fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts) | subst_typ (TVar ((a, i), S)) = (case TVars.lookup instT ((a, i), S) of SOME (T, j) => (maxify j; T) | NONE => (maxify i; raise Same.SAME)) | subst_typ _ = raise Same.SAME and subst_typs (T :: Ts) = (subst_typ T :: Same.commit subst_typs Ts handle Same.SAME => T :: subst_typs Ts) | subst_typs [] = raise Same.SAME; in subst_typ ty end; fun inst_same maxidx (instT, inst) tm = let fun maxify i = if i > ! maxidx then maxidx := i else (); val substT = instT_same maxidx instT; fun subst (Const (c, T)) = Const (c, substT T) | subst (Free (x, T)) = Free (x, substT T) | subst (Var ((x, i), T)) = let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in (case Vars.lookup inst ((x, i), T') of SOME (t, j) => (maxify j; t) | NONE => (maxify i; if same then raise Same.SAME else Var ((x, i), T'))) end | subst (Bound _) = raise Same.SAME | subst (Abs (x, T, t)) = - (Abs (x, substT T, Same.commit subst t) + (Abs (x, substT T, subst_commit t) handle Same.SAME => Abs (x, T, subst t)) - | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u); + | subst (t $ u) = (subst t $ subst_commit u handle Same.SAME => t $ subst u) + and subst_commit t = Same.commit subst t; + in subst tm end; + +(*version with local beta reduction*) +fun inst_beta_same maxidx (instT, inst) tm = + let + fun maxify i = if i > ! maxidx then maxidx := i else (); + + val substT = instT_same maxidx instT; + + fun expand_head t = + (case Term.head_of t of + Var ((x, i), T) => + let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in + (case Vars.lookup inst ((x, i), T') of + SOME (u, j) => (maxify j; SOME u) + | NONE => (maxify i; if same then NONE else SOME (Var ((x, i), T')))) + end + | _ => NONE); + + fun subst t = + (case expand_head t of + NONE => + (case t of + Const (c, T) => Const (c, substT T) + | Free (x, T) => Free (x, substT T) + | Var _ => raise Same.SAME + | Bound _ => raise Same.SAME + | Abs (x, T, b) => + (Abs (x, substT T, subst_commit b) + handle Same.SAME => Abs (x, T, subst b)) + | _ $ _ => subst_comb t) + | SOME (u as Abs _) => Term.betapplys (u, map subst_commit (Term.args_of t)) + | SOME u => subst_head u t) + and subst_comb (t $ u) = (subst_comb t $ subst_commit u handle Same.SAME => t $ subst u) + | subst_comb (Var _) = raise Same.SAME + | subst_comb t = subst t + and subst_head h (t $ u) = subst_head h t $ subst_commit u + | subst_head h _ = h + and subst_commit t = Same.commit subst t; + in subst tm end; in fun instantiateT_maxidx instT ty i = let val maxidx = Unsynchronized.ref i in (Same.commit (instT_same maxidx instT) ty, ! maxidx) end; fun instantiate_maxidx insts tm i = let val maxidx = Unsynchronized.ref i in (Same.commit (inst_same maxidx insts) tm, ! maxidx) end; +fun instantiate_beta_maxidx insts tm i = + let val maxidx = Unsynchronized.ref i + in (Same.commit (inst_beta_same maxidx insts) tm, ! maxidx) end; + + fun instantiateT_same instT ty = if TVars.is_empty instT then raise Same.SAME else instT_same (Unsynchronized.ref ~1) (no_indexesT instT) ty; fun instantiate_same (instT, inst) tm = if TVars.is_empty instT andalso Vars.is_empty inst then raise Same.SAME else inst_same (Unsynchronized.ref ~1) (no_indexesT instT, no_indexes inst) tm; +fun instantiate_beta_same (instT, inst) tm = + if TVars.is_empty instT andalso Vars.is_empty inst then raise Same.SAME + else inst_beta_same (Unsynchronized.ref ~1) (no_indexesT instT, no_indexes inst) tm; + + fun instantiateT instT ty = Same.commit (instantiateT_same instT) ty; + fun instantiate inst tm = Same.commit (instantiate_same inst) tm; +fun instantiate_beta inst tm = Same.commit (instantiate_beta_same inst) tm; + end; (* zero var indexes *) fun zero_var_inst ins mk (v as ((x, i), X)) (inst, used) = let val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used in if x = x' andalso i = 0 then (inst, used') else (ins (v, mk ((x', 0), X)) inst, used') end; fun zero_var_indexes_inst used ts = let val (instT, _) = (TVars.empty, used) |> TVars.fold (zero_var_inst TVars.add TVar o #1) (TVars.build (ts |> (fold o fold_types o fold_atyps) (fn TVar v => TVars.add (v, ()) | _ => I))); val (inst, _) = (Vars.empty, used) |> Vars.fold (zero_var_inst Vars.add Var o #1) (Vars.build (ts |> (fold o fold_aterms) (fn Var (xi, T) => Vars.add ((xi, instantiateT instT T), ()) | _ => I))); in (instT, inst) end; fun zero_var_indexes_list ts = map (instantiate (zero_var_indexes_inst Name.context ts)) ts; val zero_var_indexes = singleton zero_var_indexes_list; end; diff --git a/src/Pure/thm.ML b/src/Pure/thm.ML --- a/src/Pure/thm.ML +++ b/src/Pure/thm.ML @@ -1,2398 +1,2406 @@ (* 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 fast_term_ord: cterm ord val term_ord: cterm ord 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_fresh: string -> cterm -> cterm * cterm val dest_abs_global: 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 -> ctyp TVars.table * cterm Vars.table val first_order_match: cterm * cterm -> ctyp TVars.table * cterm Vars.table (*theorems*) val fold_terms: {hyps: bool} -> (term -> 'a -> 'a) -> thm -> 'a -> 'a val fold_atomic_ctyps: {hyps: bool} -> (typ -> bool) -> (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a val fold_atomic_cterms: {hyps: bool} -> (term -> bool) -> (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 val thm_ord: thm ord 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: Names.set * Names.set -> int -> thm -> thm val generalize_cterm: Names.set * Names.set -> int -> cterm -> cterm val generalize_ctyp: Names.set -> int -> ctyp -> ctyp val instantiate: ctyp TVars.table * cterm Vars.table -> thm -> thm + val instantiate_beta: ctyp TVars.table * cterm Vars.table -> thm -> thm val instantiate_cterm: ctyp TVars.table * cterm Vars.table -> cterm -> cterm + val instantiate_beta_cterm: ctyp TVars.table * cterm Vars.table -> cterm -> cterm val trivial: cterm -> thm val of_class: ctyp * class -> thm val unconstrainT: thm -> thm val varifyT_global': 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']); val fast_term_ord = Term_Ord.fast_term_ord o apply2 term_of; val term_ord = Term_Ord.term_ord o apply2 term_of; (* 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 gen_dest_abs dest ct = (case ct of Cterm {t = t as Abs _, T = Type ("fun", [_, U]), cert, maxidx, sorts} => let val ((x', T), t') = dest t; val v = Cterm {t = Free (x', T), T = T, cert = cert, maxidx = maxidx, sorts = sorts}; val body = Cterm {t = t', T = U, cert = cert, maxidx = maxidx, sorts = sorts}; in (v, body) end | _ => raise CTERM ("dest_abs", [ct])); val dest_abs_fresh = gen_dest_abs o Term.dest_abs_fresh; val dest_abs_global = gen_dest_abs Term.dest_abs_global; (* 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 h f (Thm (_, {tpairs, prop, hyps, ...})) = fold (fn (t, u) => f t #> f u) tpairs #> f prop #> #hyps h ? fold f hyps; fun fold_atomic_ctyps h g f (th as Thm (_, {cert, maxidx, shyps, ...})) = let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps} in (fold_terms h o fold_types o fold_atyps) (fn T => if g T then f (ctyp T) else I) th end; fun fold_atomic_cterms h g f (th as Thm (_, {cert, maxidx, shyps, ...})) = let fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps}; fun apply t T = if g t then f (cterm t T) else I; in (fold_terms h o fold_aterms) (fn t as Const (_, T) => apply t T | t as Free (_, T) => apply t T | t as Var (_, T) => apply 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; val no_prems = Logic.no_prems o prop_of; 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; (* thm order: ignores theory context! *) val thm_ord = Term_Ord.fast_term_ord o apply2 prop_of ||| list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 tpairs_of ||| list_ord Term_Ord.fast_term_ord o apply2 hyps_of ||| list_ord Term_Ord.sort_ord o apply2 shyps_of; (* 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 (TVars.build (Vartab.fold (TVars.add o mk_cTinst) Tinsts), Vars.build (Vartab.fold (Vars.add 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); 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 {hyps = true} 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 {hyps = true} 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 Names.is_empty tfrees andalso Names.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 Names.is_empty tfrees then K false else Term.exists_subtype (fn TFree (a, _) => Names.defined tfrees a | _ => false); fun bad_term (Free (x, T)) = bad_type T orelse Names.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 Names.is_empty tfrees andalso Names.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 Names.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 make_instT thy (v as (_, S)) (Ctyp {T = U, maxidx, ...}) = if Sign.of_sort thy (U, S) then (U, maxidx) else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy S, [U], []); fun make_inst thy (v as (_, T)) (Cterm {t = u, T = U, maxidx, ...}) = if T = U then (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 |> TVars.fold add_instT_cert instT |> Vars.fold add_inst_cert inst; val thy' = Context.certificate_theory cert' handle ERROR msg => raise CONTEXT (msg, TVars.dest instT |> map #2, Vars.dest inst |> map #2, [], NONE); val sorts' = sorts |> TVars.fold add_instT_sorts instT |> Vars.fold add_inst_sorts inst; val instT' = TVars.map (make_instT thy') instT; val inst' = Vars.map (make_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 (instT, inst) th = +fun gen_instantiate inst_fn (instT, inst) th = if TVars.is_empty instT andalso Vars.is_empty inst then th else 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 subst = inst_fn (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' = TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S)) instT' constraints; in Thm (deriv_rule1 (fn d => Proofterm.instantiate (TVars.map (K #1) instT', 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 (instT, inst) ct = +val instantiate = gen_instantiate Term_Subst.instantiate_maxidx; +val instantiate_beta = gen_instantiate Term_Subst.instantiate_beta_maxidx; + +fun gen_instantiate_cterm inst_fn (instT, inst) ct = if TVars.is_empty instT andalso Vars.is_empty inst then ct else 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 subst = inst_fn (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]); +val instantiate_cterm = gen_instantiate_cterm Term_Subst.instantiate_maxidx; +val instantiate_beta_cterm = gen_instantiate_cterm Term_Subst.instantiate_beta_maxidx; + 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 = build_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 TFrees.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' 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 = build_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 (TVars.make tinst, Vars.empty) 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) = build (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;