# HG changeset patch
# User wenzelm
# Date 1395673615 -3600
# Node ID da5f22a60cb3416a3a21a0c484b82fdfd9ccb3c4
# Parent  785569927666eea41564a4e8e3d18c71bf8970b4
formal check of user input, avoiding direct references of interal names;

diff -r 785569927666 -r da5f22a60cb3 src/HOL/Import/HOL_Light_Maps.thy
--- a/src/HOL/Import/HOL_Light_Maps.thy	Mon Mar 24 12:00:17 2014 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy	Mon Mar 24 16:06:55 2014 +0100
@@ -97,11 +97,11 @@
   "curry = (\<lambda>(f\<Colon>'A \<times> 'B \<Rightarrow> 'C) x y. f (x, y))"
   using curry_def .
 
-lemma [import_const ONE_ONE : Fun.inj]:
+lemma [import_const ONE_ONE : inj]:
   "inj = (\<lambda>(f\<Colon>'A \<Rightarrow> 'B). \<forall>x1 x2. f x1 = f x2 \<longrightarrow> x1 = x2)"
   by (auto simp add: fun_eq_iff inj_on_def)
 
-lemma [import_const ONTO : Fun.surj]:
+lemma [import_const ONTO : surj]:
   "surj = (\<lambda>(f\<Colon>'A \<Rightarrow> 'B). \<forall>y. \<exists>x. y = f x)"
   by (auto simp add: fun_eq_iff)
 
@@ -109,9 +109,9 @@
   by (rule_tac x="Suc_Rep" in exI)
      (metis Suc_Rep_inject' injI Suc_Rep_not_Zero_Rep surjD)
 
-import_type_map num : Nat.nat
-import_const_map "_0" : Groups.zero_class.zero
-import_const_map SUC : Nat.Suc
+import_type_map num : nat
+import_const_map "_0" : zero_class.zero
+import_const_map SUC : Suc
 
 lemma NOT_SUC: "\<forall>n. Suc n \<noteq> 0"
   by simp
@@ -141,35 +141,35 @@
 
 definition [simp]: "pred n = n - 1"
 
-lemma PRE[import_const PRE : HOL_Light_Maps.pred]:
+lemma PRE[import_const PRE : pred]:
   "pred (id (0\<Colon>nat)) = id (0\<Colon>nat) \<and> (\<forall>n\<Colon>nat. pred (Suc n) = n)"
   by simp
 
-lemma ADD[import_const "+" : Groups.plus_class.plus]:
+lemma ADD[import_const "+" : plus]:
   "(\<forall>n :: nat. (id 0) + n = n) \<and> (\<forall>m n. (Suc m) + n = Suc (m + n))"
   by simp
 
-lemma MULT[import_const "*" : Groups.times_class.times]:
+lemma MULT[import_const "*" : times]:
   "(\<forall>n :: nat. (id 0) * n = id 0) \<and> (\<forall>m n. (Suc m) * n = (m * n) + n)"
   by simp
 
-lemma EXP[import_const EXP : Power.power_class.power]:
+lemma EXP[import_const EXP : power]:
   "(\<forall>m. m ^ (id 0) = id (bit1 0)) \<and> (\<forall>(m :: nat) n. m ^ (Suc n) = m * (m ^ n))"
   by simp
 
-lemma LE[import_const "<=" : Orderings.ord_class.less_eq]:
+lemma LE[import_const "<=" : less_eq]:
   "(\<forall>m :: nat. m \<le> (id 0) = (m = id 0)) \<and> (\<forall>m n. m \<le> (Suc n) = (m = Suc n \<or> m \<le> n))"
   by auto
 
-lemma LT[import_const "<" : Orderings.ord_class.less]:
+lemma LT[import_const "<" : less]:
   "(\<forall>m :: nat. m < (id 0) = False) \<and> (\<forall>m n. m < (Suc n) = (m = n \<or> m < n))"
   by auto
 
-lemma DEF_GE[import_const ">=" : "Orderings.ord_class.greater_eq"]:
+lemma DEF_GE[import_const ">=" : greater_eq]:
   "(op \<ge>) = (\<lambda>x y :: nat. y \<le> x)"
   by simp
 
-lemma DEF_GT[import_const ">" : "Orderings.ord_class.greater"]:
+lemma DEF_GT[import_const ">" : greater]:
   "(op >) = (\<lambda>x y :: nat. y < x)"
   by simp
 
@@ -181,28 +181,28 @@
   "min = (\<lambda>x y :: nat. if x \<le> y then x else y)"
   by (auto simp add: min.absorb_iff1 fun_eq_iff)
 
-lemma EVEN[import_const "EVEN" : "Parity.even_odd_class.even"]:
+lemma EVEN[import_const "EVEN" : even]:
   "even (id 0\<Colon>nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))"
   by simp
 
-lemma SUB[import_const "-" : "Groups.minus_class.minus"]:
+lemma SUB[import_const "-" : minus]:
   "(\<forall>m\<Colon>nat. m - (id 0) = m) \<and> (\<forall>m n. m - (Suc n) = pred (m - n))"
   by simp
 
-lemma FACT[import_const "FACT" : "Fact.fact_class.fact"]:
+lemma FACT[import_const "FACT" : fact]:
   "fact (id 0) = id (bit1 0) \<and> (\<forall>n. fact (Suc n) = Suc n * fact n)"
   by simp
 
-import_const_map MOD : Divides.div_class.mod
-import_const_map DIV : Divides.div_class.div
+import_const_map MOD : mod
+import_const_map DIV : div
 
 lemma DIVISION_0:
   "\<forall>m n\<Colon>nat. if n = id 0 then m div n = id 0 \<and> m mod n = m else m = m div n * n + m mod n \<and> m mod n < n"
   by simp
 
 lemmas [import_type sum "_dest_sum" "_mk_sum"] = type_definition_sum[where 'a="'A" and 'b="'B"]
-import_const_map INL : Sum_Type.Inl
-import_const_map INR : Sum_Type.Inr
+import_const_map INL : Inl
+import_const_map INR : Inr
 
 lemma sum_INDUCT:
   "\<forall>P. (\<forall>a :: 'A. P (Inl a)) \<and> (\<forall>a :: 'B. P (Inr a)) \<longrightarrow> (\<forall>x. P x)"
@@ -212,17 +212,17 @@
   "\<forall>Inl' Inr'. \<exists>fn. (\<forall>a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \<and> (\<forall>a :: 'B. fn (Inr a) = Inr' a)"
   by (intro allI, rule_tac x="case_sum Inl' Inr'" in exI) auto
 
-lemma OUTL[import_const "OUTL" : "Sum_Type.projl"]:
+lemma OUTL[import_const "OUTL" : projl]:
   "Sum_Type.projl (Inl x) = x"
   by simp
 
-lemma OUTR[import_const "OUTR" : "Sum_Type.projr"]:
+lemma OUTR[import_const "OUTR" : projr]:
   "Sum_Type.projr (Inr y) = y"
   by simp
 
-import_type_map list : List.list
-import_const_map NIL : List.list.Nil
-import_const_map CONS : List.list.Cons
+import_type_map list : list
+import_const_map NIL : Nil
+import_const_map CONS : Cons
 
 lemma list_INDUCT:
   "\<forall>P\<Colon>'A list \<Rightarrow> bool. P [] \<and> (\<forall>a0 a1. P a1 \<longrightarrow> P (a0 # a1)) \<longrightarrow> (\<forall>x. P x)"
@@ -232,41 +232,41 @@
  "\<forall>nil' cons'. \<exists>fn\<Colon>'A list \<Rightarrow> 'Z. fn [] = nil' \<and> (\<forall>(a0\<Colon>'A) a1\<Colon>'A list. fn (a0 # a1) = cons' a0 a1 (fn a1))"
   by (intro allI, rule_tac x="rec_list nil' cons'" in exI) auto
 
-lemma HD[import_const HD : List.list.hd]:
+lemma HD[import_const HD : hd]:
   "hd ((h\<Colon>'A) # t) = h"
   by simp
 
-lemma TL[import_const TL : List.list.tl]:
+lemma TL[import_const TL : tl]:
   "tl ((h\<Colon>'A) # t) = t"
   by simp
 
-lemma APPEND[import_const APPEND : List.append]:
+lemma APPEND[import_const APPEND : append]:
   "(\<forall>l\<Colon>'A list. [] @ l = l) \<and> (\<forall>(h\<Colon>'A) t l. (h # t) @ l = h # t @ l)"
   by simp
 
-lemma REVERSE[import_const REVERSE : List.rev]:
+lemma REVERSE[import_const REVERSE : rev]:
   "rev [] = ([] :: 'A list) \<and> rev ((x\<Colon>'A) # l) = rev l @ [x]"
   by simp
 
-lemma LENGTH[import_const LENGTH : List.length]:
+lemma LENGTH[import_const LENGTH : length]:
   "length ([] :: 'A list) = id 0 \<and> (\<forall>(h\<Colon>'A) t. length (h # t) = Suc (length t))"
   by simp
 
-lemma MAP[import_const MAP : List.list.map]:
+lemma MAP[import_const MAP : map]:
   "(\<forall>f\<Colon>'A \<Rightarrow> 'B. map f [] = []) \<and>
        (\<forall>(f\<Colon>'A \<Rightarrow> 'B) h t. map f (h # t) = f h # map f t)"
   by simp
 
-lemma LAST[import_const LAST : List.last]:
+lemma LAST[import_const LAST : last]:
   "last ((h\<Colon>'A) # t) = (if t = [] then h else last t)"
   by simp
 
-lemma BUTLAST[import_const BUTLAST : List.butlast]:
+lemma BUTLAST[import_const BUTLAST : butlast]:
     "butlast [] = ([] :: 't18337 list) \<and>
      butlast ((h :: 't18337) # t) = (if t = [] then [] else h # butlast t)"
   by simp
 
-lemma REPLICATE[import_const REPLICATE : List.replicate]:
+lemma REPLICATE[import_const REPLICATE : replicate]:
   "replicate (id (0\<Colon>nat)) (x\<Colon>'t18358) = [] \<and>
    replicate (Suc n) x = x # replicate n x"
   by simp
@@ -275,38 +275,38 @@
   "List.null ([]\<Colon>'t18373 list) = True \<and> List.null ((h\<Colon>'t18373) # t) = False"
   unfolding null_def by simp
 
-lemma ALL[import_const ALL : List.list_all]:
+lemma ALL[import_const ALL : list_all]:
   "list_all (P\<Colon>'t18393 \<Rightarrow> bool) [] = True \<and>
   list_all P (h # t) = (P h \<and> list_all P t)"
   by simp
 
-lemma EX[import_const EX : List.list_ex]:
+lemma EX[import_const EX : list_ex]:
   "list_ex (P\<Colon>'t18414 \<Rightarrow> bool) [] = False \<and>
   list_ex P (h # t) = (P h \<or> list_ex P t)"
   by simp
 
-lemma ITLIST[import_const ITLIST : List.foldr]:
+lemma ITLIST[import_const ITLIST : foldr]:
   "foldr (f\<Colon>'t18437 \<Rightarrow> 't18436 \<Rightarrow> 't18436) [] b = b \<and>
   foldr f (h # t) b = f h (foldr f t b)"
   by simp
 
-lemma ALL2_DEF[import_const ALL2 : List.list.list_all2]:
+lemma ALL2_DEF[import_const ALL2 : list_all2]:
   "list_all2 (P\<Colon>'t18495 \<Rightarrow> 't18502 \<Rightarrow> bool) [] (l2\<Colon>'t18502 list) = (l2 = []) \<and>
   list_all2 P ((h1\<Colon>'t18495) # (t1\<Colon>'t18495 list)) l2 =
   (if l2 = [] then False else P h1 (hd l2) \<and> list_all2 P t1 (tl l2))"
   by simp (induct_tac l2, simp_all)
 
-lemma FILTER[import_const FILTER : List.filter]:
+lemma FILTER[import_const FILTER : filter]:
   "filter (P\<Colon>'t18680 \<Rightarrow> bool) [] = [] \<and>
   filter P ((h\<Colon>'t18680) # t) = (if P h then h # filter P t else filter P t)"
   by simp
 
-lemma ZIP[import_const ZIP : List.zip]:
+lemma ZIP[import_const ZIP : zip]:
  "zip [] [] = ([] :: ('t18824 \<times> 't18825) list) \<and>
   zip ((h1\<Colon>'t18849) # t1) ((h2\<Colon>'t18850) # t2) = (h1, h2) # zip t1 t2"
   by simp
 
-lemma WF[import_const WF : Wellfounded.wfP]:
+lemma WF[import_const WF : wfP]:
   "\<forall>u. wfP u \<longleftrightarrow> (\<forall>P. (\<exists>x :: 'A. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
 proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
   fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q
diff -r 785569927666 -r da5f22a60cb3 src/HOL/Import/import_data.ML
--- a/src/HOL/Import/import_data.ML	Mon Mar 24 12:00:17 2014 +0100
+++ b/src/HOL/Import/import_data.ML	Mon Mar 24 16:06:55 2014 +0100
@@ -13,7 +13,9 @@
   val get_typ_def : string -> theory -> thm option
 
   val add_const_map : string -> string -> theory -> theory
+  val add_const_map_cmd : string -> string -> theory -> theory
   val add_typ_map : string -> string -> theory -> theory
+  val add_typ_map_cmd : string -> string -> theory -> theory
   val add_const_def : string -> thm -> string option -> theory -> theory
   val add_typ_def : string -> string -> string -> thm -> theory -> theory
 end
@@ -49,11 +51,23 @@
     {const_map = (Symtab.update (s1, s2) const_map), ty_map = ty_map,
      const_def = const_def, ty_def = ty_def}) thy
 
+fun add_const_map_cmd s1 raw_s2 thy =
+  let
+    val ctxt = Proof_Context.init_global thy
+    val Const (s2, _) = Proof_Context.read_const {proper = true, strict = false} ctxt raw_s2
+  in add_const_map s1 s2 thy end
+
 fun add_typ_map s1 s2 thy =
   Data.map (fn {const_map, ty_map, const_def, ty_def} =>
     {const_map = const_map, ty_map = (Symtab.update (s1, s2) ty_map),
      const_def = const_def, ty_def = ty_def}) thy
 
+fun add_typ_map_cmd s1 raw_s2 thy =
+  let
+    val ctxt = Proof_Context.init_global thy
+    val Type (s2, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt raw_s2
+  in add_typ_map s1 s2 thy end
+
 fun add_const_def s th name_opt thy =
   let
     val th = Thm.legacy_freezeT th
@@ -89,7 +103,8 @@
 
 val _ = Theory.setup
   (Attrib.setup @{binding import_const}
-    (Scan.lift (Parse.name -- Scan.option (@{keyword ":"} |-- Parse.xname)) >>
+    (Scan.lift Parse.name --
+      Scan.option (Scan.lift @{keyword ":"} |-- Args.const {proper = true, strict = false}) >>
       (fn (s1, s2) => Thm.declaration_attribute
         (fn th => Context.mapping (add_const_def s1 th s2) I)))
   "declare a theorem as an equality that maps the given constant")
@@ -104,14 +119,14 @@
 val _ =
   Outer_Syntax.command @{command_spec "import_type_map"}
     "map external type name to existing Isabelle/HOL type name"
-    ((Parse.name --| @{keyword ":"}) -- Parse.xname >>
-      (fn (ty_name1, ty_name2) => Toplevel.theory (add_typ_map ty_name1 ty_name2)))
+    ((Parse.name --| @{keyword ":"}) -- Parse.type_const >>
+      (fn (ty_name1, ty_name2) => Toplevel.theory (add_typ_map_cmd ty_name1 ty_name2)))
 
 val _ =
   Outer_Syntax.command @{command_spec "import_const_map"}
     "map external const name to existing Isabelle/HOL const name"
-    ((Parse.name --| @{keyword ":"}) -- Parse.xname >>
-      (fn (cname1, cname2) => Toplevel.theory (add_const_map cname1 cname2)))
+    ((Parse.name --| @{keyword ":"}) -- Parse.const >>
+      (fn (cname1, cname2) => Toplevel.theory (add_const_map_cmd cname1 cname2)))
 
 (* Initial type and constant maps, for types and constants that are not
    defined, which means their definitions do not appear in the proof dump *)