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
7 Shared fixed point operations on bounded natural functors, including
10 header {* Shared Fixed Point Operations on Bounded Natural Functors *}
13 imports BNF_Comp BNF_Ctr_Sugar
16 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
19 lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
22 lemma unit_case_Unity: "(case u of () => f) = f"
23 by (cases u) (hypsubst, rule unit.cases)
25 lemma prod_case_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
28 lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
31 lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
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"
37 lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
38 unfolding o_def fun_eq_iff by simp
41 assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id"
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
50 using fg unfolding fun_eq_iff by simp
51 thus "EX a. b = f a" by blast
54 lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
57 "sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
58 "sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
61 lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
64 lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
68 "\<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"
69 by (rule allI) (metis sumE)
71 lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
75 "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
78 lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
81 lemma UN_compreh_eq_eq:
82 "\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
83 "\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
86 lemma Inl_Inr_False: "(Inl x = Inr y) = False"
92 unfolding fsts_def snds_def by simp+
99 unfolding sum_set_defs by simp+
102 "prod_rel P Q (x, y) (x', y') \<longleftrightarrow> P x x' \<and> Q y y'"
103 unfolding prod_rel_def by simp
106 "sum_rel P Q (Inl x) (Inl x') \<longleftrightarrow> P x x'"
107 "sum_rel P Q (Inr y) (Inr y') \<longleftrightarrow> Q y y'"
108 "sum_rel P Q (Inl x) (Inr y') \<longleftrightarrow> False"
109 "sum_rel P Q (Inr y) (Inl x') \<longleftrightarrow> False"
110 unfolding sum_rel_def by simp+
112 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
115 lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
116 unfolding o_def fun_eq_iff by auto
118 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"
119 unfolding o_def fun_eq_iff by auto
121 lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
122 unfolding o_def fun_eq_iff by auto
124 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"
125 unfolding o_def fun_eq_iff by auto
127 lemma convol_o: "<f, g> o h = <f o h, g o h>"
128 unfolding convol_def by auto
130 lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>"
131 unfolding convol_def by auto
133 lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
134 unfolding map_pair_o_convol id_o o_id ..
136 lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
137 unfolding o_def by (auto split: sum.splits)
139 lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
140 unfolding o_def by (auto split: sum.splits)
142 lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
143 unfolding sum_case_o_sum_map id_o o_id ..
145 lemma fun_rel_def_butlast:
146 "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
147 unfolding fun_rel_def ..
149 lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
152 lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
155 lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)"
156 unfolding Grp_def id_apply by blast
158 lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv>
159 (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
160 unfolding Grp_def by rule auto
162 lemma eq_ifI: "\<lbrakk>b \<Longrightarrow> t = x; \<not> b \<Longrightarrow> t = y\<rbrakk> \<Longrightarrow> t = (if b then x else y)"
166 "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
167 (if b then x else if b' then x' else f y')"
171 "(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) =
172 (if b then f y else if b' then x' else f y')"
175 lemma if_then_else_True_False:
176 "(if p then False else r) \<longleftrightarrow> \<not> p \<and> r"
177 "(if p then True else r) \<longleftrightarrow> p \<or> r"
178 "(if p then q else False) \<longleftrightarrow> p \<and> q"
179 "(if p then q else True) \<longleftrightarrow> \<not> p \<or> q"
182 lemmas bool_if_simps = bool_simps(7,8,15-17,19,21-24,29-32) if_then_else_True_False
184 ML_file "Tools/bnf_fp_util.ML"
185 ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
186 ML_file "Tools/bnf_fp_def_sugar.ML"
187 ML_file "Tools/bnf_fp_n2m_tactics.ML"
188 ML_file "Tools/bnf_fp_n2m.ML"
189 ML_file "Tools/bnf_fp_n2m_sugar.ML"
190 ML_file "Tools/bnf_fp_rec_sugar_util.ML"
191 ML_file "Tools/bnf_fp_rec_sugar_tactics.ML"
192 ML_file "Tools/bnf_fp_rec_sugar.ML"