src/HOL/Import/HOLLightCompat.thy
 author wenzelm Thu Feb 11 23:00:22 2010 +0100 (2010-02-11) changeset 35115 446c5063e4fd parent 19064 bf19cc5a7899 child 35416 d8d7d1b785af permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
1 (*  Title:      HOL/Import/HOLLightCompat.thy
2     ID:         \$Id\$
3     Author:     Steven Obua and Sebastian Skalberg (TU Muenchen)
4 *)
6 theory HOLLightCompat imports HOL4Setup HOL4Compat Divides Primes Real begin
8 lemma light_imp_def: "(t1 --> t2) = ((t1 & t2) = t1)"
9   by auto;
11 lemma comb_rule: "[| P1 = P2 ; Q1 = Q2 |] ==> P1 Q1 = P2 Q2"
12   by simp
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
33 constdefs
34    Pred :: "nat \<Rightarrow> nat"
35    "Pred n \<equiv> n - (Suc 0)"
37 lemma Pred_altdef: "Pred = (SOME PRE. PRE 0 = 0 & (ALL n. PRE (Suc n) = n))"
38   apply (rule some_equality[symmetric])
40   apply (rule ext)
41   apply (induct_tac x)
42   apply (auto simp add: Pred_def)
43   done
45 lemma NUMERAL_rew[hol4rew]: "NUMERAL x = x" by (simp add: NUMERAL_def)
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
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
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
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
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
78 lemma sub_altdef: "op - = (SOME sub. (ALL m. sub m 0 = m) & (ALL m n. sub m (Suc n) = Pred (sub m n)))"
80   apply (rule some_equality[symmetric])
81   apply auto
82   apply (rule ext)+
83   apply (induct_tac xa)
84   apply auto
85   done
87 constdefs
88   NUMERAL_BIT0 :: "nat \<Rightarrow> nat"
89   "NUMERAL_BIT0 n \<equiv> n + n"
91 lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)"