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