author  haftmann 
Wed, 02 Dec 2015 19:14:55 +0100  
changeset 61771  acc532690ee1 
parent 61708  4de2380ae3ab 
child 61772  2f33f6cc964d 
permissions  rwrr 
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 localtheory 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 localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

11 
type 'a rewrites = (Attrib.binding * 'a) list 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

12 

fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

13 
(*interpretation in proofs*) 
fd4ac1530d63
represent both algebraic and localtheory 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 localtheory 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 localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

16 

61771  17 
(*algebraic view*) 
61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

18 
val global_interpretation: Expression.expression_i > 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

19 
term defines > term rewrites > theory > Proof.state 
fd4ac1530d63
represent both algebraic and localtheory 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 localtheory 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 localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

23 
string defines > string rewrites > theory > Proof.state 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

24 
val sublocale: Expression.expression_i > 
fd4ac1530d63
represent both algebraic and localtheory 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 localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

26 
val sublocale_cmd: Expression.expression > 
fd4ac1530d63
represent both algebraic and localtheory 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 localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

28 

fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

29 
(*localtheorybased view*) 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

30 
val ephemeral_interpretation: Expression.expression_i > 
fd4ac1530d63
represent both algebraic and localtheory 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 localtheory 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 localtheory 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 localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

36 

fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

37 
(*mixed Isar interface*) 
fd4ac1530d63
represent both algebraic and localtheory 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 localtheory 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 localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

46 
(** common interpretation machinery **) 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

47 

fd4ac1530d63
represent both algebraic and localtheory 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 localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

49 
type 'a rewrites = (Attrib.binding * 'a) list 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

50 

fd4ac1530d63
represent both algebraic and localtheory 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 
(*quasiinhomogeneous 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 
61708
4de2380ae3ab
explicit nested local theory for definitions, however retaining arcane lowlevel fiddling with background theory
haftmann
parents:
61698
diff
changeset

68 
val ((_, defs), inner_def_lthy) = 
4de2380ae3ab
explicit nested local theory for definitions, however retaining arcane lowlevel fiddling with background theory
haftmann
parents:
61698
diff
changeset

69 
expr_lthy 
4de2380ae3ab
explicit nested local theory for definitions, however retaining arcane lowlevel fiddling with background theory
haftmann
parents:
61698
diff
changeset

70 
> Local_Theory.open_target 
4de2380ae3ab
explicit nested local theory for definitions, however retaining arcane lowlevel fiddling with background theory
haftmann
parents:
61698
diff
changeset

71 
>> fold_map Local_Theory.define pre_defs 
61691
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset

72 
val def_lthy = 
61708
4de2380ae3ab
explicit nested local theory for definitions, however retaining arcane lowlevel fiddling with background theory
haftmann
parents:
61698
diff
changeset

73 
inner_def_lthy 
4de2380ae3ab
explicit nested local theory for definitions, however retaining arcane lowlevel fiddling with background theory
haftmann
parents:
61698
diff
changeset

74 
> Local_Theory.close_target; 
4de2380ae3ab
explicit nested local theory for definitions, however retaining arcane lowlevel fiddling with background theory
haftmann
parents:
61698
diff
changeset

75 
val def_eqns = 
4de2380ae3ab
explicit nested local theory for definitions, however retaining arcane lowlevel fiddling with background theory
haftmann
parents:
61698
diff
changeset

76 
defs 
4de2380ae3ab
explicit nested local theory for definitions, however retaining arcane lowlevel fiddling with background theory
haftmann
parents:
61698
diff
changeset

77 
> map (Thm.symmetric o snd o snd) 
4de2380ae3ab
explicit nested local theory for definitions, however retaining arcane lowlevel fiddling with background theory
haftmann
parents:
61698
diff
changeset

78 
> Proof_Context.export inner_def_lthy def_lthy; 
4de2380ae3ab
explicit nested local theory for definitions, however retaining arcane lowlevel fiddling with background theory
haftmann
parents:
61698
diff
changeset

79 
in (def_eqns, Proof_Context.transfer (Proof_Context.theory_of def_lthy) expr_lthy) end; 
61691
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset

80 

91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset

81 
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

82 
expression raw_defs raw_eqns initial_ctxt = 
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset

83 
let 
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset

84 
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

85 
val (pre_defs, eqns) = 
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset

86 
prep_mixins prep_term prep_prop expr_ctxt 
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset

87 
(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

88 
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

89 
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

90 
val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt; 
87203a0f0041
tuned  share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset

91 
val export' = Variable.export_morphism goal_ctxt def_ctxt; 
87203a0f0041
tuned  share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset

92 
in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end; 
61669  93 

61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

94 
in 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

95 

61698  96 
fun cert_interpretation expression = 
97 
prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I) expression; 

61672
87203a0f0041
tuned  share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset

98 

61698  99 
fun read_interpretation expression = 
100 
prep_interpretation Expression.read_goal_expression Syntax.parse_term 

101 
Syntax.parse_prop Attrib.check_src expression; 

61669  102 

61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

103 
end; 
61669  104 

61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

105 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

106 
(* interpretation machinery *) 
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

107 

301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

108 
local 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

109 

61672
87203a0f0041
tuned  share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset

110 
fun meta_rewrite eqns ctxt = 
87203a0f0041
tuned  share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset

111 
(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

112 

301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

113 
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

114 
let 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

115 
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

116 
:: 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

117 
val (eqns', ctxt') = ctxt 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

118 
> note Thm.theoremK facts 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

119 
> meta_rewrite; 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

120 
val dep_morphs = map2 (fn (dep, morph) => fn wits => 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

121 
(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

122 
fun activate' dep_morph ctxt = activate dep_morph 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

123 
(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

124 
in 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

125 
ctxt' 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

126 
> fold activate' dep_morphs 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

127 
end; 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

128 

301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

129 
in 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

130 

301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

131 
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

132 
expression raw_defs raw_eqns initial_ctxt = 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

133 
let 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

134 
val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

135 
prep_interpretation expression raw_defs raw_eqns initial_ctxt; 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

136 
fun after_qed witss eqns = 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

137 
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

138 
in setup_proof after_qed propss eqns goal_ctxt end; 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

139 

61672
87203a0f0041
tuned  share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset

140 
fun generic_interpretation prep_interpretation setup_proof note add_registration expression = 
87203a0f0041
tuned  share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset

141 
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

142 

61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

143 
end; 
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

144 

301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

145 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

146 
(** interfaces **) 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

147 

fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

148 
(* interpretation in proofs *) 
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

149 

61672
87203a0f0041
tuned  share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset

150 
local 
87203a0f0041
tuned  share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset

151 

61669  152 
fun gen_interpret prep_interpretation expression raw_eqns int state = 
153 
let 

154 
val _ = Proof.assert_forward_or_chain state; 

155 
val ctxt = Proof.context_of state; 

156 
fun lift_after_qed after_qed witss eqns = 

157 
Proof.map_context (after_qed witss eqns) #> Proof.reset_facts; 

158 
fun setup_proof after_qed propss eqns goal_ctxt = 

159 
Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" 

160 
propss eqns goal_ctxt int state; 

161 
in 

162 
generic_interpretation prep_interpretation setup_proof 

163 
Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt 

164 
end; 

165 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

166 
in 
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

167 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

168 
fun interpret expression = gen_interpret cert_interpretation expression; 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

169 
fun interpret_cmd raw_expression = gen_interpret read_interpretation raw_expression; 
61669  170 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

171 
end; 
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

172 

301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

173 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

174 
(* algebraicview *) 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

175 

fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

176 
local 
61669  177 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

178 
fun gen_global_interpretation prep_interpretation expression 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

179 
raw_defs raw_eqns thy = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

180 
let 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

181 
val lthy = Named_Target.theory_init thy; 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

182 
fun setup_proof after_qed = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

183 
Element.witness_proof_eqs 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

184 
(fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit); 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

185 
in 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

186 
lthy > 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

187 
generic_interpretation_with_defs prep_interpretation setup_proof 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

188 
Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

189 
end; 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

190 

fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

191 
fun gen_global_sublocale prep_loc prep_interpretation 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

192 
raw_locale expression raw_defs raw_eqns thy = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

193 
let 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

194 
val lthy = Named_Target.init (prep_loc thy raw_locale) thy; 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

195 
fun setup_proof after_qed = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

196 
Element.witness_proof_eqs 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

197 
(fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit); 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

198 
in 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

199 
lthy > 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

200 
generic_interpretation_with_defs prep_interpretation setup_proof 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

201 
Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

202 
end; 
61669  203 

204 
fun subscribe_locale_only lthy = 

205 
let 

206 
val _ = 

207 
if Named_Target.is_theory lthy 

208 
then error "Not possible on level of global theory" 

209 
else (); 

210 
in Local_Theory.subscription end; 

211 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

212 
fun gen_sublocale prep_interpretation expression raw_defs raw_eqns lthy = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

213 
generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

214 
Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_defs raw_eqns lthy; 
61669  215 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

216 
in 
61669  217 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

218 
fun global_interpretation expression = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

219 
gen_global_interpretation cert_interpretation expression; 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

220 
fun global_sublocale expression = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

221 
gen_global_sublocale (K I) cert_interpretation expression; 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

222 
fun global_sublocale_cmd raw_expression = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

223 
gen_global_sublocale Locale.check read_interpretation raw_expression; 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

224 
fun sublocale expression = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

225 
gen_sublocale cert_interpretation expression; 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

226 
fun sublocale_cmd raw_expression = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

227 
gen_sublocale read_interpretation raw_expression; 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

228 

fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

229 
end; 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

230 

fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

231 

fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

232 
(* localtheorybased view *) 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

233 

fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

234 
local 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

235 

fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

236 
fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

237 
Local_Theory.assert_bottom true 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

238 
#> generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

239 
Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns 
61669  240 

241 
in 

242 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

243 
fun ephemeral_interpretation expression = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

244 
generic_interpretation cert_interpretation Element.witness_proof_eqs 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

245 
Local_Theory.notes_kind Locale.activate_fragment expression; 
61669  246 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

247 
fun permanent_interpretation expression = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

248 
gen_permanent_interpretation cert_interpretation expression; 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

249 
fun permanent_interpretation_cmd raw_expression = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

250 
gen_permanent_interpretation read_interpretation raw_expression; 
61669  251 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

252 
end; 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

253 

fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

254 

fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

255 
(* mixed Isar interface *) 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

256 

fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

257 
local 
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset

258 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

259 
fun subscribe_or_activate lthy = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

260 
if Named_Target.is_theory lthy 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

261 
then Local_Theory.subscription 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

262 
else Locale.activate_fragment; 
61669  263 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

264 
fun gen_local_theory_interpretation prep_interpretation expression raw_eqns lthy = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

265 
generic_interpretation prep_interpretation Element.witness_proof_eqs 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

266 
Local_Theory.notes_kind (subscribe_or_activate lthy) expression raw_eqns lthy; 
61669  267 

61673
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

268 
in 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

269 

fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

270 
fun interpretation expression = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

271 
gen_local_theory_interpretation cert_interpretation expression; 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

272 
fun interpretation_cmd raw_expression = 
fd4ac1530d63
represent both algebraic and localtheory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset

273 
gen_local_theory_interpretation read_interpretation raw_expression; 
61669  274 

275 
end; 

276 

277 
end; 