1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7(*
8 * Extend a locale by seamlessly generating sublocales.
9 *)
10
11theory Extend_Locale
12imports Main Defs
13keywords "extend_locale" :: thy_decl
14begin
15
16ML \<open>
17fun note_new_facts prev_lthy (lthy : local_theory) =
18let
19  val facts = Proof_Context.facts_of lthy;
20
21  val local_facts = Facts.dest_static false [Proof_Context.facts_of prev_lthy] facts;
22
23  val space = Facts.space_of (Proof_Context.facts_of lthy);
24
25  fun make_binding (long_name, pos) =
26    let val (qualifier, name) = split_last (Long_Name.explode long_name)
27    in fold (Binding.qualify true) qualifier (Binding.make (name, pos)) end;
28
29  fun add_entry (nm, thms) lthy =
30     let
31       val extern_nm = Name_Space.extern_shortest lthy space nm;
32       val {pos, ...} = Name_Space.the_entry space nm;
33       val b = make_binding (extern_nm, pos);
34       val (_, lthy') =  Local_Theory.note ((b,[]),thms) lthy;
35     in lthy' end
36
37in fold add_entry local_facts lthy end;
38\<close>
39
40ML \<open>
41
42val _ =
43  Outer_Syntax.command @{command_keyword extend_locale} "extend current locale"
44    (Parse.opt_target -- (Scan.repeat1 Parse_Spec.context_element) >> (fn (target, (elems)) =>
45      (Toplevel.local_theory NONE target (fn lthy =>
46      let
47        val locale_name = case Named_Target.locale_of lthy of SOME x => x | NONE => error "Not in a locale!"
48        val binding = Binding.make (Long_Name.base_name locale_name, Position.none)
49
50        val chunkN = "extchunk_"
51
52        val last_chunk =
53          case Long_Name.explode locale_name of
54            [_, chunk, _] => (unprefix chunkN chunk |> Int.fromString |> the)
55            | [_, _] => 0
56            | _ => raise Fail ("Unexpected locale naming scheme:" ^ locale_name)
57
58        val chunk = Int.toString (last_chunk + 1)
59
60
61        val (next_locale_name, lthy') = lthy
62          |> Local_Theory.map_background_naming
63               (Name_Space.parent_path #> Name_Space.add_path (chunkN ^ chunk))
64          |> Local_Theory.background_theory_result
65               (Expression.add_locale_cmd binding binding
66                  ([((locale_name,Position.none), (("#",false), (Expression.Positional [],[])))], []) elems
67                 ##> Local_Theory.exit_global)
68          ||> Local_Theory.restore_background_naming lthy
69
70
71        val lthy'' = lthy'
72          |> Local_Theory.exit_global
73          |> Named_Target.init next_locale_name
74
75      in lthy'' end)
76      )));
77
78\<close>
79
80locale Internal begin
81  definition "internal_const1 = True"
82  definition "internal_const2 = False"
83end
84
85locale Generic
86begin
87
88definition "generic_const = ((\<forall>x :: nat. x \<noteq> x))"
89
90extend_locale
91  assumes asm_1: "Internal.internal_const1 = (\<forall>x :: nat. x = x)"
92
93lemma generic_lemma_1: "Internal.internal_const1"
94  apply (insert asm_1)
95  apply simp
96  done
97
98extend_locale
99  assumes asm_2: "\<not> Internal.internal_const2"
100
101lemma generic_lemma_2: "generic_const = Internal.internal_const2"
102  by (simp add: asm_2 generic_const_def)
103
104extend_locale
105  fixes param_const_1 :: nat
106  assumes asm_3: "param_const_1 > 0"
107
108lemma generic_lemma_3: "param_const_1 \<noteq> 0"
109  by (simp add: asm_3)
110
111extend_locale
112  assumes asm_4: "\<not> generic_const"
113
114lemma generic_lemma_4: "generic_const = Internal.internal_const2"
115  by (simp add: asm_4 asm_2 generic_lemma_2)
116
117extend_locale
118  assumes asm_4: "x = param_const_1 \<Longrightarrow> y > x \<Longrightarrow> y > 1"
119
120
121end
122
123context Internal begin
124
125lemma internal_lemma1: "internal_const1 = (\<forall>x :: nat. x = x)" by (simp add: internal_const1_def)
126
127lemma internal_lemma2: "\<not> internal_const2" by (simp add: internal_const2_def)
128
129lemma internal_lemma3: "\<not> Generic.generic_const" by (simp add: Generic.generic_const_def)
130
131definition "internal_const3 = (1 :: nat)"
132
133lemma internal_lemma4: "internal_const3 > 0" by (simp add: internal_const3_def)
134
135lemma asm_4: "x = internal_const3 \<Longrightarrow> y > x \<Longrightarrow> y > 1"
136  by (simp add: internal_const3_def)
137
138end
139
140interpretation Generic
141 where param_const_1 = Internal.internal_const3
142  subgoal
143  proof -
144  interpret Internal .
145  show ?thesis
146    (* annoyingly, the proof method "fact" no longer has access to facts produced by "interpret" *)
147    apply (intro_locales; unfold_locales)
148        apply (rule internal_lemma1)
149       apply (rule internal_lemma2)
150      apply (rule internal_lemma4)
151     apply (rule internal_lemma3)
152    apply (erule (1) asm_4)
153    done
154  qed
155  done
156
157context Internal begin
158
159lemma internal_lemma5:
160  "internal_const3 \<noteq> 0"
161  by (rule generic_lemma_3)
162
163end
164
165
166end
167