Skip to content

Commit 4bd9e92

Browse files
simondfostersimondfoster
committed
Updates for Isabelle2023
1 parent 3305f36 commit 4bd9e92

File tree

2 files changed

+23
-23
lines changed

2 files changed

+23
-23
lines changed

‎Channel_Type.ML

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@ fun compile_chantype (name, chans) ctx =
6565
val thypfx =
6666
case (Named_Target.locale_of ctx) of
6767
SOME loc => loc ^ "." |
68-
NONE => Context.theory_name (Local_Theory.exit_global ctx) ^ "."
68+
NONE => Context.theory_name {long = false} (Local_Theory.exit_global ctx) ^ "."
6969
val prefix = thypfx ^ name ^ "."
7070
val attrs = @{attributes [simp, code_unfold]}
7171
val dummy_disc = absdummy dummyT @{term True}

‎Lens_Record.ML

Lines changed: 22 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ fun lens_proof tname x thy =
7777
Goal.prove_global thy [] []
7878
(hd (Type_Infer_Context.infer_types
7979
(Proof_Context.init_global thy)
80-
[mk_vwb_lens (const (Context.theory_name thy ^ "." ^ tname ^ "." ^ x))]))
80+
[mk_vwb_lens (const (Context.theory_name {long = false} thy ^ "." ^ tname ^ "." ^ x))]))
8181
(fn {context = context, prems = _}
8282
=> EVERY [ Locale.intro_locales_tac {strict = true, eager = true} context []
8383
, PARALLEL_ALLGOALS (asm_simp_tac
@@ -91,7 +91,7 @@ fun lens_sym_proof tname thy =
9191
(hd (Type_Infer_Context.infer_types
9292
(Proof_Context.init_global thy)
9393
[ Const (Trueprop, dummyT)
94-
$ (const sym_lensN $ const (Context.theory_name thy ^ "." ^ tname ^ "." ^ all_lensN))]))
94+
$ (const sym_lensN $ const (Context.theory_name {long = false} thy ^ "." ^ tname ^ "." ^ all_lensN))]))
9595
(fn {context = context, prems = _}
9696
=> EVERY [ Classical.rule_tac context [@{thm sym_lens.intro}] [] 1
9797
, PARALLEL_ALLGOALS (asm_simp_tac
@@ -144,8 +144,8 @@ fun lens_bij_proof tname thy =
144144
(Proof_Context.init_global thy)
145145
[ Const (Trueprop, dummyT)
146146
$ (const (bij_lensN) $
147-
(const (lens_plusN) $ const (Context.theory_name thy ^ "." ^ tname ^ "." ^ base_lensN)
148-
$ const (Context.theory_name thy ^ "." ^ tname ^ "." ^ child_lensN)))]))
147+
(const (lens_plusN) $ const (Context.theory_name {long = false} thy ^ "." ^ tname ^ "." ^ base_lensN)
148+
$ const (Context.theory_name {long = false} thy ^ "." ^ tname ^ "." ^ child_lensN)))]))
149149
(fn {context = context, prems = _}
150150
=> EVERY [ Locale.intro_locales_tac {strict = true, eager = true} context []
151151
, auto_tac (fold add_simp (get_thms thy lens_defsN @ [@{thm prod.case_eq_if}])
@@ -164,8 +164,8 @@ fun indep_proof tname thy (x, y) =
164164
(hd (Type_Infer_Context.infer_types
165165
(Proof_Context.init_global thy)
166166
[ mk_indep
167-
(const (Context.theory_name thy ^ "." ^ tname ^ "." ^ x))
168-
(const (Context.theory_name thy ^ "." ^ tname ^ "." ^ y))
167+
(const (Context.theory_name {long = false} thy ^ "." ^ tname ^ "." ^ x))
168+
(const (Context.theory_name {long = false} thy ^ "." ^ tname ^ "." ^ y))
169169
]))
170170
(prove_indep tname thy)
171171
end
@@ -179,7 +179,7 @@ fun equiv_one_proof tname thy fs =
179179
$ ( Const (lens_equivN, dummyT)
180180
$ Const (id_lensN, dummyT)
181181
$ foldr1 (fn (x, y) => Const (lens_plusN, dummyT) $ x $ y)
182-
(map (fn n => Const (theory_name thy ^ "." ^ tname ^ "." ^ n, dummyT)) (fs @ [child_lensN]))
182+
(map (fn n => Const (theory_name {long = false} thy ^ "." ^ tname ^ "." ^ n, dummyT)) (fs @ [child_lensN]))
183183
)]))
184184
(prove_equiv tname thy)
185185
end
@@ -194,7 +194,7 @@ fun equiv_more_proof tname pname thy fs =
194194
$ ( Const (lens_equivN, dummyT)
195195
$ Const (pname ^ "." ^ child_lensN, dummyT)
196196
$ foldr1 (fn (x, y) => Const (lens_plusN, dummyT) $ x $ y)
197-
(map (fn n => Const (theory_name thy ^ "." ^ tname ^ "." ^ n, dummyT)) (fs @ [child_lensN]))
197+
(map (fn n => Const (theory_name {long = false} thy ^ "." ^ tname ^ "." ^ n, dummyT)) (fs @ [child_lensN]))
198198
)]))
199199
(prove_equiv tname thy)
200200
end
@@ -206,10 +206,10 @@ fun equiv_base_proof tname parent thy fs =
206206
(Proof_Context.init_global thy)
207207
[ Const (Trueprop, dummyT)
208208
$ ( Const (lens_equivN, dummyT)
209-
$ Const (theory_name thy ^ "." ^ tname ^ "." ^ base_lensN, dummyT)
209+
$ Const (theory_name {long = false} thy ^ "." ^ tname ^ "." ^ base_lensN, dummyT)
210210
$ foldr1 (fn (x, y) => Const (lens_plusN, dummyT) $ x $ y)
211211
((case parent of NONE => [] | SOME (_, pname) => [Const (pname ^ "." ^ base_lensN, dummyT)]) @
212-
map (fn n => Const (theory_name thy ^ "." ^ tname ^ "." ^ n, dummyT)) fs)
212+
map (fn n => Const (theory_name {long = false} thy ^ "." ^ tname ^ "." ^ n, dummyT)) fs)
213213
)]))
214214
(prove_equiv tname thy)
215215
end
@@ -223,7 +223,7 @@ fun lenses_bij_proof tname parent thy fs =
223223
$ (const (bij_lensN) $
224224
(foldr1 (fn (x, y) => Const (lens_plusN, dummyT) $ x $ y)
225225
((case parent of NONE => [] | SOME (_, pname) => [Const (pname ^ "." ^ base_lensN, dummyT)]) @
226-
map (fn n => Const (theory_name thy ^ "." ^ tname ^ "." ^ n, dummyT)) (fs @ [child_lensN]))))
226+
map (fn n => Const (theory_name {long = false} thy ^ "." ^ tname ^ "." ^ n, dummyT)) (fs @ [child_lensN]))))
227227
]))
228228
(fn {context = context, prems = _}
229229
=> EVERY [ Locale.intro_locales_tac {strict = true, eager = true} context []
@@ -240,8 +240,8 @@ fun equiv_partition_proof tname thy =
240240
[ Const (Trueprop, dummyT)
241241
$ ( Const (lens_equivN, dummyT)
242242
$ ( Const (lens_plusN, dummyT)
243-
$ Const (theory_name thy ^ "." ^ tname ^ "." ^ base_lensN, dummyT)
244-
$ Const (theory_name thy ^ "." ^ tname ^ "." ^ child_lensN, dummyT))
243+
$ Const (theory_name {long = false} thy ^ "." ^ tname ^ "." ^ base_lensN, dummyT)
244+
$ Const (theory_name {long = false} thy ^ "." ^ tname ^ "." ^ child_lensN, dummyT))
245245
$ Const (id_lensN, dummyT)
246246
)]))
247247
(prove_equiv tname thy)
@@ -256,7 +256,7 @@ fun sublens_proof tname pname thy y x =
256256
(Proof_Context.init_global thy)
257257
[ Const (Trueprop, dummyT)
258258
$ ( Const (sublensN, dummyT)
259-
$ Const (Context.theory_name thy ^ "." ^ tname ^ "." ^ x, dummyT)
259+
$ Const (Context.theory_name {long = false} thy ^ "." ^ tname ^ "." ^ x, dummyT)
260260
$ Const (pname ^ "." ^ y, dummyT)
261261
)]))
262262
(prove_sublens tname thy)
@@ -270,10 +270,10 @@ fun quotient_proof tname thy x =
270270
[ Const (Trueprop, dummyT)
271271
$ ( Const (HOLeq, dummyT)
272272
$ (Const (lens_quotientN, dummyT)
273-
$ Const (Context.theory_name thy ^ "." ^ tname ^ "." ^ x, dummyT)
274-
$ Const (Context.theory_name thy ^ "." ^ tname ^ "." ^ base_lensN, dummyT)
273+
$ Const (Context.theory_name {long = false} thy ^ "." ^ tname ^ "." ^ x, dummyT)
274+
$ Const (Context.theory_name {long = false} thy ^ "." ^ tname ^ "." ^ base_lensN, dummyT)
275275
)
276-
$ Const (Context.theory_name thy ^ "." ^ tname ^ "." ^ x, dummyT)
276+
$ Const (Context.theory_name {long = false} thy ^ "." ^ tname ^ "." ^ x, dummyT)
277277
)]))
278278
(prove_quotient tname thy)
279279
end
@@ -286,10 +286,10 @@ fun composition_proof tname thy x =
286286
[ Const (Trueprop, dummyT)
287287
$ ( Const (HOLeq, dummyT)
288288
$ (Const (lens_compN, dummyT)
289-
$ Const (Context.theory_name thy ^ "." ^ tname ^ "." ^ x, dummyT)
290-
$ Const (Context.theory_name thy ^ "." ^ tname ^ "." ^ base_lensN, dummyT)
289+
$ Const (Context.theory_name {long = false} thy ^ "." ^ tname ^ "." ^ x, dummyT)
290+
$ Const (Context.theory_name {long = false} thy ^ "." ^ tname ^ "." ^ base_lensN, dummyT)
291291
)
292-
$ Const (Context.theory_name thy ^ "." ^ tname ^ "." ^ x, dummyT)
292+
$ Const (Context.theory_name {long = false} thy ^ "." ^ tname ^ "." ^ x, dummyT)
293293
)]))
294294
(prove_quotient tname thy)
295295
end
@@ -331,7 +331,7 @@ fun add_alphabet (params, binding) raw_parent ty_fields thy =
331331
|> (fn thy =>
332332
let
333333
(* Get the splitting theorems of all parents in reverse order *)
334-
val psplits = List.concat (map (#splits o Record.the_info thy) ((map snd (get_parents thy (Context.theory_name thy ^ "." ^ tname)))))
334+
val psplits = List.concat (map (#splits o Record.the_info thy) ((map snd (get_parents thy (Context.theory_name {long = false} thy ^ "." ^ tname)))))
335335
(* Remove the splitting theorems *)
336336
val thy1 = Context.theory_map (fold (Named_Theorems.del_thm "Lens_Instances.alpha_splits") psplits) thy
337337
(* Add them again, so they have lower priority than the child splitting theorems *)
@@ -351,7 +351,7 @@ fun add_alphabet (params, binding) raw_parent ty_fields thy =
351351
(* Add a bij lens proof for the summation of all constituent lenses and the more lens *)
352352
|> (fn thy => if raw_parent = NONE then snd (add_thm ((Binding.make (bij_lensesN, Position.none), lenses_bij_proof tname parent thy lnames), attrs) thy) else thy)
353353
(* Add sublens proofs *)
354-
|> (fn thy => snd (add_thmss [((Binding.make (sublensesN, Position.none), map (sublens_proof tname pname thy plchild) plnames @ map (sublens_proof tname (Context.theory_name thy ^ "." ^ tname) thy base_lensN) lnames), attrs)] thy))
354+
|> (fn thy => snd (add_thmss [((Binding.make (sublensesN, Position.none), map (sublens_proof tname pname thy plchild) plnames @ map (sublens_proof tname (Context.theory_name {long = false} thy ^ "." ^ tname) thy base_lensN) lnames), attrs)] thy))
355355
(* Add quotient proofs *)
356356
|> (fn thy => snd (add_thmss [((Binding.make (quotientsN, Position.none), map (quotient_proof tname thy) lnames), attrs)] thy))
357357
(* Add composition proofs *)

0 commit comments

Comments
 (0)