author  berghofe 
Tue, 22 May 2001 15:10:06 +0200  
changeset 11325  a5e0289dd56c 
parent 11003  ee0838d89deb 
child 11436  3f74b80d979f 
permissions  rwrr 
7700  1 
(* Title: HOL/Inductive.thy 
2 
ID: $Id$ 

10402  3 
Author: Markus Wenzel, TU Muenchen 
10727  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
5 

6 
Setup packages for inductive sets and types etc. 

7700  7 
*) 
1187  8 

11325
a5e0289dd56c
Inductive definitions are now introduced earlier in the theory hierarchy.
berghofe
parents:
11003
diff
changeset

9 
theory Inductive = Gfp + Sum_Type + Relation 
7700  10 
files 
10402  11 
("Tools/induct_method.ML") 
12 
("Tools/inductive_package.ML") 

13 
("Tools/datatype_aux.ML") 

14 
("Tools/datatype_prop.ML") 

15 
("Tools/datatype_rep_proofs.ML") 

16 
("Tools/datatype_abs_proofs.ML") 

17 
("Tools/datatype_package.ML") 

18 
("Tools/primrec_package.ML"): 

19 

10727  20 

21 
(* handling of proper rules *) 

22 

10402  23 
constdefs 
24 
forall :: "('a => bool) => bool" 

25 
"forall P == \<forall>x. P x" 

26 
implies :: "bool => bool => bool" 

27 
"implies A B == A > B" 

10434  28 
equal :: "'a => 'a => bool" 
29 
"equal x y == x = y" 

10727  30 
conj :: "bool => bool => bool" 
31 
"conj A B == A & B" 

10402  32 

33 
lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))" 

10434  34 
by (simp only: atomize_all forall_def) 
6437  35 

10402  36 
lemma implies_eq: "(A ==> B) == Trueprop (implies A B)" 
10434  37 
by (simp only: atomize_imp implies_def) 
38 

39 
lemma equal_eq: "(x == y) == Trueprop (equal x y)" 

40 
by (simp only: atomize_eq equal_def) 

10402  41 

10727  42 
lemma forall_conj: "forall (\<lambda>x. conj (A x) (B x)) = conj (forall A) (forall B)" 
43 
by (unfold forall_def conj_def) blast 

44 

45 
lemma implies_conj: "implies C (conj A B) = conj (implies C A) (implies C B)" 

46 
by (unfold implies_def conj_def) blast 

47 

48 
lemma conj_curry: "(conj A B ==> C) == (A ==> B ==> C)" 

49 
by (simp only: atomize_imp atomize_eq conj_def) (rule equal_intr_rule, blast+) 

10434  50 

51 
lemmas inductive_atomize = forall_eq implies_eq equal_eq 

52 
lemmas inductive_rulify1 = inductive_atomize [symmetric, standard] 

10727  53 
lemmas inductive_rulify2 = forall_def implies_def equal_def conj_def 
54 
lemmas inductive_conj = forall_conj implies_conj conj_curry 

55 

56 
hide const forall implies equal conj 

57 

58 

59 
(* setup packages *) 

10402  60 

61 
use "Tools/induct_method.ML" 

8303  62 
setup InductMethod.setup 
10402  63 

64 
use "Tools/inductive_package.ML" 

6437  65 
setup InductivePackage.setup 
10402  66 

67 
use "Tools/datatype_aux.ML" 

68 
use "Tools/datatype_prop.ML" 

69 
use "Tools/datatype_rep_proofs.ML" 

70 
use "Tools/datatype_abs_proofs.ML" 

71 
use "Tools/datatype_package.ML" 

7700  72 
setup DatatypePackage.setup 
10402  73 

74 
use "Tools/primrec_package.ML" 

8482  75 
setup PrimrecPackage.setup 
7700  76 

10312  77 
theorems basic_monos [mono] = 
11003  78 
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2 
10727  79 
Collect_mono in_mono vimage_mono 
80 
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj 

81 
not_all not_ex 

82 
Ball_def Bex_def 

83 
inductive_rulify2 

84 

6437  85 
end 