author  blanchet 
Mon, 17 Sep 2012 21:13:30 +0200  
changeset 49429  64ac3471005a 
parent 49428  93f158d59ead 
child 49430  6df729c6a1a6 
permissions  rwrr 
49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

1 
(* Title: HOL/Codatatype/BNF_FP.thy 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

2 
Author: Dmitriy Traytel, TU Muenchen 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

3 
Author: Jasmin Blanchette, TU Muenchen 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

4 
Copyright 2012 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

5 

6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

6 
Composition of bounded natural functors. 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

7 
*) 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

8 

6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

9 
header {* Composition of Bounded Natural Functors *} 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

10 

6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

11 
theory BNF_FP 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

12 
imports BNF_Comp BNF_Wrap 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

13 
keywords 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

14 
"defaults" 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

15 
begin 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

16 

49312  17 
lemma case_unit: "(case u of () => f) = f" 
18 
by (cases u) (hypsubst, rule unit.cases) 

19 

49335  20 
lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" 
21 
by simp 

22 

23 
lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" 

24 
by clarify 

25 

26 
lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" 

27 
by auto 

28 

49368  29 
lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" 
30 
by simp 

49312  31 

49368  32 
lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" 
33 
by clarsimp 

49312  34 

35 
lemma rev_bspec: "a \<in> A \<Longrightarrow> \<forall>z \<in> A. P z \<Longrightarrow> P a" 

36 
by simp 

37 

38 
lemma Un_cong: "\<lbrakk>A = B; C = D\<rbrakk> \<Longrightarrow> A \<union> C = B \<union> D" 

39 
by simp 

40 

41 
definition convol ("<_ , _>") where 

42 
"<f , g> \<equiv> %a. (f a, g a)" 

43 

44 
lemma fst_convol: 

45 
"fst o <f , g> = f" 

46 
apply(rule ext) 

47 
unfolding convol_def by simp 

48 

49 
lemma snd_convol: 

50 
"snd o <f , g> = g" 

51 
apply(rule ext) 

52 
unfolding convol_def by simp 

53 

54 
lemma pointfree_idE: "f o g = id \<Longrightarrow> f (g x) = x" 

55 
unfolding o_def fun_eq_iff by simp 

56 

57 
lemma o_bij: 

58 
assumes gf: "g o f = id" and fg: "f o g = id" 

59 
shows "bij f" 

60 
unfolding bij_def inj_on_def surj_def proof safe 

61 
fix a1 a2 assume "f a1 = f a2" 

62 
hence "g ( f a1) = g (f a2)" by simp 

63 
thus "a1 = a2" using gf unfolding fun_eq_iff by simp 

64 
next 

65 
fix b 

66 
have "b = f (g b)" 

67 
using fg unfolding fun_eq_iff by simp 

68 
thus "EX a. b = f a" by blast 

69 
qed 

70 

71 
lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp 

72 

73 
lemma sum_case_step: 

74 
"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p" 

75 
"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p" 

76 
by auto 

77 

78 
lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 

79 
by simp 

80 

81 
lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P" 

82 
by blast 

83 

49325  84 
lemma obj_sumE_f': 
85 
"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> s = f x \<longrightarrow> P" 

86 
by (cases x) blast+ 

87 

49312  88 
lemma obj_sumE_f: 
89 
"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P" 

49325  90 
by (rule allI) (rule obj_sumE_f') 
49312  91 

92 
lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P" 

93 
by (cases s) auto 

94 

49325  95 
lemma obj_sum_step': 
96 
"\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> s = f (Inr x) \<longrightarrow> P" 

97 
by (cases x) blast+ 

98 

49312  99 
lemma obj_sum_step: 
49325  100 
"\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f (Inr x) \<longrightarrow> P" 
101 
by (rule allI) (rule obj_sum_step') 

49312  102 

103 
lemma sum_case_if: 

104 
"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)" 

105 
by simp 

106 

49426  107 
lemma UN_compreh_bex_eq_empty: 
108 
"\<Union>{y. \<exists>x\<in>A. y = {}} = {}" 

109 
by blast 

110 

111 
lemma UN_compreh_bex_eq_singleton: 

112 
"\<Union>{y. \<exists>x\<in>A. y = {f x}} = {y. \<exists>x\<in>A. y = f x}" 

113 
by blast 

114 

115 
lemma mem_UN_comprehI: 

116 
"z \<in> {y. \<exists>x\<in>A. y = f x} \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = {f x}}" 

117 
"z \<in> {y. \<exists>x\<in>A. y = f x} \<union> B \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = {f x}} \<union> B" 

118 
"z \<in> \<Union>{y. \<exists>x\<in>A. y = F x} \<union> \<Union>{y. \<exists>x\<in>A. y = G x} \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = F x \<union> G x}" 

119 
"z \<in> \<Union>{y. \<exists>x\<in>A. y = F x} \<union> (\<Union>{y. \<exists>x\<in>A. y = G x} \<union> B) \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = F x \<union> G x} \<union> B" 

49368  120 
by blast+ 
121 

49426  122 
lemma mem_UN_comprehI': 
123 
"\<exists>y. (\<exists>x\<in>A. y = F x) \<and> z \<in> y \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = {y. \<exists>y'\<in>F x. y = y'}}" 

124 
by blast 

125 

49428
93f158d59ead
handle the general case with more than two levels of nesting when discharging induction prem prems
blanchet
parents:
49427
diff
changeset

126 
lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)" 
93f158d59ead
handle the general case with more than two levels of nesting when discharging induction prem prems
blanchet
parents:
49427
diff
changeset

127 
by blast 
93f158d59ead
handle the general case with more than two levels of nesting when discharging induction prem prems
blanchet
parents:
49427
diff
changeset

128 

93f158d59ead
handle the general case with more than two levels of nesting when discharging induction prem prems
blanchet
parents:
49427
diff
changeset

129 
lemma eq_UN_compreh_Un: "(xa = \<Union>{y. \<exists>x\<in>A. y = c_set1 x \<union> c_set2 x}) = 
93f158d59ead
handle the general case with more than two levels of nesting when discharging induction prem prems
blanchet
parents:
49427
diff
changeset

130 
(xa = (\<Union>{y. \<exists>x\<in>A. y = c_set1 x} \<union> \<Union>{y. \<exists>x\<in>A. y = c_set2 x}))" 
93f158d59ead
handle the general case with more than two levels of nesting when discharging induction prem prems
blanchet
parents:
49427
diff
changeset

131 
by blast 
93f158d59ead
handle the general case with more than two levels of nesting when discharging induction prem prems
blanchet
parents:
49427
diff
changeset

132 

49427  133 
lemma mem_compreh_eq_iff: 
49428
93f158d59ead
handle the general case with more than two levels of nesting when discharging induction prem prems
blanchet
parents:
49427
diff
changeset

134 
"z \<in> {y. \<exists>x\<in>A. y = f x} = (\<exists> x. x \<in> A & z \<in> {f x})" 
49427  135 
by blast 
136 

137 
lemma ex_mem_singleton: "(\<exists>y. y \<in> A \<and> y \<in> {x}) = (x \<in> A)" 

138 
by simp 

139 

49429
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

140 
lemma prod_set_simps: 
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

141 
"fsts (x, y) = {x}" 
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

142 
"snds (x, y) = {y}" 
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

143 
unfolding fsts_def snds_def by simp+ 
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

144 

64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

145 
lemma sum_set_simps: 
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

146 
"sum_setl (Inl x) = {x}" 
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

147 
"sum_setl (Inr x) = {}" 
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

148 
"sum_setr (Inl x) = {}" 
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

149 
"sum_setr (Inr x) = {x}" 
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

150 
unfolding sum_setl_def sum_setr_def by simp+ 
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

151 

49427  152 
lemma induct_set_step: 
153 
"\<lbrakk>b \<in> A; c \<in> F b\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> c \<in> F x" 

154 
"\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and>c \<in> C" 

155 
by blast+ 

49368  156 

49309
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset

157 
ML_file "Tools/bnf_fp_util.ML" 
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset

158 
ML_file "Tools/bnf_fp_sugar_tactics.ML" 
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset

159 
ML_file "Tools/bnf_fp_sugar.ML" 
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset

160 

49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

161 
end 