# HG changeset patch # User wenzelm # Date 1635281900 -7200 # Node ID ea5d28c7f5e57ecf3f368e3179c8f8c6938f7f17 # Parent 3c587b7c3d5cc693018dddc88096fdca5591079f# Parent 55d4f8e1877f2301a9416a6922a1ee6474431c36 merged diff -r 3c587b7c3d5c -r ea5d28c7f5e5 src/HOL/Statespace/StateSpaceEx.thy --- a/src/HOL/Statespace/StateSpaceEx.thy Tue Oct 26 14:43:59 2021 +0000 +++ b/src/HOL/Statespace/StateSpaceEx.thy Tue Oct 26 22:58:20 2021 +0200 @@ -222,7 +222,7 @@ text \Sharing of names in side-by-side statespaces is also possible as long as they are mapped -to the same type.}\ +to the same type.\ statespace vars1 = n::nat m::nat statespace vars2 = n::nat k::nat diff -r 3c587b7c3d5c -r ea5d28c7f5e5 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Tue Oct 26 14:43:59 2021 +0000 +++ b/src/HOL/Tools/record.ML Tue Oct 26 22:58:20 2021 +0200 @@ -2117,16 +2117,17 @@ (* 3rd stage: thms_thy *) val record_ss = get_simpset defs_thy; - fun sel_upd_ctxt ctxt' = - put_simpset record_ss ctxt' - addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms); + val sel_upd_ss = + simpset_of + (put_simpset record_ss defs_ctxt + addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms)); val (sel_convs, upd_convs) = timeit_msg defs_ctxt "record sel_convs/upd_convs proof:" (fn () => grouped 10 Par_List.map (fn prop => Goal.prove_sorry_global defs_thy [] [] prop (fn {context = ctxt', ...} => - ALLGOALS (asm_full_simp_tac (sel_upd_ctxt ctxt')))) + ALLGOALS (asm_full_simp_tac (put_simpset sel_upd_ss ctxt')))) (sel_conv_props @ upd_conv_props)) |> chop (length sel_conv_props); diff -r 3c587b7c3d5c -r ea5d28c7f5e5 src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML Tue Oct 26 14:43:59 2021 +0000 +++ b/src/Pure/ML/ml_antiquotations.ML Tue Oct 26 22:58:20 2021 +0200 @@ -8,14 +8,6 @@ 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: Position.T -> cinsts -> ctyp -> ctyp - val instantiate_term: insts -> term -> term - val instantiate_cterm: Position.T -> cinsts -> cterm -> cterm end; structure ML_Antiquotations: ML_ANTIQUOTATIONS = @@ -227,179 +219,6 @@ (Scan.succeed "ML_Antiquotations.dest_judgment ML_context")); -(* type/term instantiations *) - -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 pos (cinsts: cinsts) cT = - Thm.instantiate_ctyp (TVars.make (#1 cinsts)) cT - handle CTERM (msg, args) => Exn.reraise (CTERM (msg ^ Position.here pos, args)); - -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_beta (instT, inst) end; - -fun instantiate_cterm pos (cinsts: cinsts) ct = - 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_beta_cterm (cinstT, cinst) ct end - handle CTERM (msg, args) => Exn.reraise (CTERM (msg ^ Position.here pos, args)); - - -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 missing_instT envT instT = - (case filter_out (fn (a, _) => exists (fn (b, _) => a = b) instT) envT of - [] => () - | bad => error ("No instantiation for free type variable(s) " ^ commas_quote (map #1 bad))); - -fun missing_inst env inst = - (case filter_out (fn (a, _) => exists (fn (b, _) => a = b) inst) env of - [] => () - | bad => error ("No instantiation for free variable(s) " ^ commas_quote (map #1 bad))); - -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 term_env t = (Term.add_tfrees t [], Term.add_frees t []); - -fun prepare_insts ctxt1 ctxt0 (instT, inst) t = - let - val (envT, env) = term_env 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 (envT', env') = term_env t'; - val _ = missing_instT (subtract (eq_fst op =) envT' envT) instT; - val _ = missing_inst (subtract (eq_fst op =) env' env) inst; - - 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; - -val ml_here = ML_Syntax.atomic o ML_Syntax.print_position; - -fun typ_ml (kind, _: Position.T) = (kind, "", "ML_Antiquotations.instantiate_typ "); -fun term_ml (kind, _: Position.T) = (kind, "", "ML_Antiquotations.instantiate_term "); -fun ctyp_ml (kind, pos) = - (kind, "ML_Antiquotations.make_ctyp ML_context", - "ML_Antiquotations.instantiate_ctyp " ^ ml_here pos); -fun cterm_ml (kind, pos) = - (kind, "ML_Antiquotations.make_cterm ML_context", - "ML_Antiquotations.instantiate_cterm " ^ ml_here pos); - -val command_name = Parse.position o Parse.command_name; - -fun parse_body range = - (command_name "typ" >> typ_ml || command_name "ctyp" >> ctyp_ml) -- - Parse.!!! Parse.typ >> prepare_type range || - (command_name "term" >> term_ml || command_name "cterm" >> cterm_ml) - -- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_term range || - (command_name "prop" >> term_ml || 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; - - (* type/term constructors *) local diff -r 3c587b7c3d5c -r ea5d28c7f5e5 src/Pure/ML/ml_instantiate.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_instantiate.ML Tue Oct 26 22:58:20 2021 +0200 @@ -0,0 +1,194 @@ +(* Title: Pure/ML/ml_instantiate.ML + Author: Makarius + +ML antiquotation to instantiate logical entities. +*) + +signature ML_INSTANTIATE = +sig + 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: Position.T -> cinsts -> ctyp -> ctyp + val instantiate_term: insts -> term -> term + val instantiate_cterm: Position.T -> cinsts -> cterm -> cterm +end; + +structure ML_Instantiate: ML_INSTANTIATE = +struct + +(* exported operations *) + +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 pos (cinsts: cinsts) cT = + Thm.instantiate_ctyp (TVars.make (#1 cinsts)) cT + handle CTERM (msg, args) => Exn.reraise (CTERM (msg ^ Position.here pos, args)); + +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_beta (instT, inst) end; + +fun instantiate_cterm pos (cinsts: cinsts) ct = + 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_beta_cterm (cinstT, cinst) ct end + handle CTERM (msg, args) => Exn.reraise (CTERM (msg ^ Position.here pos, args)); + + +(* ML antiquotation *) + +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 missing_instT envT instT = + (case filter_out (fn (a, _) => exists (fn (b, _) => a = b) instT) envT of + [] => () + | bad => error ("No instantiation for free type variable(s) " ^ commas_quote (map #1 bad))); + +fun missing_inst env inst = + (case filter_out (fn (a, _) => exists (fn (b, _) => a = b) inst) env of + [] => () + | bad => error ("No instantiation for free variable(s) " ^ commas_quote (map #1 bad))); + +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 term_env t = (Term.add_tfrees t [], Term.add_frees t []); + +fun prepare_insts ctxt1 ctxt0 (instT, inst) t = + let + val (envT, env) = term_env 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 (envT', env') = term_env t'; + val _ = missing_instT (subtract (eq_fst op =) envT' envT) instT; + val _ = missing_inst (subtract (eq_fst op =) env' env) inst; + + 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; + +val ml_here = ML_Syntax.atomic o ML_Syntax.print_position; + +fun typ_ml (kind, _: Position.T) = (kind, "", "ML_Instantiate.instantiate_typ "); +fun term_ml (kind, _: Position.T) = (kind, "", "ML_Instantiate.instantiate_term "); +fun ctyp_ml (kind, pos) = + (kind, "ML_Instantiate.make_ctyp ML_context", "ML_Instantiate.instantiate_ctyp " ^ ml_here pos); +fun cterm_ml (kind, pos) = + (kind, "ML_Instantiate.make_cterm ML_context", "ML_Instantiate.instantiate_cterm " ^ ml_here pos); + +val command_name = Parse.position o Parse.command_name; + +fun parse_body range = + (command_name "typ" >> typ_ml || command_name "ctyp" >> ctyp_ml) -- + Parse.!!! Parse.typ >> prepare_type range || + (command_name "term" >> term_ml || command_name "cterm" >> cterm_ml) + -- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_term range || + (command_name "prop" >> term_ml || 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; + +end; diff -r 3c587b7c3d5c -r ea5d28c7f5e5 src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Tue Oct 26 14:43:59 2021 +0000 +++ b/src/Pure/ML/ml_thms.ML Tue Oct 26 22:58:20 2021 +0200 @@ -102,7 +102,7 @@ val thms = Proof_Context.get_fact ctxt' (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN))); - in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end)); + in thm_binding "lemma" (length thms = 1) thms ctxt end)); (* old-style theorem bindings *) diff -r 3c587b7c3d5c -r ea5d28c7f5e5 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Oct 26 14:43:59 2021 +0000 +++ b/src/Pure/ROOT.ML Tue Oct 26 22:58:20 2021 +0200 @@ -339,6 +339,7 @@ ML_file "ML/ml_pp.ML"; ML_file "ML/ml_thms.ML"; +ML_file "ML/ml_instantiate.ML"; ML_file "ML/ml_file.ML"; ML_file "Tools/build.ML";