src/HOL/Import/HOLLightCompat.thy
author wenzelm
Sun Jan 16 15:53:03 2011 +0100 (2011-01-16)
changeset 41589 bbd861837ebc
parent 35416 d8d7d1b785af
child 43787 5be84619e4d4
permissions -rw-r--r--
tuned headers;
     1 (*  Title:      HOL/Import/HOLLightCompat.thy
     2     Author:     Steven Obua and Sebastian Skalberg, TU Muenchen
     3 *)
     4 
     5 theory HOLLightCompat imports HOL4Setup HOL4Compat Divides Primes Real begin
     6 
     7 lemma light_imp_def: "(t1 --> t2) = ((t1 & t2) = t1)"
     8   by auto;
     9 
    10 lemma comb_rule: "[| P1 = P2 ; Q1 = Q2 |] ==> P1 Q1 = P2 Q2"
    11   by simp
    12 
    13 lemma light_and_def: "(t1 & t2) = ((%f. f t1 t2::bool) = (%f. f True True))"
    14 proof auto
    15   assume a: "(%f. f t1 t2::bool) = (%f. f True True)"
    16   have b: "(%(x::bool) (y::bool). x) = (%x y. x)" ..
    17   with a
    18   have "t1 = True"
    19     by (rule comb_rule)
    20   thus t1
    21     by simp
    22 next
    23   assume a: "(%f. f t1 t2::bool) = (%f. f True True)"
    24   have b: "(%(x::bool) (y::bool). y) = (%x y. y)" ..
    25   with a
    26   have "t2 = True"
    27     by (rule comb_rule)
    28   thus t2
    29     by simp
    30 qed
    31 
    32 definition Pred :: "nat \<Rightarrow> nat" where
    33    "Pred n \<equiv> n - (Suc 0)"
    34 
    35 lemma Pred_altdef: "Pred = (SOME PRE. PRE 0 = 0 & (ALL n. PRE (Suc n) = n))"
    36   apply (rule some_equality[symmetric])
    37   apply (simp add: Pred_def)
    38   apply (rule ext)
    39   apply (induct_tac x)
    40   apply (auto simp add: Pred_def)
    41   done
    42 
    43 lemma NUMERAL_rew[hol4rew]: "NUMERAL x = x" by (simp add: NUMERAL_def)
    44 
    45 lemma REP_ABS_PAIR: "\<forall> x y. Rep_Prod (Abs_Prod (Pair_Rep x y)) = Pair_Rep x y"
    46   apply (subst Abs_Prod_inverse)
    47   apply (auto simp add: Prod_def)
    48   done
    49 
    50 lemma fst_altdef: "fst = (%p. SOME x. EX y. p = (x, y))"
    51   apply (rule ext, rule someI2)
    52   apply (auto intro: fst_conv[symmetric])
    53   done
    54 
    55 lemma snd_altdef: "snd = (%p. SOME x. EX y. p = (y, x))"
    56   apply (rule ext, rule someI2)
    57   apply (auto intro: snd_conv[symmetric])
    58   done
    59 
    60 lemma add_altdef: "op + = (SOME add. (ALL n. add 0 n = n) & (ALL m n. add (Suc m) n = Suc (add m n)))"
    61   apply (rule some_equality[symmetric])
    62   apply auto
    63   apply (rule ext)+
    64   apply (induct_tac x)
    65   apply auto
    66   done
    67 
    68 lemma mult_altdef: "op * = (SOME mult. (ALL n. mult 0 n = 0) & (ALL m n. mult (Suc m) n = mult m n + n))"
    69   apply (rule some_equality[symmetric])
    70   apply auto
    71   apply (rule ext)+
    72   apply (induct_tac x)
    73   apply auto
    74   done
    75 
    76 lemma sub_altdef: "op - = (SOME sub. (ALL m. sub m 0 = m) & (ALL m n. sub m (Suc n) = Pred (sub m n)))"
    77   apply (simp add: Pred_def)
    78   apply (rule some_equality[symmetric])
    79   apply auto
    80   apply (rule ext)+
    81   apply (induct_tac xa)
    82   apply auto
    83   done
    84 
    85 definition NUMERAL_BIT0 :: "nat \<Rightarrow> nat" where
    86   "NUMERAL_BIT0 n \<equiv> n + n"
    87 
    88 lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)"
    89   by (simp add: NUMERAL_BIT1_def)
    90 
    91 consts
    92   sumlift :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> (('a + 'b) \<Rightarrow> 'c)"
    93 
    94 primrec
    95   "sumlift f g (Inl a) = f a"
    96   "sumlift f g (Inr b) = g b"
    97   
    98 lemma sum_Recursion: "\<exists> f. (\<forall> a. f (Inl a) = Inl' a) \<and> (\<forall> b. f (Inr b) = Inr' b)"
    99   apply (rule exI[where x="sumlift Inl' Inr'"])
   100   apply auto
   101   done
   102 
   103 end