author  wenzelm 
Sat, 18 Jul 2015 22:58:50 +0200  
changeset 60758  d8d85a8172b5 
parent 58916  229765cc3414 
child 60918  4ceef1592e8c 
permissions  rwrr 
58128  1 
(* Title: HOL/BNF_Fixpoint_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 
57698  5 
Author: Martin Desharnais, TU Muenchen 
6 
Copyright 2012, 2013, 2014 

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

7 

58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
58179
diff
changeset

8 
Shared fixpoint 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

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

10 

60758  11 
section \<open>Shared Fixpoint Operations on Bounded Natural Functors\<close> 
49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

12 

58128  13 
theory BNF_Fixpoint_Base 
14 
imports BNF_Composition 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

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 

57525  17 
lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True" 
18 
by default simp_all 

19 

20 
lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)" 

21 
by default simp_all 

22 

49590  23 
lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" 
58159  24 
by auto 
49590  25 

57303  26 
lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y" 
57302  27 
by auto 
28 

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

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

31 

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

32 
lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f" 
58159  33 
by (cases u) (hypsubst, rule unit.case) 
49312  34 

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

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

37 

49335  38 
lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" 
58159  39 
by simp 
49335  40 

49683  41 
lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x" 
58159  42 
unfolding comp_def fun_eq_iff by simp 
49312  43 

44 
lemma o_bij: 

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

48 
fix a1 a2 assume "f a1 = f a2" 

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

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

51 
next 

52 
fix b 

53 
have "b = f (g b)" 

54 
using fg unfolding fun_eq_iff by simp 

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

56 
qed 

57 

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

49312  60 

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

61 
lemma case_sum_step: 
58159  62 
"case_sum (case_sum f' g') g (Inl p) = case_sum f' g' p" 
63 
"case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p" 

64 
by auto 

49312  65 

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

58159  67 
by blast 
49312  68 

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

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

72 
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

73 

49312  74 
lemma obj_sumE_f: 
55811  75 
assumes "\<forall>x. s = f (Inl x) \<longrightarrow> P" "\<forall>x. s = f (Inr x) \<longrightarrow> P" 
76 
shows "\<forall>x. s = f x \<longrightarrow> P" 

77 
proof 

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

79 
qed 

49312  80 

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

81 
lemma case_sum_if: 
58159  82 
"case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)" 
83 
by simp 

49312  84 

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

85 
lemma prod_set_simps: 
58159  86 
"fsts (x, y) = {x}" 
87 
"snds (x, y) = {y}" 

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

89 

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

90 
lemma sum_set_simps: 
58159  91 
"setl (Inl x) = {x}" 
92 
"setl (Inr x) = {}" 

93 
"setr (Inl x) = {}" 

94 
"setr (Inr x) = {x}" 

95 
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

96 

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

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

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

99 

57471  100 
lemma Inr_Inl_False: "(Inr x = Inl y) = False" 
101 
by simp 

102 

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

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

105 

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

106 
lemma rewriteR_comp_comp: "\<lbrakk>g \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = f \<circ> r" 
55066  107 
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

108 

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

109 
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  110 
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

111 

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

112 
lemma rewriteL_comp_comp: "\<lbrakk>f \<circ> g = l\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l \<circ> h" 
55066  113 
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

114 

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

115 
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  116 
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

117 

57641
dc59f147b27d
more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
wenzelm
parents:
57525
diff
changeset

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

119 
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

120 

57641
dc59f147b27d
more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
wenzelm
parents:
57525
diff
changeset

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

122 
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

123 

57641
dc59f147b27d
more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
wenzelm
parents:
57525
diff
changeset

124 
lemma map_prod_o_convol_id: "(map_prod f id \<circ> \<langle>id, g\<rangle>) x = \<langle>id \<circ> f, g\<rangle> x" 
55932  125 
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

126 

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

127 
lemma o_case_sum: "h \<circ> case_sum f g = case_sum (h \<circ> f) (h \<circ> g)" 
55066  128 
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

129 

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

130 
lemma case_sum_o_map_sum: "case_sum f g \<circ> map_sum h1 h2 = case_sum (f \<circ> h1) (g \<circ> h2)" 
55066  131 
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

132 

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

133 
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  134 
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

135 

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

138 
unfolding rel_fun_def .. 

52731  139 

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

140 
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

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

142 

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

143 
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

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

145 

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

148 

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

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

151 
unfolding Grp_def by rule auto 

152 

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

153 
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

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

155 

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

156 
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

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

158 

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

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

160 
assumes "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 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

162 
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

163 
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

164 

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

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

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

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

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

169 
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

170 
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

171 
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

172 
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

173 

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

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

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

176 

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

177 
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

178 
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

179 

58446  180 
lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g" 
181 
unfolding rel_fun_def vimage2p_def by auto 

182 

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

183 
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

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

185 

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

186 
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

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

188 

58734  189 
lemma map_sum_if_distrib_then: 
190 
"\<And>f g e x y. map_sum f g (if e then Inl x else y) = (if e then Inl (f x) else map_sum f g y)" 

191 
"\<And>f g e x y. map_sum f g (if e then Inr x else y) = (if e then Inr (g x) else map_sum f g y)" 

192 
by simp_all 

193 

194 
lemma map_sum_if_distrib_else: 

195 
"\<And>f g e x y. map_sum f g (if e then x else Inl y) = (if e then map_sum f g x else Inl (f y))" 

196 
"\<And>f g e x y. map_sum f g (if e then x else Inr y) = (if e then map_sum f g x else Inr (g y))" 

197 
by simp_all 

198 

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

199 
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

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

201 

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

202 
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

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

204 

58446  205 
lemma case_sum_transfer: 
206 
"rel_fun (rel_fun R T) (rel_fun (rel_fun S T) (rel_fun (rel_sum R S) T)) case_sum case_sum" 

58916  207 
unfolding rel_fun_def by (auto split: sum.splits) 
58446  208 

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

209 
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

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

211 

58732  212 
lemma case_prod_o_map_prod: "case_prod f \<circ> map_prod g1 g2 = case_prod (\<lambda>l r. f (g1 l) (g2 r))" 
213 
unfolding comp_def by auto 

214 

58446  215 
lemma case_prod_transfer: 
216 
"(rel_fun (rel_fun A (rel_fun B C)) (rel_fun (rel_prod A B) C)) case_prod case_prod" 

58916  217 
unfolding rel_fun_def by simp 
56650
1f9ab71d43a5
no need to make 'size' generation an interpretation  overkill
blanchet
parents:
56640
diff
changeset

218 

57489  219 
lemma eq_ifI: "(P \<longrightarrow> t = u1) \<Longrightarrow> (\<not> P \<longrightarrow> t = u2) \<Longrightarrow> t = (if P then u1 else u2)" 
220 
by simp 

221 

58446  222 
lemma comp_transfer: 
223 
"rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (op \<circ>) (op \<circ>)" 

224 
unfolding rel_fun_def by simp 

225 

58448  226 
lemma If_transfer: "rel_fun (op =) (rel_fun A (rel_fun A A)) If If" 
227 
unfolding rel_fun_def by simp 

228 

229 
lemma Abs_transfer: 

230 
assumes type_copy1: "type_definition Rep1 Abs1 UNIV" 

231 
assumes type_copy2: "type_definition Rep2 Abs2 UNIV" 

232 
shows "rel_fun R (vimage2p Rep1 Rep2 R) Abs1 Abs2" 

233 
unfolding vimage2p_def rel_fun_def 

234 
type_definition.Abs_inverse[OF type_copy1 UNIV_I] 

235 
type_definition.Abs_inverse[OF type_copy2 UNIV_I] by simp 

236 

237 
lemma Inl_transfer: 

238 
"rel_fun S (rel_sum S T) Inl Inl" 

239 
by auto 

240 

241 
lemma Inr_transfer: 

242 
"rel_fun T (rel_sum S T) Inr Inr" 

243 
by auto 

244 

245 
lemma Pair_transfer: "rel_fun A (rel_fun B (rel_prod A B)) Pair Pair" 

58916  246 
unfolding rel_fun_def by simp 
58448  247 

55062  248 
ML_file "Tools/BNF/bnf_fp_util.ML" 
249 
ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" 

250 
ML_file "Tools/BNF/bnf_fp_def_sugar.ML" 

251 
ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML" 

252 
ML_file "Tools/BNF/bnf_fp_n2m.ML" 

253 
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

254 

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

255 
end 