1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/BNF/BNF_FP_Base.thy Fri Aug 30 12:43:39 2013 +0200
1.3 @@ -0,0 +1,184 @@
1.4 +(* Title: HOL/BNF/BNF_FP_Base.thy
1.5 + Author: Lorenz Panny, TU Muenchen
1.6 + Author: Dmitriy Traytel, TU Muenchen
1.7 + Author: Jasmin Blanchette, TU Muenchen
1.8 + Copyright 2012, 2013
1.9 +
1.10 +Shared fixed point operations on bounded natural functors, including
1.11 +*)
1.12 +
1.13 +header {* Shared Fixed Point Operations on Bounded Natural Functors *}
1.14 +
1.15 +theory BNF_FP_Base
1.16 +imports BNF_Comp BNF_Ctr_Sugar
1.17 +keywords
1.18 + "defaults"
1.19 +begin
1.20 +
1.21 +lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
1.22 +by auto
1.23 +
1.24 +lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
1.25 +by blast
1.26 +
1.27 +lemma unit_case_Unity: "(case u of () => f) = f"
1.28 +by (cases u) (hypsubst, rule unit.cases)
1.29 +
1.30 +lemma prod_case_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
1.31 +by simp
1.32 +
1.33 +lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
1.34 +by simp
1.35 +
1.36 +lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
1.37 +by clarify
1.38 +
1.39 +lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
1.40 +by auto
1.41 +
1.42 +lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
1.43 +unfolding o_def fun_eq_iff by simp
1.44 +
1.45 +lemma o_bij:
1.46 + assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id"
1.47 + shows "bij f"
1.48 +unfolding bij_def inj_on_def surj_def proof safe
1.49 + fix a1 a2 assume "f a1 = f a2"
1.50 + hence "g ( f a1) = g (f a2)" by simp
1.51 + thus "a1 = a2" using gf unfolding fun_eq_iff by simp
1.52 +next
1.53 + fix b
1.54 + have "b = f (g b)"
1.55 + using fg unfolding fun_eq_iff by simp
1.56 + thus "EX a. b = f a" by blast
1.57 +qed
1.58 +
1.59 +lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
1.60 +
1.61 +lemma sum_case_step:
1.62 +"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
1.63 +"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
1.64 +by auto
1.65 +
1.66 +lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
1.67 +by simp
1.68 +
1.69 +lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
1.70 +by blast
1.71 +
1.72 +lemma obj_sumE_f:
1.73 +"\<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"
1.74 +by (rule allI) (metis sumE)
1.75 +
1.76 +lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
1.77 +by (cases s) auto
1.78 +
1.79 +lemma sum_case_if:
1.80 +"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
1.81 +by simp
1.82 +
1.83 +lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
1.84 +by blast
1.85 +
1.86 +lemma UN_compreh_eq_eq:
1.87 +"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
1.88 +"\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
1.89 +by blast+
1.90 +
1.91 +lemma Inl_Inr_False: "(Inl x = Inr y) = False"
1.92 +by simp
1.93 +
1.94 +lemma prod_set_simps:
1.95 +"fsts (x, y) = {x}"
1.96 +"snds (x, y) = {y}"
1.97 +unfolding fsts_def snds_def by simp+
1.98 +
1.99 +lemma sum_set_simps:
1.100 +"setl (Inl x) = {x}"
1.101 +"setl (Inr x) = {}"
1.102 +"setr (Inl x) = {}"
1.103 +"setr (Inr x) = {x}"
1.104 +unfolding sum_set_defs by simp+
1.105 +
1.106 +lemma prod_rel_simp:
1.107 +"prod_rel P Q (x, y) (x', y') \<longleftrightarrow> P x x' \<and> Q y y'"
1.108 +unfolding prod_rel_def by simp
1.109 +
1.110 +lemma sum_rel_simps:
1.111 +"sum_rel P Q (Inl x) (Inl x') \<longleftrightarrow> P x x'"
1.112 +"sum_rel P Q (Inr y) (Inr y') \<longleftrightarrow> Q y y'"
1.113 +"sum_rel P Q (Inl x) (Inr y') \<longleftrightarrow> False"
1.114 +"sum_rel P Q (Inr y) (Inl x') \<longleftrightarrow> False"
1.115 +unfolding sum_rel_def by simp+
1.116 +
1.117 +lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
1.118 +by blast
1.119 +
1.120 +lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
1.121 + unfolding o_def fun_eq_iff by auto
1.122 +
1.123 +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"
1.124 + unfolding o_def fun_eq_iff by auto
1.125 +
1.126 +lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
1.127 + unfolding o_def fun_eq_iff by auto
1.128 +
1.129 +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"
1.130 + unfolding o_def fun_eq_iff by auto
1.131 +
1.132 +lemma convol_o: "<f, g> o h = <f o h, g o h>"
1.133 + unfolding convol_def by auto
1.134 +
1.135 +lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>"
1.136 + unfolding convol_def by auto
1.137 +
1.138 +lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
1.139 + unfolding map_pair_o_convol id_o o_id ..
1.140 +
1.141 +lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
1.142 + unfolding o_def by (auto split: sum.splits)
1.143 +
1.144 +lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
1.145 + unfolding o_def by (auto split: sum.splits)
1.146 +
1.147 +lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
1.148 + unfolding sum_case_o_sum_map id_o o_id ..
1.149 +
1.150 +lemma fun_rel_def_butlast:
1.151 + "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
1.152 + unfolding fun_rel_def ..
1.153 +
1.154 +lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
1.155 + by auto
1.156 +
1.157 +lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
1.158 + by auto
1.159 +
1.160 +lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)"
1.161 + unfolding Grp_def id_apply by blast
1.162 +
1.163 +lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv>
1.164 + (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
1.165 + unfolding Grp_def by rule auto
1.166 +
1.167 +lemma if_if_True:
1.168 + "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
1.169 + (if b then x else if b' then x' else f y')"
1.170 + by simp
1.171 +
1.172 +lemma if_if_False:
1.173 + "(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) =
1.174 + (if b then f y else if b' then x' else f y')"
1.175 + by simp
1.176 +
1.177 +ML_file "Tools/bnf_fp_util.ML"
1.178 +ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
1.179 +ML_file "Tools/bnf_fp_def_sugar.ML"
1.180 +ML_file "Tools/bnf_fp_n2m_tactics.ML"
1.181 +ML_file "Tools/bnf_fp_n2m.ML"
1.182 +ML_file "Tools/bnf_fp_n2m_sugar.ML"
1.183 +ML_file "Tools/bnf_fp_rec_sugar_util.ML"
1.184 +ML_file "Tools/bnf_fp_rec_sugar_tactics.ML"
1.185 +ML_file "Tools/bnf_fp_rec_sugar.ML"
1.186 +
1.187 +end
2.1 --- a/src/HOL/BNF/BNF_FP_Basic.thy Fri Aug 30 12:37:03 2013 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,183 +0,0 @@
2.4 -(* Title: HOL/BNF/BNF_FP_Basic.thy
2.5 - Author: Dmitriy Traytel, TU Muenchen
2.6 - Author: Jasmin Blanchette, TU Muenchen
2.7 - Copyright 2012
2.8 -
2.9 -Basic fixed point operations on bounded natural functors.
2.10 -*)
2.11 -
2.12 -header {* Basic Fixed Point Operations on Bounded Natural Functors *}
2.13 -
2.14 -theory BNF_FP_Basic
2.15 -imports BNF_Comp BNF_Ctr_Sugar
2.16 -keywords
2.17 - "defaults"
2.18 -begin
2.19 -
2.20 -lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
2.21 -by auto
2.22 -
2.23 -lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
2.24 -by blast
2.25 -
2.26 -lemma unit_case_Unity: "(case u of () => f) = f"
2.27 -by (cases u) (hypsubst, rule unit.cases)
2.28 -
2.29 -lemma prod_case_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
2.30 -by simp
2.31 -
2.32 -lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
2.33 -by simp
2.34 -
2.35 -lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
2.36 -by clarify
2.37 -
2.38 -lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
2.39 -by auto
2.40 -
2.41 -lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
2.42 -unfolding o_def fun_eq_iff by simp
2.43 -
2.44 -lemma o_bij:
2.45 - assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id"
2.46 - shows "bij f"
2.47 -unfolding bij_def inj_on_def surj_def proof safe
2.48 - fix a1 a2 assume "f a1 = f a2"
2.49 - hence "g ( f a1) = g (f a2)" by simp
2.50 - thus "a1 = a2" using gf unfolding fun_eq_iff by simp
2.51 -next
2.52 - fix b
2.53 - have "b = f (g b)"
2.54 - using fg unfolding fun_eq_iff by simp
2.55 - thus "EX a. b = f a" by blast
2.56 -qed
2.57 -
2.58 -lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
2.59 -
2.60 -lemma sum_case_step:
2.61 -"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
2.62 -"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
2.63 -by auto
2.64 -
2.65 -lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
2.66 -by simp
2.67 -
2.68 -lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
2.69 -by blast
2.70 -
2.71 -lemma obj_sumE_f:
2.72 -"\<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"
2.73 -by (rule allI) (metis sumE)
2.74 -
2.75 -lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
2.76 -by (cases s) auto
2.77 -
2.78 -lemma sum_case_if:
2.79 -"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
2.80 -by simp
2.81 -
2.82 -lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
2.83 -by blast
2.84 -
2.85 -lemma UN_compreh_eq_eq:
2.86 -"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
2.87 -"\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
2.88 -by blast+
2.89 -
2.90 -lemma Inl_Inr_False: "(Inl x = Inr y) = False"
2.91 -by simp
2.92 -
2.93 -lemma prod_set_simps:
2.94 -"fsts (x, y) = {x}"
2.95 -"snds (x, y) = {y}"
2.96 -unfolding fsts_def snds_def by simp+
2.97 -
2.98 -lemma sum_set_simps:
2.99 -"setl (Inl x) = {x}"
2.100 -"setl (Inr x) = {}"
2.101 -"setr (Inl x) = {}"
2.102 -"setr (Inr x) = {x}"
2.103 -unfolding sum_set_defs by simp+
2.104 -
2.105 -lemma prod_rel_simp:
2.106 -"prod_rel P Q (x, y) (x', y') \<longleftrightarrow> P x x' \<and> Q y y'"
2.107 -unfolding prod_rel_def by simp
2.108 -
2.109 -lemma sum_rel_simps:
2.110 -"sum_rel P Q (Inl x) (Inl x') \<longleftrightarrow> P x x'"
2.111 -"sum_rel P Q (Inr y) (Inr y') \<longleftrightarrow> Q y y'"
2.112 -"sum_rel P Q (Inl x) (Inr y') \<longleftrightarrow> False"
2.113 -"sum_rel P Q (Inr y) (Inl x') \<longleftrightarrow> False"
2.114 -unfolding sum_rel_def by simp+
2.115 -
2.116 -lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
2.117 -by blast
2.118 -
2.119 -lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
2.120 - unfolding o_def fun_eq_iff by auto
2.121 -
2.122 -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"
2.123 - unfolding o_def fun_eq_iff by auto
2.124 -
2.125 -lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
2.126 - unfolding o_def fun_eq_iff by auto
2.127 -
2.128 -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"
2.129 - unfolding o_def fun_eq_iff by auto
2.130 -
2.131 -lemma convol_o: "<f, g> o h = <f o h, g o h>"
2.132 - unfolding convol_def by auto
2.133 -
2.134 -lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>"
2.135 - unfolding convol_def by auto
2.136 -
2.137 -lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
2.138 - unfolding map_pair_o_convol id_o o_id ..
2.139 -
2.140 -lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
2.141 - unfolding o_def by (auto split: sum.splits)
2.142 -
2.143 -lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
2.144 - unfolding o_def by (auto split: sum.splits)
2.145 -
2.146 -lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
2.147 - unfolding sum_case_o_sum_map id_o o_id ..
2.148 -
2.149 -lemma fun_rel_def_butlast:
2.150 - "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
2.151 - unfolding fun_rel_def ..
2.152 -
2.153 -lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
2.154 - by auto
2.155 -
2.156 -lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
2.157 - by auto
2.158 -
2.159 -lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)"
2.160 - unfolding Grp_def id_apply by blast
2.161 -
2.162 -lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv>
2.163 - (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
2.164 - unfolding Grp_def by rule auto
2.165 -
2.166 -lemma if_if_True:
2.167 - "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
2.168 - (if b then x else if b' then x' else f y')"
2.169 - by simp
2.170 -
2.171 -lemma if_if_False:
2.172 - "(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) =
2.173 - (if b then f y else if b' then x' else f y')"
2.174 - by simp
2.175 -
2.176 -ML_file "Tools/bnf_fp_util.ML"
2.177 -ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
2.178 -ML_file "Tools/bnf_fp_def_sugar.ML"
2.179 -ML_file "Tools/bnf_fp_n2m_tactics.ML"
2.180 -ML_file "Tools/bnf_fp_n2m.ML"
2.181 -ML_file "Tools/bnf_fp_n2m_sugar.ML"
2.182 -ML_file "Tools/bnf_fp_rec_sugar_util.ML"
2.183 -ML_file "Tools/bnf_fp_rec_sugar_tactics.ML"
2.184 -ML_file "Tools/bnf_fp_rec_sugar.ML"
2.185 -
2.186 -end
3.1 --- a/src/HOL/BNF/BNF_GFP.thy Fri Aug 30 12:37:03 2013 +0200
3.2 +++ b/src/HOL/BNF/BNF_GFP.thy Fri Aug 30 12:43:39 2013 +0200
3.3 @@ -8,7 +8,7 @@
3.4 header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
3.5
3.6 theory BNF_GFP
3.7 -imports BNF_FP_Basic Equiv_Relations_More "~~/src/HOL/Library/Sublist"
3.8 +imports BNF_FP_Base Equiv_Relations_More "~~/src/HOL/Library/Sublist"
3.9 keywords
3.10 "codatatype" :: thy_decl and
3.11 "primcorec" :: thy_goal and
4.1 --- a/src/HOL/BNF/BNF_LFP.thy Fri Aug 30 12:37:03 2013 +0200
4.2 +++ b/src/HOL/BNF/BNF_LFP.thy Fri Aug 30 12:43:39 2013 +0200
4.3 @@ -10,7 +10,7 @@
4.4 header {* Least Fixed Point Operation on Bounded Natural Functors *}
4.5
4.6 theory BNF_LFP
4.7 -imports BNF_FP_Basic
4.8 +imports BNF_FP_Base
4.9 keywords
4.10 "datatype_new" :: thy_decl and
4.11 "datatype_new_compat" :: thy_decl and