|
1 (* Title: HOL/BNF/BNF_FP_Base.thy |
|
2 Author: Lorenz Panny, TU Muenchen |
|
3 Author: Dmitriy Traytel, TU Muenchen |
|
4 Author: Jasmin Blanchette, TU Muenchen |
|
5 Copyright 2012, 2013 |
|
6 |
|
7 Shared fixed point operations on bounded natural functors, including |
|
8 *) |
|
9 |
|
10 header {* Shared Fixed Point Operations on Bounded Natural Functors *} |
|
11 |
|
12 theory BNF_FP_Base |
|
13 imports BNF_Comp BNF_Ctr_Sugar |
|
14 keywords |
|
15 "defaults" |
|
16 begin |
|
17 |
|
18 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" |
|
19 by auto |
|
20 |
|
21 lemma eq_sym_Unity_conv: "(x = (() = ())) = x" |
|
22 by blast |
|
23 |
|
24 lemma unit_case_Unity: "(case u of () => f) = f" |
|
25 by (cases u) (hypsubst, rule unit.cases) |
|
26 |
|
27 lemma prod_case_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p" |
|
28 by simp |
|
29 |
|
30 lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" |
|
31 by simp |
|
32 |
|
33 lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" |
|
34 by clarify |
|
35 |
|
36 lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" |
|
37 by auto |
|
38 |
|
39 lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x" |
|
40 unfolding o_def fun_eq_iff by simp |
|
41 |
|
42 lemma o_bij: |
|
43 assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id" |
|
44 shows "bij f" |
|
45 unfolding bij_def inj_on_def surj_def proof safe |
|
46 fix a1 a2 assume "f a1 = f a2" |
|
47 hence "g ( f a1) = g (f a2)" by simp |
|
48 thus "a1 = a2" using gf unfolding fun_eq_iff by simp |
|
49 next |
|
50 fix b |
|
51 have "b = f (g b)" |
|
52 using fg unfolding fun_eq_iff by simp |
|
53 thus "EX a. b = f a" by blast |
|
54 qed |
|
55 |
|
56 lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp |
|
57 |
|
58 lemma sum_case_step: |
|
59 "sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p" |
|
60 "sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p" |
|
61 by auto |
|
62 |
|
63 lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
|
64 by simp |
|
65 |
|
66 lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P" |
|
67 by blast |
|
68 |
|
69 lemma obj_sumE_f: |
|
70 "\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P" |
|
71 by (rule allI) (metis sumE) |
|
72 |
|
73 lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
|
74 by (cases s) auto |
|
75 |
|
76 lemma sum_case_if: |
|
77 "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)" |
|
78 by simp |
|
79 |
|
80 lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)" |
|
81 by blast |
|
82 |
|
83 lemma UN_compreh_eq_eq: |
|
84 "\<Union>{y. \<exists>x\<in>A. y = {}} = {}" |
|
85 "\<Union>{y. \<exists>x\<in>A. y = {x}} = A" |
|
86 by blast+ |
|
87 |
|
88 lemma Inl_Inr_False: "(Inl x = Inr y) = False" |
|
89 by simp |
|
90 |
|
91 lemma prod_set_simps: |
|
92 "fsts (x, y) = {x}" |
|
93 "snds (x, y) = {y}" |
|
94 unfolding fsts_def snds_def by simp+ |
|
95 |
|
96 lemma sum_set_simps: |
|
97 "setl (Inl x) = {x}" |
|
98 "setl (Inr x) = {}" |
|
99 "setr (Inl x) = {}" |
|
100 "setr (Inr x) = {x}" |
|
101 unfolding sum_set_defs by simp+ |
|
102 |
|
103 lemma prod_rel_simp: |
|
104 "prod_rel P Q (x, y) (x', y') \<longleftrightarrow> P x x' \<and> Q y y'" |
|
105 unfolding prod_rel_def by simp |
|
106 |
|
107 lemma sum_rel_simps: |
|
108 "sum_rel P Q (Inl x) (Inl x') \<longleftrightarrow> P x x'" |
|
109 "sum_rel P Q (Inr y) (Inr y') \<longleftrightarrow> Q y y'" |
|
110 "sum_rel P Q (Inl x) (Inr y') \<longleftrightarrow> False" |
|
111 "sum_rel P Q (Inr y) (Inl x') \<longleftrightarrow> False" |
|
112 unfolding sum_rel_def by simp+ |
|
113 |
|
114 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y" |
|
115 by blast |
|
116 |
|
117 lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r" |
|
118 unfolding o_def fun_eq_iff by auto |
|
119 |
|
120 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" |
|
121 unfolding o_def fun_eq_iff by auto |
|
122 |
|
123 lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h" |
|
124 unfolding o_def fun_eq_iff by auto |
|
125 |
|
126 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" |
|
127 unfolding o_def fun_eq_iff by auto |
|
128 |
|
129 lemma convol_o: "<f, g> o h = <f o h, g o h>" |
|
130 unfolding convol_def by auto |
|
131 |
|
132 lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>" |
|
133 unfolding convol_def by auto |
|
134 |
|
135 lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x" |
|
136 unfolding map_pair_o_convol id_o o_id .. |
|
137 |
|
138 lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)" |
|
139 unfolding o_def by (auto split: sum.splits) |
|
140 |
|
141 lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)" |
|
142 unfolding o_def by (auto split: sum.splits) |
|
143 |
|
144 lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x" |
|
145 unfolding sum_case_o_sum_map id_o o_id .. |
|
146 |
|
147 lemma fun_rel_def_butlast: |
|
148 "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))" |
|
149 unfolding fun_rel_def .. |
|
150 |
|
151 lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)" |
|
152 by auto |
|
153 |
|
154 lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)" |
|
155 by auto |
|
156 |
|
157 lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)" |
|
158 unfolding Grp_def id_apply by blast |
|
159 |
|
160 lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv> |
|
161 (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)" |
|
162 unfolding Grp_def by rule auto |
|
163 |
|
164 lemma if_if_True: |
|
165 "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) = |
|
166 (if b then x else if b' then x' else f y')" |
|
167 by simp |
|
168 |
|
169 lemma if_if_False: |
|
170 "(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) = |
|
171 (if b then f y else if b' then x' else f y')" |
|
172 by simp |
|
173 |
|
174 ML_file "Tools/bnf_fp_util.ML" |
|
175 ML_file "Tools/bnf_fp_def_sugar_tactics.ML" |
|
176 ML_file "Tools/bnf_fp_def_sugar.ML" |
|
177 ML_file "Tools/bnf_fp_n2m_tactics.ML" |
|
178 ML_file "Tools/bnf_fp_n2m.ML" |
|
179 ML_file "Tools/bnf_fp_n2m_sugar.ML" |
|
180 ML_file "Tools/bnf_fp_rec_sugar_util.ML" |
|
181 ML_file "Tools/bnf_fp_rec_sugar_tactics.ML" |
|
182 ML_file "Tools/bnf_fp_rec_sugar.ML" |
|
183 |
|
184 end |