1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7(*
8  Requalify constants, types and facts into the current naming
9*)
10
11theory Requalify
12imports Main
13keywords "requalify_facts" :: thy_decl and "requalify_types" :: thy_decl and "requalify_consts" :: thy_decl and
14         "global_naming" :: thy_decl
15begin
16
17ML \<open>
18
19local
20
21
22fun all_facts_of ctxt =
23  let
24    val thy = Proof_Context.theory_of ctxt;
25    val global_facts = Global_Theory.facts_of thy;
26  in
27   Facts.dest_static false [] global_facts
28  end;
29
30fun global_fact ctxt nm =
31let
32   val facts = Proof_Context.facts_of ctxt;
33   val {name, thms, ...} = (Facts.retrieve (Context.Proof ctxt) facts (nm, Position.none));
34
35   fun tl' (_ :: xs) = xs
36     | tl' _ = []
37
38   fun matches suf (gnm, gthms)  =
39   let
40     val gsuf = Long_Name.explode gnm |> tl' |> tl' |> Long_Name.implode;
41
42   in suf = gsuf andalso eq_list (Thm.equiv_thm (Proof_Context.theory_of ctxt)) (thms, gthms)
43   end
44in
45  case Long_Name.dest_local name of NONE => (name, thms) | SOME suf =>
46    (case (find_first (matches suf) (all_facts_of ctxt)) of
47       SOME x => x
48     | NONE => raise Fail ("Couldn't find global equivalent of local fact: " ^ nm))
49end
50
51fun syntax_alias global_alias local_alias b (name : string) =
52  Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
53    let val b' = Morphism.binding phi b
54    in Context.mapping (global_alias b' name) (local_alias b' name) end);
55
56val alias_fact = syntax_alias Global_Theory.alias_fact Proof_Context.alias_fact;
57val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;
58val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
59
60in
61
62fun gen_requalify get_proper_nm parse_nm check_nm alias =
63  (Parse.opt_target  --  Scan.repeat1 (Parse.position (Scan.ahead parse_nm -- Parse.name))
64    >> (fn (target,bs) =>
65      Toplevel.local_theory NONE target (fn lthy =>
66      let
67
68        fun read_entry ((entry, t), pos) lthy =
69        let
70          val local_nm = get_proper_nm lthy t;
71          val _ = check_nm lthy (entry, (local_nm, pos));
72          val b = Binding.make (Long_Name.base_name t, pos)
73
74          val lthy' = lthy
75          |> alias b local_nm
76
77        in lthy' end
78
79       in fold read_entry bs lthy  end)))
80
81local
82
83val get_const_nm = ((fst o dest_Const) oo (Proof_Context.read_const {proper = true, strict = false}))
84val get_type_nm = ((fst o dest_Type) oo (Proof_Context.read_type_name {proper = true, strict = false}))
85val get_fact_nm = (fst oo global_fact)
86
87fun check_fact lthy (_, (nm, pos)) = Proof_Context.get_fact lthy (Facts.Named ((nm,pos), NONE))
88
89in
90
91val _ =
92  Outer_Syntax.command @{command_keyword requalify_consts} "alias const with current naming"
93    (gen_requalify get_const_nm Parse.const (fn lthy => fn (e, _) => get_const_nm lthy e) const_alias)
94
95val _ =
96  Outer_Syntax.command @{command_keyword requalify_types} "alias type with current naming"
97    (gen_requalify get_type_nm Parse.typ (fn lthy => fn (e, _) => get_type_nm lthy e) type_alias)
98
99val _ =
100  Outer_Syntax.command @{command_keyword requalify_facts} "alias fact with current naming"
101    (gen_requalify get_fact_nm Parse.thm check_fact alias_fact)
102
103val _ =
104  Outer_Syntax.command @{command_keyword global_naming} "change global naming of context block"
105    (Parse.binding >> (fn naming =>
106      Toplevel.local_theory NONE NONE
107        (Local_Theory.map_background_naming (Name_Space.parent_path #> Name_Space.qualified_path true naming))))
108
109end
110
111end
112\<close>
113
114(*Tests and examples *)
115
116locale Requalify_Locale
117begin
118
119typedecl requalify_type
120
121definition "requalify_const == (undefined :: requalify_type)"
122
123
124end
125
126typedecl requalify_type
127definition "requalify_const == (undefined :: requalify_type)"
128
129context Requalify_Locale begin global_naming Requalify_Locale2
130
131requalify_consts requalify_const
132requalify_types requalify_type
133requalify_facts requalify_const_def
134
135end
136
137term "requalify_const :: requalify_type"
138term "Requalify_Locale2.requalify_const :: Requalify_Locale2.requalify_type"
139lemma "Requalify_Locale2.requalify_const = (undefined :: Requalify_Locale2.requalify_type)"
140  by (simp add: Requalify_Locale2.requalify_const_def)
141
142consts requalify_test_f :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
143
144lemma
145  assumes f1: "requalify_test_f requalify_const Requalify_Locale2.requalify_const"
146  and f2: "requalify_test_f Requalify_Locale2.requalify_const Requalify.requalify_const"
147  shows "requalify_test_f Requalify_Locale2.requalify_const requalify_const" "requalify_const = undefined"
148  apply (rule f1)?
149  apply (rule f2)
150  apply (simp add: requalify_const_def)
151  done
152
153context Requalify_Locale begin
154
155lemma
156  assumes f1: "requalify_test_f requalify_const Requalify_Locale2.requalify_const"
157  and f2: "requalify_test_f Requalify_Locale2.requalify_const Requalify.requalify_const"
158  shows "requalify_test_f Requalify_Locale2.requalify_const requalify_const" "requalify_const = undefined"
159  apply (rule f2)?
160  apply (rule f1)
161  apply (simp add: requalify_const_def)
162  done
163
164end
165
166context Requalify_Locale begin global_naming global
167
168requalify_consts Requalify.requalify_const
169requalify_types Requalify.requalify_type
170requalify_facts Requalify.requalify_const_def
171
172end
173
174context Requalify_Locale begin
175
176lemma
177  assumes f1: "requalify_test_f requalify_const Requalify_Locale2.requalify_const"
178  and f2: "requalify_test_f Requalify_Locale2.requalify_const global.requalify_const"
179  shows "requalify_test_f Requalify_Locale2.requalify_const requalify_const" "requalify_const = undefined"
180  apply (rule f1)?
181  apply (rule f2)
182  apply (simp add: requalify_const_def)
183  done
184end
185
186context begin interpretation Requalify_Locale .
187
188lemma
189  assumes f1: "requalify_test_f requalify_const Requalify_Locale2.requalify_const"
190  and f2: "requalify_test_f Requalify_Locale2.requalify_const global.requalify_const"
191  shows "requalify_test_f Requalify_Locale2.requalify_const requalify_const" "requalify_const = undefined"
192  apply (rule f1)?
193  apply (rule f2)
194  apply (simp add: requalify_const_def)
195  done
196end
197
198locale Requalify_Locale3
199begin
200
201typedecl requalify_type2
202definition "requalify_const2 == (undefined :: requalify_type2)"
203
204end
205
206context begin interpretation Requalify_Locale3 .
207
208requalify_consts requalify_const2
209requalify_types requalify_type2
210requalify_facts requalify_const2_def
211
212end
213
214lemma "(requalify_const2 :: requalify_type2) = undefined"
215  by (simp add: requalify_const2_def)
216
217context Requalify_Locale3 begin
218
219lemma "(requalify_const2 :: requalify_type2) = undefined"
220  by (simp add: requalify_const2_def)
221
222end
223
224
225end
226