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