author  traytel 
Fri, 28 Feb 2014 17:54:52 +0100  
changeset 55811  aa1acc25126b 
parent 55803  74d3fe9031d8 
child 55854  ee270328a781 
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 
55083  13 
imports BNF_Comp 
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 

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

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

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

21 

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

22 
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

23 
by (cases u) (hypsubst, rule unit.case) 
49312  24 

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

25 
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

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

27 

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

30 

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

32 
by clarify 

33 

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

35 
by auto 

36 

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

40 
lemma o_bij: 

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

44 
fix a1 a2 assume "f a1 = f a2" 

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

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

47 
next 

48 
fix b 

49 
have "b = f (g b)" 

50 
using fg unfolding fun_eq_iff by simp 

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

52 
qed 

53 

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

55 

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

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

57 
"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

58 
"case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p" 
49312  59 
by auto 
60 

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

62 
by simp 

63 

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

65 
by blast 

66 

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

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

70 
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

71 

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

75 
proof 

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

77 
qed 

49312  78 

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

80 
by (cases s) auto 

81 

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

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

83 
"case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)" 
49312  84 
by simp 
85 

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

86 
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

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

88 

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

89 
lemma UN_compreh_eq_eq: 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49539
diff
changeset

90 
"\<Union>{y. \<exists>x\<in>A. y = {}} = {}" 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49539
diff
changeset

91 
"\<Union>{y. \<exists>x\<in>A. y = {x}} = A" 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49539
diff
changeset

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

93 

51745
a06a3c777add
simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
blanchet
parents:
51740
diff
changeset

94 
lemma Inl_Inr_False: "(Inl x = Inr y) = False" 
a06a3c777add
simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
blanchet
parents:
51740
diff
changeset

95 
by simp 
a06a3c777add
simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
blanchet
parents:
51740
diff
changeset

96 

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

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

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

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

100 
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

101 

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

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

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

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

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

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

107 
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

108 

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

109 
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

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

111 

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

112 
lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r" 
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 

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

115 
lemma rewriteR_comp_comp2: "\<lbrakk>g o h = r1 o r2; f o r1 = l\<rbrakk> \<Longrightarrow> f o g o h = l o r2" 
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 

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

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

120 

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

121 
lemma rewriteL_comp_comp2: "\<lbrakk>f o g = l1 o l2; l2 o h = r\<rbrakk> \<Longrightarrow> f o (g o h) = l1 o r" 
55066  122 
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

123 

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

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

125 
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

126 

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

127 
lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>" 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

128 
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

129 

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

130 
lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x" 
55066  131 
unfolding map_pair_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

132 

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

133 
lemma o_case_sum: "h o case_sum f g = case_sum (h o f) (h o g)" 
55066  134 
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

135 

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

136 
lemma case_sum_o_sum_map: "case_sum f g o sum_map h1 h2 = case_sum (f o h1) (g o h2)" 
55066  137 
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

138 

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

139 
lemma case_sum_o_sum_map_id: "(case_sum id g o sum_map f id) x = case_sum (f o id) g x" 
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55083
diff
changeset

140 
unfolding case_sum_o_sum_map 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

141 

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

143 
"fun_rel R (fun_rel S T) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))" 
52731  144 
unfolding fun_rel_def .. 
145 

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

146 
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

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

148 

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

149 
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

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

151 

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

154 

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

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

157 
unfolding Grp_def by rule auto 

158 

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

159 
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

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

161 

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

162 
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

163 
unfolding vimage2p_def by auto 
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 
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 
shows type_copy_Rep_o_Abs: "Rep \<circ> Abs = id" and type_copy_Abs_o_Rep: "Abs o Rep = id" 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

168 
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

169 
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

170 

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

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

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

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

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

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

176 
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

177 
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

178 
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

179 

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

180 
lemma vimage2p_comp: "vimage2p (f1 o f2) (g1 o g2) = vimage2p f2 g2 o vimage2p f1 g1" 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55702
diff
changeset

181 
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

182 

55062  183 
ML_file "Tools/BNF/bnf_fp_util.ML" 
184 
ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" 

185 
ML_file "Tools/BNF/bnf_fp_def_sugar.ML" 

186 
ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML" 

187 
ML_file "Tools/BNF/bnf_fp_n2m.ML" 

188 
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

189 

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

190 
end 