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