src/HOL/Import/HOL4Compat.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 40607 30d512bf47a7
child 41413 64cd30d6b0b8
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     1 (*  Title:      HOL/Import/HOL4Compat.thy
     2     Author:     Sebastian Skalberg (TU Muenchen)
     3 *)
     4 
     5 theory HOL4Compat
     6 imports HOL4Setup Complex_Main "~~/src/HOL/Old_Number_Theory/Primes" ContNotDenum
     7 begin
     8 
     9 abbreviation (input) mem (infixl "mem" 55) where "x mem xs \<equiv> List.member xs x"
    10 no_notation differentiable (infixl "differentiable" 60)
    11 no_notation sums (infixr "sums" 80)
    12 
    13 lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
    14   by auto
    15 
    16 lemma COND_DEF:"(If b t f) = (@x. ((b = True) --> (x = t)) & ((b = False) --> (x = f)))"
    17   by auto
    18 
    19 definition LET :: "['a \<Rightarrow> 'b,'a] \<Rightarrow> 'b" where
    20   "LET f s == f s"
    21 
    22 lemma [hol4rew]: "LET f s = Let s f"
    23   by (simp add: LET_def Let_def)
    24 
    25 lemmas [hol4rew] = ONE_ONE_rew
    26 
    27 lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)"
    28   by simp
    29 
    30 lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))"
    31   by safe
    32 
    33 (*lemma INL_neq_INR: "ALL v1 v2. Sum_Type.Inr v2 ~= Sum_Type.Inl v1"
    34   by simp*)
    35 
    36 primrec ISL :: "'a + 'b => bool" where
    37   "ISL (Inl x) = True"
    38 | "ISL (Inr x) = False"
    39 
    40 primrec ISR :: "'a + 'b => bool" where
    41   "ISR (Inl x) = False"
    42 | "ISR (Inr x) = True"
    43 
    44 lemma ISL: "(ALL x. ISL (Inl x)) & (ALL y. ~ISL (Inr y))"
    45   by simp
    46 
    47 lemma ISR: "(ALL x. ISR (Inr x)) & (ALL y. ~ISR (Inl y))"
    48   by simp
    49 
    50 primrec OUTL :: "'a + 'b => 'a" where
    51   "OUTL (Inl x) = x"
    52 
    53 primrec OUTR :: "'a + 'b => 'b" where
    54   "OUTR (Inr x) = x"
    55 
    56 lemma OUTL: "OUTL (Inl x) = x"
    57   by simp
    58 
    59 lemma OUTR: "OUTR (Inr x) = x"
    60   by simp
    61 
    62 lemma sum_case_def: "(ALL f g x. sum_case f g (Inl x) = f x) & (ALL f g y. sum_case f g (Inr y) = g y)"
    63   by simp;
    64 
    65 lemma one: "ALL v. v = ()"
    66   by simp;
    67 
    68 lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)"
    69   by simp
    70 
    71 lemma OPTION_MAP_DEF: "(!f x. Option.map f (Some x) = Some (f x)) & (!f. Option.map f None = None)"
    72   by simp
    73 
    74 primrec IS_SOME :: "'a option => bool" where
    75   "IS_SOME (Some x) = True"
    76 | "IS_SOME None = False"
    77 
    78 primrec IS_NONE :: "'a option => bool" where
    79   "IS_NONE (Some x) = False"
    80 | "IS_NONE None = True"
    81 
    82 lemma IS_NONE_DEF: "(!x. IS_NONE (Some x) = False) & (IS_NONE None = True)"
    83   by simp
    84 
    85 lemma IS_SOME_DEF: "(!x. IS_SOME (Some x) = True) & (IS_SOME None = False)"
    86   by simp
    87 
    88 primrec OPTION_JOIN :: "'a option option => 'a option" where
    89   "OPTION_JOIN None = None"
    90 | "OPTION_JOIN (Some x) = x"
    91 
    92 lemma OPTION_JOIN_DEF: "(OPTION_JOIN None = None) & (ALL x. OPTION_JOIN (Some x) = x)"
    93   by simp
    94 
    95 lemma PAIR: "(fst x,snd x) = x"
    96   by simp
    97 
    98 lemma PAIR_MAP: "map_pair f g p = (f (fst p),g (snd p))"
    99   by (simp add: map_pair_def split_def)
   100 
   101 lemma pair_case_def: "split = split"
   102   ..;
   103 
   104 lemma LESS_OR_EQ: "m <= (n::nat) = (m < n | m = n)"
   105   by auto
   106 
   107 definition nat_gt :: "nat => nat => bool" where
   108   "nat_gt == %m n. n < m"
   109 
   110 definition nat_ge :: "nat => nat => bool" where
   111   "nat_ge == %m n. nat_gt m n | m = n"
   112 
   113 lemma [hol4rew]: "nat_gt m n = (n < m)"
   114   by (simp add: nat_gt_def)
   115 
   116 lemma [hol4rew]: "nat_ge m n = (n <= m)"
   117   by (auto simp add: nat_ge_def nat_gt_def)
   118 
   119 lemma GREATER_DEF: "ALL m n. (n < m) = (n < m)"
   120   by simp
   121 
   122 lemma GREATER_OR_EQ: "ALL m n. n <= (m::nat) = (n < m | m = n)"
   123   by auto
   124 
   125 lemma LESS_DEF: "m < n = (? P. (!n. P (Suc n) --> P n) & P m & ~P n)"
   126 proof safe
   127   assume "m < n"
   128   def P == "%n. n <= m"
   129   have "(!n. P (Suc n) \<longrightarrow> P n) & P m & ~P n"
   130   proof (auto simp add: P_def)
   131     assume "n <= m"
   132     from prems
   133     show False
   134       by auto
   135   qed
   136   thus "? P. (!n. P (Suc n) \<longrightarrow> P n) & P m & ~P n"
   137     by auto
   138 next
   139   fix P
   140   assume alln: "!n. P (Suc n) \<longrightarrow> P n"
   141   assume pm: "P m"
   142   assume npn: "~P n"
   143   have "!k q. q + k = m \<longrightarrow> P q"
   144   proof
   145     fix k
   146     show "!q. q + k = m \<longrightarrow> P q"
   147     proof (induct k,simp_all)
   148       show "P m" by fact
   149     next
   150       fix k
   151       assume ind: "!q. q + k = m \<longrightarrow> P q"
   152       show "!q. Suc (q + k) = m \<longrightarrow> P q"
   153       proof (rule+)
   154         fix q
   155         assume "Suc (q + k) = m"
   156         hence "(Suc q) + k = m"
   157           by simp
   158         with ind
   159         have psq: "P (Suc q)"
   160           by simp
   161         from alln
   162         have "P (Suc q) --> P q"
   163           ..
   164         with psq
   165         show "P q"
   166           by simp
   167       qed
   168     qed
   169   qed
   170   hence "!q. q + (m - n) = m \<longrightarrow> P q"
   171     ..
   172   hence hehe: "n + (m - n) = m \<longrightarrow> P n"
   173     ..
   174   show "m < n"
   175   proof (rule classical)
   176     assume "~(m<n)"
   177     hence "n <= m"
   178       by simp
   179     with hehe
   180     have "P n"
   181       by simp
   182     with npn
   183     show "m < n"
   184       ..
   185   qed
   186 qed;
   187 
   188 definition FUNPOW :: "('a => 'a) => nat => 'a => 'a" where
   189   "FUNPOW f n == f ^^ n"
   190 
   191 lemma FUNPOW: "(ALL f x. (f ^^ 0) x = x) &
   192   (ALL f n x. (f ^^ Suc n) x = (f ^^ n) (f x))"
   193   by (simp add: funpow_swap1)
   194 
   195 lemma [hol4rew]: "FUNPOW f n = f ^^ n"
   196   by (simp add: FUNPOW_def)
   197 
   198 lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))"
   199   by simp
   200 
   201 lemma MULT: "(!n. (0::nat) * n = 0) & (!m n. Suc m * n = m * n + n)"
   202   by simp
   203 
   204 lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
   205   by (simp) arith
   206 
   207 lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
   208   by (simp add: max_def)
   209 
   210 lemma MIN_DEF: "min (m::nat) n = (if m < n then m else n)"
   211   by (simp add: min_def)
   212 
   213 lemma DIVISION: "(0::nat) < n --> (!k. (k = k div n * n + k mod n) & k mod n < n)"
   214   by simp
   215 
   216 definition ALT_ZERO :: nat where 
   217   "ALT_ZERO == 0"
   218 
   219 definition NUMERAL_BIT1 :: "nat \<Rightarrow> nat" where 
   220   "NUMERAL_BIT1 n == n + (n + Suc 0)"
   221 
   222 definition NUMERAL_BIT2 :: "nat \<Rightarrow> nat" where 
   223   "NUMERAL_BIT2 n == n + (n + Suc (Suc 0))"
   224 
   225 definition NUMERAL :: "nat \<Rightarrow> nat" where 
   226   "NUMERAL x == x"
   227 
   228 lemma [hol4rew]: "NUMERAL ALT_ZERO = 0"
   229   by (simp add: ALT_ZERO_def NUMERAL_def)
   230 
   231 lemma [hol4rew]: "NUMERAL (NUMERAL_BIT1 ALT_ZERO) = 1"
   232   by (simp add: ALT_ZERO_def NUMERAL_BIT1_def NUMERAL_def)
   233 
   234 lemma [hol4rew]: "NUMERAL (NUMERAL_BIT2 ALT_ZERO) = 2"
   235   by (simp add: ALT_ZERO_def NUMERAL_BIT2_def NUMERAL_def)
   236 
   237 lemma EXP: "(!m. m ^ 0 = (1::nat)) & (!m n. m ^ Suc n = m * (m::nat) ^ n)"
   238   by auto
   239 
   240 lemma num_case_def: "(!b f. nat_case b f 0 = b) & (!b f n. nat_case b f (Suc n) = f n)"
   241   by simp;
   242 
   243 lemma divides_def: "(a::nat) dvd b = (? q. b = q * a)"
   244   by (auto simp add: dvd_def);
   245 
   246 lemma list_case_def: "(!v f. list_case v f [] = v) & (!v f a0 a1. list_case v f (a0#a1) = f a0 a1)"
   247   by simp
   248 
   249 primrec list_size :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat" where
   250   "list_size f [] = 0"
   251 | "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)"
   252 
   253 lemma list_size_def': "(!f. list_size f [] = 0) &
   254          (!f a0 a1. list_size f (a0#a1) = 1 + (f a0 + list_size f a1))"
   255   by simp
   256 
   257 lemma list_case_cong: "! M M' v f. M = M' & (M' = [] \<longrightarrow>  v = v') &
   258            (!a0 a1. (M' = a0#a1) \<longrightarrow> (f a0 a1 = f' a0 a1)) -->
   259            (list_case v f M = list_case v' f' M')"
   260 proof clarify
   261   fix M M' v f
   262   assume "M' = [] \<longrightarrow> v = v'"
   263     and "!a0 a1. M' = a0 # a1 \<longrightarrow> f a0 a1 = f' a0 a1"
   264   show "list_case v f M' = list_case v' f' M'"
   265   proof (rule List.list.case_cong)
   266     show "M' = M'"
   267       ..
   268   next
   269     assume "M' = []"
   270     with prems
   271     show "v = v'"
   272       by auto
   273   next
   274     fix a0 a1
   275     assume "M' = a0 # a1"
   276     with prems
   277     show "f a0 a1 = f' a0 a1"
   278       by auto
   279   qed
   280 qed
   281 
   282 lemma list_Axiom: "ALL f0 f1. EX fn. (fn [] = f0) & (ALL a0 a1. fn (a0#a1) = f1 a0 a1 (fn a1))"
   283 proof safe
   284   fix f0 f1
   285   def fn == "list_rec f0 f1"
   286   have "fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))"
   287     by (simp add: fn_def)
   288   thus "EX fn. fn [] = f0 & (ALL a0 a1. fn (a0 # a1) = f1 a0 a1 (fn a1))"
   289     by auto
   290 qed
   291 
   292 lemma list_Axiom_old: "EX! fn. (fn [] = x) & (ALL h t. fn (h#t) = f (fn t) h t)"
   293 proof safe
   294   def fn == "list_rec x (%h t r. f r h t)"
   295   have "fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)"
   296     by (simp add: fn_def)
   297   thus "EX fn. fn [] = x & (ALL h t. fn (h # t) = f (fn t) h t)"
   298     by auto
   299 next
   300   fix fn1 fn2
   301   assume "ALL h t. fn1 (h # t) = f (fn1 t) h t"
   302   assume "ALL h t. fn2 (h # t) = f (fn2 t) h t"
   303   assume "fn2 [] = fn1 []"
   304   show "fn1 = fn2"
   305   proof
   306     fix xs
   307     show "fn1 xs = fn2 xs"
   308       by (induct xs,simp_all add: prems) 
   309   qed
   310 qed
   311 
   312 lemma NULL_DEF: "(List.null [] = True) & (!h t. List.null (h # t) = False)"
   313   by (simp add: null_def)
   314 
   315 definition sum :: "nat list \<Rightarrow> nat" where
   316   "sum l == foldr (op +) l 0"
   317 
   318 lemma SUM: "(sum [] = 0) & (!h t. sum (h#t) = h + sum t)"
   319   by (simp add: sum_def)
   320 
   321 lemma APPEND: "(!l. [] @ l = l) & (!l1 l2 h. (h#l1) @ l2 = h# l1 @ l2)"
   322   by simp
   323 
   324 lemma FLAT: "(concat [] = []) & (!h t. concat (h#t) = h @ (concat t))"
   325   by simp
   326 
   327 lemma LENGTH: "(length [] = 0) & (!h t. length (h#t) = Suc (length t))"
   328   by simp
   329 
   330 lemma MAP: "(!f. map f [] = []) & (!f h t. map f (h#t) = f h#map f t)"
   331   by simp
   332 
   333 lemma MEM: "(!x. List.member [] x = False) & (!x h t. List.member (h#t) x = ((x = h) | List.member t x))"
   334   by (simp add: member_def)
   335 
   336 lemma FILTER: "(!P. filter P [] = []) & (!P h t.
   337            filter P (h#t) = (if P h then h#filter P t else filter P t))"
   338   by simp
   339 
   340 lemma REPLICATE: "(ALL x. replicate 0 x = []) &
   341   (ALL n x. replicate (Suc n) x = x # replicate n x)"
   342   by simp
   343 
   344 definition FOLDR :: "[['a,'b]\<Rightarrow>'b,'b,'a list] \<Rightarrow> 'b" where
   345   "FOLDR f e l == foldr f l e"
   346 
   347 lemma [hol4rew]: "FOLDR f e l = foldr f l e"
   348   by (simp add: FOLDR_def)
   349 
   350 lemma FOLDR: "(!f e. foldr f [] e = e) & (!f e x l. foldr f (x#l) e = f x (foldr f l e))"
   351   by simp
   352 
   353 lemma FOLDL: "(!f e. foldl f e [] = e) & (!f e x l. foldl f e (x#l) = foldl f (f e x) l)"
   354   by simp
   355 
   356 lemma EVERY_DEF: "(!P. list_all P [] = True) & (!P h t. list_all P (h#t) = (P h & list_all P t))"
   357   by simp
   358 
   359 lemma list_exists_DEF: "(!P. list_ex P [] = False) & (!P h t. list_ex P (h#t) = (P h | list_ex P t))"
   360   by simp
   361 
   362 primrec map2 :: "[['a,'b]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> 'c list" where
   363   map2_Nil: "map2 f [] l2 = []"
   364 | map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)"
   365 
   366 lemma MAP2: "(!f. map2 f [] [] = []) & (!f h1 t1 h2 t2. map2 f (h1#t1) (h2#t2) = f h1 h2#map2 f t1 t2)"
   367   by simp
   368 
   369 lemma list_INDUCT: "\<lbrakk> P [] ; !t. P t \<longrightarrow> (!h. P (h#t)) \<rbrakk> \<Longrightarrow> !l. P l"
   370 proof
   371   fix l
   372   assume "P []"
   373   assume allt: "!t. P t \<longrightarrow> (!h. P (h # t))"
   374   show "P l"
   375   proof (induct l)
   376     show "P []" by fact
   377   next
   378     fix h t
   379     assume "P t"
   380     with allt
   381     have "!h. P (h # t)"
   382       by auto
   383     thus "P (h # t)"
   384       ..
   385   qed
   386 qed
   387 
   388 lemma list_CASES: "(l = []) | (? t h. l = h#t)"
   389   by (induct l,auto)
   390 
   391 definition ZIP :: "'a list * 'b list \<Rightarrow> ('a * 'b) list" where
   392   "ZIP == %(a,b). zip a b"
   393 
   394 lemma ZIP: "(zip [] [] = []) &
   395   (!x1 l1 x2 l2. zip (x1#l1) (x2#l2) = (x1,x2)#zip l1 l2)"
   396   by simp
   397 
   398 lemma [hol4rew]: "ZIP (a,b) = zip a b"
   399   by (simp add: ZIP_def)
   400 
   401 primrec unzip :: "('a * 'b) list \<Rightarrow> 'a list * 'b list" where
   402   unzip_Nil: "unzip [] = ([],[])"
   403 | unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))"
   404 
   405 lemma UNZIP: "(unzip [] = ([],[])) &
   406          (!x l. unzip (x#l) = (fst x#fst (unzip l),snd x#snd (unzip l)))"
   407   by (simp add: Let_def)
   408 
   409 lemma REVERSE: "(rev [] = []) & (!h t. rev (h#t) = (rev t) @ [h])"
   410   by simp;
   411 
   412 lemma REAL_SUP_ALLPOS: "\<lbrakk> ALL x. P (x::real) \<longrightarrow> 0 < x ; EX x. P x; EX z. ALL x. P x \<longrightarrow> x < z \<rbrakk> \<Longrightarrow> EX s. ALL y. (EX x. P x & y < x) = (y < s)"
   413 proof safe
   414   fix x z
   415   assume allx: "ALL x. P x \<longrightarrow> 0 < x"
   416   assume px: "P x"
   417   assume allx': "ALL x. P x \<longrightarrow> x < z"
   418   have "EX s. ALL y. (EX x : Collect P. y < x) = (y < s)"
   419   proof (rule posreal_complete)
   420     show "ALL x : Collect P. 0 < x"
   421     proof safe
   422       fix x
   423       assume "P x"
   424       from allx
   425       have "P x \<longrightarrow> 0 < x"
   426         ..
   427       thus "0 < x"
   428         by (simp add: prems)
   429     qed
   430   next
   431     from px
   432     show "EX x. x : Collect P"
   433       by auto
   434   next
   435     from allx'
   436     show "EX y. ALL x : Collect P. x < y"
   437       apply simp
   438       ..
   439   qed
   440   thus "EX s. ALL y. (EX x. P x & y < x) = (y < s)"
   441     by simp
   442 qed
   443 
   444 lemma REAL_10: "~((1::real) = 0)"
   445   by simp
   446 
   447 lemma REAL_ADD_ASSOC: "(x::real) + (y + z) = x + y + z"
   448   by simp
   449 
   450 lemma REAL_MUL_ASSOC: "(x::real) * (y * z) = x * y * z"
   451   by simp
   452 
   453 lemma REAL_ADD_LINV:  "-x + x = (0::real)"
   454   by simp
   455 
   456 lemma REAL_MUL_LINV: "x ~= (0::real) ==> inverse x * x = 1"
   457   by simp
   458 
   459 lemma REAL_LT_TOTAL: "((x::real) = y) | x < y | y < x"
   460   by auto;
   461 
   462 lemma [hol4rew]: "real (0::nat) = 0"
   463   by simp
   464 
   465 lemma [hol4rew]: "real (1::nat) = 1"
   466   by simp
   467 
   468 lemma [hol4rew]: "real (2::nat) = 2"
   469   by simp
   470 
   471 lemma real_lte: "((x::real) <= y) = (~(y < x))"
   472   by auto
   473 
   474 lemma real_of_num: "((0::real) = 0) & (!n. real (Suc n) = real n + 1)"
   475   by (simp add: real_of_nat_Suc)
   476 
   477 lemma abs: "abs (x::real) = (if 0 <= x then x else -x)"
   478   by (simp add: abs_if)
   479 
   480 lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)"
   481   by simp
   482 
   483 definition real_gt :: "real => real => bool" where 
   484   "real_gt == %x y. y < x"
   485 
   486 lemma [hol4rew]: "real_gt x y = (y < x)"
   487   by (simp add: real_gt_def)
   488 
   489 lemma real_gt: "ALL x (y::real). (y < x) = (y < x)"
   490   by simp
   491 
   492 definition real_ge :: "real => real => bool" where
   493   "real_ge x y == y <= x"
   494 
   495 lemma [hol4rew]: "real_ge x y = (y <= x)"
   496   by (simp add: real_ge_def)
   497 
   498 lemma real_ge: "ALL x y. (y <= x) = (y <= x)"
   499   by simp
   500 
   501 end