author  wenzelm 
Sat, 03 Nov 2001 01:33:54 +0100  
changeset 12023  d982f98e0f0d 
parent 11990  c1daefc08eff 
child 12437  6d4e02b6dd43 
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) 
11688  5 
*) 
10727  6 

11688  7 
header {* Support for inductive sets and types *} 
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/inductive_package.ML") 
12 
("Tools/datatype_aux.ML") 

13 
("Tools/datatype_prop.ML") 

14 
("Tools/datatype_rep_proofs.ML") 

15 
("Tools/datatype_abs_proofs.ML") 

16 
("Tools/datatype_package.ML") 

17 
("Tools/primrec_package.ML"): 

18 

10727  19 

11688  20 
subsection {* Inductive sets *} 
21 

22 
text {* Inversion of injective functions. *} 

11436  23 

24 
constdefs 

25 
myinv :: "('a => 'b) => ('b => 'a)" 

26 
"myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y" 

27 

28 
lemma myinv_f_f: "inj f ==> myinv f (f x) = x" 

29 
proof  

30 
assume "inj f" 

31 
hence "(THE x'. f x' = f x) = (THE x'. x' = x)" 

32 
by (simp only: inj_eq) 

33 
also have "... = x" by (rule the_eq_trivial) 

11439  34 
finally show ?thesis by (unfold myinv_def) 
11436  35 
qed 
36 

37 
lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y" 

38 
proof (unfold myinv_def) 

39 
assume inj: "inj f" 

40 
assume "y \<in> range f" 

41 
then obtain x where "y = f x" .. 

42 
hence x: "f x = y" .. 

43 
thus "f (THE x. f x = y) = y" 

44 
proof (rule theI) 

45 
fix x' assume "f x' = y" 

46 
with x have "f x' = f x" by simp 

47 
with inj show "x' = x" by (rule injD) 

48 
qed 

49 
qed 

50 

51 
hide const myinv 

52 

53 

11688  54 
text {* Package setup. *} 
10402  55 

56 
use "Tools/inductive_package.ML" 

6437  57 
setup InductivePackage.setup 
10402  58 

11688  59 
theorems basic_monos [mono] = 
60 
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2 

61 
Collect_mono in_mono vimage_mono 

62 
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj 

63 
not_all not_ex 

64 
Ball_def Bex_def 

11990  65 
induct_rulify2 
11688  66 

67 

12023  68 
subsection {* Inductive datatypes and primitive recursion *} 
11688  69 

11825  70 
text {* Package setup. *} 
71 

10402  72 
use "Tools/datatype_aux.ML" 
73 
use "Tools/datatype_prop.ML" 

74 
use "Tools/datatype_rep_proofs.ML" 

75 
use "Tools/datatype_abs_proofs.ML" 

76 
use "Tools/datatype_package.ML" 

7700  77 
setup DatatypePackage.setup 
10402  78 

79 
use "Tools/primrec_package.ML" 

8482  80 
setup PrimrecPackage.setup 
7700  81 

6437  82 
end 