author  haftmann 
Tue, 10 Jul 2007 17:30:49 +0200  
changeset 23708  b5eb0b4dd17d 
parent 23529  958f9d9cfb63 
child 23734  0e11b904b3a3 
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 
23708  9 
imports FixedPoint Product_Type Sum_Type 
16417  10 
uses 
10402  11 
("Tools/inductive_package.ML") 
21018
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

12 
("Tools/old_inductive_package.ML") 
13705  13 
("Tools/inductive_realizer.ML") 
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

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

17 
("Tools/datatype_rep_proofs.ML") 

18 
("Tools/datatype_abs_proofs.ML") 

13469  19 
("Tools/datatype_realizer.ML") 
19599  20 
("Tools/datatype_hooks.ML") 
22783  21 
("Tools/datatype_case.ML") 
10402  22 
("Tools/datatype_package.ML") 
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

23 
("Tools/datatype_codegen.ML") 
15131  24 
("Tools/primrec_package.ML") 
25 
begin 

10727  26 

11688  27 
subsection {* Inductive sets *} 
28 

29 
text {* Inversion of injective functions. *} 

11436  30 

31 
constdefs 

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

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

34 

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

36 
proof  

37 
assume "inj f" 

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

39 
by (simp only: inj_eq) 

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

11439  41 
finally show ?thesis by (unfold myinv_def) 
11436  42 
qed 
43 

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

45 
proof (unfold myinv_def) 

46 
assume inj: "inj f" 

47 
assume "y \<in> range f" 

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

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

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

51 
proof (rule theI) 

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

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

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

55 
qed 

56 
qed 

57 

58 
hide const myinv 

59 

60 

11688  61 
text {* Package setup. *} 
10402  62 

22886  63 
ML {* setmp tolerate_legacy_features true use "Tools/old_inductive_package.ML" *} 
21018
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

64 
setup OldInductivePackage.setup 
10402  65 

11688  66 
theorems basic_monos [mono] = 
22218  67 
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj 
11688  68 
Collect_mono in_mono vimage_mono 
69 
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj 

70 
not_all not_ex 

71 
Ball_def Bex_def 

18456  72 
induct_rulify_fallback 
11688  73 

21018
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

74 
use "Tools/inductive_package.ML" 
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

75 
setup InductivePackage.setup 
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

76 

e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

77 
theorems [mono2] = 
22218  78 
imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj 
21018
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

79 
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj 
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

80 
not_all not_ex 
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

81 
Ball_def Bex_def 
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

82 
induct_rulify_fallback 
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

83 

20604  84 
lemma False_meta_all: 
85 
"Trueprop False \<equiv> (\<And>P\<Colon>bool. P)" 

86 
proof 

87 
fix P 

88 
assume False 

89 
then show P .. 

90 
next 

91 
assume "\<And>P\<Colon>bool. P" 

23389  92 
then show False . 
20604  93 
qed 
94 

95 
lemma not_eq_False: 

96 
assumes not_eq: "x \<noteq> y" 

22886  97 
and eq: "x \<equiv> y" 
20604  98 
shows False 
99 
using not_eq eq by auto 

100 

101 
lemmas not_eq_quodlibet = 

102 
not_eq_False [simplified False_meta_all] 

103 

11688  104 

12023  105 
subsection {* Inductive datatypes and primitive recursion *} 
11688  106 

11825  107 
text {* Package setup. *} 
108 

10402  109 
use "Tools/datatype_aux.ML" 
110 
use "Tools/datatype_prop.ML" 

111 
use "Tools/datatype_rep_proofs.ML" 

112 
use "Tools/datatype_abs_proofs.ML" 

22783  113 
use "Tools/datatype_case.ML" 
13469  114 
use "Tools/datatype_realizer.ML" 
19599  115 

116 
use "Tools/datatype_hooks.ML" 

117 

10402  118 
use "Tools/datatype_package.ML" 
7700  119 
setup DatatypePackage.setup 
10402  120 

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

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

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

123 

13705  124 
use "Tools/inductive_realizer.ML" 
125 
setup InductiveRealizer.setup 

126 

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

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

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

129 

10402  130 
use "Tools/primrec_package.ML" 
7700  131 

23526  132 
text{* Lambdaabstractions with pattern matching: *} 
133 

134 
syntax 

23529  135 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(%_)" 10) 
23526  136 
syntax (xsymbols) 
23529  137 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(\<lambda>_)" 10) 
23526  138 

23529  139 
parse_translation (advanced) {* 
140 
let 

141 
fun fun_tr ctxt [cs] = 

142 
let 

143 
val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT); 

144 
val ft = DatatypeCase.case_tr DatatypePackage.datatype_of_constr ctxt 

145 
[x, cs] 

146 
in lambda x ft end 

147 
in [("_lam_pats_syntax", fun_tr)] end 

23526  148 
*} 
149 

150 
end 