author  wenzelm 
Fri, 10 Nov 2000 19:03:55 +0100  
changeset 10434  6ea4735c3955 
parent 10402  5e82d6cafb5f 
child 10727  2ccafccb81c0 
permissions  rwrr 
7700  1 
(* Title: HOL/Inductive.thy 
2 
ID: $Id$ 

10402  3 
Author: Markus Wenzel, TU Muenchen 
7700  4 
*) 
1187  5 

10212  6 
theory Inductive = Gfp + Sum_Type + NatDef 
7700  7 
files 
10402  8 
("Tools/induct_method.ML") 
9 
("Tools/inductive_package.ML") 

10 
("Tools/datatype_aux.ML") 

11 
("Tools/datatype_prop.ML") 

12 
("Tools/datatype_rep_proofs.ML") 

13 
("Tools/datatype_abs_proofs.ML") 

14 
("Tools/datatype_package.ML") 

15 
("Tools/primrec_package.ML"): 

16 

17 
constdefs 

18 
forall :: "('a => bool) => bool" 

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

20 
implies :: "bool => bool => bool" 

21 
"implies A B == A > B" 

10434  22 
equal :: "'a => 'a => bool" 
23 
"equal x y == x = y" 

10402  24 

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

10434  26 
by (simp only: atomize_all forall_def) 
6437  27 

10402  28 
lemma implies_eq: "(A ==> B) == Trueprop (implies A B)" 
10434  29 
by (simp only: atomize_imp implies_def) 
30 

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

32 
by (simp only: atomize_eq equal_def) 

10402  33 

10434  34 
hide const forall implies equal 
35 

36 
lemmas inductive_atomize = forall_eq implies_eq equal_eq 

37 
lemmas inductive_rulify1 = inductive_atomize [symmetric, standard] 

38 
lemmas inductive_rulify2 = forall_def implies_def equal_def 

10402  39 

40 
use "Tools/induct_method.ML" 

8303  41 
setup InductMethod.setup 
10402  42 

43 
use "Tools/inductive_package.ML" 

6437  44 
setup InductivePackage.setup 
10402  45 

46 
use "Tools/datatype_aux.ML" 

47 
use "Tools/datatype_prop.ML" 

48 
use "Tools/datatype_rep_proofs.ML" 

49 
use "Tools/datatype_abs_proofs.ML" 

50 
use "Tools/datatype_package.ML" 

7700  51 
setup DatatypePackage.setup 
10402  52 

53 
use "Tools/primrec_package.ML" 

8482  54 
setup PrimrecPackage.setup 
7700  55 

10312  56 
theorems basic_monos [mono] = 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset

57 
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset

58 
Collect_mono in_mono vimage_mono 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset

59 
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset

60 
not_all not_ex 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset

61 
Ball_def Bex_def 
6437  62 

10312  63 
(*belongs to theory Transitive_Closure*) 
64 
declare rtrancl_induct [induct set: rtrancl] 

65 
declare rtranclE [cases set: rtrancl] 

66 
declare trancl_induct [induct set: trancl] 

67 
declare tranclE [cases set: trancl] 

68 

6437  69 
end 