61 (term * term list) list list |
61 (term * term list) list list |
62 val cert_context_statement: string option -> Element.context_i element list -> |
62 val cert_context_statement: string option -> Element.context_i element list -> |
63 (term * term list) list list -> Proof.context -> |
63 (term * term list) list list -> Proof.context -> |
64 string option * (cterm list * Proof.context) * (cterm list * Proof.context) * |
64 string option * (cterm list * Proof.context) * (cterm list * Proof.context) * |
65 (term * term list) list list |
65 (term * term list) list list |
|
66 val read_expr: expr -> Element.context list -> Proof.context -> |
|
67 Element.context_i list * Proof.context |
|
68 val cert_expr: expr -> Element.context_i list -> Proof.context -> |
|
69 Element.context_i list * Proof.context |
66 |
70 |
67 (* Diagnostic functions *) |
71 (* Diagnostic functions *) |
68 val print_locales: theory -> unit |
72 val print_locales: theory -> unit |
69 val print_locale: theory -> bool -> expr -> Element.context list -> unit |
73 val print_locale: theory -> bool -> expr -> Element.context list -> unit |
70 val print_global_registrations: bool -> string -> theory -> unit |
74 val print_global_registrations: bool -> string -> theory -> unit |
132 Elem of 'a | Expr of expr; |
137 Elem of 'a | Expr of expr; |
133 |
138 |
134 fun map_elem f (Elem e) = Elem (f e) |
139 fun map_elem f (Elem e) = Elem (f e) |
135 | map_elem _ (Expr e) = Expr e; |
140 | map_elem _ (Expr e) = Expr e; |
136 |
141 |
137 type witness = term * thm; (*hypothesis as fact*) |
|
138 type locale = |
142 type locale = |
139 {predicate: cterm list * witness list, |
143 {predicate: cterm list * Element.witness list, |
140 (* CB: For locales with "(open)" this entry is ([], []). |
144 (* CB: For locales with "(open)" this entry is ([], []). |
141 For new-style locales, which declare predicates, if the locale declares |
145 For new-style locales, which declare predicates, if the locale declares |
142 no predicates, this is also ([], []). |
146 no predicates, this is also ([], []). |
143 If the locale declares predicates, the record field is |
147 If the locale declares predicates, the record field is |
144 ([statement], axioms), where statement is the locale predicate applied |
148 ([statement], axioms), where statement is the locale predicate applied |
149 import: expr, (*dynamic import*) |
153 import: expr, (*dynamic import*) |
150 elems: (Element.context_i * stamp) list, (*static content*) |
154 elems: (Element.context_i * stamp) list, (*static content*) |
151 params: ((string * typ) * mixfix) list, (*all params*) |
155 params: ((string * typ) * mixfix) list, (*all params*) |
152 lparams: string list, (*local parmas*) |
156 lparams: string list, (*local parmas*) |
153 term_syntax: ((Proof.context -> Proof.context) * stamp) list, (* FIXME depend on morphism *) |
157 term_syntax: ((Proof.context -> Proof.context) * stamp) list, (* FIXME depend on morphism *) |
154 regs: ((string * string list) * (term * thm) list) list} |
158 regs: ((string * string list) * Element.witness list) list} |
155 (* Registrations: indentifiers and witness theorems of locales interpreted |
159 (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *) |
156 in the locale. |
|
157 *) |
|
158 |
160 |
159 |
161 |
160 (* CB: an internal (Int) locale element was either imported or included, |
162 (* CB: an internal (Int) locale element was either imported or included, |
161 an external (Ext) element appears directly in the locale text. *) |
163 an external (Ext) element appears directly in the locale text. *) |
162 |
164 |
169 structure Registrations : |
171 structure Registrations : |
170 sig |
172 sig |
171 type T |
173 type T |
172 val empty: T |
174 val empty: T |
173 val join: T * T -> T |
175 val join: T * T -> T |
174 val dest: T -> (term list * ((string * Attrib.src list) * witness list)) list |
176 val dest: T -> (term list * ((string * Attrib.src list) * Element.witness list)) list |
175 val lookup: theory -> T * term list -> |
177 val lookup: theory -> T * term list -> |
176 ((string * Attrib.src list) * witness list) option |
178 ((string * Attrib.src list) * Element.witness list) option |
177 val insert: theory -> term list * (string * Attrib.src list) -> T -> |
179 val insert: theory -> term list * (string * Attrib.src list) -> T -> |
178 T * (term list * ((string * Attrib.src list) * witness list)) list |
180 T * (term list * ((string * Attrib.src list) * Element.witness list)) list |
179 val add_witness: term list -> witness -> T -> T |
181 val add_witness: term list -> Element.witness -> T -> T |
180 end = |
182 end = |
181 struct |
183 struct |
182 (* a registration consists of theorems instantiating locale assumptions |
184 (* a registration consists of theorems instantiating locale assumptions |
183 and prefix and attributes, indexed by parameter instantiation *) |
185 and prefix and attributes, indexed by parameter instantiation *) |
184 type T = ((string * Attrib.src list) * witness list) Termtab.table; |
186 type T = ((string * Attrib.src list) * Element.witness list) Termtab.table; |
185 |
187 |
186 val empty = Termtab.empty; |
188 val empty = Termtab.empty; |
187 |
189 |
188 (* term list represented as single term, for simultaneous matching *) |
190 (* term list represented as single term, for simultaneous matching *) |
189 fun termify ts = |
191 fun termify ts = |
202 (* registrations that subsume t *) |
204 (* registrations that subsume t *) |
203 fun subsumers thy t regs = |
205 fun subsumers thy t regs = |
204 filter (fn (t', _) => Pattern.matches thy (t', t)) (Termtab.dest regs); |
206 filter (fn (t', _) => Pattern.matches thy (t', t)) (Termtab.dest regs); |
205 |
207 |
206 (* look up registration, pick one that subsumes the query *) |
208 (* look up registration, pick one that subsumes the query *) |
207 fun lookup sign (regs, ts) = |
209 fun lookup thy (regs, ts) = |
208 let |
210 let |
209 val t = termify ts; |
211 val t = termify ts; |
210 val subs = subsumers sign t regs; |
212 val subs = subsumers thy t regs; |
211 in (case subs of |
213 in (case subs of |
212 [] => NONE |
214 [] => NONE |
213 | ((t', (attn, thms)) :: _) => let |
215 | ((t', (attn, thms)) :: _) => let |
214 val (tinst, inst) = Pattern.match sign (t', t) (Vartab.empty, Vartab.empty); |
216 val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty); |
215 (* thms contain Frees, not Vars *) |
217 (* thms contain Frees, not Vars *) |
216 val tinst' = tinst |> Vartab.dest |
218 val tinst' = tinst |> Vartab.dest |
217 |> map (fn ((x, 0), (_, T)) => (x, Type.unvarifyT T)) |
219 |> map (fn ((x, 0), (_, T)) => (x, Type.unvarifyT T)) |
218 |> Symtab.make; |
220 |> Symtab.make; |
219 val inst' = inst |> Vartab.dest |
221 val inst' = inst |> Vartab.dest |
220 |> map (fn ((x, 0), (_, t)) => (x, Logic.unvarify t)) |
222 |> map (fn ((x, 0), (_, t)) => (x, Logic.unvarify t)) |
221 |> Symtab.make; |
223 |> Symtab.make; |
222 in |
224 in |
223 SOME (attn, map (fn (t, th) => |
225 SOME (attn, map (Element.inst_witness thy (tinst', inst')) thms) |
224 (Element.inst_term (tinst', inst') t, |
|
225 Element.inst_thm sign (tinst', inst') th)) thms) |
|
226 end) |
226 end) |
227 end; |
227 end; |
228 |
228 |
229 (* add registration if not subsumed by ones already present, |
229 (* add registration if not subsumed by ones already present, |
230 additionally returns registrations that are strictly subsumed *) |
230 additionally returns registrations that are strictly subsumed *) |
430 val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; |
430 val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; |
431 fun prt_inst ts = |
431 fun prt_inst ts = |
432 Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts)); |
432 Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts)); |
433 fun prt_attn (prfx, atts) = |
433 fun prt_attn (prfx, atts) = |
434 Pretty.breaks (Pretty.str prfx :: Args.pretty_attribs ctxt atts); |
434 Pretty.breaks (Pretty.str prfx :: Args.pretty_attribs ctxt atts); |
435 fun prt_thm (_, th) = Pretty.quote (ProofContext.pretty_thm ctxt th); |
435 fun prt_witns witns = Pretty.enclose "[" "]" |
436 fun prt_thms thms = |
436 (Pretty.breaks (map (prt_term o Element.witness_prop) witns)); |
437 Pretty.enclose "[" "]" (Pretty.breaks (map prt_thm thms)); |
437 fun prt_reg (ts, (("", []), witns)) = |
438 fun prt_reg (ts, (("", []), thms)) = |
|
439 if show_wits |
438 if show_wits |
440 then Pretty.block [prt_inst ts, Pretty.fbrk, prt_thms thms] |
439 then Pretty.block [prt_inst ts, Pretty.fbrk, prt_witns witns] |
441 else prt_inst ts |
440 else prt_inst ts |
442 | prt_reg (ts, (attn, thms)) = |
441 | prt_reg (ts, (attn, witns)) = |
443 if show_wits |
442 if show_wits |
444 then Pretty.block ((prt_attn attn @ |
443 then Pretty.block ((prt_attn attn @ |
445 [Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk, |
444 [Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk, |
446 prt_thms thms])) |
445 prt_witns witns])) |
447 else Pretty.block ((prt_attn attn @ |
446 else Pretty.block ((prt_attn attn @ |
448 [Pretty.str ":", Pretty.brk 1, prt_inst ts])); |
447 [Pretty.str ":", Pretty.brk 1, prt_inst ts])); |
449 |
448 |
450 val loc_int = intern thy loc; |
449 val loc_int = intern thy loc; |
451 val regs = get_regs thy_ctxt; |
450 val regs = get_regs thy_ctxt; |
489 |
488 |
490 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); |
489 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); |
491 |
490 |
492 |
491 |
493 |
492 |
494 (** witnesses -- protected facts **) |
|
495 |
|
496 fun assume_protected thy t = |
|
497 (t, Goal.protect (Thm.assume (Thm.cterm_of thy t))); |
|
498 |
|
499 fun prove_protected thy t tac = |
|
500 (t, Goal.prove thy [] [] (Logic.protect t) (fn _ => |
|
501 Tactic.rtac Drule.protectI 1 THEN tac)); |
|
502 |
|
503 val conclude_protected = Goal.conclude #> Goal.norm_hhf; |
|
504 |
|
505 fun satisfy_protected pths thm = |
|
506 let |
|
507 fun satisfy chyp = |
|
508 (case find_first (fn (t, _) => Thm.term_of chyp aconv t) pths of |
|
509 NONE => I |
|
510 | SOME (_, th) => Drule.implies_intr_protected [chyp] #> Goal.comp_hhf th); |
|
511 in fold satisfy (#hyps (Thm.crep_thm thm)) thm end; |
|
512 |
|
513 |
|
514 |
|
515 (** structured contexts: rename + merge + implicit type instantiation **) |
493 (** structured contexts: rename + merge + implicit type instantiation **) |
516 |
494 |
517 (* parameter types *) |
495 (* parameter types *) |
518 |
496 |
519 fun frozen_tvars ctxt Ts = |
497 fun frozen_tvars ctxt Ts = |
626 let |
604 let |
627 val thy = ProofContext.theory_of ctxt; |
605 val thy = ProofContext.theory_of ctxt; |
628 val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss); |
606 val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss); |
629 fun inst ((((name, ps), mode), elems), env) = |
607 fun inst ((((name, ps), mode), elems), env) = |
630 (((name, map (apsnd (Option.map (Element.instT_type env))) ps), |
608 (((name, map (apsnd (Option.map (Element.instT_type env))) ps), |
631 map_mode (map (fn (t, th) => |
609 map_mode (map (Element.instT_witness thy env)) mode), |
632 (Element.instT_term env t, Element.instT_thm thy env th))) mode), |
|
633 map (Element.instT_ctxt thy env) elems); |
610 map (Element.instT_ctxt thy env) elems); |
634 in map inst (elemss ~~ envs) end; |
611 in map inst (elemss ~~ envs) end; |
635 |
612 |
636 (* like unify_elemss, but does not touch mode, additional |
613 (* like unify_elemss, but does not touch mode, additional |
637 parameter c_parms for enforcing further constraints (eg. syntax) *) |
614 parameter c_parms for enforcing further constraints (eg. syntax) *) |
684 fun rename_parms top ren ((name, ps), (parms, mode)) = |
661 fun rename_parms top ren ((name, ps), (parms, mode)) = |
685 let val ps' = map (Element.rename ren) ps in |
662 let val ps' = map (Element.rename ren) ps in |
686 (case duplicates (op =) ps' of |
663 (case duplicates (op =) ps' of |
687 [] => ((name, ps'), |
664 [] => ((name, ps'), |
688 if top then (map (Element.rename ren) parms, |
665 if top then (map (Element.rename ren) parms, |
689 map_mode (map (fn (t, th) => |
666 map_mode (map (Element.rename_witness ren)) mode) |
690 (Element.rename_term ren t, Element.rename_thm ren th))) mode) |
|
691 else (parms, mode)) |
667 else (parms, mode)) |
692 | dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')]) |
668 | dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')]) |
693 end; |
669 end; |
694 |
670 |
695 (* add registrations of (name, ps), recursively; |
671 (* add registrations of (name, ps), recursively; adjust hyps of witnesses *) |
696 adjust hyps of witness theorems *) |
|
697 |
672 |
698 fun add_regs (name, ps) (ths, ids) = |
673 fun add_regs (name, ps) (ths, ids) = |
699 let |
674 let |
700 val {params, regs, ...} = the_locale thy name; |
675 val {params, regs, ...} = the_locale thy name; |
701 val ps' = map #1 params; |
676 val ps' = map #1 params; |
708 ((name, map (Element.rename ren) ps), ths)) regs; |
683 ((name, map (Element.rename ren) ps), ths)) regs; |
709 val new_regs = gen_rems (eq_fst (op =)) (regs', ids); |
684 val new_regs = gen_rems (eq_fst (op =)) (regs', ids); |
710 val new_ids = map fst new_regs; |
685 val new_ids = map fst new_regs; |
711 val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids; |
686 val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids; |
712 |
687 |
713 val new_ths = new_regs |> map (fn (_, ths') => ths' |> map (fn (t, th) => |
688 val new_ths = new_regs |> map (#2 #> map |
714 (t |> Element.instT_term env |> Element.rename_term ren, |
689 (Element.instT_witness thy env #> |
715 th |> Element.instT_thm thy env |> Element.rename_thm ren |> satisfy_protected ths))); |
690 Element.rename_witness ren #> |
|
691 Element.satisfy_witness ths)); |
716 val new_ids' = map (fn (id, ths) => |
692 val new_ids' = map (fn (id, ths) => |
717 (id, ([], Derived ths))) (new_ids ~~ new_ths); |
693 (id, ([], Derived ths))) (new_ids ~~ new_ths); |
718 in |
694 in |
719 fold add_regs new_idTs (ths @ flat new_ths, ids @ new_ids') |
695 fold add_regs new_idTs (ths @ flat new_ths, ids @ new_ids') |
720 end; |
696 end; |
821 val [env] = unify_parms ctxt all_params [ps]; |
797 val [env] = unify_parms ctxt all_params [ps]; |
822 val t' = Element.instT_term env t; |
798 val t' = Element.instT_term env t; |
823 val th' = Element.instT_thm thy env th; |
799 val th' = Element.instT_thm thy env th; |
824 in (t', th') end; |
800 in (t', th') end; |
825 val final_elemss = map (fn ((id, mode), elems) => |
801 val final_elemss = map (fn ((id, mode), elems) => |
826 ((id, map_mode (map inst_th) mode), elems)) elemss'; |
802 ((id, map_mode (map (Element.map_witness inst_th)) mode), elems)) elemss'; |
827 |
803 |
828 in ((prev_idents @ idents, syntax), final_elemss) end; |
804 in ((prev_idents @ idents, syntax), final_elemss) end; |
829 |
805 |
830 end; |
806 end; |
831 |
807 |
885 else let |
861 else let |
886 val ps' = map (fn (n, SOME T) => Free (n, T)) ps; |
862 val ps' = map (fn (n, SOME T) => Free (n, T)) ps; |
887 val ctxt'' = put_local_registration (name, ps') ("", []) ctxt' |
863 val ctxt'' = put_local_registration (name, ps') ("", []) ctxt' |
888 in case mode of |
864 in case mode of |
889 Assumed axs => |
865 Assumed axs => |
890 fold (add_local_witness (name, ps') o assume_protected thy o #1) axs ctxt'' |
866 fold (add_local_witness (name, ps') o |
|
867 Element.assume_witness thy o Element.witness_prop) axs ctxt'' |
891 | Derived ths => fold (add_local_witness (name, ps')) ths ctxt'' |
868 | Derived ths => fold (add_local_witness (name, ps')) ths ctxt'' |
892 end |
869 end |
893 in (ProofContext.restore_naming ctxt ctxt'', res) end; |
870 in (ProofContext.restore_naming ctxt ctxt'', res) end; |
894 |
871 |
895 fun activate_elemss prep_facts = |
872 fun activate_elemss prep_facts = |
1101 |
1078 |
1102 |
1079 |
1103 (* for finish_elems (Int), |
1080 (* for finish_elems (Int), |
1104 remove redundant elements of derived identifiers, |
1081 remove redundant elements of derived identifiers, |
1105 turn assumptions and definitions into facts, |
1082 turn assumptions and definitions into facts, |
1106 adjust hypotheses of facts using witness theorems *) |
1083 adjust hypotheses of facts using witnesses *) |
1107 |
1084 |
1108 fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes) |
1085 fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes) |
1109 | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts) |
1086 | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts) |
1110 | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms) |
1087 | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms) |
1111 | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs) |
1088 | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs) |
1112 |
1089 |
1113 | finish_derived _ _ (Derived _) (Fixes _) = NONE |
1090 | finish_derived _ _ (Derived _) (Fixes _) = NONE |
1114 | finish_derived _ _ (Derived _) (Constrains _) = NONE |
1091 | finish_derived _ _ (Derived _) (Constrains _) = NONE |
1115 | finish_derived sign wits (Derived _) (Assumes asms) = asms |
1092 | finish_derived sign wits (Derived _) (Assumes asms) = asms |
1116 |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], [])))) |
1093 |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], [])))) |
1117 |> Notes |> Element.map_ctxt_values I I (satisfy_protected wits) |> SOME |
1094 |> Notes |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME |
1118 | finish_derived sign wits (Derived _) (Defines defs) = defs |
1095 | finish_derived sign wits (Derived _) (Defines defs) = defs |
1119 |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])])) |
1096 |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])])) |
1120 |> Notes |> Element.map_ctxt_values I I (satisfy_protected wits) |> SOME |
1097 |> Notes |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME |
1121 |
1098 |
1122 | finish_derived _ wits _ (Notes facts) = (Notes facts) |
1099 | finish_derived _ wits _ (Notes facts) = (Notes facts) |
1123 |> Element.map_ctxt_values I I (satisfy_protected wits) |> SOME; |
1100 |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME; |
1124 |
1101 |
1125 (* CB: for finish_elems (Ext) *) |
1102 (* CB: for finish_elems (Ext) *) |
1126 |
1103 |
1127 fun closeup _ false elem = elem |
1104 fun closeup _ false elem = elem |
1128 | closeup ctxt true elem = |
1105 | closeup ctxt true elem = |
1290 fun cert_facts x = prep_facts (K I) (K I) x; |
1267 fun cert_facts x = prep_facts (K I) (K I) x; |
1291 |
1268 |
1292 end; |
1269 end; |
1293 |
1270 |
1294 |
1271 |
1295 (* Get the specification of a locale *) |
1272 (* specification of a locale *) |
1296 |
1273 |
1297 (* The global specification is made from the parameters and global |
1274 (*The global specification is made from the parameters and global |
1298 assumptions, the local specification from the parameters and the local |
1275 assumptions, the local specification from the parameters and the |
1299 assumptions. *) |
1276 local assumptions.*) |
1300 |
1277 |
1301 local |
1278 local |
1302 |
1279 |
1303 fun gen_asms_of get thy name = |
1280 fun gen_asms_of get thy name = |
1304 let |
1281 let |
1305 val ctxt = ProofContext.init thy; |
1282 val ctxt = ProofContext.init thy; |
1306 val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name)); |
1283 val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name)); |
1307 val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss []; |
1284 val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss []; |
1308 in |
1285 in |
1309 elemss |> get |
1286 elemss |> get |
1310 |> map (fn (_, es) => map (fn Int e => e) es) |
1287 |> maps (fn (_, es) => map (fn Int e => e) es) |
1311 |> flat |
1288 |> maps (fn Assumes asms => asms | _ => []) |
1312 |> map_filter (fn Assumes asms => SOME asms | _ => NONE) |
|
1313 |> flat |
|
1314 |> map (apsnd (map fst)) |
1289 |> map (apsnd (map fst)) |
1315 end; |
1290 end; |
1316 |
1291 |
1317 in |
1292 in |
1318 |
1293 |
1367 activate_facts prep_facts (context, ps); |
1342 activate_facts prep_facts (context, ps); |
1368 |
1343 |
1369 val (ctxt, (elemss, _)) = |
1344 val (ctxt, (elemss, _)) = |
1370 activate_facts prep_facts (import_ctxt, qs); |
1345 activate_facts prep_facts (import_ctxt, qs); |
1371 val stmt = distinct Term.aconv |
1346 val stmt = distinct Term.aconv |
1372 (maps (fn ((_, Assumed axs), _) => maps (#hyps o Thm.rep_thm o #2) axs |
1347 (maps (fn ((_, Assumed axs), _) => maps Element.witness_hyps axs |
1373 | ((_, Derived _), _) => []) qs); |
1348 | ((_, Derived _), _) => []) qs); |
1374 val cstmt = map (cterm_of thy) stmt; |
1349 val cstmt = map (cterm_of thy) stmt; |
1375 in |
1350 in |
1376 ((((import_ctxt, import_elemss), (ctxt, elemss, syn)), (parms, spec, defs)), (cstmt, concl)) |
1351 ((((import_ctxt, import_elemss), (ctxt, elemss, syn)), (parms, spec, defs)), (cstmt, concl)) |
1377 end; |
1352 end; |
1388 in (stmt, map fst ps, Locale name) end); |
1363 in (stmt, map fst ps, Locale name) end); |
1389 val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), (elems_stmt, concl')) = |
1364 val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), (elems_stmt, concl')) = |
1390 prep_ctxt false fixed_params import elems concl ctxt; |
1365 prep_ctxt false fixed_params import elems concl ctxt; |
1391 in (locale, (locale_stmt, locale_ctxt), (elems_stmt, elems_ctxt), concl') end; |
1366 in (locale, (locale_stmt, locale_ctxt), (elems_stmt, elems_ctxt), concl') end; |
1392 |
1367 |
|
1368 fun prep_expr prep import body ctxt = |
|
1369 let |
|
1370 val (((_, import_elemss), (ctxt', elemss, _)), _) = prep import body ctxt; |
|
1371 val all_elems = maps snd (import_elemss @ elemss); |
|
1372 in (all_elems, ctxt') end; |
|
1373 |
1393 in |
1374 in |
1394 |
1375 |
1395 val read_ctxt = prep_context_statement intern_expr read_elemss read_facts; |
1376 val read_ctxt = prep_context_statement intern_expr read_elemss read_facts; |
1396 val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts; |
1377 val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts; |
1397 |
1378 |
1398 fun read_context import body ctxt = #1 (read_ctxt true [] import (map Elem body) [] ctxt); |
1379 fun read_context import body ctxt = #1 (read_ctxt true [] import (map Elem body) [] ctxt); |
1399 fun cert_context import body ctxt = #1 (cert_ctxt true [] import (map Elem body) [] ctxt); |
1380 fun cert_context import body ctxt = #1 (cert_ctxt true [] import (map Elem body) [] ctxt); |
1400 |
1381 |
|
1382 val read_expr = prep_expr read_context; |
|
1383 val cert_expr = prep_expr cert_context; |
|
1384 |
1401 val read_context_statement = prep_statement intern read_ctxt; |
1385 val read_context_statement = prep_statement intern read_ctxt; |
1402 val cert_context_statement = prep_statement (K I) cert_ctxt; |
1386 val cert_context_statement = prep_statement (K I) cert_ctxt; |
1403 |
1387 |
1404 end; |
1388 end; |
1405 |
1389 |
1406 |
1390 |
1407 (* print locale *) |
1391 (* print locale *) |
1408 |
1392 |
1409 fun print_locale thy show_facts import body = |
1393 fun print_locale thy show_facts import body = |
1410 let |
1394 let |
1411 val (((_, import_elemss), (ctxt, elemss, _)), _) = |
1395 val (all_elems, ctxt) = read_expr import body (ProofContext.init thy); |
1412 read_context import body (ProofContext.init thy); |
|
1413 val prt_elem = Element.pretty_ctxt ctxt; |
1396 val prt_elem = Element.pretty_ctxt ctxt; |
1414 val all_elems = maps #2 (import_elemss @ elemss); |
|
1415 in |
1397 in |
1416 Pretty.big_list "locale elements:" (all_elems |
1398 Pretty.big_list "locale elements:" (all_elems |
1417 |> (if show_facts then I else filter (fn Notes _ => false | _ => true)) |
1399 |> (if show_facts then I else filter (fn Notes _ => false | _ => true)) |
1418 |> map (Pretty.chunks o prt_elem)) |
1400 |> map (Pretty.chunks o prt_elem)) |
1419 |> Pretty.writeln |
1401 |> Pretty.writeln |
1434 |
1416 |
1435 fun local_note_prefix_i prfx args ctxt = |
1417 fun local_note_prefix_i prfx args ctxt = |
1436 ctxt |
1418 ctxt |
1437 |> ProofContext.qualified_names |
1419 |> ProofContext.qualified_names |
1438 |> ProofContext.sticky_prefix prfx |
1420 |> ProofContext.sticky_prefix prfx |
1439 |> ProofContext.note_thmss_i args |> swap |
1421 |> ProofContext.note_thmss_i args |
1440 |>> ProofContext.restore_naming ctxt; |
1422 ||> ProofContext.restore_naming ctxt; |
1441 |
1423 |
1442 |
1424 |
1443 (* collect witness theorems for global registration; |
1425 (* collect witnesses for global registration; |
1444 requires parameters and flattened list of (assumed!) identifiers |
1426 requires parameters and flattened list of (assumed!) identifiers |
1445 instead of recomputing it from the target *) |
1427 instead of recomputing it from the target *) |
1446 |
1428 |
1447 fun collect_global_witnesses thy parms ids vts = let |
1429 fun collect_global_witnesses thy parms ids vts = let |
1448 val ts = map Logic.unvarify vts; |
1430 val ts = map Logic.unvarify vts; |
1480 val inst_atts = |
1462 val inst_atts = |
1481 Args.map_values I (Element.instT_type (#1 insts)) |
1463 Args.map_values I (Element.instT_type (#1 insts)) |
1482 (Element.inst_term insts) (Element.inst_thm thy insts); |
1464 (Element.inst_term insts) (Element.inst_thm thy insts); |
1483 val args' = args |> map (fn ((n, atts), [(ths, [])]) => |
1465 val args' = args |> map (fn ((n, atts), [(ths, [])]) => |
1484 ((n, map (Attrib.attribute_i thy) (map inst_atts atts @ atts2)), |
1466 ((n, map (Attrib.attribute_i thy) (map inst_atts atts @ atts2)), |
1485 [(map (Drule.standard o satisfy_protected prems o |
1467 [(map (Drule.standard o Element.satisfy_thm prems o |
1486 Element.inst_thm thy insts) ths, [])])); |
1468 Element.inst_thm thy insts) ths, [])])); |
1487 in global_note_prefix_i kind prfx args' thy |> snd end; |
1469 in global_note_prefix_i kind prfx args' thy |> snd end; |
1488 in fold activate regs thy end; |
1470 in fold activate regs thy end; |
1489 |
1471 |
1490 |
1472 |
1624 val conjuncts = |
1606 val conjuncts = |
1625 (Drule.equal_elim_rule2 OF [body_eq, |
1607 (Drule.equal_elim_rule2 OF [body_eq, |
1626 Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))]) |
1608 Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))]) |
1627 |> Conjunction.elim_precise [length ts] |> hd; |
1609 |> Conjunction.elim_precise [length ts] |> hd; |
1628 val axioms = ts ~~ conjuncts |> map (fn (t, ax) => |
1610 val axioms = ts ~~ conjuncts |> map (fn (t, ax) => |
1629 prove_protected defs_thy t |
1611 Element.prove_witness defs_thy t |
1630 (Tactic.rewrite_goals_tac defs THEN |
1612 (Tactic.rewrite_goals_tac defs THEN |
1631 Tactic.compose_tac (false, ax, 0) 1)); |
1613 Tactic.compose_tac (false, ax, 0) 1)); |
1632 in ((statement, intro, axioms), defs_thy) end; |
1614 in ((statement, intro, axioms), defs_thy) end; |
1633 |
1615 |
1634 fun assumes_to_notes (Assumes asms) axms = |
1616 fun assumes_to_notes (Assumes asms) axms = |
1643 |
1625 |
1644 fun change_elemss axioms elemss = |
1626 fun change_elemss axioms elemss = |
1645 let |
1627 let |
1646 fun change (id as ("", _), es)= |
1628 fun change (id as ("", _), es)= |
1647 fold_map assumes_to_notes |
1629 fold_map assumes_to_notes |
1648 (map (Element.map_ctxt_values I I (satisfy_protected axioms)) es) |
1630 (map (Element.map_ctxt_values I I (Element.satisfy_thm axioms)) es) |
1649 #-> (fn es' => pair (id, es')) |
1631 #-> (fn es' => pair (id, es')) |
1650 | change e = pair e; |
1632 | change e = pair e; |
1651 in |
1633 in |
1652 fst (fold_map change elemss (map (conclude_protected o snd) axioms)) |
1634 fst (fold_map change elemss (map Element.conclude_witness axioms)) |
1653 end; |
1635 end; |
1654 |
1636 |
1655 in |
1637 in |
1656 |
1638 |
1657 (* CB: main predicate definition function *) |
1639 (* CB: main predicate definition function *) |
1683 val cstatement = Thm.cterm_of def_thy statement; |
1665 val cstatement = Thm.cterm_of def_thy statement; |
1684 in |
1666 in |
1685 def_thy |
1667 def_thy |
1686 |> PureThy.note_thmss_qualified "" bname |
1668 |> PureThy.note_thmss_qualified "" bname |
1687 [((introN, []), [([intro], [])]), |
1669 [((introN, []), [([intro], [])]), |
1688 ((axiomsN, []), [(map (Drule.standard o conclude_protected o #2) axioms, [])])] |
1670 ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])] |
1689 |> snd |
1671 |> snd |
1690 |> pair ([cstatement], axioms) |
1672 |> pair ([cstatement], axioms) |
1691 end; |
1673 end; |
1692 in ((elemss', predicate), thy'') end; |
1674 in ((elemss', predicate), thy'') end; |
1693 |
1675 |
1851 theorem_in_locale kind NONE (K (K I)) loc a elems concl; |
1833 theorem_in_locale kind NONE (K (K I)) loc a elems concl; |
1852 |
1834 |
1853 end; |
1835 end; |
1854 |
1836 |
1855 |
1837 |
|
1838 |
1856 (** Interpretation commands **) |
1839 (** Interpretation commands **) |
1857 |
1840 |
1858 local |
1841 local |
1859 |
1842 |
1860 (* extract proof obligations (assms and defs) from elements *) |
1843 (* extract proof obligations (assms and defs) from elements *) |
1861 |
1844 |
1862 fun extract_asms_elem (Fixes _) ts = ts |
1845 fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems) |
1863 | extract_asms_elem (Constrains _) ts = ts |
|
1864 | extract_asms_elem (Assumes asms) ts = |
|
1865 ts @ maps (fn (_, ams) => map (fn (t, _) => t) ams) asms |
|
1866 | extract_asms_elem (Defines defs) ts = |
|
1867 ts @ map (fn (_, (def, _)) => def) defs |
|
1868 | extract_asms_elem (Notes _) ts = ts; |
|
1869 |
|
1870 fun extract_asms_elems ((id, Assumed _), elems) = |
|
1871 (id, fold extract_asms_elem elems []) |
|
1872 | extract_asms_elems ((id, Derived _), _) = (id, []); |
1846 | extract_asms_elems ((id, Derived _), _) = (id, []); |
1873 |
1847 |
1874 fun extract_asms_elemss elemss = map extract_asms_elems elemss; |
|
1875 |
1848 |
1876 (* activate instantiated facts in theory or context *) |
1849 (* activate instantiated facts in theory or context *) |
1877 |
1850 |
1878 fun gen_activate_facts_elemss get_reg note attrib std put_reg add_wit |
1851 fun gen_activate_facts_elemss get_reg note attrib std put_reg add_wit |
1879 attn all_elemss new_elemss propss thmss thy_ctxt = |
1852 attn all_elemss new_elemss propss thmss thy_ctxt = |
1885 |> Attrib.map_facts (attrib thy_ctxt o Args.map_values I I I disch) |
1858 |> Attrib.map_facts (attrib thy_ctxt o Args.map_values I I I disch) |
1886 (* insert interpretation attributes *) |
1859 (* insert interpretation attributes *) |
1887 |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts))) |
1860 |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts))) |
1888 (* discharge hyps *) |
1861 (* discharge hyps *) |
1889 |> map (apsnd (map (apfst (map disch)))); |
1862 |> map (apsnd (map (apfst (map disch)))); |
1890 in fst (note prfx facts' thy_ctxt) end |
1863 in snd (note prfx facts' thy_ctxt) end |
1891 | activate_elem _ _ _ thy_ctxt = thy_ctxt; |
1864 | activate_elem _ _ _ thy_ctxt = thy_ctxt; |
1892 |
1865 |
1893 fun activate_elems disch ((id, _), elems) thy_ctxt = |
1866 fun activate_elems disch ((id, _), elems) thy_ctxt = |
1894 let |
1867 let |
1895 val ((prfx, atts2), _) = the (get_reg thy_ctxt id) |
1868 val ((prfx, atts2), _) = the (get_reg thy_ctxt id) |
1901 |
1874 |
1902 val thy_ctxt' = thy_ctxt |
1875 val thy_ctxt' = thy_ctxt |
1903 (* add registrations *) |
1876 (* add registrations *) |
1904 |> fold (fn ((id, _), _) => put_reg id attn) new_elemss |
1877 |> fold (fn ((id, _), _) => put_reg id attn) new_elemss |
1905 (* add witnesses of Assumed elements *) |
1878 (* add witnesses of Assumed elements *) |
1906 |> fold (fn (id, thms) => fold (add_wit id) thms) |
1879 |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss); |
1907 (map fst propss ~~ thmss); |
|
1908 |
1880 |
1909 val prems = flat (map_filter |
1881 val prems = flat (map_filter |
1910 (fn ((id, Assumed _), _) => Option.map snd (get_reg thy_ctxt' id) |
1882 (fn ((id, Assumed _), _) => Option.map snd (get_reg thy_ctxt' id) |
1911 | ((_, Derived _), _) => NONE) all_elemss); |
1883 | ((_, Derived _), _) => NONE) all_elemss); |
1912 val disch = satisfy_protected prems; |
|
1913 val disch' = std o disch; (* FIXME *) |
|
1914 |
|
1915 val thy_ctxt'' = thy_ctxt' |
1884 val thy_ctxt'' = thy_ctxt' |
1916 (* add witnesses of Derived elements *) |
1885 (* add witnesses of Derived elements *) |
1917 |> fold (fn (id, thms) => fold (add_wit id o apsnd disch) thms) |
1886 |> fold (fn (id, thms) => fold (add_wit id o Element.satisfy_witness prems) thms) |
1918 (map_filter (fn ((_, Assumed _), _) => NONE |
1887 (map_filter (fn ((_, Assumed _), _) => NONE |
1919 | ((id, Derived thms), _) => SOME (id, thms)) all_elemss) |
1888 | ((id, Derived thms), _) => SOME (id, thms)) all_elemss) |
|
1889 |
|
1890 val disch' = std o Element.satisfy_thm prems; (* FIXME *) |
1920 in |
1891 in |
1921 thy_ctxt'' |
1892 thy_ctxt'' |
1922 (* add facts to theory or context *) |
1893 (* add facts to theory or context *) |
1923 |> fold (activate_elems disch') new_elemss |
1894 |> fold (activate_elems disch') new_elemss |
1924 end; |
1895 end; |
1925 |
1896 |
1926 fun global_activate_facts_elemss x = gen_activate_facts_elemss |
1897 fun global_activate_facts_elemss x = gen_activate_facts_elemss |
1927 (fn thy => fn (name, ps) => |
1898 (fn thy => fn (name, ps) => |
1928 get_global_registration thy (name, map Logic.varify ps)) |
1899 get_global_registration thy (name, map Logic.varify ps)) |
1929 (swap ooo global_note_prefix_i "") |
1900 (global_note_prefix_i "") |
1930 Attrib.attribute_i Drule.standard |
1901 Attrib.attribute_i Drule.standard |
1931 (fn (name, ps) => put_global_registration (name, map Logic.varify ps)) |
1902 (fn (name, ps) => put_global_registration (name, map Logic.varify ps)) |
1932 (fn (n, ps) => fn (t, th) => |
1903 (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o |
1933 add_global_witness (n, map Logic.varify ps) |
1904 Element.map_witness (fn (t, th) => (Logic.unvarify t, Drule.freeze_all th)) |
1934 (Logic.unvarify t, Drule.freeze_all th)) x; |
1905 (* FIXME *)) x; |
1935 |
1906 |
1936 fun local_activate_facts_elemss x = gen_activate_facts_elemss |
1907 fun local_activate_facts_elemss x = gen_activate_facts_elemss |
1937 get_local_registration |
1908 get_local_registration |
1938 local_note_prefix_i |
1909 local_note_prefix_i |
1939 (Attrib.attribute_i o ProofContext.theory_of) I |
1910 (Attrib.attribute_i o ProofContext.theory_of) I |
2011 ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode)) ids; |
1982 ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode)) ids; |
2012 (* instantiate ids and elements *) |
1983 (* instantiate ids and elements *) |
2013 val inst_elemss = (ids' ~~ all_elemss) |> map (fn (((n, ps), _), ((_, mode), elems)) => |
1984 val inst_elemss = (ids' ~~ all_elemss) |> map (fn (((n, ps), _), ((_, mode), elems)) => |
2014 ((n, map (Element.inst_term insts) ps), |
1985 ((n, map (Element.inst_term insts) ps), |
2015 map (fn Int e => Element.inst_ctxt thy insts e) elems) |
1986 map (fn Int e => Element.inst_ctxt thy insts e) elems) |
2016 |> apfst (fn id => (id, map_mode (map (fn (t, th) => |
1987 |> apfst (fn id => (id, map_mode (map (Element.inst_witness thy insts)) mode))); |
2017 (Element.inst_term insts t, Element.inst_thm thy insts th))) mode))); |
|
2018 |
1988 |
2019 (* remove fragments already registered with theory or context *) |
1989 (* remove fragments already registered with theory or context *) |
2020 val new_inst_elemss = filter (fn ((id, _), _) => |
1990 val new_inst_elemss = filter (fn ((id, _), _) => |
2021 not (test_reg thy_ctxt id)) inst_elemss; |
1991 not (test_reg thy_ctxt id)) inst_elemss; |
2022 val new_ids = map #1 new_inst_elemss; |
1992 val new_ids = map #1 new_inst_elemss; |
2023 |
1993 |
2024 val propss = extract_asms_elemss new_inst_elemss; |
1994 val propss = map extract_asms_elems new_inst_elemss; |
2025 |
1995 |
2026 val bind_attrib = Attrib.crude_closure ctxt o Args.assignable; |
1996 val bind_attrib = Attrib.crude_closure ctxt o Args.assignable; |
2027 val attn' = apsnd (map (bind_attrib o Attrib.intern_src thy)) attn; |
1997 val attn' = apsnd (map (bind_attrib o Attrib.intern_src thy)) attn; |
2028 |
1998 |
2029 in (propss, activate attn' inst_elemss new_inst_elemss propss) end; |
1999 in (propss, activate attn' inst_elemss new_inst_elemss propss) end; |
2061 (* remove Int markers *) |
2031 (* remove Int markers *) |
2062 val elemss' = map (fn (_, es) => |
2032 val elemss' = map (fn (_, es) => |
2063 map (fn Int e => e) es) elemss |
2033 map (fn Int e => e) es) elemss |
2064 (* extract assumptions and defs *) |
2034 (* extract assumptions and defs *) |
2065 val ids_elemss = ids' ~~ elemss'; |
2035 val ids_elemss = ids' ~~ elemss'; |
2066 val propss = extract_asms_elemss ids_elemss; |
2036 val propss = map extract_asms_elems ids_elemss; |
2067 |
2037 |
2068 (** activation function: |
2038 (** activation function: |
2069 - add registrations to the target locale |
2039 - add registrations to the target locale |
2070 - add induced registrations for all global registrations of |
2040 - add induced registrations for all global registrations of |
2071 the target, unless already present |
2041 the target, unless already present |
2073 |
2043 |
2074 val t_ids = map_filter |
2044 val t_ids = map_filter |
2075 (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids; |
2045 (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids; |
2076 |
2046 |
2077 fun activate thmss thy = let |
2047 fun activate thmss thy = let |
2078 val satisfy = satisfy_protected (flat thmss); |
2048 val satisfy = Element.satisfy_thm (flat thmss); |
2079 val ids_elemss_thmss = ids_elemss ~~ thmss; |
2049 val ids_elemss_thmss = ids_elemss ~~ thmss; |
2080 val regs = get_global_registrations thy target; |
2050 val regs = get_global_registrations thy target; |
2081 |
2051 |
2082 fun activate_id (((id, Assumed _), _), thms) thy = |
2052 fun activate_id (((id, Assumed _), _), thms) thy = |
2083 thy |> put_registration_in_locale target id |
2053 thy |> put_registration_in_locale target id |
2086 |
2056 |
2087 fun activate_reg (vts, ((prfx, atts2), _)) thy = let |
2057 fun activate_reg (vts, ((prfx, atts2), _)) thy = let |
2088 val (insts, wits) = collect_global_witnesses thy fixed t_ids vts; |
2058 val (insts, wits) = collect_global_witnesses thy fixed t_ids vts; |
2089 fun inst_parms ps = map |
2059 fun inst_parms ps = map |
2090 (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps; |
2060 (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps; |
2091 val disch = satisfy_protected wits; |
2061 val disch = Element.satisfy_thm wits; |
2092 val new_elemss = filter (fn (((name, ps), _), _) => |
2062 val new_elemss = filter (fn (((name, ps), _), _) => |
2093 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss); |
2063 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss); |
2094 fun activate_assumed_id (((_, Derived _), _), _) thy = thy |
2064 fun activate_assumed_id (((_, Derived _), _), _) thy = thy |
2095 | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let |
2065 | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let |
2096 val ps' = inst_parms ps; |
2066 val ps' = inst_parms ps; |
2097 in |
2067 in |
2098 if test_global_registration thy (name, ps') |
2068 if test_global_registration thy (name, ps') |
2099 then thy |
2069 then thy |
2100 else thy |
2070 else thy |
2101 |> put_global_registration (name, ps') (prfx, atts2) |
2071 |> put_global_registration (name, ps') (prfx, atts2) |
2102 |> fold (fn (t, th) => fn thy => add_global_witness (name, ps') |
2072 |> fold (fn witn => fn thy => add_global_witness (name, ps') |
2103 (Element.inst_term insts t, disch (Element.inst_thm thy insts th)) thy) thms |
2073 (Element.inst_witness thy insts witn) thy) thms |
2104 end; |
2074 end; |
2105 |
2075 |
2106 fun activate_derived_id ((_, Assumed _), _) thy = thy |
2076 fun activate_derived_id ((_, Assumed _), _) thy = thy |
2107 | activate_derived_id (((name, ps), Derived ths), _) thy = let |
2077 | activate_derived_id (((name, ps), Derived ths), _) thy = let |
2108 val ps' = inst_parms ps; |
2078 val ps' = inst_parms ps; |
2109 in |
2079 in |
2110 if test_global_registration thy (name, ps') |
2080 if test_global_registration thy (name, ps') |
2111 then thy |
2081 then thy |
2112 else thy |
2082 else thy |
2113 |> put_global_registration (name, ps') (prfx, atts2) |
2083 |> put_global_registration (name, ps') (prfx, atts2) |
2114 |> fold (fn (t, th) => fn thy => add_global_witness (name, ps') |
2084 |> fold (fn witn => fn thy => add_global_witness (name, ps') |
|
2085 (witn |> Element.map_witness (fn (t, th) => (* FIXME *) |
2115 (Element.inst_term insts t, |
2086 (Element.inst_term insts t, |
2116 disch (Element.inst_thm thy insts (satisfy th))) thy) ths |
2087 disch (Element.inst_thm thy insts (satisfy th))))) thy) ths |
2117 end; |
2088 end; |
2118 |
2089 |
2119 fun activate_elem (Notes facts) thy = |
2090 fun activate_elem (Notes facts) thy = |
2120 let |
2091 let |
2121 val facts' = facts |
2092 val facts' = facts |
2143 end; |
2114 end; |
2144 |
2115 |
2145 in (propss, activate) end; |
2116 in (propss, activate) end; |
2146 |
2117 |
2147 fun prep_propp propss = propss |> map (fn ((name, _), props) => |
2118 fun prep_propp propss = propss |> map (fn ((name, _), props) => |
2148 (("", []), map (rpair [] o Logic.protect) props)); |
2119 (("", []), map (rpair [] o Element.mark_witness) props)); |
2149 |
2120 |
2150 fun prep_result propps thmss = |
2121 fun prep_result propps thmss = |
2151 ListPair.map (fn ((_, props), thms) => (props ~~ thms)) (propps, thmss); |
2122 ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss); |
2152 |
|
2153 val refine_protected = |
|
2154 Proof.refine (Method.Basic (K (Method.RAW_METHOD |
|
2155 (K (ALLGOALS |
|
2156 (PRECISE_CONJUNCTS ~1 (ALLGOALS |
|
2157 (PRECISE_CONJUNCTS ~1 (ALLGOALS (Tactic.rtac Drule.protectI)))))))))) |
|
2158 #> Seq.hd; |
|
2159 |
2123 |
2160 fun goal_name thy kind target propss = |
2124 fun goal_name thy kind target propss = |
2161 kind ^ Proof.goal_names (Option.map (extern thy) target) "" |
2125 kind ^ Proof.goal_names (Option.map (extern thy) target) "" |
2162 (propss |> map (fn ((name, _), _) => extern thy name)); |
2126 (propss |> map (fn ((name, _), _) => extern thy name)); |
2163 |
2127 |