author  wenzelm 
Mon, 06 Nov 2000 22:49:16 +0100  
changeset 10402  5e82d6cafb5f 
parent 10312  4c5a03649af7 
child 10434  6ea4735c3955 
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" 

22 

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

24 
proof 

25 
assume "!!x. P x" 

26 
thus "forall (\<lambda>x. P x)" by (unfold forall_def) blast 

27 
next 

28 
fix x 

29 
assume "forall (\<lambda>x. P x)" 

30 
thus "P x" by (unfold forall_def) blast 

31 
qed 

6437  32 

10402  33 
lemma implies_eq: "(A ==> B) == Trueprop (implies A B)" 
34 
proof 

35 
assume "A ==> B" 

36 
thus "implies A B" by (unfold implies_def) blast 

37 
next 

38 
assume "implies A B" and A 

39 
thus B by (unfold implies_def) blast 

40 
qed 

41 

42 
lemmas inductive_atomize = forall_eq implies_eq 

43 
lemmas inductive_rulify = inductive_atomize [symmetric, standard] 

44 
hide const forall implies 

45 

46 
use "Tools/induct_method.ML" 

8303  47 
setup InductMethod.setup 
10402  48 

49 
use "Tools/inductive_package.ML" 

6437  50 
setup InductivePackage.setup 
10402  51 

52 
use "Tools/datatype_aux.ML" 

53 
use "Tools/datatype_prop.ML" 

54 
use "Tools/datatype_rep_proofs.ML" 

55 
use "Tools/datatype_abs_proofs.ML" 

56 
use "Tools/datatype_package.ML" 

7700  57 
setup DatatypePackage.setup 
10402  58 

59 
use "Tools/primrec_package.ML" 

8482  60 
setup PrimrecPackage.setup 
7700  61 

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

63 
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

64 
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

65 
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

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

67 
Ball_def Bex_def 
6437  68 

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

71 
declare rtranclE [cases set: rtrancl] 

72 
declare trancl_induct [induct set: trancl] 

73 
declare tranclE [cases set: trancl] 

74 

6437  75 
end 