1.1 --- a/src/HOL/Codatatype/BNF_FP.thy Fri Sep 21 16:34:40 2012 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,113 +0,0 @@
1.4 -(* Title: HOL/BNF/BNF_FP.thy
1.5 - Author: Dmitriy Traytel, TU Muenchen
1.6 - Author: Jasmin Blanchette, TU Muenchen
1.7 - Copyright 2012
1.8 -
1.9 -Composition of bounded natural functors.
1.10 -*)
1.11 -
1.12 -header {* Composition of Bounded Natural Functors *}
1.13 -
1.14 -theory BNF_FP
1.15 -imports BNF_Comp BNF_Wrap
1.16 -keywords
1.17 - "defaults"
1.18 -begin
1.19 -
1.20 -lemma case_unit: "(case u of () => f) = f"
1.21 -by (cases u) (hypsubst, rule unit.cases)
1.22 -
1.23 -lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
1.24 -by simp
1.25 -
1.26 -lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
1.27 -by clarify
1.28 -
1.29 -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.30 -by auto
1.31 -
1.32 -lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()"
1.33 -by simp
1.34 -
1.35 -lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))"
1.36 -by clarsimp
1.37 -
1.38 -lemma rev_bspec: "a \<in> A \<Longrightarrow> \<forall>z \<in> A. P z \<Longrightarrow> P a"
1.39 -by simp
1.40 -
1.41 -lemma Un_cong: "\<lbrakk>A = B; C = D\<rbrakk> \<Longrightarrow> A \<union> C = B \<union> D"
1.42 -by simp
1.43 -
1.44 -lemma pointfree_idE: "f o g = id \<Longrightarrow> f (g x) = x"
1.45 -unfolding o_def fun_eq_iff by simp
1.46 -
1.47 -lemma o_bij:
1.48 - assumes gf: "g o f = id" and fg: "f o g = id"
1.49 - shows "bij f"
1.50 -unfolding bij_def inj_on_def surj_def proof safe
1.51 - fix a1 a2 assume "f a1 = f a2"
1.52 - hence "g ( f a1) = g (f a2)" by simp
1.53 - thus "a1 = a2" using gf unfolding fun_eq_iff by simp
1.54 -next
1.55 - fix b
1.56 - have "b = f (g b)"
1.57 - using fg unfolding fun_eq_iff by simp
1.58 - thus "EX a. b = f a" by blast
1.59 -qed
1.60 -
1.61 -lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
1.62 -
1.63 -lemma sum_case_step:
1.64 - "sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
1.65 - "sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
1.66 -by auto
1.67 -
1.68 -lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
1.69 -by simp
1.70 -
1.71 -lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
1.72 -by blast
1.73 -
1.74 -lemma obj_sumE_f':
1.75 -"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> s = f x \<longrightarrow> P"
1.76 -by (cases x) blast+
1.77 -
1.78 -lemma obj_sumE_f:
1.79 -"\<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.80 -by (rule allI) (rule obj_sumE_f')
1.81 -
1.82 -lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
1.83 -by (cases s) auto
1.84 -
1.85 -lemma obj_sum_step':
1.86 -"\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> s = f (Inr x) \<longrightarrow> P"
1.87 -by (cases x) blast+
1.88 -
1.89 -lemma obj_sum_step:
1.90 -"\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f (Inr x) \<longrightarrow> P"
1.91 -by (rule allI) (rule obj_sum_step')
1.92 -
1.93 -lemma sum_case_if:
1.94 -"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
1.95 -by simp
1.96 -
1.97 -lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
1.98 -by blast
1.99 -
1.100 -lemma prod_set_simps:
1.101 -"fsts (x, y) = {x}"
1.102 -"snds (x, y) = {y}"
1.103 -unfolding fsts_def snds_def by simp+
1.104 -
1.105 -lemma sum_set_simps:
1.106 -"setl (Inl x) = {x}"
1.107 -"setl (Inr x) = {}"
1.108 -"setr (Inl x) = {}"
1.109 -"setr (Inr x) = {x}"
1.110 -unfolding sum_set_defs by simp+
1.111 -
1.112 -ML_file "Tools/bnf_fp.ML"
1.113 -ML_file "Tools/bnf_fp_sugar_tactics.ML"
1.114 -ML_file "Tools/bnf_fp_sugar.ML"
1.115 -
1.116 -end