src/HOL/Import/HOL_Light_Maps.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63950 cdc1e59aa513
child 67399 eab6ce8368fa
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Import/HOL_Light_Maps.thy
     2     Author:     Cezary Kaliszyk, University of Innsbruck
     3     Author:     Alexander Krauss, QAware GmbH
     4 
     5 Based on earlier code by Steven Obua and Sebastian Skalberg
     6 *)
     7 
     8 section \<open>Type and constant mappings of HOL Light importer\<close>
     9 
    10 theory HOL_Light_Maps
    11 imports Import_Setup
    12 begin
    13 
    14 lemma [import_const T]:
    15   "True = ((\<lambda>p :: bool. p) = (\<lambda>p. p))"
    16   by simp
    17 
    18 lemma [import_const "/\\"]:
    19   "(op \<and>) = (\<lambda>p q. (\<lambda>f. f p q :: bool) = (\<lambda>f. f True True))"
    20   by metis
    21 
    22 lemma [import_const "==>"]:
    23   "(op \<longrightarrow>) = (\<lambda>(p::bool) q::bool. (p \<and> q) = p)"
    24   by auto
    25 
    26 lemma [import_const "!"]:
    27   "All = (\<lambda>P::'A \<Rightarrow> bool. P = (\<lambda>x::'A. True))"
    28   by auto
    29 
    30 lemma [import_const "?"]:
    31   "Ex = (\<lambda>P::'A \<Rightarrow> bool. All (\<lambda>q::bool. (All (\<lambda>x::'A::type. (P x) \<longrightarrow> q)) \<longrightarrow> q))"
    32   by auto
    33 
    34 lemma [import_const "\\/"]:
    35   "(op \<or>) = (\<lambda>p q. \<forall>r. (p \<longrightarrow> r) \<longrightarrow> (q \<longrightarrow> r) \<longrightarrow> r)"
    36   by auto
    37 
    38 lemma [import_const F]:
    39   "False = (\<forall>p. p)"
    40   by auto
    41 
    42 lemma [import_const "~"]:
    43   "Not = (\<lambda>p. p \<longrightarrow> False)"
    44   by simp
    45 
    46 lemma [import_const "?!"]:
    47   "Ex1 = (\<lambda>P::'A \<Rightarrow> bool. Ex P \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> x = y))"
    48   by auto
    49 
    50 lemma [import_const "_FALSITY_"]: "False = False"
    51   by simp
    52 
    53 lemma hl_ax1: "\<forall>t::'A \<Rightarrow> 'B. (\<lambda>x. t x) = t"
    54   by metis
    55 
    56 lemma hl_ax2: "\<forall>P x::'A. P x \<longrightarrow> P (Eps P)"
    57   by (auto intro: someI)
    58 
    59 lemma [import_const COND]:
    60   "If = (\<lambda>t (t1 :: 'A) t2. SOME x. (t = True \<longrightarrow> x = t1) \<and> (t = False \<longrightarrow> x = t2))"
    61   unfolding fun_eq_iff by auto
    62 
    63 lemma [import_const o]:
    64   "(op \<circ>) = (\<lambda>(f::'B \<Rightarrow> 'C) g x::'A. f (g x))"
    65   unfolding fun_eq_iff by simp
    66 
    67 lemma [import_const I]: "id = (\<lambda>x::'A. x)"
    68   by auto
    69 
    70 lemma [import_type 1 one_ABS one_REP]:
    71   "type_definition Rep_unit Abs_unit (Collect (\<lambda>b. b))"
    72   by (metis (full_types) Collect_cong singleton_conv2 type_definition_unit)
    73 
    74 lemma [import_const one]: "() = (SOME x::unit. True)"
    75   by auto
    76 
    77 lemma [import_const mk_pair]:
    78   "Pair_Rep = (\<lambda>(x::'A) (y::'B) (a::'A) b::'B. a = x \<and> b = y)"
    79   by (simp add: Pair_Rep_def fun_eq_iff)
    80 
    81 lemma [import_type prod ABS_prod REP_prod]:
    82   "type_definition Rep_prod Abs_prod (Collect (\<lambda>x::'A \<Rightarrow> 'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b))"
    83   using type_definition_prod[unfolded Product_Type.prod_def] by simp
    84 
    85 lemma [import_const ","]: "Pair = (\<lambda>(x::'A) y::'B. Abs_prod (Pair_Rep x y))"
    86   by (metis Pair_def)
    87 
    88 lemma [import_const FST]:
    89   "fst = (\<lambda>p::'A \<times> 'B. SOME x::'A. \<exists>y::'B. p = (x, y))"
    90   by auto
    91 
    92 lemma [import_const SND]:
    93   "snd = (\<lambda>p::'A \<times> 'B. SOME y::'B. \<exists>x::'A. p = (x, y))"
    94   by auto
    95 
    96 lemma CURRY_DEF[import_const CURRY]:
    97   "curry = (\<lambda>(f::'A \<times> 'B \<Rightarrow> 'C) x y. f (x, y))"
    98   using curry_def .
    99 
   100 lemma [import_const ONE_ONE : inj]:
   101   "inj = (\<lambda>(f::'A \<Rightarrow> 'B). \<forall>x1 x2. f x1 = f x2 \<longrightarrow> x1 = x2)"
   102   by (auto simp add: fun_eq_iff inj_on_def)
   103 
   104 lemma [import_const ONTO : surj]:
   105   "surj = (\<lambda>(f::'A \<Rightarrow> 'B). \<forall>y. \<exists>x. y = f x)"
   106   by (auto simp add: fun_eq_iff)
   107 
   108 lemma hl_ax3: "\<exists>f::ind \<Rightarrow> ind. inj f \<and> \<not> surj f"
   109   by (rule_tac x="Suc_Rep" in exI)
   110      (metis Suc_Rep_inject' injI Suc_Rep_not_Zero_Rep surjD)
   111 
   112 import_type_map num : nat
   113 import_const_map "_0" : zero_class.zero
   114 import_const_map SUC : Suc
   115 
   116 lemma NOT_SUC: "\<forall>n. Suc n \<noteq> 0"
   117   by simp
   118 
   119 lemma SUC_INJ: "\<forall>m n. (Suc m = Suc n) = (m = n)"
   120   by simp
   121 
   122 lemma num_INDUCTION:
   123   "\<forall>P. P 0 \<and> (\<forall>n. P n \<longrightarrow> P (Suc n)) \<longrightarrow> (\<forall>n. P n)"
   124   by (auto intro: nat.induct)
   125 
   126 lemma [import_const NUMERAL]: "id = (\<lambda>x :: nat. x)"
   127   by auto
   128 
   129 definition [simp]: "bit0 n = 2 * n"
   130 
   131 lemma [import_const BIT0]:
   132   "bit0 = (SOME fn. fn (id 0) = id 0 \<and> (\<forall>n. fn (Suc n) = Suc (Suc (fn n))))"
   133   apply (auto intro!: some_equality[symmetric])
   134   apply (auto simp add: fun_eq_iff)
   135   apply (induct_tac x)
   136   apply auto
   137   done
   138 
   139 definition [import_const BIT1, simp]:
   140   "bit1 = (\<lambda>x. Suc (bit0 x))"
   141 
   142 definition [simp]: "pred n = n - 1"
   143 
   144 lemma PRE[import_const PRE : pred]:
   145   "pred (id (0::nat)) = id (0::nat) \<and> (\<forall>n::nat. pred (Suc n) = n)"
   146   by simp
   147 
   148 lemma ADD[import_const "+" : plus]:
   149   "(\<forall>n :: nat. (id 0) + n = n) \<and> (\<forall>m n. (Suc m) + n = Suc (m + n))"
   150   by simp
   151 
   152 lemma MULT[import_const "*" : times]:
   153   "(\<forall>n :: nat. (id 0) * n = id 0) \<and> (\<forall>m n. (Suc m) * n = (m * n) + n)"
   154   by simp
   155 
   156 lemma EXP[import_const EXP : power]:
   157   "(\<forall>m. m ^ (id 0) = id (bit1 0)) \<and> (\<forall>(m :: nat) n. m ^ (Suc n) = m * (m ^ n))"
   158   by simp
   159 
   160 lemma LE[import_const "<=" : less_eq]:
   161   "(\<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))"
   162   by auto
   163 
   164 lemma LT[import_const "<" : less]:
   165   "(\<forall>m :: nat. m < (id 0) = False) \<and> (\<forall>m n. m < (Suc n) = (m = n \<or> m < n))"
   166   by auto
   167 
   168 lemma DEF_GE[import_const ">=" : greater_eq]:
   169   "(op \<ge>) = (\<lambda>x y :: nat. y \<le> x)"
   170   by simp
   171 
   172 lemma DEF_GT[import_const ">" : greater]:
   173   "(op >) = (\<lambda>x y :: nat. y < x)"
   174   by simp
   175 
   176 lemma DEF_MAX[import_const "MAX"]:
   177   "max = (\<lambda>x y :: nat. if x \<le> y then y else x)"
   178   by (auto simp add: max.absorb_iff2 fun_eq_iff)
   179 
   180 lemma DEF_MIN[import_const "MIN"]:
   181   "min = (\<lambda>x y :: nat. if x \<le> y then x else y)"
   182   by (auto simp add: min.absorb_iff1 fun_eq_iff)
   183 
   184 definition even
   185 where
   186   "even = Parity.even"
   187   
   188 lemma EVEN[import_const "EVEN" : even]:
   189   "even (id 0::nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))"
   190   by (simp add: even_def)
   191 
   192 lemma SUB[import_const "-" : minus]:
   193   "(\<forall>m::nat. m - (id 0) = m) \<and> (\<forall>m n. m - (Suc n) = pred (m - n))"
   194   by simp
   195 
   196 lemma FACT[import_const "FACT" : fact]:
   197   "fact (id 0) = id (bit1 0) \<and> (\<forall>n. fact (Suc n) = Suc n * fact n)"
   198   by simp
   199 
   200 import_const_map MOD : modulo
   201 import_const_map DIV : divide
   202 
   203 lemma DIVISION_0:
   204   "\<forall>m n::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"
   205   by simp
   206 
   207 lemmas [import_type sum "_dest_sum" "_mk_sum"] = type_definition_sum[where 'a="'A" and 'b="'B"]
   208 import_const_map INL : Inl
   209 import_const_map INR : Inr
   210 
   211 lemma sum_INDUCT:
   212   "\<forall>P. (\<forall>a :: 'A. P (Inl a)) \<and> (\<forall>a :: 'B. P (Inr a)) \<longrightarrow> (\<forall>x. P x)"
   213   by (auto intro: sum.induct)
   214 
   215 lemma sum_RECURSION:
   216   "\<forall>Inl' Inr'. \<exists>fn. (\<forall>a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \<and> (\<forall>a :: 'B. fn (Inr a) = Inr' a)"
   217   by (intro allI, rule_tac x="case_sum Inl' Inr'" in exI) auto
   218 
   219 lemma OUTL[import_const "OUTL" : projl]:
   220   "Sum_Type.projl (Inl x) = x"
   221   by simp
   222 
   223 lemma OUTR[import_const "OUTR" : projr]:
   224   "Sum_Type.projr (Inr y) = y"
   225   by simp
   226 
   227 import_type_map list : list
   228 import_const_map NIL : Nil
   229 import_const_map CONS : Cons
   230 
   231 lemma list_INDUCT:
   232   "\<forall>P::'A list \<Rightarrow> bool. P [] \<and> (\<forall>a0 a1. P a1 \<longrightarrow> P (a0 # a1)) \<longrightarrow> (\<forall>x. P x)"
   233   using list.induct by auto
   234 
   235 lemma list_RECURSION:
   236  "\<forall>nil' cons'. \<exists>fn::'A list \<Rightarrow> 'Z. fn [] = nil' \<and> (\<forall>(a0::'A) a1::'A list. fn (a0 # a1) = cons' a0 a1 (fn a1))"
   237   by (intro allI, rule_tac x="rec_list nil' cons'" in exI) auto
   238 
   239 lemma HD[import_const HD : hd]:
   240   "hd ((h::'A) # t) = h"
   241   by simp
   242 
   243 lemma TL[import_const TL : tl]:
   244   "tl ((h::'A) # t) = t"
   245   by simp
   246 
   247 lemma APPEND[import_const APPEND : append]:
   248   "(\<forall>l::'A list. [] @ l = l) \<and> (\<forall>(h::'A) t l. (h # t) @ l = h # t @ l)"
   249   by simp
   250 
   251 lemma REVERSE[import_const REVERSE : rev]:
   252   "rev [] = ([] :: 'A list) \<and> rev ((x::'A) # l) = rev l @ [x]"
   253   by simp
   254 
   255 lemma LENGTH[import_const LENGTH : length]:
   256   "length ([] :: 'A list) = id 0 \<and> (\<forall>(h::'A) t. length (h # t) = Suc (length t))"
   257   by simp
   258 
   259 lemma MAP[import_const MAP : map]:
   260   "(\<forall>f::'A \<Rightarrow> 'B. map f [] = []) \<and>
   261        (\<forall>(f::'A \<Rightarrow> 'B) h t. map f (h # t) = f h # map f t)"
   262   by simp
   263 
   264 lemma LAST[import_const LAST : last]:
   265   "last ((h::'A) # t) = (if t = [] then h else last t)"
   266   by simp
   267 
   268 lemma BUTLAST[import_const BUTLAST : butlast]:
   269     "butlast [] = ([] :: 't18337 list) \<and>
   270      butlast ((h :: 't18337) # t) = (if t = [] then [] else h # butlast t)"
   271   by simp
   272 
   273 lemma REPLICATE[import_const REPLICATE : replicate]:
   274   "replicate (id (0::nat)) (x::'t18358) = [] \<and>
   275    replicate (Suc n) x = x # replicate n x"
   276   by simp
   277 
   278 lemma NULL[import_const NULL : List.null]:
   279   "List.null ([]::'t18373 list) = True \<and> List.null ((h::'t18373) # t) = False"
   280   unfolding null_def by simp
   281 
   282 lemma ALL[import_const ALL : list_all]:
   283   "list_all (P::'t18393 \<Rightarrow> bool) [] = True \<and>
   284   list_all P (h # t) = (P h \<and> list_all P t)"
   285   by simp
   286 
   287 lemma EX[import_const EX : list_ex]:
   288   "list_ex (P::'t18414 \<Rightarrow> bool) [] = False \<and>
   289   list_ex P (h # t) = (P h \<or> list_ex P t)"
   290   by simp
   291 
   292 lemma ITLIST[import_const ITLIST : foldr]:
   293   "foldr (f::'t18437 \<Rightarrow> 't18436 \<Rightarrow> 't18436) [] b = b \<and>
   294   foldr f (h # t) b = f h (foldr f t b)"
   295   by simp
   296 
   297 lemma ALL2_DEF[import_const ALL2 : list_all2]:
   298   "list_all2 (P::'t18495 \<Rightarrow> 't18502 \<Rightarrow> bool) [] (l2::'t18502 list) = (l2 = []) \<and>
   299   list_all2 P ((h1::'t18495) # (t1::'t18495 list)) l2 =
   300   (if l2 = [] then False else P h1 (hd l2) \<and> list_all2 P t1 (tl l2))"
   301   by simp (induct_tac l2, simp_all)
   302 
   303 lemma FILTER[import_const FILTER : filter]:
   304   "filter (P::'t18680 \<Rightarrow> bool) [] = [] \<and>
   305   filter P ((h::'t18680) # t) = (if P h then h # filter P t else filter P t)"
   306   by simp
   307 
   308 lemma ZIP[import_const ZIP : zip]:
   309  "zip [] [] = ([] :: ('t18824 \<times> 't18825) list) \<and>
   310   zip ((h1::'t18849) # t1) ((h2::'t18850) # t2) = (h1, h2) # zip t1 t2"
   311   by simp
   312 
   313 lemma WF[import_const WF : wfP]:
   314   "\<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)))"
   315 proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
   316   fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q
   317   assume a: "xa \<in> Q"
   318   assume "\<forall>P. Ex P \<longrightarrow> (\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y))"
   319   then have "Ex (\<lambda>x. x \<in> Q) \<longrightarrow> (\<exists>xa. (\<lambda>x. x \<in> Q) xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> (\<lambda>x. x \<in> Q) y))" by auto
   320   then show "\<exists>z\<in>Q. \<forall>y. x y z \<longrightarrow> y \<notin> Q" using a by auto
   321 next
   322   fix x P and xa :: 'A and z
   323   assume "P xa" "z \<in> {a. P a}" "\<And>y. x y z \<Longrightarrow> y \<notin> {a. P a}"
   324   then show "\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y)" by auto
   325 qed auto
   326 
   327 end
   328