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