author  avigad 
Wed, 03 Aug 2005 14:48:13 +0200  
changeset 17009  932e0e370926 
parent 16417  9bc16273c2d4 
child 18456  8cc35e95450a 
permissions  rwrr 
7700  1 
(* Title: HOL/Inductive.thy 
2 
ID: $Id$ 

10402  3 
Author: Markus Wenzel, TU Muenchen 
11688  4 
*) 
10727  5 

11688  6 
header {* Support for inductive sets and types *} 
1187  7 

15131  8 
theory Inductive 
17009  9 
imports FixedPoint Sum_Type Relation Record 
16417  10 
uses 
10402  11 
("Tools/inductive_package.ML") 
13705  12 
("Tools/inductive_realizer.ML") 
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

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

16 
("Tools/datatype_rep_proofs.ML") 

17 
("Tools/datatype_abs_proofs.ML") 

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

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

21 
("Tools/recfun_codegen.ML") 
15131  22 
("Tools/primrec_package.ML") 
23 
begin 

10727  24 

11688  25 
subsection {* Inductive sets *} 
26 

27 
text {* Inversion of injective functions. *} 

11436  28 

29 
constdefs 

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

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

32 

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

34 
proof  

35 
assume "inj f" 

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

37 
by (simp only: inj_eq) 

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

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

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

43 
proof (unfold myinv_def) 

44 
assume inj: "inj f" 

45 
assume "y \<in> range f" 

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

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

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

49 
proof (rule theI) 

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

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

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

53 
qed 

54 
qed 

55 

56 
hide const myinv 

57 

58 

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

61 
use "Tools/inductive_package.ML" 

6437  62 
setup InductivePackage.setup 
10402  63 

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

66 
Collect_mono in_mono vimage_mono 

67 
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj 

68 
not_all not_ex 

69 
Ball_def Bex_def 

11990  70 
induct_rulify2 
11688  71 

72 

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

11825  75 
text {* Package setup. *} 
76 

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

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

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

79 

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

82 
use "Tools/datatype_rep_proofs.ML" 

83 
use "Tools/datatype_abs_proofs.ML" 

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

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

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

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

90 

13705  91 
use "Tools/inductive_realizer.ML" 
92 
setup InductiveRealizer.setup 

93 

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

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

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

96 

10402  97 
use "Tools/primrec_package.ML" 
7700  98 

6437  99 
end 