equal
deleted
inserted
replaced
1 (* Title: HOL/Import/HOL4Compat.thy |
1 (* Title: HOL/Import/HOL4Compat.thy |
2 ID: $Id$ |
|
3 Author: Sebastian Skalberg (TU Muenchen) |
2 Author: Sebastian Skalberg (TU Muenchen) |
4 *) |
3 *) |
5 |
4 |
6 theory HOL4Compat imports HOL4Setup Divides Primes Real ContNotDenum |
5 theory HOL4Compat |
|
6 imports HOL4Setup Complex_Main Primes ContNotDenum |
7 begin |
7 begin |
|
8 |
|
9 no_notation differentiable (infixl "differentiable" 60) |
|
10 no_notation sums (infixr "sums" 80) |
8 |
11 |
9 lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))" |
12 lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))" |
10 by auto |
13 by auto |
11 |
14 |
12 lemma COND_DEF:"(If b t f) = (@x. ((b = True) --> (x = t)) & ((b = False) --> (x = f)))" |
15 lemma COND_DEF:"(If b t f) = (@x. ((b = True) --> (x = t)) & ((b = False) --> (x = f)))" |
20 by (simp add: LET_def Let_def) |
23 by (simp add: LET_def Let_def) |
21 |
24 |
22 lemmas [hol4rew] = ONE_ONE_rew |
25 lemmas [hol4rew] = ONE_ONE_rew |
23 |
26 |
24 lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)" |
27 lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)" |
25 by simp; |
28 by simp |
26 |
29 |
27 lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))" |
30 lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))" |
28 by safe |
31 by safe |
29 |
32 |
30 (*lemma INL_neq_INR: "ALL v1 v2. Sum_Type.Inr v2 ~= Sum_Type.Inl v1" |
33 (*lemma INL_neq_INR: "ALL v1 v2. Sum_Type.Inr v2 ~= Sum_Type.Inl v1" |