101 val no_base_names: Proof.context -> Proof.context |
101 val no_base_names: Proof.context -> Proof.context |
102 val qualified_names: Proof.context -> Proof.context |
102 val qualified_names: Proof.context -> Proof.context |
103 val sticky_prefix: string -> Proof.context -> Proof.context |
103 val sticky_prefix: string -> Proof.context -> Proof.context |
104 val restore_naming: Proof.context -> Proof.context -> Proof.context |
104 val restore_naming: Proof.context -> Proof.context -> Proof.context |
105 val reset_naming: Proof.context -> Proof.context |
105 val reset_naming: Proof.context -> Proof.context |
106 val note_thmss: string -> |
106 val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list -> |
107 ((binding * attribute list) * (Facts.ref * attribute list) list) list -> |
107 Proof.context -> (string * thm list) list * Proof.context |
108 Proof.context -> (string * thm list) list * Proof.context |
108 val note_thmss_i: string -> (Thm.binding * (thm list * attribute list) list) list -> |
109 val note_thmss_i: string -> |
109 Proof.context -> (string * thm list) list * Proof.context |
110 ((binding * attribute list) * (thm list * attribute list) list) list -> |
|
111 Proof.context -> (string * thm list) list * Proof.context |
|
112 val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context |
110 val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context |
113 val read_vars: (binding * string option * mixfix) list -> Proof.context -> |
111 val read_vars: (binding * string option * mixfix) list -> Proof.context -> |
114 (binding * typ option * mixfix) list * Proof.context |
112 (binding * typ option * mixfix) list * Proof.context |
115 val cert_vars: (binding * typ option * mixfix) list -> Proof.context -> |
113 val cert_vars: (binding * typ option * mixfix) list -> Proof.context -> |
116 (binding * typ option * mixfix) list * Proof.context |
114 (binding * typ option * mixfix) list * Proof.context |
119 val add_fixes_i: (binding * typ option * mixfix) list -> |
117 val add_fixes_i: (binding * typ option * mixfix) list -> |
120 Proof.context -> string list * Proof.context |
118 Proof.context -> string list * Proof.context |
121 val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a) |
119 val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a) |
122 val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context |
120 val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context |
123 val add_assms: Assumption.export -> |
121 val add_assms: Assumption.export -> |
124 ((binding * attribute list) * (string * string list) list) list -> |
122 (Thm.binding * (string * string list) list) list -> |
125 Proof.context -> (string * thm list) list * Proof.context |
123 Proof.context -> (string * thm list) list * Proof.context |
126 val add_assms_i: Assumption.export -> |
124 val add_assms_i: Assumption.export -> |
127 ((binding * attribute list) * (term * term list) list) list -> |
125 (Thm.binding * (term * term list) list) list -> |
128 Proof.context -> (string * thm list) list * Proof.context |
126 Proof.context -> (string * thm list) list * Proof.context |
129 val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context |
127 val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context |
130 val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context |
128 val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context |
131 val get_case: Proof.context -> string -> string option list -> RuleCases.T |
129 val get_case: Proof.context -> string -> string option list -> RuleCases.T |
132 val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context |
130 val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context |
973 val name = full_name ctxt b; |
971 val name = full_name ctxt b; |
974 val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos; |
972 val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos; |
975 |
973 |
976 val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts); |
974 val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts); |
977 fun app (th, attrs) x = |
975 fun app (th, attrs) x = |
978 swap (foldl_map (Thm.proof_attributes (surround (Thm.kind k) (attrs @ more_attrs))) (x, th)); |
976 swap (Library.foldl_map (Thm.proof_attributes (surround (Thm.kind k) (attrs @ more_attrs))) (x, th)); |
979 val (res, ctxt') = fold_map app facts ctxt; |
977 val (res, ctxt') = fold_map app facts ctxt; |
980 val thms = PureThy.name_thms false false pos name (flat res); |
978 val thms = PureThy.name_thms false false pos name (flat res); |
981 val Mode {stmt, ...} = get_mode ctxt; |
979 val Mode {stmt, ...} = get_mode ctxt; |
982 in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end); |
980 in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end); |
983 |
981 |
1008 local |
1006 local |
1009 |
1007 |
1010 fun prep_vars prep_typ internal = |
1008 fun prep_vars prep_typ internal = |
1011 fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt => |
1009 fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt => |
1012 let |
1010 let |
1013 val raw_x = Binding.base_name raw_b; |
1011 val raw_x = Binding.name_of raw_b; |
1014 val (x, mx) = Syntax.const_mixfix raw_x raw_mx; |
1012 val (x, mx) = Syntax.const_mixfix raw_x raw_mx; |
1015 val _ = Syntax.is_identifier (no_skolem internal x) orelse |
1013 val _ = Syntax.is_identifier (no_skolem internal x) orelse |
1016 error ("Illegal variable name: " ^ quote x); |
1014 error ("Illegal variable name: " ^ quote x); |
1017 |
1015 |
1018 fun cond_tvars T = |
1016 fun cond_tvars T = |
1019 if internal then T |
1017 if internal then T |
1020 else Type.no_tvars T handle TYPE (msg, _, _) => error msg; |
1018 else Type.no_tvars T handle TYPE (msg, _, _) => error msg; |
1021 val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T; |
1019 val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T; |
1022 val var = (Binding.map_base (K x) raw_b, opt_T, mx); |
1020 val var = (Binding.map_name (K x) raw_b, opt_T, mx); |
1023 in (var, ctxt |> declare_var (x, opt_T, mx) |> #2) end); |
1021 in (var, ctxt |> declare_var (x, opt_T, mx) |> #2) end); |
1024 |
1022 |
1025 in |
1023 in |
1026 |
1024 |
1027 val read_vars = prep_vars Syntax.parse_typ false; |
1025 val read_vars = prep_vars Syntax.parse_typ false; |
1091 in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end; |
1089 in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end; |
1092 |
1090 |
1093 fun add_abbrev mode tags (b, raw_t) ctxt = |
1091 fun add_abbrev mode tags (b, raw_t) ctxt = |
1094 let |
1092 let |
1095 val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t |
1093 val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t |
1096 handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b)); |
1094 handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b)); |
1097 val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0]; |
1095 val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0]; |
1098 val ((lhs, rhs), consts') = consts_of ctxt |
1096 val ((lhs, rhs), consts') = consts_of ctxt |
1099 |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t); |
1097 |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t); |
1100 in |
1098 in |
1101 ctxt |
1099 ctxt |
1118 else (true, (x, T, mx)); |
1116 else (true, (x, T, mx)); |
1119 |
1117 |
1120 fun gen_fixes prep raw_vars ctxt = |
1118 fun gen_fixes prep raw_vars ctxt = |
1121 let |
1119 let |
1122 val (vars, _) = prep raw_vars ctxt; |
1120 val (vars, _) = prep raw_vars ctxt; |
1123 val (xs', ctxt') = Variable.add_fixes (map (Binding.base_name o #1) vars) ctxt; |
1121 val (xs', ctxt') = Variable.add_fixes (map (Binding.name_of o #1) vars) ctxt; |
1124 val ctxt'' = |
1122 val ctxt'' = |
1125 ctxt' |
1123 ctxt' |
1126 |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars) |
1124 |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars) |
1127 |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix); |
1125 |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix); |
1128 val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') => |
1126 val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') => |