src/HOL/Import/HOLLightCompat.thy
changeset 17322 781abf7011e6
child 19064 bf19cc5a7899
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Import/HOLLightCompat.thy	Mon Sep 12 15:52:00 2005 +0200
     1.3 @@ -0,0 +1,96 @@
     1.4 +(*  Title:      HOL/Import/HOLLightCompat.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Steven Obua and Sebastian Skalberg (TU Muenchen)
     1.7 +*)
     1.8 +
     1.9 +theory HOLLightCompat imports HOL4Setup HOL4Compat Divides Primes Real begin
    1.10 +
    1.11 +lemma light_imp_def: "(t1 --> t2) = ((t1 & t2) = t1)"
    1.12 +  by auto;
    1.13 +
    1.14 +lemma comb_rule: "[| P1 = P2 ; Q1 = Q2 |] ==> P1 Q1 = P2 Q2"
    1.15 +  by simp
    1.16 +
    1.17 +lemma light_and_def: "(t1 & t2) = ((%f. f t1 t2::bool) = (%f. f True True))"
    1.18 +proof auto
    1.19 +  assume a: "(%f. f t1 t2::bool) = (%f. f True True)"
    1.20 +  have b: "(%(x::bool) (y::bool). x) = (%x y. x)" ..
    1.21 +  with a
    1.22 +  have "t1 = True"
    1.23 +    by (rule comb_rule)
    1.24 +  thus t1
    1.25 +    by simp
    1.26 +next
    1.27 +  assume a: "(%f. f t1 t2::bool) = (%f. f True True)"
    1.28 +  have b: "(%(x::bool) (y::bool). y) = (%x y. y)" ..
    1.29 +  with a
    1.30 +  have "t2 = True"
    1.31 +    by (rule comb_rule)
    1.32 +  thus t2
    1.33 +    by simp
    1.34 +qed
    1.35 +
    1.36 +constdefs
    1.37 +   Pred :: "nat \<Rightarrow> nat"
    1.38 +   "Pred n \<equiv> n - (Suc 0)"
    1.39 +
    1.40 +lemma Pred_altdef: "Pred = (SOME PRE. PRE 0 = 0 & (ALL n. PRE (Suc n) = n))"
    1.41 +  apply (rule some_equality[symmetric])
    1.42 +  apply (simp add: Pred_def)
    1.43 +  apply (rule ext)
    1.44 +  apply (induct_tac x)
    1.45 +  apply (auto simp add: Pred_def)
    1.46 +  done
    1.47 +
    1.48 +lemma NUMERAL_rew[hol4rew]: "NUMERAL x = x" by (simp add: NUMERAL_def)
    1.49 +
    1.50 +lemma REP_ABS_PAIR: "\<forall> x y. Rep_Prod (Abs_Prod (Pair_Rep x y)) = Pair_Rep x y"
    1.51 +  apply (subst Abs_Prod_inverse)
    1.52 +  apply (auto simp add: Prod_def)
    1.53 +  done
    1.54 +
    1.55 +lemma fst_altdef: "fst = (%p. SOME x. EX y. p = (x, y))"
    1.56 +  apply (rule ext, rule someI2)
    1.57 +  apply (auto intro: fst_conv[symmetric])
    1.58 +  done
    1.59 +
    1.60 +lemma snd_altdef: "snd = (%p. SOME x. EX y. p = (y, x))"
    1.61 +  apply (rule ext, rule someI2)
    1.62 +  apply (auto intro: snd_conv[symmetric])
    1.63 +  done
    1.64 +
    1.65 +lemma add_altdef: "op + = (SOME add. (ALL n. add 0 n = n) & (ALL m n. add (Suc m) n = Suc (add m n)))"
    1.66 +  apply (rule some_equality[symmetric])
    1.67 +  apply auto
    1.68 +  apply (rule ext)+
    1.69 +  apply (induct_tac x)
    1.70 +  apply auto
    1.71 +  done
    1.72 +
    1.73 +lemma mult_altdef: "op * = (SOME mult. (ALL n. mult 0 n = 0) & (ALL m n. mult (Suc m) n = mult m n + n))"
    1.74 +  apply (rule some_equality[symmetric])
    1.75 +  apply auto
    1.76 +  apply (rule ext)+
    1.77 +  apply (induct_tac x)
    1.78 +  apply auto
    1.79 +  done
    1.80 +
    1.81 +lemma sub_altdef: "op - = (SOME sub. (ALL m. sub m 0 = m) & (ALL m n. sub m (Suc n) = Pred (sub m n)))"
    1.82 +  apply (simp add: Pred_def)
    1.83 +  apply (rule some_equality[symmetric])
    1.84 +  apply auto
    1.85 +  apply (rule ext)+
    1.86 +  apply (induct_tac xa)
    1.87 +  apply auto
    1.88 +  done
    1.89 +
    1.90 +constdefs
    1.91 +  NUMERAL_BIT0 :: "nat \<Rightarrow> nat"
    1.92 +  "NUMERAL_BIT0 n \<equiv> n + n"
    1.93 +
    1.94 +lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)"
    1.95 +  by (simp add: NUMERAL_BIT1_def)
    1.96 +
    1.97 +
    1.98 +
    1.99 +end