equal
deleted
inserted
replaced
8 *) |
8 *) |
9 |
9 |
10 header {* Shared Fixed Point Operations on Bounded Natural Functors *} |
10 header {* Shared Fixed Point Operations on Bounded Natural Functors *} |
11 |
11 |
12 theory BNF_FP_Base |
12 theory BNF_FP_Base |
13 imports BNF_Comp Ctr_Sugar |
13 imports BNF_Comp |
14 begin |
14 begin |
15 |
15 |
16 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" |
16 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" |
17 by auto |
17 by auto |
18 |
18 |
96 "setl (Inr x) = {}" |
96 "setl (Inr x) = {}" |
97 "setr (Inl x) = {}" |
97 "setr (Inl x) = {}" |
98 "setr (Inr x) = {x}" |
98 "setr (Inr x) = {x}" |
99 unfolding sum_set_defs by simp+ |
99 unfolding sum_set_defs by simp+ |
100 |
100 |
101 lemma prod_rel_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 |
|
104 |
|
105 lemma sum_rel_simps: |
|
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+ |
|
111 |
|
112 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y" |
101 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y" |
113 by blast |
102 by blast |
114 |
103 |
115 lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r" |
104 lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r" |
116 unfolding comp_def fun_eq_iff by auto |
105 unfolding comp_def fun_eq_iff by auto |