author | haftmann |
Mon, 16 Nov 2015 19:08:38 +0100 | |
changeset 61691 | 91854ba66adb |
parent 61684 | 048ba34613bb |
child 61698 | c4a6edbfec49 |
permissions | -rw-r--r-- |
61669 | 1 |
(* Title: Pure/Isar/interpretation.ML |
2 |
Author: Clemens Ballarin, TU Muenchen |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
3 |
Author: Florian Haftmann, TU Muenchen |
61669 | 4 |
|
5 |
Locale interpretation. |
|
6 |
*) |
|
7 |
||
8 |
signature INTERPRETATION = |
|
9 |
sig |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
10 |
type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
11 |
type 'a rewrites = (Attrib.binding * 'a) list |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
12 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
13 |
(*interpretation in proofs*) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
14 |
val interpret: Expression.expression_i -> term rewrites -> bool -> Proof.state -> Proof.state |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
15 |
val interpret_cmd: Expression.expression -> string rewrites -> bool -> Proof.state -> Proof.state |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
16 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
17 |
(*algebraic-view*) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
18 |
val global_interpretation: Expression.expression_i -> |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
19 |
term defines -> term rewrites -> theory -> Proof.state |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
20 |
val global_sublocale: string -> Expression.expression_i -> |
61676 | 21 |
term defines -> term rewrites -> theory -> Proof.state |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
22 |
val global_sublocale_cmd: xstring * Position.T -> Expression.expression -> |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
23 |
string defines -> string rewrites -> theory -> Proof.state |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
24 |
val sublocale: Expression.expression_i -> |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
25 |
term defines -> term rewrites -> local_theory -> Proof.state |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
26 |
val sublocale_cmd: Expression.expression -> |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
27 |
string defines -> string rewrites -> local_theory -> Proof.state |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
28 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
29 |
(*local-theory-based view*) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
30 |
val ephemeral_interpretation: Expression.expression_i -> |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
31 |
term rewrites -> local_theory -> Proof.state |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
32 |
val permanent_interpretation: Expression.expression_i -> |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
33 |
term defines -> term rewrites -> local_theory -> Proof.state |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
34 |
val permanent_interpretation_cmd: Expression.expression -> |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
35 |
string defines -> string rewrites -> local_theory -> Proof.state |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
36 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
37 |
(*mixed Isar interface*) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
38 |
val interpretation: Expression.expression_i -> term rewrites -> local_theory -> Proof.state |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
39 |
val interpretation_cmd: Expression.expression -> string rewrites -> |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
40 |
local_theory -> Proof.state |
61669 | 41 |
end; |
42 |
||
43 |
structure Interpretation : INTERPRETATION = |
|
44 |
struct |
|
45 |
||
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
46 |
(** common interpretation machinery **) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
47 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
48 |
type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
49 |
type 'a rewrites = (Attrib.binding * 'a) list |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
50 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
51 |
(* reading of locale expressions with rewrite morphisms *) |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
52 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
53 |
local |
61669 | 54 |
|
61691
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
55 |
fun prep_mixins prep_term prep_prop expr_ctxt deps_ctxt raw_defs raw_eqns = |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
56 |
let |
61684 | 57 |
val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt expr_ctxt; |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
58 |
val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
59 |
val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs => |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
60 |
((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss; |
61691
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
61 |
val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns; |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
62 |
in (pre_defs, eqns) end; |
61669 | 63 |
|
61691
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
64 |
fun define_mixins [] expr_ctxt = ([], expr_ctxt) |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
65 |
(*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*) |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
66 |
| define_mixins pre_defs expr_lthy = |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
67 |
let |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
68 |
val (defs, forked_lthy) = fold_map Local_Theory.define pre_defs expr_lthy; |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
69 |
val def_lthy = |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
70 |
Proof_Context.transfer (Proof_Context.theory_of forked_lthy) expr_lthy; |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
71 |
val def_eqns = defs |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
72 |
|> map (Thm.symmetric o |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
73 |
Morphism.thm (Local_Theory.standard_morphism forked_lthy def_lthy) o snd o snd); |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
74 |
in (def_eqns, def_lthy) end; |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
75 |
|
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
76 |
fun prep_interpretation prep_expr prep_term prep_prop prep_attr |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
77 |
expression raw_defs raw_eqns initial_ctxt = |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
78 |
let |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
79 |
val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt; |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
80 |
val (pre_defs, eqns) = |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
81 |
prep_mixins prep_term prep_prop expr_ctxt |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
82 |
(fold Locale.activate_declarations deps expr_ctxt) raw_defs raw_eqns; |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
83 |
val (def_eqns, def_ctxt) = define_mixins pre_defs expr_ctxt; |
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
84 |
val attrss = map (apsnd (map (prep_attr def_ctxt)) o fst) raw_eqns; |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
85 |
val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt; |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
86 |
val export' = Variable.export_morphism goal_ctxt def_ctxt; |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
87 |
in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end; |
61669 | 88 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
89 |
in |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
90 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
91 |
val cert_interpretation = |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
92 |
prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I); |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
93 |
|
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
94 |
val read_interpretation = |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
95 |
prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src; |
61669 | 96 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
97 |
end; |
61669 | 98 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
99 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
100 |
(* interpretation machinery *) |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
101 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
102 |
local |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
103 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
104 |
fun meta_rewrite eqns ctxt = |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
105 |
(map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt); |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
106 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
107 |
fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt = |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
108 |
let |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
109 |
val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])]) |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
110 |
:: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
111 |
val (eqns', ctxt') = ctxt |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
112 |
|> note Thm.theoremK facts |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
113 |
|-> meta_rewrite; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
114 |
val dep_morphs = map2 (fn (dep, morph) => fn wits => |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
115 |
(dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
116 |
fun activate' dep_morph ctxt = activate dep_morph |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
117 |
(Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
118 |
in |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
119 |
ctxt' |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
120 |
|> fold activate' dep_morphs |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
121 |
end; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
122 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
123 |
in |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
124 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
125 |
fun generic_interpretation_with_defs prep_interpretation setup_proof note add_registration |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
126 |
expression raw_defs raw_eqns initial_ctxt = |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
127 |
let |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
128 |
val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
129 |
prep_interpretation expression raw_defs raw_eqns initial_ctxt; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
130 |
fun after_qed witss eqns = |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
131 |
note_eqns_register note add_registration deps witss def_eqns eqns attrss export export'; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
132 |
in setup_proof after_qed propss eqns goal_ctxt end; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
133 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
134 |
fun generic_interpretation prep_interpretation setup_proof note add_registration expression = |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
135 |
generic_interpretation_with_defs prep_interpretation setup_proof note add_registration expression []; |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
136 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
137 |
end; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
138 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
139 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
140 |
(** interfaces **) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
141 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
142 |
(* interpretation in proofs *) |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
143 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
144 |
local |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
145 |
|
61669 | 146 |
fun gen_interpret prep_interpretation expression raw_eqns int state = |
147 |
let |
|
148 |
val _ = Proof.assert_forward_or_chain state; |
|
149 |
val ctxt = Proof.context_of state; |
|
150 |
fun lift_after_qed after_qed witss eqns = |
|
151 |
Proof.map_context (after_qed witss eqns) #> Proof.reset_facts; |
|
152 |
fun setup_proof after_qed propss eqns goal_ctxt = |
|
153 |
Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" |
|
154 |
propss eqns goal_ctxt int state; |
|
155 |
in |
|
156 |
generic_interpretation prep_interpretation setup_proof |
|
157 |
Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt |
|
158 |
end; |
|
159 |
||
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
160 |
in |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
161 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
162 |
fun interpret expression = gen_interpret cert_interpretation expression; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
163 |
fun interpret_cmd raw_expression = gen_interpret read_interpretation raw_expression; |
61669 | 164 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
165 |
end; |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
166 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
167 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
168 |
(* algebraic-view *) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
169 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
170 |
local |
61669 | 171 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
172 |
fun gen_global_interpretation prep_interpretation expression |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
173 |
raw_defs raw_eqns thy = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
174 |
let |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
175 |
val lthy = Named_Target.theory_init thy; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
176 |
fun setup_proof after_qed = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
177 |
Element.witness_proof_eqs |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
178 |
(fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit); |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
179 |
in |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
180 |
lthy |> |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
181 |
generic_interpretation_with_defs prep_interpretation setup_proof |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
182 |
Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
183 |
end; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
184 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
185 |
fun gen_global_sublocale prep_loc prep_interpretation |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
186 |
raw_locale expression raw_defs raw_eqns thy = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
187 |
let |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
188 |
val lthy = Named_Target.init (prep_loc thy raw_locale) thy; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
189 |
fun setup_proof after_qed = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
190 |
Element.witness_proof_eqs |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
191 |
(fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit); |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
192 |
in |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
193 |
lthy |> |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
194 |
generic_interpretation_with_defs prep_interpretation setup_proof |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
195 |
Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
196 |
end; |
61669 | 197 |
|
198 |
fun subscribe_locale_only lthy = |
|
199 |
let |
|
200 |
val _ = |
|
201 |
if Named_Target.is_theory lthy |
|
202 |
then error "Not possible on level of global theory" |
|
203 |
else (); |
|
204 |
in Local_Theory.subscription end; |
|
205 |
||
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
206 |
fun gen_sublocale prep_interpretation expression raw_defs raw_eqns lthy = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
207 |
generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
208 |
Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_defs raw_eqns lthy; |
61669 | 209 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
210 |
in |
61669 | 211 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
212 |
fun global_interpretation expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
213 |
gen_global_interpretation cert_interpretation expression; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
214 |
fun global_sublocale expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
215 |
gen_global_sublocale (K I) cert_interpretation expression; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
216 |
fun global_sublocale_cmd raw_expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
217 |
gen_global_sublocale Locale.check read_interpretation raw_expression; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
218 |
fun sublocale expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
219 |
gen_sublocale cert_interpretation expression; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
220 |
fun sublocale_cmd raw_expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
221 |
gen_sublocale read_interpretation raw_expression; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
222 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
223 |
end; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
224 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
225 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
226 |
(* local-theory-based view *) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
227 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
228 |
local |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
229 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
230 |
fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
231 |
Local_Theory.assert_bottom true |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
232 |
#> generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
233 |
Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns |
61669 | 234 |
|
235 |
in |
|
236 |
||
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
237 |
fun ephemeral_interpretation expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
238 |
generic_interpretation cert_interpretation Element.witness_proof_eqs |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
239 |
Local_Theory.notes_kind Locale.activate_fragment expression; |
61669 | 240 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
241 |
fun permanent_interpretation expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
242 |
gen_permanent_interpretation cert_interpretation expression; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
243 |
fun permanent_interpretation_cmd raw_expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
244 |
gen_permanent_interpretation read_interpretation raw_expression; |
61669 | 245 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
246 |
end; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
247 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
248 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
249 |
(* mixed Isar interface *) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
250 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
251 |
local |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
252 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
253 |
fun subscribe_or_activate lthy = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
254 |
if Named_Target.is_theory lthy |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
255 |
then Local_Theory.subscription |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
256 |
else Locale.activate_fragment; |
61669 | 257 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
258 |
fun gen_local_theory_interpretation prep_interpretation expression raw_eqns lthy = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
259 |
generic_interpretation prep_interpretation Element.witness_proof_eqs |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
260 |
Local_Theory.notes_kind (subscribe_or_activate lthy) expression raw_eqns lthy; |
61669 | 261 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
262 |
in |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
263 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
264 |
fun interpretation expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
265 |
gen_local_theory_interpretation cert_interpretation expression; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
266 |
fun interpretation_cmd raw_expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
267 |
gen_local_theory_interpretation read_interpretation raw_expression; |
61669 | 268 |
|
269 |
end; |
|
270 |
||
271 |
end; |