author  berghofe 
Wed, 07 Aug 2002 16:48:20 +0200  
changeset 13469  70d8dfef587d 
parent 12920  32292d83367b 
child 13705  934d6c1421f2 
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 

12920  9 
theory Inductive = Gfp + Sum_Type + Relation + Record 
7700  10 
files 
10402  11 
("Tools/inductive_package.ML") 
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

12 
("Tools/inductive_codegen.ML") 
10402  13 
("Tools/datatype_aux.ML") 
14 
("Tools/datatype_prop.ML") 

15 
("Tools/datatype_rep_proofs.ML") 

16 
("Tools/datatype_abs_proofs.ML") 

13469  17 
("Tools/datatype_realizer.ML") 
10402  18 
("Tools/datatype_package.ML") 
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

19 
("Tools/datatype_codegen.ML") 
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

20 
("Tools/recfun_codegen.ML") 
10402  21 
("Tools/primrec_package.ML"): 
22 

10727  23 

11688  24 
subsection {* Inductive sets *} 
25 

26 
text {* Inversion of injective functions. *} 

11436  27 

28 
constdefs 

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

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

31 

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

33 
proof  

34 
assume "inj f" 

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

36 
by (simp only: inj_eq) 

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

11439  38 
finally show ?thesis by (unfold myinv_def) 
11436  39 
qed 
40 

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

42 
proof (unfold myinv_def) 

43 
assume inj: "inj f" 

44 
assume "y \<in> range f" 

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

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

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

48 
proof (rule theI) 

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

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

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

52 
qed 

53 
qed 

54 

55 
hide const myinv 

56 

57 

11688  58 
text {* Package setup. *} 
10402  59 

60 
use "Tools/inductive_package.ML" 

6437  61 
setup InductivePackage.setup 
10402  62 

11688  63 
theorems basic_monos [mono] = 
64 
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2 

65 
Collect_mono in_mono vimage_mono 

66 
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj 

67 
not_all not_ex 

68 
Ball_def Bex_def 

11990  69 
induct_rulify2 
11688  70 

71 

12023  72 
subsection {* Inductive datatypes and primitive recursion *} 
11688  73 

11825  74 
text {* Package setup. *} 
75 

12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

76 
use "Tools/recfun_codegen.ML" 
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

77 
setup RecfunCodegen.setup 
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

78 

10402  79 
use "Tools/datatype_aux.ML" 
80 
use "Tools/datatype_prop.ML" 

81 
use "Tools/datatype_rep_proofs.ML" 

82 
use "Tools/datatype_abs_proofs.ML" 

13469  83 
use "Tools/datatype_realizer.ML" 
10402  84 
use "Tools/datatype_package.ML" 
7700  85 
setup DatatypePackage.setup 
10402  86 

12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

87 
use "Tools/datatype_codegen.ML" 
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

88 
setup DatatypeCodegen.setup 
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

89 

6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

90 
use "Tools/inductive_codegen.ML" 
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

91 
setup InductiveCodegen.setup 
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

92 

10402  93 
use "Tools/primrec_package.ML" 
7700  94 

6437  95 
end 