author  desharna 
Tue, 01 Jul 2014 17:01:28 +0200  
changeset 57471  11cd462e31ec 
parent 57303  498a62e65f5f 
child 57489  8f0ba9f2d10f 
permissions  rwrr 
55059  1 
(* Title: HOL/BNF_FP_Base.thy 
53311  2 
Author: Lorenz Panny, TU Muenchen 
49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

3 
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

4 
Author: Jasmin Blanchette, TU Muenchen 
53311  5 
Copyright 2012, 2013 
49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

6 

55059  7 
Shared fixed point operations on bounded natural functors. 
49308
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 

53311  10 
header {* Shared Fixed Point Operations on Bounded Natural Functors *} 
49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

11 

53311  12 
theory BNF_FP_Base 
55936  13 
imports BNF_Comp Basic_BNFs 
49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

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

15 

49590  16 
lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" 
17 
by auto 

18 

57303  19 
lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y" 
57302  20 
by auto 
21 

49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

22 
lemma eq_sym_Unity_conv: "(x = (() = ())) = x" 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49539
diff
changeset

23 
by blast 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49539
diff
changeset

24 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55083
diff
changeset

25 
lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f" 
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55575
diff
changeset

26 
by (cases u) (hypsubst, rule unit.case) 
49312  27 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55083
diff
changeset

28 
lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p" 
49539
be6cbf960aa7
fixed bug in "fold" tactic with nested products (beyond the sum of product corresponding to constructors)
blanchet
parents:
49510
diff
changeset

29 
by simp 
be6cbf960aa7
fixed bug in "fold" tactic with nested products (beyond the sum of product corresponding to constructors)
blanchet
parents:
49510
diff
changeset

30 

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

33 

49683  34 
lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x" 
55066  35 
unfolding comp_def fun_eq_iff by simp 
49312  36 

37 
lemma o_bij: 

49683  38 
assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id" 
49312  39 
shows "bij f" 
40 
unfolding bij_def inj_on_def surj_def proof safe 

41 
fix a1 a2 assume "f a1 = f a2" 

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

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

44 
next 

45 
fix b 

46 
have "b = f (g b)" 

47 
using fg unfolding fun_eq_iff by simp 

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

49 
qed 

50 

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

52 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55083
diff
changeset

53 
lemma case_sum_step: 
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55083
diff
changeset

54 
"case_sum (case_sum f' g') g (Inl p) = case_sum f' g' p" 
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55083
diff
changeset

55 
"case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p" 
49312  56 
by auto 
57 

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

59 
by blast 

60 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

61 
lemma type_copy_obj_one_point_absE: 
55811  62 
assumes "type_definition Rep Abs UNIV" "\<forall>x. s = Abs x \<longrightarrow> P" shows P 
63 
using type_definition.Rep_inverse[OF assms(1)] 

64 
by (intro mp[OF spec[OF assms(2), of "Rep s"]]) simp 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

65 

49312  66 
lemma obj_sumE_f: 
55811  67 
assumes "\<forall>x. s = f (Inl x) \<longrightarrow> P" "\<forall>x. s = f (Inr x) \<longrightarrow> P" 
68 
shows "\<forall>x. s = f x \<longrightarrow> P" 

69 
proof 

70 
fix x from assms show "s = f x \<longrightarrow> P" by (cases x) auto 

71 
qed 

49312  72 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55083
diff
changeset

73 
lemma case_sum_if: 
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55083
diff
changeset

74 
"case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)" 
49312  75 
by simp 
76 

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

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

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

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

80 
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

81 

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

82 
lemma sum_set_simps: 
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49430
diff
changeset

83 
"setl (Inl x) = {x}" 
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49430
diff
changeset

84 
"setl (Inr x) = {}" 
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49430
diff
changeset

85 
"setr (Inl x) = {}" 
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49430
diff
changeset

86 
"setr (Inr x) = {x}" 
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49430
diff
changeset

87 
unfolding sum_set_defs by simp+ 
49429
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

88 

57301
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

89 
lemma Inl_Inr_False: "(Inl x = Inr y) = False" 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

90 
by simp 
7b997028aaac
generate 'rel_coinduct0' theorem for codatatypes
desharna
parents:
57279
diff
changeset

91 

57471  92 
lemma Inr_Inl_False: "(Inr x = Inl y) = False" 
93 
by simp 

94 

52505
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52349
diff
changeset

95 
lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y" 
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52349
diff
changeset

96 
by blast 
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52349
diff
changeset

97 

56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
55966
diff
changeset

98 
lemma rewriteR_comp_comp: "\<lbrakk>g \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = f \<circ> r" 
55066  99 
unfolding comp_def fun_eq_iff by auto 
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

100 

56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
55966
diff
changeset

101 
lemma rewriteR_comp_comp2: "\<lbrakk>g \<circ> h = r1 \<circ> r2; f \<circ> r1 = l\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = l \<circ> r2" 
55066  102 
unfolding comp_def fun_eq_iff by auto 
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

103 

56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
55966
diff
changeset

104 
lemma rewriteL_comp_comp: "\<lbrakk>f \<circ> g = l\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l \<circ> h" 
55066  105 
unfolding comp_def fun_eq_iff by auto 
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

106 

56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
55966
diff
changeset

107 
lemma rewriteL_comp_comp2: "\<lbrakk>f \<circ> g = l1 \<circ> l2; l2 \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l1 \<circ> r" 
55066  108 
unfolding comp_def fun_eq_iff by auto 
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

109 

56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
55966
diff
changeset

110 
lemma convol_o: "<f, g> \<circ> h = <f \<circ> h, g \<circ> h>" 
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

111 
unfolding convol_def by auto 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

112 

56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
55966
diff
changeset

113 
lemma map_prod_o_convol: "map_prod h1 h2 \<circ> <f, g> = <h1 \<circ> f, h2 \<circ> g>" 
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

114 
unfolding convol_def by auto 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

115 

55932  116 
lemma map_prod_o_convol_id: "(map_prod f id \<circ> <id , g>) x = <id \<circ> f , g> x" 
117 
unfolding map_prod_o_convol id_comp comp_id .. 

52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

118 

56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
55966
diff
changeset

119 
lemma o_case_sum: "h \<circ> case_sum f g = case_sum (h \<circ> f) (h \<circ> g)" 
55066  120 
unfolding comp_def by (auto split: sum.splits) 
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

121 

56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
55966
diff
changeset

122 
lemma case_sum_o_map_sum: "case_sum f g \<circ> map_sum h1 h2 = case_sum (f \<circ> h1) (g \<circ> h2)" 
55066  123 
unfolding comp_def by (auto split: sum.splits) 
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

124 

56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
55966
diff
changeset

125 
lemma case_sum_o_map_sum_id: "(case_sum id g \<circ> map_sum f id) x = case_sum (f \<circ> id) g x" 
55931  126 
unfolding case_sum_o_map_sum id_comp comp_id .. 
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

127 

55945  128 
lemma rel_fun_def_butlast: 
129 
"rel_fun R (rel_fun S T) f g = (\<forall>x y. R x y \<longrightarrow> (rel_fun S T) (f x) (g y))" 

130 
unfolding rel_fun_def .. 

52731  131 

53105
ec38e9f4352f
simpler (forward) derivation of strong (upto equality) coinduction properties
traytel
parents:
52913
diff
changeset

132 
lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)" 
ec38e9f4352f
simpler (forward) derivation of strong (upto equality) coinduction properties
traytel
parents:
52913
diff
changeset

133 
by auto 
ec38e9f4352f
simpler (forward) derivation of strong (upto equality) coinduction properties
traytel
parents:
52913
diff
changeset

134 

ec38e9f4352f
simpler (forward) derivation of strong (upto equality) coinduction properties
traytel
parents:
52913
diff
changeset

135 
lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)" 
ec38e9f4352f
simpler (forward) derivation of strong (upto equality) coinduction properties
traytel
parents:
52913
diff
changeset

136 
by auto 
ec38e9f4352f
simpler (forward) derivation of strong (upto equality) coinduction properties
traytel
parents:
52913
diff
changeset

137 

53308  138 
lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)" 
139 
unfolding Grp_def id_apply by blast 

140 

141 
lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv> 

142 
(\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)" 

143 
unfolding Grp_def by rule auto 

144 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

145 
lemma vimage2p_mono: "vimage2p f g R x y \<Longrightarrow> R \<le> S \<Longrightarrow> vimage2p f g S x y" 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

146 
unfolding vimage2p_def by blast 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

147 

74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

148 
lemma vimage2p_refl: "(\<And>x. R x x) \<Longrightarrow> vimage2p f f R x x" 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

149 
unfolding vimage2p_def by auto 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

150 

74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

151 
lemma 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

152 
assumes "type_definition Rep Abs UNIV" 
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
55966
diff
changeset

153 
shows type_copy_Rep_o_Abs: "Rep \<circ> Abs = id" and type_copy_Abs_o_Rep: "Abs \<circ> Rep = id" 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

154 
unfolding fun_eq_iff comp_apply id_apply 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

155 
type_definition.Abs_inverse[OF assms UNIV_I] type_definition.Rep_inverse[OF assms] by simp_all 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

156 

74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

157 
lemma type_copy_map_comp0_undo: 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

158 
assumes "type_definition Rep Abs UNIV" 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

159 
"type_definition Rep' Abs' UNIV" 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

160 
"type_definition Rep'' Abs'' UNIV" 
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
55966
diff
changeset

161 
shows "Abs' \<circ> M \<circ> Rep'' = (Abs' \<circ> M1 \<circ> Rep) \<circ> (Abs \<circ> M2 \<circ> Rep'') \<Longrightarrow> M1 \<circ> M2 = M" 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

162 
by (rule sym) (auto simp: fun_eq_iff type_definition.Abs_inject[OF assms(2) UNIV_I UNIV_I] 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

163 
type_definition.Abs_inverse[OF assms(1) UNIV_I] 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

164 
type_definition.Abs_inverse[OF assms(3) UNIV_I] dest: spec[of _ "Abs'' x" for x]) 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

165 

55854
ee270328a781
make 'typedef' optional, depending on size of original type
blanchet
parents:
55811
diff
changeset

166 
lemma vimage2p_id: "vimage2p id id R = R" 
ee270328a781
make 'typedef' optional, depending on size of original type
blanchet
parents:
55811
diff
changeset

167 
unfolding vimage2p_def by auto 
ee270328a781
make 'typedef' optional, depending on size of original type
blanchet
parents:
55811
diff
changeset

168 

56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
55966
diff
changeset

169 
lemma vimage2p_comp: "vimage2p (f1 \<circ> f2) (g1 \<circ> g2) = vimage2p f2 g2 \<circ> vimage2p f1 g1" 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

170 
unfolding fun_eq_iff vimage2p_def o_apply by simp 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

171 

56650
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

172 
lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g" 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

173 
by (erule arg_cong) 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

174 

56684
d8f32f55e463
more unfolding and more folding in size equations, to look more natural in the nested case
blanchet
parents:
56651
diff
changeset

175 
lemma inj_on_convol_ident: "inj_on (\<lambda>x. (x, f x)) X" 
56650
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

176 
unfolding inj_on_def by simp 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

177 

1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

178 
lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x" 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

179 
by (case_tac x) simp 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

180 

1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

181 
lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x" 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

182 
by (case_tac x) simp+ 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

183 

1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

184 
lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x" 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

185 
by (case_tac x) simp+ 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

186 

1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

187 
lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)" 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

188 
by (simp add: inj_on_def) 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

189 

55062  190 
ML_file "Tools/BNF/bnf_fp_util.ML" 
191 
ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" 

56650
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

192 
ML_file "Tools/BNF/bnf_lfp_size.ML" 
55062  193 
ML_file "Tools/BNF/bnf_fp_def_sugar.ML" 
194 
ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML" 

195 
ML_file "Tools/BNF/bnf_fp_n2m.ML" 

196 
ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML" 

55702
63c80031d8dd
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents:
55700
diff
changeset

197 

56650
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

198 
ML_file "Tools/Function/size.ML" 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

199 
setup Size.setup 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

200 

1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

201 
lemma size_bool[code]: "size (b\<Colon>bool) = 0" 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

202 
by (cases b) auto 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

203 

56846
9df717fef2bb
renamed 'xxx_size' to 'size_xxx' for old datatype package
blanchet
parents:
56684
diff
changeset

204 
lemma size_nat[simp, code]: "size (n\<Colon>nat) = n" 
56650
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

205 
by (induct n) simp_all 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

206 

1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

207 
declare prod.size[no_atp] 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

208 

56846
9df717fef2bb
renamed 'xxx_size' to 'size_xxx' for old datatype package
blanchet
parents:
56684
diff
changeset

209 
lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)" 
56650
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

210 
by (rule ext) (case_tac x, auto) 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

211 

56846
9df717fef2bb
renamed 'xxx_size' to 'size_xxx' for old datatype package
blanchet
parents:
56684
diff
changeset

212 
lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)" 
56650
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

213 
by (rule ext) auto 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

214 

1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

215 
setup {* 
56846
9df717fef2bb
renamed 'xxx_size' to 'size_xxx' for old datatype package
blanchet
parents:
56684
diff
changeset

216 
BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size} 
9df717fef2bb
renamed 'xxx_size' to 'size_xxx' for old datatype package
blanchet
parents:
56684
diff
changeset

217 
@{thms size_sum_o_map} 
9df717fef2bb
renamed 'xxx_size' to 'size_xxx' for old datatype package
blanchet
parents:
56684
diff
changeset

218 
#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size} 
9df717fef2bb
renamed 'xxx_size' to 'size_xxx' for old datatype package
blanchet
parents:
56684
diff
changeset

219 
@{thms size_prod_o_map} 
56650
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

220 
*} 
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

221 

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

222 
end 