theory Extended_Feature_Algebra imports Main begin class semigroup_one = times + fixes one :: 'a ("\<^bold>1") class ordr = fixes less_eq_r :: "'a \ 'a \ bool" and less_r :: "'a \ 'a \ bool" begin notation less_eq_r ("op <=r") and less_eq_r ("(_/ <=r _)" [51, 51] 50) and less_r ("op \<^sub>r") and less_eq_r ("(_/ \\<^sub>r _)" [51, 51] 50) and less_r ("op <\<^sub>r") and less_r ("(_/ <\<^sub>r _)" [51, 51] 50) end class ordl = fixes less_eq_l :: "'a \ 'a \ bool" and less_l :: "'a \ 'a \ bool" begin notation less_eq_l ("op <=l") and less_eq_l ("(_/ <=l _)" [51, 51] 50) and less_l ("op \<^sub>l") and less_eq_l ("(_/ \\<^sub>l _)" [51, 51] 50) and less_l ("op <\<^sub>l") and less_l ("(_/ <\<^sub>l _)" [51, 51] 50) end class plus_ord_rl = plus + ordr + ordl + assumes less_eq_r_def [simp]: "x \\<^sub>r y \ (\z. x + z = y)" and less_r_def [simp]: "x <\<^sub>r y \ x \\<^sub>r y \ \(y \\<^sub>r x)" and less_eq_l_def [simp]: "x \\<^sub>l y \ (\z. z + x = y)" and less_l_def [simp]: "x <\<^sub>l y \ x \\<^sub>l y \ \(y \\<^sub>l x)" class monoid_ord_rl = plus_ord_rl + fixes zero ("\<^bold>0") assumes add_assoc [simp]: "(x + y) + z = x + (y + z)" and add_zero_l [simp]: "\<^bold>0 + x = x" and add_zero_r [simp]: "x + \<^bold>0 = x" (*class dist_idem_monoid = monoid_ord + assumes dist_idem [simp]: "x + y + x = y + x"*) begin (*lemma idem [simp]: "x + x = x" by (metis add_zero_r dist_idem) *) sublocale ord_r: preorder less_eq_r less_r proof fix x y z :: 'a show "x <\<^sub>r y \ x \\<^sub>r y \ \ y \\<^sub>r x" by simp show "x \\<^sub>r x" by(metis add_zero_r less_eq_r_def) show "x \\<^sub>r y \ y \\<^sub>r z \ x \\<^sub>r z" by (metis add_assoc less_eq_r_def) qed (* would be nice to have double-sublocale *) sublocale ord_l: preorder less_eq_l less_l proof fix x y z :: 'a show "x <\<^sub>l y \ x \\<^sub>l y \ \ y \\<^sub>l x" by simp show "x \\<^sub>l x" by(metis add_zero_l less_eq_l_def) show "x \\<^sub>l y \ y \\<^sub>l z \ x \\<^sub>l z" by (metis add_assoc less_eq_l_def) qed lemma zero_least_r: "\<^bold>0 \\<^sub>r x" by(simp) lemma zero_least_l: "\<^bold>0 \\<^sub>l x" by(simp) lemma lm68b: "\\a b. (a+b = \<^bold>0 \ (a=\<^bold>0 \ b=\<^bold>0)) ; \a b. (a + b = a \ b = \<^bold>0) ; x \\<^sub>r y ; y \\<^sub>r x\ \ x = y" by (metis add_assoc less_eq_r_def) lemma lm68b': "\\a b. (a+b = \<^bold>0 \ (a=\<^bold>0 \ b=\<^bold>0)) ; \a b. (b+a = a \ b = \<^bold>0) ; x \\<^sub>l y ; y \\<^sub>l x\ \ x = y" by (metis add_assoc less_eq_l_def) (* Lm 68c *) lemma add_ub1 [simp]: "x \\<^sub>r x + y" by(auto) lemma add_ub2 [simp]: "x \\<^sub>l y + x" by auto lemma lm68d: "x \\<^sub>r y \ z+x \\<^sub>r z+y" by auto lemma lm68d': "x \\<^sub>l y \ x+z \\<^sub>l y+z" by auto lemma lm69c: "\\ a b. a+b = b+a\ \ (x \\<^sub>r y \ x \\<^sub>l y)" by simp definition equiv_r (infix "\\<^sub>r" 50) where "equiv_r x y \ x\\<^sub>ry \ y\\<^sub>rx" definition equiv_l (infix "\\<^sub>l" 50) where "equiv_l x y \ x\\<^sub>ly \ y\\<^sub>lx" lemma zero_strict_r': "x=\<^bold>0 \ x \\<^sub>r \<^bold>0" by simp lemma zero_strict_r'': "\\a b. (a+b = \<^bold>0 \ (a=\<^bold>0 \ b=\<^bold>0)) ; x \\<^sub>r \<^bold>0\ \ x=\<^bold>0" using local.less_eq_r_def by blast lemma zero_strict_r: assumes "\a b. (a+b = \<^bold>0 \ (a=\<^bold>0 \ b=\<^bold>0))" shows "x \\<^sub>r \<^bold>0 \ x = \<^bold>0 " by(smt assms zero_strict_r' zero_strict_r'') lemma zero_strict_l': "x=\<^bold>0 \ x \\<^sub>l \<^bold>0" by simp lemma zero_strict_l'': "\\a b. (a+b = \<^bold>0 \ (a=\<^bold>0 \ b=\<^bold>0)) ; x \\<^sub>l \<^bold>0\ \ x=\<^bold>0" using local.less_eq_l_def by blast lemma zero_strict_l: assumes "\a b. (a+b = \<^bold>0 \ (a=\<^bold>0 \ b=\<^bold>0))" shows "x \\<^sub>l \<^bold>0 \ x = \<^bold>0 " by(smt assms zero_strict_l' zero_strict_l'') lemma lm69a: assumes "\ a b. a+b+a = b+a" shows "(x \\<^sub>r y) = (x+y=y)" by (metis assms local.add_assoc local.less_eq_r_def) lemma lm69b: assumes "\ a b. a+b+a = b+a" shows "x \\<^sub>l y \ x \\<^sub>r y " by (metis add_ub1 assms local.add_assoc local.less_eq_l_def) end locale feature_algebra = M : semigroup_one "op *" "\<^bold>1"+ I: monoid_ord_rl "op \\<^sub>l" "op <\<^sub>l" "op \\<^sub>r" "op <\<^sub>r" "op +" "\<^bold>0" + fixes app (infix "\" 70) assumes distrib_left [simp, intro]: "m \ (i + j) = (m \ i) + (m \ j)" and app_app [simp, intro]: " (m * n) \ i = m \ (n \ i)" and one_app [simp, intro]: "\<^bold>1 \ i = i" and anni_right [simp, intro]: "m \ \<^bold>0 = \<^bold>0" begin definition app_equiv (infix "\" 50) where "app_equiv m n \ (\i. m \ i = n \ i)" lemma mi_neutral_right: "m \ i = m \ i + m \ \<^bold>0" by(simp) lemma mi_neutral_left: "m \ i = m \ \<^bold>0 + m \ i" by(simp) lemma mul_assoc: "((m * n) * p) \ i = (m * (n * p)) \ i" by(simp) lemma mul_quasi_assoc:"(m * n) * p \ m * (n * p)" by(simp add: app_equiv_def mul_assoc) lemma mul_one_right: "(m * \<^bold>1) \ i = m \ i" by(simp) lemma mul_one_left: "(\<^bold>1 * m) \ i = m \ i" by(simp) lemma mul_quasi_one_right: "m * \<^bold>1 \ m" by(simp add: app_equiv_def mul_one_right) lemma mul_quasi_one_left: "\<^bold>1 * m \ m" by(simp add: app_equiv_def mul_one_left) end end