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