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