src/HOL/Import/HOLLightCompat.thy
author obua
Mon Sep 12 15:52:00 2005 +0200 (2005-09-12)
changeset 17322 781abf7011e6
child 19064 bf19cc5a7899
permissions -rw-r--r--
Added HOLLight support to importer.
     1 (*  Title:      HOL/Import/HOLLightCompat.thy
     2     ID:         $Id$
     3     Author:     Steven Obua and Sebastian Skalberg (TU Muenchen)
     4 *)
     5 
     6 theory HOLLightCompat imports HOL4Setup HOL4Compat Divides Primes Real begin
     7 
     8 lemma light_imp_def: "(t1 --> t2) = ((t1 & t2) = t1)"
     9   by auto;
    10 
    11 lemma comb_rule: "[| P1 = P2 ; Q1 = Q2 |] ==> P1 Q1 = P2 Q2"
    12   by simp
    13 
    14 lemma light_and_def: "(t1 & t2) = ((%f. f t1 t2::bool) = (%f. f True True))"
    15 proof auto
    16   assume a: "(%f. f t1 t2::bool) = (%f. f True True)"
    17   have b: "(%(x::bool) (y::bool). x) = (%x y. x)" ..
    18   with a
    19   have "t1 = True"
    20     by (rule comb_rule)
    21   thus t1
    22     by simp
    23 next
    24   assume a: "(%f. f t1 t2::bool) = (%f. f True True)"
    25   have b: "(%(x::bool) (y::bool). y) = (%x y. y)" ..
    26   with a
    27   have "t2 = True"
    28     by (rule comb_rule)
    29   thus t2
    30     by simp
    31 qed
    32 
    33 constdefs
    34    Pred :: "nat \<Rightarrow> nat"
    35    "Pred n \<equiv> n - (Suc 0)"
    36 
    37 lemma Pred_altdef: "Pred = (SOME PRE. PRE 0 = 0 & (ALL n. PRE (Suc n) = n))"
    38   apply (rule some_equality[symmetric])
    39   apply (simp add: Pred_def)
    40   apply (rule ext)
    41   apply (induct_tac x)
    42   apply (auto simp add: Pred_def)
    43   done
    44 
    45 lemma NUMERAL_rew[hol4rew]: "NUMERAL x = x" by (simp add: NUMERAL_def)
    46 
    47 lemma REP_ABS_PAIR: "\<forall> x y. Rep_Prod (Abs_Prod (Pair_Rep x y)) = Pair_Rep x y"
    48   apply (subst Abs_Prod_inverse)
    49   apply (auto simp add: Prod_def)
    50   done
    51 
    52 lemma fst_altdef: "fst = (%p. SOME x. EX y. p = (x, y))"
    53   apply (rule ext, rule someI2)
    54   apply (auto intro: fst_conv[symmetric])
    55   done
    56 
    57 lemma snd_altdef: "snd = (%p. SOME x. EX y. p = (y, x))"
    58   apply (rule ext, rule someI2)
    59   apply (auto intro: snd_conv[symmetric])
    60   done
    61 
    62 lemma add_altdef: "op + = (SOME add. (ALL n. add 0 n = n) & (ALL m n. add (Suc m) n = Suc (add m n)))"
    63   apply (rule some_equality[symmetric])
    64   apply auto
    65   apply (rule ext)+
    66   apply (induct_tac x)
    67   apply auto
    68   done
    69 
    70 lemma mult_altdef: "op * = (SOME mult. (ALL n. mult 0 n = 0) & (ALL m n. mult (Suc m) n = mult m n + n))"
    71   apply (rule some_equality[symmetric])
    72   apply auto
    73   apply (rule ext)+
    74   apply (induct_tac x)
    75   apply auto
    76   done
    77 
    78 lemma sub_altdef: "op - = (SOME sub. (ALL m. sub m 0 = m) & (ALL m n. sub m (Suc n) = Pred (sub m n)))"
    79   apply (simp add: Pred_def)
    80   apply (rule some_equality[symmetric])
    81   apply auto
    82   apply (rule ext)+
    83   apply (induct_tac xa)
    84   apply auto
    85   done
    86 
    87 constdefs
    88   NUMERAL_BIT0 :: "nat \<Rightarrow> nat"
    89   "NUMERAL_BIT0 n \<equiv> n + n"
    90 
    91 lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)"
    92   by (simp add: NUMERAL_BIT1_def)
    93 
    94 
    95 
    96 end