--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/BNF_FP_Base.thy Fri Aug 30 12:43:39 2013 +0200
@@ -0,0 +1,184 @@
+(* Title: HOL/BNF/BNF_FP_Base.thy
+ Author: Lorenz Panny, TU Muenchen
+ Author: Dmitriy Traytel, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2012, 2013
+
+Shared fixed point operations on bounded natural functors, including
+*)
+
+header {* Shared Fixed Point Operations on Bounded Natural Functors *}
+
+theory BNF_FP_Base
+imports BNF_Comp BNF_Ctr_Sugar
+keywords
+ "defaults"
+begin
+
+lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
+by auto
+
+lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
+by blast
+
+lemma unit_case_Unity: "(case u of () => f) = f"
+by (cases u) (hypsubst, rule unit.cases)
+
+lemma prod_case_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
+by simp
+
+lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
+by simp
+
+lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
+by clarify
+
+lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
+by auto
+
+lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
+unfolding o_def fun_eq_iff by simp
+
+lemma o_bij:
+ assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id"
+ shows "bij f"
+unfolding bij_def inj_on_def surj_def proof safe
+ fix a1 a2 assume "f a1 = f a2"
+ hence "g ( f a1) = g (f a2)" by simp
+ thus "a1 = a2" using gf unfolding fun_eq_iff by simp
+next
+ fix b
+ have "b = f (g b)"
+ using fg unfolding fun_eq_iff by simp
+ thus "EX a. b = f a" by blast
+qed
+
+lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
+
+lemma sum_case_step:
+"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
+"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
+by auto
+
+lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+by simp
+
+lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
+by blast
+
+lemma obj_sumE_f:
+"\<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"
+by (rule allI) (metis sumE)
+
+lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+by (cases s) auto
+
+lemma sum_case_if:
+"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
+by simp
+
+lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
+by blast
+
+lemma UN_compreh_eq_eq:
+"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
+"\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
+by blast+
+
+lemma Inl_Inr_False: "(Inl x = Inr y) = False"
+by simp
+
+lemma prod_set_simps:
+"fsts (x, y) = {x}"
+"snds (x, y) = {y}"
+unfolding fsts_def snds_def by simp+
+
+lemma sum_set_simps:
+"setl (Inl x) = {x}"
+"setl (Inr x) = {}"
+"setr (Inl x) = {}"
+"setr (Inr x) = {x}"
+unfolding sum_set_defs by simp+
+
+lemma prod_rel_simp:
+"prod_rel P Q (x, y) (x', y') \<longleftrightarrow> P x x' \<and> Q y y'"
+unfolding prod_rel_def by simp
+
+lemma sum_rel_simps:
+"sum_rel P Q (Inl x) (Inl x') \<longleftrightarrow> P x x'"
+"sum_rel P Q (Inr y) (Inr y') \<longleftrightarrow> Q y y'"
+"sum_rel P Q (Inl x) (Inr y') \<longleftrightarrow> False"
+"sum_rel P Q (Inr y) (Inl x') \<longleftrightarrow> False"
+unfolding sum_rel_def by simp+
+
+lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
+by blast
+
+lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
+ unfolding o_def fun_eq_iff by auto
+
+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"
+ unfolding o_def fun_eq_iff by auto
+
+lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
+ unfolding o_def fun_eq_iff by auto
+
+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"
+ unfolding o_def fun_eq_iff by auto
+
+lemma convol_o: "<f, g> o h = <f o h, g o h>"
+ unfolding convol_def by auto
+
+lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>"
+ unfolding convol_def by auto
+
+lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
+ unfolding map_pair_o_convol id_o o_id ..
+
+lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
+ unfolding o_def by (auto split: sum.splits)
+
+lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
+ unfolding o_def by (auto split: sum.splits)
+
+lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
+ unfolding sum_case_o_sum_map id_o o_id ..
+
+lemma fun_rel_def_butlast:
+ "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
+ unfolding fun_rel_def ..
+
+lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
+ by auto
+
+lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
+ by auto
+
+lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)"
+ unfolding Grp_def id_apply by blast
+
+lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv>
+ (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
+ unfolding Grp_def by rule auto
+
+lemma if_if_True:
+ "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
+ (if b then x else if b' then x' else f y')"
+ by simp
+
+lemma if_if_False:
+ "(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) =
+ (if b then f y else if b' then x' else f y')"
+ by simp
+
+ML_file "Tools/bnf_fp_util.ML"
+ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
+ML_file "Tools/bnf_fp_def_sugar.ML"
+ML_file "Tools/bnf_fp_n2m_tactics.ML"
+ML_file "Tools/bnf_fp_n2m.ML"
+ML_file "Tools/bnf_fp_n2m_sugar.ML"
+ML_file "Tools/bnf_fp_rec_sugar_util.ML"
+ML_file "Tools/bnf_fp_rec_sugar_tactics.ML"
+ML_file "Tools/bnf_fp_rec_sugar.ML"
+
+end
--- a/src/HOL/BNF/BNF_FP_Basic.thy Fri Aug 30 12:37:03 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,183 +0,0 @@
-(* Title: HOL/BNF/BNF_FP_Basic.thy
- Author: Dmitriy Traytel, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
- Copyright 2012
-
-Basic fixed point operations on bounded natural functors.
-*)
-
-header {* Basic Fixed Point Operations on Bounded Natural Functors *}
-
-theory BNF_FP_Basic
-imports BNF_Comp BNF_Ctr_Sugar
-keywords
- "defaults"
-begin
-
-lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
-by auto
-
-lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
-by blast
-
-lemma unit_case_Unity: "(case u of () => f) = f"
-by (cases u) (hypsubst, rule unit.cases)
-
-lemma prod_case_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
-by simp
-
-lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
-by simp
-
-lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
-by clarify
-
-lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
-by auto
-
-lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
-unfolding o_def fun_eq_iff by simp
-
-lemma o_bij:
- assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id"
- shows "bij f"
-unfolding bij_def inj_on_def surj_def proof safe
- fix a1 a2 assume "f a1 = f a2"
- hence "g ( f a1) = g (f a2)" by simp
- thus "a1 = a2" using gf unfolding fun_eq_iff by simp
-next
- fix b
- have "b = f (g b)"
- using fg unfolding fun_eq_iff by simp
- thus "EX a. b = f a" by blast
-qed
-
-lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
-
-lemma sum_case_step:
-"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
-"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
-by auto
-
-lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by simp
-
-lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
-by blast
-
-lemma obj_sumE_f:
-"\<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"
-by (rule allI) (metis sumE)
-
-lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by (cases s) auto
-
-lemma sum_case_if:
-"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
-by simp
-
-lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
-by blast
-
-lemma UN_compreh_eq_eq:
-"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
-"\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
-by blast+
-
-lemma Inl_Inr_False: "(Inl x = Inr y) = False"
-by simp
-
-lemma prod_set_simps:
-"fsts (x, y) = {x}"
-"snds (x, y) = {y}"
-unfolding fsts_def snds_def by simp+
-
-lemma sum_set_simps:
-"setl (Inl x) = {x}"
-"setl (Inr x) = {}"
-"setr (Inl x) = {}"
-"setr (Inr x) = {x}"
-unfolding sum_set_defs by simp+
-
-lemma prod_rel_simp:
-"prod_rel P Q (x, y) (x', y') \<longleftrightarrow> P x x' \<and> Q y y'"
-unfolding prod_rel_def by simp
-
-lemma sum_rel_simps:
-"sum_rel P Q (Inl x) (Inl x') \<longleftrightarrow> P x x'"
-"sum_rel P Q (Inr y) (Inr y') \<longleftrightarrow> Q y y'"
-"sum_rel P Q (Inl x) (Inr y') \<longleftrightarrow> False"
-"sum_rel P Q (Inr y) (Inl x') \<longleftrightarrow> False"
-unfolding sum_rel_def by simp+
-
-lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
-by blast
-
-lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
- unfolding o_def fun_eq_iff by auto
-
-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"
- unfolding o_def fun_eq_iff by auto
-
-lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
- unfolding o_def fun_eq_iff by auto
-
-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"
- unfolding o_def fun_eq_iff by auto
-
-lemma convol_o: "<f, g> o h = <f o h, g o h>"
- unfolding convol_def by auto
-
-lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>"
- unfolding convol_def by auto
-
-lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
- unfolding map_pair_o_convol id_o o_id ..
-
-lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
- unfolding o_def by (auto split: sum.splits)
-
-lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
- unfolding o_def by (auto split: sum.splits)
-
-lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
- unfolding sum_case_o_sum_map id_o o_id ..
-
-lemma fun_rel_def_butlast:
- "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
- unfolding fun_rel_def ..
-
-lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
- by auto
-
-lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
- by auto
-
-lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)"
- unfolding Grp_def id_apply by blast
-
-lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv>
- (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
- unfolding Grp_def by rule auto
-
-lemma if_if_True:
- "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
- (if b then x else if b' then x' else f y')"
- by simp
-
-lemma if_if_False:
- "(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) =
- (if b then f y else if b' then x' else f y')"
- by simp
-
-ML_file "Tools/bnf_fp_util.ML"
-ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
-ML_file "Tools/bnf_fp_def_sugar.ML"
-ML_file "Tools/bnf_fp_n2m_tactics.ML"
-ML_file "Tools/bnf_fp_n2m.ML"
-ML_file "Tools/bnf_fp_n2m_sugar.ML"
-ML_file "Tools/bnf_fp_rec_sugar_util.ML"
-ML_file "Tools/bnf_fp_rec_sugar_tactics.ML"
-ML_file "Tools/bnf_fp_rec_sugar.ML"
-
-end
--- a/src/HOL/BNF/BNF_GFP.thy Fri Aug 30 12:37:03 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy Fri Aug 30 12:43:39 2013 +0200
@@ -8,7 +8,7 @@
header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
theory BNF_GFP
-imports BNF_FP_Basic Equiv_Relations_More "~~/src/HOL/Library/Sublist"
+imports BNF_FP_Base Equiv_Relations_More "~~/src/HOL/Library/Sublist"
keywords
"codatatype" :: thy_decl and
"primcorec" :: thy_goal and
--- a/src/HOL/BNF/BNF_LFP.thy Fri Aug 30 12:37:03 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy Fri Aug 30 12:43:39 2013 +0200
@@ -10,7 +10,7 @@
header {* Least Fixed Point Operation on Bounded Natural Functors *}
theory BNF_LFP
-imports BNF_FP_Basic
+imports BNF_FP_Base
keywords
"datatype_new" :: thy_decl and
"datatype_new_compat" :: thy_decl and