author | blanchet |
Thu, 06 Mar 2014 13:36:15 +0100 | |
changeset 55931 | 62156e694f3d |
parent 55930 | 25a90cebbbe5 |
child 55932 | 68c5104d2204 |
permissions | -rw-r--r-- |
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 high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset
|
19 |
lemma eq_sym_Unity_conv: "(x = (() = ())) = x" |
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49539
diff
changeset
|
20 |
by blast |
5c4a12550491
generate high-level "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 fp-operations
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 fp-operations
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 |
||
51745
a06a3c777add
simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
blanchet
parents:
51740
diff
changeset
|
86 |
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
|
87 |
by simp |
a06a3c777add
simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
blanchet
parents:
51740
diff
changeset
|
88 |
|
49429
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset
|
89 |
lemma prod_set_simps: |
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset
|
90 |
"fsts (x, y) = {x}" |
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset
|
91 |
"snds (x, y) = {y}" |
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset
|
92 |
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
|
93 |
|
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset
|
94 |
lemma sum_set_simps: |
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49430
diff
changeset
|
95 |
"setl (Inl x) = {x}" |
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49430
diff
changeset
|
96 |
"setl (Inr x) = {}" |
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49430
diff
changeset
|
97 |
"setr (Inl x) = {}" |
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49430
diff
changeset
|
98 |
"setr (Inr x) = {x}" |
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49430
diff
changeset
|
99 |
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
|
100 |
|
52505
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52349
diff
changeset
|
101 |
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
|
102 |
by blast |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52349
diff
changeset
|
103 |
|
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset
|
104 |
lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r" |
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 |
|
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset
|
107 |
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 | 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 |
|
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset
|
110 |
lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h" |
55066 | 111 |
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
|
112 |
|
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset
|
113 |
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 | 114 |
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
|
115 |
|
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset
|
116 |
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
|
117 |
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
|
118 |
|
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset
|
119 |
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
|
120 |
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
|
121 |
|
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset
|
122 |
lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x" |
55066 | 123 |
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
|
124 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55083
diff
changeset
|
125 |
lemma o_case_sum: "h o case_sum f g = case_sum (h o f) (h o g)" |
55066 | 126 |
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
|
127 |
|
55931 | 128 |
lemma case_sum_o_map_sum: "case_sum f g o map_sum h1 h2 = case_sum (f o h1) (g o h2)" |
55066 | 129 |
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
|
130 |
|
55931 | 131 |
lemma case_sum_o_map_sum_id: "(case_sum id g o map_sum f id) x = case_sum (f o id) g x" |
132 |
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
|
133 |
|
52731 | 134 |
lemma fun_rel_def_butlast: |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
135 |
"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 | 136 |
unfolding fun_rel_def .. |
137 |
||
53105
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
52913
diff
changeset
|
138 |
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 (up-to equality) coinduction properties
traytel
parents:
52913
diff
changeset
|
139 |
by auto |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
52913
diff
changeset
|
140 |
|
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
52913
diff
changeset
|
141 |
lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)" |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
52913
diff
changeset
|
142 |
by auto |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
52913
diff
changeset
|
143 |
|
53308 | 144 |
lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)" |
145 |
unfolding Grp_def id_apply by blast |
|
146 |
||
147 |
lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv> |
|
148 |
(\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)" |
|
149 |
unfolding Grp_def by rule auto |
|
150 |
||
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
151 |
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 fp-operations
traytel
parents:
55702
diff
changeset
|
152 |
unfolding vimage2p_def by blast |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
153 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
154 |
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 fp-operations
traytel
parents:
55702
diff
changeset
|
155 |
unfolding vimage2p_def by auto |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
156 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
157 |
lemma |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
158 |
assumes "type_definition Rep Abs UNIV" |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
159 |
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 fp-operations
traytel
parents:
55702
diff
changeset
|
160 |
unfolding fun_eq_iff comp_apply id_apply |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
161 |
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 fp-operations
traytel
parents:
55702
diff
changeset
|
162 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
163 |
lemma type_copy_map_comp0_undo: |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
164 |
assumes "type_definition Rep Abs UNIV" |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
165 |
"type_definition Rep' Abs' UNIV" |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
166 |
"type_definition Rep'' Abs'' UNIV" |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
167 |
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 fp-operations
traytel
parents:
55702
diff
changeset
|
168 |
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 fp-operations
traytel
parents:
55702
diff
changeset
|
169 |
type_definition.Abs_inverse[OF assms(1) UNIV_I] |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
170 |
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 fp-operations
traytel
parents:
55702
diff
changeset
|
171 |
|
55854
ee270328a781
make 'typedef' optional, depending on size of original type
blanchet
parents:
55811
diff
changeset
|
172 |
lemma vimage2p_id: "vimage2p id id R = R" |
ee270328a781
make 'typedef' optional, depending on size of original type
blanchet
parents:
55811
diff
changeset
|
173 |
unfolding vimage2p_def by auto |
ee270328a781
make 'typedef' optional, depending on size of original type
blanchet
parents:
55811
diff
changeset
|
174 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
175 |
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 fp-operations
traytel
parents:
55702
diff
changeset
|
176 |
unfolding fun_eq_iff vimage2p_def o_apply by simp |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55702
diff
changeset
|
177 |
|
55062 | 178 |
ML_file "Tools/BNF/bnf_fp_util.ML" |
179 |
ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" |
|
180 |
ML_file "Tools/BNF/bnf_fp_def_sugar.ML" |
|
181 |
ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML" |
|
182 |
ML_file "Tools/BNF/bnf_fp_n2m.ML" |
|
183 |
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
|
184 |
|
49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
185 |
end |