17322
|
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 |
|
19064
|
94 |
consts
|
|
95 |
sumlift :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> (('a + 'b) \<Rightarrow> 'c)"
|
17322
|
96 |
|
19064
|
97 |
primrec
|
|
98 |
"sumlift f g (Inl a) = f a"
|
|
99 |
"sumlift f g (Inr b) = g b"
|
|
100 |
|
|
101 |
lemma sum_Recursion: "\<exists> f. (\<forall> a. f (Inl a) = Inl' a) \<and> (\<forall> b. f (Inr b) = Inr' b)"
|
|
102 |
apply (rule exI[where x="sumlift Inl' Inr'"])
|
|
103 |
apply auto
|
|
104 |
done
|
17322
|
105 |
|
|
106 |
end
|