author  haftmann 
Thu, 04 Oct 2007 19:54:46 +0200  
changeset 24845  abcd15369ffa 
parent 24720  4d2f2e375fa1 
child 24915  fc90277c0dd7 
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 
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24626
diff
changeset

9 
imports FixedPoint Sum_Type 
16417  10 
uses 
10402  11 
("Tools/inductive_package.ML") 
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
24349
diff
changeset

12 
"Tools/dseq.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") 

22783  18 
("Tools/datatype_case.ML") 
10402  19 
("Tools/datatype_package.ML") 
15131  20 
("Tools/primrec_package.ML") 
21 
begin 

10727  22 

23734  23 
subsection {* Inductive predicates and sets *} 
11688  24 

25 
text {* Inversion of injective functions. *} 

11436  26 

27 
constdefs 

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

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

30 

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

32 
proof  

33 
assume "inj f" 

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

35 
by (simp only: inj_eq) 

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

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

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

41 
proof (unfold myinv_def) 

42 
assume inj: "inj f" 

43 
assume "y \<in> range f" 

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

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

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

47 
proof (rule theI) 

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

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

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

51 
qed 

52 
qed 

53 

54 
hide const myinv 

55 

56 

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

23734  59 
theorems basic_monos = 
22218  60 
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj 
11688  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 

18456  65 
induct_rulify_fallback 
11688  66 

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

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

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

69 

23734  70 
theorems [mono] = 
22218  71 
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

72 
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

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

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

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

76 

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

79 
proof 

80 
fix P 

81 
assume False 

82 
then show P .. 

83 
next 

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

23389  85 
then show False . 
20604  86 
qed 
87 

88 
lemma not_eq_False: 

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

22886  90 
and eq: "x \<equiv> y" 
20604  91 
shows False 
92 
using not_eq eq by auto 

93 

94 
lemmas not_eq_quodlibet = 

95 
not_eq_False [simplified False_meta_all] 

96 

11688  97 

12023  98 
subsection {* Inductive datatypes and primitive recursion *} 
11688  99 

11825  100 
text {* Package setup. *} 
101 

10402  102 
use "Tools/datatype_aux.ML" 
103 
use "Tools/datatype_prop.ML" 

104 
use "Tools/datatype_rep_proofs.ML" 

105 
use "Tools/datatype_abs_proofs.ML" 

22783  106 
use "Tools/datatype_case.ML" 
10402  107 
use "Tools/datatype_package.ML" 
7700  108 
setup DatatypePackage.setup 
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24626
diff
changeset

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

110 

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

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

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

113 

23526  114 
text{* Lambdaabstractions with pattern matching: *} 
115 

116 
syntax 

23529  117 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(%_)" 10) 
23526  118 
syntax (xsymbols) 
23529  119 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(\<lambda>_)" 10) 
23526  120 

23529  121 
parse_translation (advanced) {* 
122 
let 

123 
fun fun_tr ctxt [cs] = 

124 
let 

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

24349  126 
val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr 
127 
ctxt [x, cs] 

23529  128 
in lambda x ft end 
129 
in [("_lam_pats_syntax", fun_tr)] end 

23526  130 
*} 
131 

132 
end 