(* Walter Guttmann, 2011.03.23, extended 2011.05.20, extended 2011.10.28 *) (* use with Isabelle2011 *) theory AFI imports Main begin (* theory Notation imports Main begin *) class mult = times begin notation times (infixl "\" 70) and times (infixl ";" 70) end class neg = uminus begin no_notation uminus ("- _" [81] 80) notation uminus ("- _" [80] 80) end (* end theory Fixpoint imports Main begin *) context order begin definition isotone :: "('a \ 'a) \ bool" where "isotone f \ (\x y . x \ y \ f(x) \ f(y))" definition is_fixpoint :: "('a \ 'a) \ 'a \ bool" where "is_fixpoint f x \ f(x) = x" definition is_prefixpoint :: "('a \ 'a) \ 'a \ bool" where "is_prefixpoint f x \ f(x) \ x" definition is_postfixpoint :: "('a \ 'a) \ 'a \ bool" where "is_postfixpoint f x \ f(x) \ x" definition is_least_fixpoint :: "('a \ 'a) \ 'a \ bool" where "is_least_fixpoint f x \ f(x) = x \ (\y . f(y) = y \ x \ y)" definition is_greatest_fixpoint :: "('a \ 'a) \ 'a \ bool" where "is_greatest_fixpoint f x \ f(x) = x \ (\y . f(y) = y \ x \ y)" definition is_least_prefixpoint :: "('a \ 'a) \ 'a \ bool" where "is_least_prefixpoint f x \ f(x) \ x \ (\y . f(y) \ y \ x \ y)" definition is_greatest_postfixpoint :: "('a \ 'a) \ 'a \ bool" where "is_greatest_postfixpoint f x \ f(x) \ x \ (\y . f(y) \ y \ x \ y)" definition has_fixpoint :: "('a \ 'a) \ bool" where "has_fixpoint f \ (\x . is_fixpoint f x)" definition has_prefixpoint :: "('a \ 'a) \ bool" where "has_prefixpoint f \ (\x . is_prefixpoint f x)" definition has_postfixpoint :: "('a \ 'a) \ bool" where "has_postfixpoint f \ (\x . is_postfixpoint f x)" definition has_least_fixpoint :: "('a \ 'a) \ bool" where "has_least_fixpoint f \ (\x . is_least_fixpoint f x)" definition has_greatest_fixpoint :: "('a \ 'a) \ bool" where "has_greatest_fixpoint f \ (\x . is_greatest_fixpoint f x)" definition has_least_prefixpoint :: "('a \ 'a) \ bool" where "has_least_prefixpoint f \ (\x . is_least_prefixpoint f x)" definition has_greatest_postfixpoint :: "('a \ 'a) \ bool" where "has_greatest_postfixpoint f \ (\x . is_greatest_postfixpoint f x)" definition the_least_fixpoint :: "('a \ 'a) \ 'a" ("\ _" [201] 200) where "\ f = (THE x . is_least_fixpoint f x)" definition the_greatest_fixpoint :: "('a \ 'a) \ 'a" ("\ _" [201] 200) where "\ f = (THE x . is_greatest_fixpoint f x)" definition the_least_prefixpoint :: "('a \ 'a) \ 'a" ("p\ _" [201] 200) where "p\ f = (THE x . is_least_prefixpoint f x)" definition the_greatest_postfixpoint :: "('a \ 'a) \ 'a" ("p\ _" [201] 200) where "p\ f = (THE x . is_greatest_postfixpoint f x)" lemma least_fixpoint_unique: "has_least_fixpoint f \ (\!x . is_least_fixpoint f x)" by (smt antisym has_least_fixpoint_def is_least_fixpoint_def) lemma greatest_fixpoint_unique: "has_greatest_fixpoint f \ (\!x . is_greatest_fixpoint f x)" by (smt antisym has_greatest_fixpoint_def is_greatest_fixpoint_def) lemma least_prefixpoint_unique: "has_least_prefixpoint f \ (\!x . is_least_prefixpoint f x)" by (smt antisym has_least_prefixpoint_def is_least_prefixpoint_def) lemma greatest_postfixpoint_unique: "has_greatest_postfixpoint f \ (\!x . is_greatest_postfixpoint f x)" by (smt antisym has_greatest_postfixpoint_def is_greatest_postfixpoint_def) lemma least_fixpoint: "has_least_fixpoint f \ is_least_fixpoint f (\ f)" proof assume "has_least_fixpoint f" hence "is_least_fixpoint f (THE x . is_least_fixpoint f x)" by (smt least_fixpoint_unique theI') thus "is_least_fixpoint f (\ f)" by (simp add: is_least_fixpoint_def the_least_fixpoint_def) qed lemma greatest_fixpoint: "has_greatest_fixpoint f \ is_greatest_fixpoint f (\ f)" proof assume "has_greatest_fixpoint f" hence "is_greatest_fixpoint f (THE x . is_greatest_fixpoint f x)" by (smt greatest_fixpoint_unique theI') thus "is_greatest_fixpoint f (\ f)" by (simp add: is_greatest_fixpoint_def the_greatest_fixpoint_def) qed lemma least_prefixpoint: "has_least_prefixpoint f \ is_least_prefixpoint f (p\ f)" proof assume "has_least_prefixpoint f" hence "is_least_prefixpoint f (THE x . is_least_prefixpoint f x)" by (smt least_prefixpoint_unique theI') thus "is_least_prefixpoint f (p\ f)" by (simp add: is_least_prefixpoint_def the_least_prefixpoint_def) qed lemma greatest_postfixpoint: "has_greatest_postfixpoint f \ is_greatest_postfixpoint f (p\ f)" proof assume "has_greatest_postfixpoint f" hence "is_greatest_postfixpoint f (THE x . is_greatest_postfixpoint f x)" by (smt greatest_postfixpoint_unique theI') thus "is_greatest_postfixpoint f (p\ f)" by (simp add: is_greatest_postfixpoint_def the_greatest_postfixpoint_def) qed lemma least_fixpoint_same: "is_least_fixpoint f x \ x = \ f" by (metis least_fixpoint least_fixpoint_unique has_least_fixpoint_def) lemma greatest_fixpoint_same: "is_greatest_fixpoint f x \ x = \ f" by (metis greatest_fixpoint greatest_fixpoint_unique has_greatest_fixpoint_def) lemma least_prefixpoint_same: "is_least_prefixpoint f x \ x = p\ f" by (metis least_prefixpoint least_prefixpoint_unique has_least_prefixpoint_def) lemma greatest_postfixpoint_same: "is_greatest_postfixpoint f x \ x = p\ f" by (metis greatest_postfixpoint greatest_postfixpoint_unique has_greatest_postfixpoint_def) lemma least_fixpoint_char: "is_least_fixpoint f x \ has_least_fixpoint f \ x = \ f" by (metis least_fixpoint_same has_least_fixpoint_def) lemma least_prefixpoint_char: "is_least_prefixpoint f x \ has_least_prefixpoint f \ x = p\ f" by (metis least_prefixpoint_same has_least_prefixpoint_def) lemma greatest_fixpoint_char: "is_greatest_fixpoint f x \ has_greatest_fixpoint f \ x = \ f" by (metis greatest_fixpoint_same has_greatest_fixpoint_def) lemma greatest_postfixpoint_char: "is_greatest_postfixpoint f x \ has_greatest_postfixpoint f \ x = p\ f" by (metis greatest_postfixpoint_same has_greatest_postfixpoint_def) lemma least_prefixpoint_fixpoint: "has_least_prefixpoint f \ isotone f \ is_least_fixpoint f (p\ f)" by (smt eq_iff is_least_fixpoint_def is_least_prefixpoint_def isotone_def least_prefixpoint) lemma pmu_mu: "has_least_prefixpoint f \ isotone f \ p\ f = \ f" by (smt has_least_fixpoint_def is_least_fixpoint_def least_fixpoint_unique least_prefixpoint_fixpoint least_fixpoint) definition lifted_less_eq :: "('a \ 'a) \ ('a \ 'a) \ bool" ("(_ \\ _)" [51, 51] 50) where "f \\ g \ (\x . f(x) \ g(x))" lemma lifted_reflexive: "f = g \ f \\ g" by (metis lifted_less_eq_def order_refl) lemma lifted_transitive: "f \\ g \ g \\ h \ f \\ h" by (smt lifted_less_eq_def order_trans) lemma lifted_antisymmetric: "f \\ g \ g \\ f \ f = g" by (metis antisym ext lifted_less_eq_def) lemma pmu_isotone: "has_least_prefixpoint f \ has_least_prefixpoint g \ f \\ g \ p\ f \ p\ g" by (smt is_least_prefixpoint_def least_prefixpoint lifted_less_eq_def order_trans) lemma mu_isotone: "has_least_prefixpoint f \ has_least_prefixpoint g \ isotone f \ isotone g \ f \\ g \ \ f \ \ g" by (metis pmu_isotone pmu_mu) lemma greatest_postfixpoint_fixpoint: "has_greatest_postfixpoint f \ isotone f \ is_greatest_fixpoint f (p\ f)" by (smt eq_iff is_greatest_fixpoint_def is_greatest_postfixpoint_def isotone_def greatest_postfixpoint) lemma pnu_nu: "has_greatest_postfixpoint f \ isotone f \ p\ f = \ f" by (smt has_greatest_fixpoint_def is_greatest_fixpoint_def greatest_fixpoint_unique greatest_postfixpoint_fixpoint greatest_fixpoint) lemma pnu_isotone: "has_greatest_postfixpoint f \ has_greatest_postfixpoint g \ f \\ g \ p\ f \ p\ g" by (smt is_greatest_postfixpoint_def lifted_less_eq_def order_trans greatest_postfixpoint) lemma nu_isotone: "has_greatest_postfixpoint f \ has_greatest_postfixpoint g \ isotone f \ isotone g \ f \\ g \ \ f \ \ g" by (metis pnu_isotone pnu_nu) lemma mu_square: "isotone f \ has_least_fixpoint f \ has_least_fixpoint (f \ f) \ \ f = \ (f \ f)" by (metis antisym is_least_fixpoint_def isotone_def least_fixpoint_char least_fixpoint_unique o_apply) lemma nu_square: "isotone f \ has_greatest_fixpoint f \ has_greatest_fixpoint (f \ f) \ \ f = \ (f \ f)" by (metis antisym is_greatest_fixpoint_def isotone_def greatest_fixpoint_char greatest_fixpoint_unique o_apply) lemma mu_roll: "isotone g \ has_least_fixpoint (f \ g) \ has_least_fixpoint (g \ f) \ \ (g \ f) = g(\ (f \ g))" apply (rule impI, rule antisym) apply (smt is_least_fixpoint_def least_fixpoint o_apply) by (smt is_least_fixpoint_def isotone_def least_fixpoint o_apply) lemma nu_roll: "isotone g \ has_greatest_fixpoint (f \ g) \ has_greatest_fixpoint (g \ f) \ \ (g \ f) = g(\ (f \ g))" apply (rule impI, rule antisym) apply (smt is_greatest_fixpoint_def greatest_fixpoint isotone_def o_apply) by (smt is_greatest_fixpoint_def greatest_fixpoint o_apply) lemma mu_below_nu: "has_least_fixpoint f \ has_greatest_fixpoint f \ \ f \ \ f" by (metis is_greatest_fixpoint_def is_least_fixpoint_def least_fixpoint greatest_fixpoint) lemma pmu_below_pnu_fix: "has_fixpoint f \ has_least_prefixpoint f \ has_greatest_postfixpoint f \ p\ f \ p\ f" by (smt has_fixpoint_def is_fixpoint_def is_greatest_postfixpoint_def is_least_prefixpoint_def le_less order_trans least_prefixpoint greatest_postfixpoint) lemma pmu_below_pnu_iso: "isotone f \ has_least_prefixpoint f \ has_greatest_postfixpoint f \ p\ f \ p\ f" by (metis has_fixpoint_def is_fixpoint_def is_least_fixpoint_def least_prefixpoint_fixpoint pmu_below_pnu_fix) definition galois :: "('a \ 'a) \ ('a \ 'a) \ bool" where "galois l u \ (\x y . l(x) \ y \ x \ u(y))" lemma galois_char: "galois l u \ (\x . x \ u(l(x))) \ (\x . l(u(x)) \ x) \ isotone l \ isotone u" apply (rule iffI) apply (smt galois_def isotone_def order_refl order_trans) by (metis galois_def isotone_def order_trans) lemma galois_closure: "galois l u \ l(x) = l(u(l(x))) \ u(x) = u(l(u(x)))" by (smt antisym galois_char isotone_def) lemma mu_fusion_1: "galois l u \ isotone h \ has_least_prefixpoint g \ has_least_fixpoint h \ l(g(u(\ h))) \ h(l(u(\ h))) \ l(p\ g) \ \ h" proof assume 1: "galois l u \ isotone h \ has_least_prefixpoint g \ has_least_fixpoint h \ l(g(u(\ h))) \ h(l(u(\ h)))" hence "l(u(\ h)) \ \ h" by (metis galois_char) hence "g(u(\ h)) \ u(\ h)" using 1 by (smt galois_def least_fixpoint_same least_fixpoint_unique is_least_fixpoint_def isotone_def order_trans) thus "l(p\ g) \ \ h" using 1 by (metis galois_def least_prefixpoint is_least_prefixpoint_def) qed lemma mu_fusion_2: "galois l u \ isotone h \ has_least_prefixpoint g \ has_least_fixpoint h \ l \ g \\ h \ l \ l(p\ g) \ \ h" by (metis lifted_less_eq_def mu_fusion_1 o_apply) lemma mu_fusion_equal_1: "galois l u \ isotone g \ isotone h \ has_least_prefixpoint g \ has_least_fixpoint h \ l(g(u(\ h))) \ h(l(u(\ h))) \ l(g(p\ g)) = h(l(p\ g)) \ \ h = l(p\ g) \ \ h = l(\ g)" by (metis antisym least_fixpoint least_prefixpoint_fixpoint is_least_fixpoint_def mu_fusion_1 pmu_mu) lemma mu_fusion_equal_2: "galois l u \ isotone h \ has_least_prefixpoint g \ has_least_prefixpoint h \ l(g(u(\ h))) \ h(l(u(\ h))) \ l(g(p\ g)) = h(l(p\ g)) \ p\ h = l(p\ g) \ \ h = l(p\ g)" by (smt antisym galois_char least_fixpoint_char least_prefixpoint least_prefixpoint_fixpoint is_least_prefixpoint_def isotone_def mu_fusion_1) lemma mu_fusion_equal_3: "galois l u \ isotone g \ isotone h \ has_least_prefixpoint g \ has_least_fixpoint h \ l \ g = h \ l \ \ h = l(p\ g) \ \ h = l(\ g)" by (smt mu_fusion_equal_1 o_apply order_refl) lemma mu_fusion_equal_4: "galois l u \ isotone h \ has_least_prefixpoint g \ has_least_prefixpoint h \ l \ g = h \ l \ p\ h = l(p\ g) \ \ h = l(p\ g)" by (smt mu_fusion_equal_2 o_apply order_refl) lemma nu_fusion_1: "galois l u \ isotone h \ has_greatest_postfixpoint g \ has_greatest_fixpoint h \ h(u(l(\ h))) \ u(g(l(\ h))) \ \ h \ u(p\ g)" proof assume 1: "galois l u \ isotone h \ has_greatest_postfixpoint g \ has_greatest_fixpoint h \ h(u(l(\ h))) \ u(g(l(\ h)))" hence "\ h \ u(l(\ h))" by (metis galois_char) hence "l(\ h) \ g(l(\ h))" using 1 by (smt galois_def greatest_fixpoint_same greatest_fixpoint_unique is_greatest_fixpoint_def isotone_def order_trans) thus "\ h \ u(p\ g)" using 1 by (metis galois_def greatest_postfixpoint is_greatest_postfixpoint_def) qed lemma nu_fusion_2: "galois l u \ isotone h \ has_greatest_postfixpoint g \ has_greatest_fixpoint h \ h \ u \\ u \ g \ \ h \ u(p\ g)" by (metis lifted_less_eq_def nu_fusion_1 o_apply) lemma nu_fusion_equal_1: "galois l u \ isotone g \ isotone h \ has_greatest_postfixpoint g \ has_greatest_fixpoint h \ h(u(l(\ h))) \ u(g(l(\ h))) \ h(u(p\ g)) = u(g(p\ g)) \ \ h = u(p\ g) \ \ h = u(\ g)" by (metis antisym greatest_fixpoint greatest_postfixpoint_fixpoint is_greatest_fixpoint_def nu_fusion_1 pnu_nu) lemma nu_fusion_equal_2: "galois l u \ isotone h \ has_greatest_postfixpoint g \ has_greatest_postfixpoint h \ h(u(l(\ h))) \ u(g(l(\ h))) \ h(u(p\ g)) = u(g(p\ g)) \ p\ h = u(p\ g) \ \ h = u(p\ g)" by (smt antisym galois_char greatest_fixpoint_char greatest_postfixpoint greatest_postfixpoint_fixpoint is_greatest_postfixpoint_def isotone_def nu_fusion_1) lemma nu_fusion_equal_3: "galois l u \ isotone g \ isotone h \ has_greatest_postfixpoint g \ has_greatest_fixpoint h \ h \ u = u \ g \ \ h = u(p\ g) \ \ h = u(\ g)" by (metis nu_fusion_equal_1 o_apply order_refl) lemma nu_fusion_equal_4: "galois l u \ isotone h \ has_greatest_postfixpoint g \ has_greatest_postfixpoint h \ h \ u = u \ g \ p\ h = u(p\ g) \ \ h = u(p\ g)" by (smt nu_fusion_equal_2 o_apply order_refl) lemma mu_exchange_1: "galois l u \ isotone g \ isotone h \ has_least_prefixpoint (l \ h) \ has_least_prefixpoint (h \ g) \ has_least_fixpoint (g \ h) \ l \ h \ g \\ g \ h \ l \ \(l \ h) \ \(g \ h)" by (smt galois_char is_least_prefixpoint_def isotone_def least_fixpoint_char least_prefixpoint least_prefixpoint_fixpoint mu_fusion_2 mu_roll o_apply o_assoc) lemma mu_exchange_2: "galois l u \ isotone g \ isotone h \ has_least_prefixpoint (l \ h) \ has_least_prefixpoint (h \ l) \ has_least_prefixpoint (h \ g) \ has_least_fixpoint (g \ h) \ has_least_fixpoint (h \ g) \ l \ h \ g \\ g \ h \ l \ \(h \ l) \ \(h \ g)" by (smt galois_char isotone_def least_fixpoint_char least_prefixpoint_fixpoint mu_exchange_1 mu_roll o_apply) lemma mu_exchange_equal: "galois l u \ galois k t \ isotone h \ has_least_prefixpoint (l \ h) \ has_least_prefixpoint (h \ l) \ has_least_prefixpoint (k \ h) \ has_least_prefixpoint (h \ k) \ l \ h \ k = k \ h \ l \ \(l \ h) = \(k \ h) \ \(h \ l) = \(h \ k)" by (smt antisym galois_char isotone_def least_fixpoint_char least_prefixpoint_fixpoint lifted_reflexive mu_exchange_1 mu_exchange_2 o_apply) lemma nu_exchange_1: "galois l u \ isotone g \ isotone h \ has_greatest_postfixpoint (u \ h) \ has_greatest_postfixpoint (h \ g) \ has_greatest_fixpoint (g \ h) \ g \ h \ u \\ u \ h \ g \ \(g \ h) \ \(u \ h)" by (smt galois_char is_greatest_postfixpoint_def isotone_def greatest_fixpoint_char greatest_postfixpoint greatest_postfixpoint_fixpoint nu_fusion_2 nu_roll o_apply o_assoc) lemma nu_exchange_2: "galois l u \ isotone g \ isotone h \ has_greatest_postfixpoint (u \ h) \ has_greatest_postfixpoint (h \ u) \ has_greatest_postfixpoint (h \ g) \ has_greatest_fixpoint (g \ h) \ has_greatest_fixpoint (h \ g) \ g \ h \ u \\ u \ h \ g \ \(h \ g) \ \(h \ u)" by (smt galois_char isotone_def greatest_fixpoint_char greatest_postfixpoint_fixpoint nu_exchange_1 nu_roll o_apply) lemma nu_exchange_equal: "galois l u \ galois k t \ isotone h \ has_greatest_postfixpoint (u \ h) \ has_greatest_postfixpoint (h \ u) \ has_greatest_postfixpoint (t \ h) \ has_greatest_postfixpoint (h \ t) \ u \ h \ t = t \ h \ u \ \(u \ h) = \(t \ h) \ \(h \ u) = \(h \ t)" by (smt antisym galois_char isotone_def greatest_fixpoint_char greatest_postfixpoint_fixpoint lifted_reflexive nu_exchange_1 nu_exchange_2 o_apply) lemma mu_commute_fixpoint_1: "isotone f \ has_least_fixpoint (f \ g) \ f \ g = g \ f \ is_fixpoint f (\(f \ g))" by (metis is_fixpoint_def mu_roll) lemma mu_commute_fixpoint_2: "isotone g \ has_least_fixpoint (f \ g) \ f \ g = g \ f \ is_fixpoint g (\(f \ g))" by (metis is_fixpoint_def mu_roll) lemma mu_commute_least_fixpoint: "isotone f \ isotone g \ has_least_fixpoint f \ has_least_fixpoint g \ has_least_fixpoint (f \ g) \ f \ g = g \ f \ (\(f \ g) = \ f \ \ g \ \ f)" by (metis is_least_fixpoint_def least_fixpoint_same least_fixpoint_unique mu_roll) (* converse claimed by [Davey & Priestley 2002, page 200, exercise 8.27(iii)] for continuous f, g on a CPO ; does it hold without additional assumptions? lemma mu_commute_least_fixpoint_converse: "isotone f \ isotone g \ has_least_prefixpoint f \ has_least_prefixpoint g \ has_least_prefixpoint (f \ g) \ f \ g = g \ f \ (\ g \ \ f \ \(f \ g) = \ f)" *) lemma nu_commute_fixpoint_1: "isotone f \ has_greatest_fixpoint (f \ g) \ f \ g = g \ f \ is_fixpoint f (\(f \ g))" by (metis is_fixpoint_def nu_roll) lemma nu_commute_fixpoint_2: "isotone g \ has_greatest_fixpoint (f \ g) \ f \ g = g \ f \ is_fixpoint g (\(f \ g))" by (metis is_fixpoint_def nu_roll) lemma nu_commute_greatest_fixpoint: "isotone f \ isotone g \ has_greatest_fixpoint f \ has_greatest_fixpoint g \ has_greatest_fixpoint (f \ g) \ f \ g = g \ f \ (\(f \ g) = \ f \ \ f \ \ g)" by (smt is_greatest_fixpoint_def greatest_fixpoint_same greatest_fixpoint_unique nu_roll) lemma mu_diagonal_1: "isotone (\x . f x x) \ (\x . isotone (\y . f x y)) \ isotone (\x . \(\y . f x y)) \ (\x . has_least_fixpoint (\y . f x y)) \ has_least_prefixpoint (\x . \(\y . f x y)) \ \(\x . f x x) = \(\x . \(\y . f x y))" by (smt is_least_fixpoint_def is_least_prefixpoint_def least_fixpoint_same least_fixpoint_unique least_prefixpoint least_prefixpoint_fixpoint) lemma mu_diagonal_2: "(\x . isotone (\y . f x y) \ isotone (\y . f y x) \ has_least_prefixpoint (\y . f x y)) \ has_least_prefixpoint (\x . \(\y . f x y)) \ \(\x . f x x) = \(\x . \(\y . f x y))" by (smt is_least_fixpoint_def is_least_prefixpoint_def isotone_def least_fixpoint_same least_prefixpoint least_prefixpoint_fixpoint) lemma nu_diagonal_1: "isotone (\x . f x x) \ (\x . isotone (\y . f x y)) \ isotone (\x . \(\y . f x y)) \ (\x . has_greatest_fixpoint (\y . f x y)) \ has_greatest_postfixpoint (\x . \(\y . f x y)) \ \(\x . f x x) = \(\x . \(\y . f x y))" by (smt is_greatest_fixpoint_def is_greatest_postfixpoint_def greatest_fixpoint_same greatest_fixpoint_unique greatest_postfixpoint greatest_postfixpoint_fixpoint) lemma nu_diagonal_2: "(\x . isotone (\y . f x y) \ isotone (\y . f y x) \ has_greatest_postfixpoint (\y . f x y)) \ has_greatest_postfixpoint (\x . \(\y . f x y)) \ \(\x . f x x) = \(\x . \(\y . f x y))" using [[ smt_timeout = 120 ]] by (smt is_greatest_fixpoint_def is_greatest_postfixpoint_def isotone_def greatest_fixpoint_same greatest_postfixpoint greatest_postfixpoint_fixpoint) end (* end theory Tests imports Notation begin *) class tests = mult + neg + one + ord + plus + zero + assumes sub_assoc: "-x ; (-y ; -z) = (-x ; -y) ; -z" assumes sub_comm: "-x ; -y = -y ; -x" assumes sub_compl: "-x = -(--x ; -y) ; -(--x ; --y)" assumes sub_mult_closed: "-x ; -y = --(-x ; -y)" assumes the_zero_def: "0 = (THE x . (\y . x = -y ; --y))" -- {* define without imposing uniqueness *} assumes one_def: "1 = - 0" assumes plus_def: "-x + -y = -(--x ; --y)" assumes leq_def: "-x \ -y \ -x ; -y = -x" assumes strict_leq_def: "-x < -y \ -x \ -y \ \ (-y \ -x)" begin -- {* uniqueness of 0, resulting in the lemma zero_def to replace the assumption the_zero_def *} lemma unique_zero: "-x ; --x = -y ; --y" by (metis sub_assoc sub_comm sub_compl) definition is_zero :: "'a \ bool" where is_zero_def: "is_zero(x) \ (\y . x = -y ; --y)" (* This is an auxiliary predicate for the following lemma. *) lemma the_zero_def_p: "0 = (THE x . is_zero(x))" by (simp only: the_zero_def is_zero_def) (* This auxiliary lemma replaces the assumption the_zero_def in the proof of the following lemma. *) lemma zero_def: "0 = -x ; --x" by (metis unique_zero the_zero_def_p is_zero_def theI') (* Metis does not terminate if the original assumption the_zero_def is used. *) -- {* consequences for meet and complement *} lemma double_negation: "-x = ---x" by (metis sub_mult_closed sub_compl) lemma compl_1: "--x = -(-x ; -y) ; -(-x ; --y)" by (metis double_negation sub_compl) lemma right_zero: "-x ; (-y ; --y) = -z ; --z" by (metis compl_1 sub_assoc sub_mult_closed zero_def) lemma right_one: "-x ; -x = -x ; -(-y ; --y)" by (metis compl_1 right_zero sub_mult_closed zero_def) lemma mult_idempotent: "-x ; -x = -x" by (metis compl_1 double_negation sub_assoc sub_mult_closed zero_def) lemma compl_2: "-x = -(-(-x ; -y) ; -(-x ; --y))" by (metis compl_1 double_negation) -- {* consequences for join *} lemma plus_idempotent: "-x + -x = -x" by (metis double_negation mult_idempotent plus_def) lemma plus_comm: "-x + -y = -y + -x" by (metis plus_def sub_comm) lemma plus_assoc: "-x + (-y + -z) = (-x + -y) + -z" by (metis plus_def sub_assoc sub_mult_closed) lemma plus_absorb: "-x ; -y + -x = -x" by (smt compl_1 mult_idempotent plus_def sub_assoc sub_mult_closed) lemma mult_cases: "-x = (-x + -y) ; (-x + --y)" by (metis compl_1 double_negation plus_def) lemma mult_deMorgan: "-(-x ; -y) = --x + --y" by (metis double_negation plus_def) lemma plus_deMorgan: "-(-x + -y) = --x ; --y" by (metis plus_def sub_mult_closed) lemma plus_cases: "-x = -x ; -y + -x ; --y" by (smt mult_deMorgan double_negation mult_cases sub_mult_closed) lemma plus_compl_intro: "(-x ; -y) + --x = -y + --x" by (smt compl_1 mult_deMorgan plus_absorb plus_cases sub_assoc sub_comm sub_mult_closed) lemma mult_absorb: "-x ; (-x + -y) = -x" by (smt plus_absorb plus_def sub_mult_closed sub_comm) lemma plus_closed: "-x + -y = --(-x + -y)" by (metis plus_def double_negation) lemma plus_distr_mult: "-x + (-y ; -z) = (-x + -y) ; (-x + -z)" by (smt mult_cases sub_mult_closed plus_closed plus_assoc plus_absorb plus_compl_intro mult_absorb sub_assoc plus_comm) lemma mult_distr_plus: "-x ; (-y + -z) = (-x ; -y) + (-x ; -z)" by (smt plus_def double_negation plus_deMorgan plus_distr_mult mult_deMorgan sub_mult_closed) lemma mult_compl_intro: "-x ; -y = -x ; (--x + -y)" by (metis sub_mult_closed mult_cases plus_absorb plus_compl_intro plus_comm) lemma case_duality: "(--x + -y) ; (-x + -z) = -x ; -y + --x ; -z" proof - have "(--x + -y) ; (-x + -z) = --(-y ; -z ; -x) + --(-y ; -x) + (--(-y ; -z ; --x) + --(--x ; -z))" by (smt mult_distr_plus plus_closed mult_compl_intro sub_comm plus_assoc plus_cases sub_mult_closed plus_comm) thus ?thesis by (smt sub_comm sub_assoc sub_mult_closed plus_absorb) qed lemma case_duality_2: "(-x + -y) ; (--x + -z) = -x ; -z + --x ; -y" by (metis case_duality double_negation plus_comm sub_mult_closed) lemma compl_cases: "(-v + -w) ; (--v + -x) + -((-v + -y) ; (--v + -z)) = (-v + -w + --y) ; (--v + -x + --z)" by (smt mult_deMorgan plus_deMorgan sub_mult_closed plus_closed double_negation case_duality sub_comm plus_assoc plus_comm mult_distr_plus case_duality_2) lemma plus_cases_2: "--x = -(-x + -y) + -(-x + --y)" by (metis mult_deMorgan plus_deMorgan double_negation mult_cases sub_mult_closed plus_closed) -- {* consequences for 0 and 1 *} lemma mult_compl: "-x ; --x = 0" by (metis zero_def) lemma plus_compl: "-x + --x = 1" by (metis one_def plus_def zero_def) lemma one_compl: "- 1 = 0" by (metis mult_compl one_def sub_mult_closed) lemma bs_mult_right_zero: "-x ; 0 = 0" by (metis right_zero zero_def) lemma bs_mult_left_zero: "0 ; -x = 0" by (metis bs_mult_right_zero one_compl sub_comm) lemma plus_right_one: "-x + 1 = 1" by (metis one_compl one_def mult_deMorgan double_negation bs_mult_right_zero) lemma plus_left_one: "1 + -x = 1" by (metis plus_right_one one_def plus_comm) lemma bs_mult_right_one: "-x ; 1 = -x" by (metis mult_compl one_def mult_idempotent right_one) lemma bs_mult_left_one: "1 ; -x = -x" by (metis one_def bs_mult_right_one sub_comm) lemma plus_right_zero: "-x + 0 = -x" by (metis mult_compl mult_cases plus_distr_mult) lemma plus_left_zero: "0 + -x = -x" by (metis plus_right_zero one_compl plus_comm) lemma one_double_compl: "-- 1 = 1" by (metis one_compl one_def) lemma zero_double_compl: "-- 0 = 0" by (metis one_compl one_def) -- {* consequences for the order *} lemma reflexive: "-x \ -x" by (metis leq_def mult_idempotent) lemma transitive: "-x \ -y \ -y \ -z \ -x \ -z" by (metis leq_def sub_assoc) lemma antisymmetric: "-x \ -y \ -y \ -x \ -x = -y" by (metis leq_def sub_comm) lemma zero_least_test: "0 \ -x" by (metis one_compl leq_def bs_mult_right_zero sub_comm) lemma one_greatest: "-x \ 1" by (metis leq_def one_def bs_mult_right_one) lemma lower_bound_left: "-x ; -y \ -x" by (metis leq_def mult_idempotent sub_assoc sub_mult_closed sub_comm) lemma lower_bound_right: "-x ; -y \ -y" by (metis leq_def mult_idempotent sub_assoc sub_mult_closed) lemma mult_iso_left: "-x \ -y \ -x ; -z \ -y ; -z" by (metis leq_def lower_bound_left sub_assoc sub_comm sub_mult_closed) lemma mult_iso_right: "-x \ -y \ -z ; -x \ -z ; -y" by (metis mult_iso_left sub_comm) lemma compl_anti: "-x \ -y \ --y \ --x" by (metis one_compl plus_compl plus_deMorgan double_negation leq_def plus_comm plus_compl_intro plus_right_zero) lemma leq_plus: "-x \ -y \ -x + -y = -y" by (metis double_negation leq_def mult_absorb plus_def sub_comm) lemma plus_compl_iso: "-x \ -y \ -(-y + -z) \ -(-x + -z)" by (metis plus_deMorgan leq_plus lower_bound_left mult_iso_left) lemma plus_iso_left: "-x \ -y \ -x + -z \ -y + -z" by (metis plus_compl_iso compl_anti double_negation plus_def) lemma plus_iso_right: "-x \ -y \ -z + -x \ -z + -y" by (metis plus_iso_left plus_comm) lemma greatest_lower_bound: "-x \ -y \ -x \ -z \ -x \ -y ; -z" by (metis leq_def plus_absorb plus_comm sub_assoc sub_mult_closed) lemma upper_bound_left: "-x \ -x + -y" by (metis one_compl plus_iso_right plus_right_zero zero_least_test) lemma upper_bound_right: "-y \ -x + -y" by (metis upper_bound_left plus_comm) lemma least_upper_bound: "-x \ -z \ -y \ -z \ -x + -y \ -z" by (metis leq_plus plus_assoc plus_def upper_bound_right) lemma leq_mult_zero: "-x \ -y \ -x ; --y = 0" proof - have "-x \ -y \ -x ; --y = 0" by (metis leq_def sub_assoc mult_compl bs_mult_right_zero) also have "-x ; --y = 0 \ -x \ -y" by (metis compl_1 one_def leq_def bs_mult_right_one sub_mult_closed) ultimately show ?thesis by metis qed lemma leq_plus_right_one: "-x \ -y \ --x + -y = 1" by (metis one_compl one_def mult_deMorgan plus_deMorgan double_negation leq_mult_zero) lemma shunting: "-x ; -y \ -z \ -y \ --x + -z" by (smt leq_mult_zero sub_assoc sub_mult_closed sub_comm plus_deMorgan double_negation mult_deMorgan) lemma shunting_right: "-x ; -y \ -z \ -x \ -z + --y" by (metis plus_comm shunting sub_comm) lemma leq_cases: "-x ; -y \ -z \ --x ; -y \ -z \ -y \ -z" by (smt least_upper_bound sub_mult_closed mult_distr_plus sub_comm plus_compl bs_mult_right_one) lemma leq_cases_2: "-x ; -y \ -x ; -z \ --x ; -y \ --x ; -z \ -y \ -z" by (metis greatest_lower_bound leq_cases sub_mult_closed) lemma leq_cases_3: "-y ; -x \ -z ; -x \ -y ; --x \ -z ; --x \ -y \ -z" by (metis leq_cases_2 sub_comm) lemma eq_cases: "-x ; -y = -x ; -z \ --x ; -y = --x ; -z \ -y = -z" by (metis plus_cases sub_comm) lemma eq_cases_2: "-y ; -x = -z ; -x \ -y ; --x = -z ; --x \ -y = -z" by (metis eq_cases sub_comm) lemma mult_distr_plus_right: "(-y + -z) ; -x = (-y ; -x) + (-z ; -x)" by (metis mult_distr_plus plus_def sub_comm) lemma wnf_lemma_1: "(-x ; -y + --x ; -z) ; -x = -x ; -y" by (smt mult_compl mult_distr_plus_right mult_idempotent plus_right_zero sub_assoc sub_comm sub_mult_closed) lemma wnf_lemma_2: "(-x ; -y + -z ; --y) ; -y = -x ; -y" by (metis sub_comm wnf_lemma_1) lemma wnf_lemma_3: "(-x ; -z + --x ; -y) ; --x = --x ; -y" by (smt mult_compl mult_distr_plus_right mult_idempotent plus_comm plus_right_zero sub_assoc sub_comm sub_mult_closed) lemma wnf_lemma_4: "(-z ; -y + -x ; --y) ; --y = -x ; --y" by (metis sub_comm wnf_lemma_3) end (* end theory Semiring imports Notation begin *) class semiring = mult + one + ord + plus + zero + assumes add_associative : "(x + y) + z = x + (y + z)" assumes add_commutative : "x + y = y + x" assumes add_idempotent : "x + x = x" assumes add_left_zero : "0 + x = x" assumes mult_associative : "(x ; y) ; z = x ; (y ; z)" assumes mult_left_one : "1 ; x = x" assumes mult_right_one : "x ; 1 = x" assumes mult_left_dist_add : "x ; (y + z) = x ; y + x ; z" assumes mult_right_dist_add: "(x + y) ; z = x ; z + y ; z" assumes mult_left_zero : "0 ; x = 0" assumes less_eq_def : "x \ y \ x + y = y" assumes less_def : "x < y \ x \ y \ \ (y \ x)" begin subclass order by unfold_locales (metis less_def, metis add_idempotent less_eq_def, metis add_associative less_eq_def, metis add_commutative less_eq_def) lemma add_left_isotone: "x \ y \ x + z \ y + z" by (smt add_associative add_commutative add_idempotent less_eq_def) lemma add_right_isotone: "x \ y \ z + x \ z + y" by (metis add_commutative add_left_isotone) lemma add_isotone: "w \ y \ x \ z \ w + x \ y + z" by (smt add_associative add_commutative less_eq_def) lemma add_left_upper_bound: "x \ x + y" by (metis add_associative add_idempotent less_eq_def) lemma add_right_upper_bound: "y \ x + y" by (metis add_commutative add_left_upper_bound) lemma add_least_upper_bound: "x \ z \ y \ z \ x + y \ z" by (smt add_associative add_commutative add_left_upper_bound less_eq_def) lemma add_left_divisibility: "x \ y \ (\z . x + z = y)" by (metis add_left_upper_bound less_eq_def) lemma add_right_divisibility: "x \ y \ (\z . z + x = y)" by (metis add_commutative add_left_divisibility) lemma add_right_zero: "x + 0 = x" by (metis add_commutative add_left_zero) lemma zero_least: "0 \ x" by (metis add_left_upper_bound add_left_zero) lemma mult_left_isotone: "x \ y \ x ; z \ y ; z" by (metis less_eq_def mult_right_dist_add) lemma mult_right_isotone: "x \ y \ z ; x \ z ; y" by (metis less_eq_def mult_left_dist_add) lemma mult_isotone: "w \ y \ x \ z \ w ; x \ y ; z" by (smt mult_left_isotone mult_right_isotone order_trans) lemma mult_left_subdist_add_left: "x ; y \ x ; (y + z)" by (metis add_left_upper_bound mult_left_dist_add) lemma mult_left_subdist_add_right: "x ; z \ x ; (y + z)" by (metis add_right_upper_bound mult_left_dist_add) lemma mult_right_subdist_add_left: "x ; z \ (x + y) ; z" by (metis add_left_upper_bound mult_right_dist_add) lemma mult_right_subdist_add_right: "y ; z \ (x + y) ; z" by (metis add_right_upper_bound mult_right_dist_add) lemma case_split_left: "1 \ w + z \ w ; x \ y \ z ; x \ y \ x \ y" by (smt add_least_upper_bound mult_left_isotone mult_left_one mult_right_dist_add order_trans) lemma case_split_left_equal: "w + z = 1 \ w ; x = w ; y \ z ; x = z ; y \ x = y" by (metis mult_left_one mult_right_dist_add) lemma case_split_right: "1 \ w + z \ x ; w \ y \ x ; z \ y \ x \ y" by (smt add_least_upper_bound mult_right_isotone mult_right_one mult_left_dist_add order_trans) lemma case_split_right_equal: "w + z = 1 \ x ; w = y ; w \ x ; z = y ; z \ x = y" by (metis mult_left_dist_add mult_right_one) lemma zero_right_mult_decreasing: "x ; 0 \ x" by (metis add_right_zero mult_left_subdist_add_right mult_right_one) lemma add_same_context:"x \ y + z \ y \ x + z \ x + z = y + z" by (smt add_associative add_commutative less_eq_def) end class semiring_T = semiring + fixes T :: "'a" ("\") assumes add_left_top: "T + x = T" begin lemma add_right_top: "x + T = T" by (metis add_commutative add_left_top) lemma top_greatest: "x \ T" by (metis add_left_top add_right_upper_bound) lemma top_left_mult_increasing: "x \ T ; x" by (metis mult_left_isotone mult_left_one top_greatest) lemma top_right_mult_increasing: "x \ x ; T" by (metis mult_right_isotone mult_right_one top_greatest) lemma top_mult_top: "T ; T = T" by (metis add_right_divisibility add_right_top top_right_mult_increasing) definition vector :: "'a \ bool" where "vector x \ x = x ; T" lemma vector_zero: "vector 0" by (metis mult_left_zero vector_def) lemma vector_top: "vector T" by (metis top_mult_top vector_def) lemma vector_add_closed: "vector x \ vector y \ vector (x + y)" by (metis mult_right_dist_add vector_def) lemma vector_left_mult_closed: "vector y \ vector (x ; y)" by (metis mult_associative vector_def) end (* end theory Domain imports Semiring Tests begin *) class dom = fixes d :: "'a \ 'a" class domain_semiring = semiring + dom + assumes d_restrict: "x + d(x) ; x = d(x) ; x" assumes d_mult_d : "d(x ; y) = d(x ; d(y))" assumes d_plus_one: "d(x) + 1 = 1" assumes d_zero : "d(0) = 0" assumes d_dist_add: "d(x + y) = d(x) + d(y)" begin text {* Most lemmas in this class are taken from Georg Struth's theories. *} lemma d_restrict_equals: "x = d(x) ; x" by (metis add_commutative d_plus_one d_restrict mult_left_one mult_right_dist_add) lemma d_involutive: "d(d(x)) = d(x)" by (metis d_mult_d mult_left_one) lemma d_fixpoint: "(\y . x = d(y)) \ x = d(x)" by (metis d_involutive) lemma d_type: "\P . (\x . x = d(x) \ P(x)) \ (\x . P(d(x)))" by (metis d_involutive) lemma d_mult_sub: "d(x ; y) \ d(x)" by (metis d_dist_add d_mult_d d_plus_one less_eq_def mult_left_subdist_add_left mult_right_one) lemma d_sub_one: "x \ 1 \ x \ d(x)" by (metis d_restrict_equals mult_right_isotone mult_right_one) lemma d_strict: "d(x) = 0 \ x = 0" by (metis d_restrict_equals d_zero mult_left_zero) lemma d_one: "d(1) = 1" by (metis d_restrict_equals mult_right_one) lemma d_below_one: "d(x) \ 1" by (metis d_plus_one less_eq_def) lemma d_isotone: "x \ y \ d(x) \ d(y)" by (metis d_dist_add less_eq_def) lemma d_plus_left_upper_bound: "d(x) \ d(x + y)" by (metis add_left_upper_bound d_isotone) lemma d_export: "d(d(x) ; y) = d(x) ; d(y)" by (smt add_commutative antisym d_mult_d d_mult_sub d_plus_left_upper_bound d_plus_one d_restrict d_sub_one mult_isotone mult_left_one mult_left_subdist_add_right mult_right_dist_add mult_right_one) lemma d_idempotent: "d(x) ; d(x) = d(x)" by (metis d_export d_restrict_equals) lemma d_commutative: "d(x) ; d(y) = d(y) ; d(x)" by (smt antisym d_export d_mult_d d_mult_sub d_one d_restrict_equals mult_isotone mult_left_one) lemma d_least_left_preserver: "x \ d(y) ; x \ d(x) \ d(y)" by (metis d_below_one d_involutive d_mult_sub d_restrict_equals eq_iff mult_left_isotone mult_left_one) lemma d_weak_locality: "x ; y = 0 \ x ; d(y) = 0" by (metis d_mult_d d_strict) lemma d_add_closed: "d(d(x) + d(y)) = d(x) + d(y)" by (metis d_dist_add d_involutive) lemma d_mult_closed: "d(d(x) ; d(y)) = d(x) ; d(y)" by (metis d_export d_mult_d) lemma d_mult_left_lower_bound: "d(x) ; d(y) \ d(x)" by (metis d_export d_involutive d_mult_sub) lemma d_mult_greatest_lower_bound: "d(x) \ d(y) ; d(z) \ d(x) \ d(y) \ d(x) \ d(z)" by (metis d_commutative d_idempotent d_mult_left_lower_bound mult_isotone order_trans) lemma d_mult_left_absorb_add: "d(x) ; (d(x) + d(y)) = d(x)" by (metis add_commutative d_idempotent d_plus_one mult_left_dist_add mult_right_one) lemma d_add_left_absorb_mult: "d(x) + d(x) ; d(y) = d(x)" by (metis add_commutative d_mult_left_lower_bound less_eq_def) lemma d_add_left_dist_mult: "d(x) + d(y) ; d(z) = (d(x) + d(y)) ; (d(x) + d(z))" by (smt add_associative d_commutative d_idempotent d_mult_left_absorb_add mult_left_dist_add mult_right_dist_add) lemma d_order: "d(x) \ d(y) \ d(x) = d(x) ; d(y)" by (metis d_mult_greatest_lower_bound d_mult_left_absorb_add less_eq_def order_refl) end class antidomain_semiring = semiring + dom + neg + assumes a_restrict : "-x ; x = 0" assumes a_plus_mult_d: "-(x ; y) + -(x ; --y) = -(x ; --y)" assumes a_complement : "--x + -x = 1" assumes d_def : "d(x) = --x" begin text {* Most lemmas in this class are taken from Georg Struth's theories. *} notation uminus ("a") lemma a_greatest_left_absorber: "a(x) ; y = 0 \ a(x) \ a(y)" by (rule, metis a_complement a_plus_mult_d a_restrict add_left_zero add_right_zero mult_left_dist_add mult_left_one mult_right_one mult_right_subdist_add_right, metis a_restrict add_right_zero less_eq_def mult_right_dist_add) lemma a_mult_d: "a(x ; y) = a(x ; d(y))" by (metis a_complement a_greatest_left_absorber a_plus_mult_d d_def less_eq_def mult_associative mult_left_one mult_left_zero mult_right_dist_add a_restrict add_commutative) lemma a_d_closed: "d(a(x)) = a(x)" by (metis a_mult_d d_def mult_left_one) lemma a_plus_left_lower_bound: "a(x + y) \ a(x)" by (metis a_greatest_left_absorber eq_iff mult_left_subdist_add_left zero_least) lemma a_idempotent: "a(x) ; a(x) = a(x)" by (metis a_complement a_d_closed a_restrict add_right_zero d_def mult_left_dist_add mult_right_one) lemma a_below_one: "a(x) \ 1" by (metis a_complement add_commutative add_left_upper_bound) lemma a_3: "a(x) ; a(y) ; d(x + y) = 0" by (metis a_below_one a_greatest_left_absorber a_mult_d a_plus_left_lower_bound a_restrict less_eq_def mult_associative mult_left_dist_add mult_left_isotone mult_left_one) lemma a_dist_add: "a(x) ; a(y) = a(x + y)" proof - have "a(x) ; a(y) = a(x) ; a(y) ; a(x + y)" by (metis a_3 a_complement add_left_zero d_def mult_left_dist_add mult_right_one) hence "a(x) ; a(y) \ a(x + y)" by (metis a_below_one mult_left_isotone mult_left_one order_trans) thus ?thesis by (metis a_idempotent a_plus_left_lower_bound add_commutative antisym mult_left_isotone mult_right_isotone order_trans) qed lemma a_export: "a(a(x) ; y) = d(x) + a(y)" proof - have "a(a(x) ; y) = a(a(x) ; y) ; d(y) + a(a(x) ; y) ; a(y)" by (metis a_complement d_def mult_left_dist_add mult_right_one) hence "a(a(x) ; y) \ a(a(x) ; y) ; d(y) + a(y)" by (metis a_below_one a_dist_add less_eq_def mult_left_isotone mult_left_one) hence "a(a(x) ; y) \ a(a(x) ; y) ; (a(x) + d(x)) ; d(y) + a(y)" by (metis a_complement add_commutative d_def mult_associative mult_left_one) hence "a(a(x) ; y) \ a(a(x) ; y) ; d(x) ; d(y) + a(y)" by (smt a_mult_d a_restrict add_left_zero mult_associative mult_left_dist_add mult_right_dist_add) hence "a(a(x) ; y) \ d(x) + a(y)" by (metis a_dist_add a_plus_left_lower_bound add_commutative add_right_isotone d_def order_trans) thus ?thesis by (metis a_restrict a_greatest_left_absorber a_dist_add add_commutative mult_left_zero d_def add_least_upper_bound mult_associative antisym) qed subclass domain_semiring apply unfold_locales apply (smt a_complement a_d_closed a_idempotent a_restrict case_split_left_equal d_def eq_refl less_eq_def mult_associative) apply (metis a_mult_d d_def) apply (metis a_below_one d_def less_eq_def) apply (metis a_3 a_d_closed a_dist_add d_def) by (metis a_dist_add a_export d_def) subclass tests apply unfold_locales apply (metis mult_associative) apply (metis a_dist_add add_commutative) apply (metis a_complement a_d_closed a_dist_add d_def mult_left_dist_add mult_right_one) apply (metis a_d_closed a_dist_add d_def) apply (rule the_equality[THEN sym]) apply (metis a_d_closed a_restrict d_def) apply (metis a_d_closed a_restrict d_def) apply (metis a_complement a_restrict add_right_zero mult_right_one) apply (metis a_d_closed a_export d_def) apply (smt a_d_closed a_dist_add a_plus_left_lower_bound add_commutative d_def less_eq_def) by (metis less_def) lemma a_fixpoint: "\x . (a(x) = x \ (\y . y = 0))" by (metis a_complement a_restrict add_idempotent mult_left_one mult_left_zero) lemma a_strict: "a(x) = 1 \ x = 0" by (metis a_complement a_restrict add_right_zero mult_left_one mult_right_one) lemma d_complement_zero: "d(x) ; a(x) = 0" by (metis a_restrict d_def) lemma a_complement_zero: "a(x) ; d(x) = 0" by (metis d_def zero_def) lemma a_shunting_zero: "a(x) ; d(y) = 0 \ a(x) \ a(y)" by (metis a_greatest_left_absorber d_weak_locality) lemma a_antitone: "x \ y \ a(y) \ a(x)" by (metis a_plus_left_lower_bound less_eq_def) lemma a_mult_deMorgan: "a(a(x) ; a(y)) = d(x + y)" by (metis a_dist_add d_def) lemma a_mult_deMorgan_1: "a(a(x) ; a(y)) = d(x) + d(y)" by (metis a_mult_deMorgan d_dist_add) lemma a_mult_deMorgan_2: "a(d(x) ; d(y)) = a(x) + a(y)" by (metis d_def plus_def) lemma a_plus_deMorgan: "a(a(x) + a(y)) = d(x) ; d(y)" by (metis a_dist_add d_def) lemma a_plus_deMorgan_1: "a(d(x) + d(y)) = a(x) ; a(y)" by (metis a_mult_deMorgan_1 sub_mult_closed) lemma a_mult_left_upper_bound: "a(x) \ a(x ; y)" by (metis a_greatest_left_absorber d_def d_mult_sub leq_mult_zero sub_comm) lemma d_a_closed: "a(d(x)) = a(x)" by (metis a_d_closed d_def) lemma a_export_d: "a(d(x) ; y) = a(x) + a(y)" by (metis a_mult_d a_mult_deMorgan_2) lemma a_7: "d(x) ; a(d(y) + d(z)) = d(x) ; a(y) ; a(z)" by (metis a_plus_deMorgan_1 mult_associative) lemma d_a_shunting: "d(x) ; a(y) \ d(z) \ d(x) \ d(z) + d(y)" by (smt a_dist_add d_def plus_closed shunting sub_comm) lemma d_d_shunting: "d(x) ; d(y) \ d(z) \ d(x) \ d(z) + a(y)" by (metis d_a_closed d_a_shunting d_def) lemma d_cancellation_1: "d(x) \ d(y) + (d(x) ; a(y))" by (metis a_dist_add add_commutative add_left_upper_bound d_def plus_compl_intro) lemma d_cancellation_2: "(d(z) + d(y)) ; a(y) \ d(z)" by (metis d_a_shunting d_dist_add eq_refl) lemma a_add_closed: "d(a(x) + a(y)) = a(x) + a(y)" by (metis d_def plus_closed) lemma a_mult_closed: "d(a(x) ; a(y)) = a(x) ; a(y)" by (metis d_def sub_mult_closed) lemma d_a_shunting_zero: "d(x) ; a(y) = 0 \ d(x) \ d(y)" by (metis a_greatest_left_absorber d_def) lemma d_d_shunting_zero: "d(x) ; d(y) = 0 \ d(x) \ a(y)" by (metis d_def leq_mult_zero) lemma d_compl_intro: "d(x) + d(y) = d(x) + a(x) ; d(y)" by (metis add_commutative d_def plus_compl_intro) lemma a_compl_intro: "a(x) + a(y) = a(x) + d(x) ; a(y)" by (smt a_dist_add add_commutative d_def mult_right_one plus_compl plus_distr_mult) lemma kat_2: "y ; a(z) \ a(x) ; y \ d(x) ; y ; a(z) = 0" by (smt a_export a_plus_left_lower_bound add_least_upper_bound d_d_shunting_zero d_export d_strict less_eq_def mult_associative) lemma kat_3: "d(x) ; y ; a(z) = 0 \ d(x) ; y = d(x) ; y ; d(z)" by (metis add_left_zero d_def mult_left_dist_add mult_right_one plus_compl) lemma kat_4: "d(x) ; y = d(x) ; y ; d(z) \ d(x) ; y \ y ; d(z)" by (metis a_below_one d_def mult_left_isotone mult_left_one) lemma kat_2_equiv: "y ; a(z) \ a(x) ; y \ d(x) ; y ; a(z) = 0" by (smt kat_2 a_below_one a_complement add_left_zero d_def mult_left_one mult_right_dist_add mult_right_isotone mult_right_one) lemma kat_4_equiv: "d(x) ; y = d(x) ; y ; d(z) \ d(x) ; y \ y ; d(z)" by (rule, metis kat_4, rule antisym, metis d_idempotent less_eq_def mult_associative mult_left_dist_add, metis d_plus_one less_eq_def mult_left_dist_add mult_right_one) lemma kat_3_equiv_opp: "a(z) ; y ; d(x) = 0 \ y ; d(x) = d(z) ; y ; d(x)" by (smt a_complement a_restrict add_left_zero d_a_closed d_def mult_associative mult_left_one mult_left_zero mult_right_dist_add) lemma kat_4_equiv_opp: "y ; d(x) = d(z) ; y ; d(x) \ y ; d(x) \ d(z) ; y" by (metis d_def double_negation kat_2_equiv kat_3_equiv_opp) lemma d_restrict_iff: "(x \ y) \ (x \ d(x) ; y)" by (smt add_least_upper_bound d_below_one d_restrict_equals less_eq_def mult_left_dist_add mult_left_isotone mult_left_one) lemma d_restrict_iff_1: "(d(x) ; y \ z) \ (d(x) ; y \ d(x) ; z)" by (metis add_commutative d_export d_mult_left_lower_bound d_plus_one d_restrict_iff mult_left_isotone mult_left_one mult_right_subdist_add_right order_trans) end (* end theory Iteration imports Semiring Fixpoint begin *) class itering_0 = semiring + fixes circ :: "'a \ 'a" ("_\<^sup>\" [100] 100) assumes circ_mult: "(x ; y)\<^sup>\ = 1 + x ; (y ; x)\<^sup>\ ; y" assumes circ_add: "(x + y)\<^sup>\ = (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" begin lemma circ_isotone: "x \ y \ x\<^sup>\ \ y\<^sup>\" by (metis add_left_divisibility circ_add circ_mult mult_left_one mult_right_subdist_add_left) lemma circ_slide: "x ; (y ; x)\<^sup>\ = (x ; y)\<^sup>\ ; x" by (smt circ_mult mult_associative mult_left_dist_add mult_left_one mult_right_dist_add mult_right_one) lemma circ_right_unfold: "1 + x\<^sup>\ ; x = x\<^sup>\" by (metis circ_mult mult_left_one mult_right_one) lemma circ_left_unfold: "1 + x ; x\<^sup>\ = x\<^sup>\" by (metis circ_mult circ_slide mult_associative mult_right_one) lemma circ_zero: "0\<^sup>\ = 1" by (metis add_right_zero circ_left_unfold mult_left_zero) lemma circ_increasing: "x \ x\<^sup>\" by (metis add_right_upper_bound circ_right_unfold mult_left_one mult_right_subdist_add_left order_trans) lemma circ_transitive_equal: "x\<^sup>\ ; x\<^sup>\ = x\<^sup>\" by (metis add_idempotent circ_add circ_mult mult_associative mult_left_one mult_right_one) lemma circ_circ_circ: "x\<^sup>\\<^sup>\\<^sup>\ = x\<^sup>\\<^sup>\" by (metis add_idempotent circ_add circ_increasing circ_transitive_equal less_eq_def) lemma circ_one: "1\<^sup>\ = 1\<^sup>\\<^sup>\" by (metis circ_circ_circ circ_zero) lemma circ_add_1: "(x + y)\<^sup>\ = x\<^sup>\ ; (y ; x\<^sup>\)\<^sup>\" by (metis circ_add circ_slide) lemma circ_reflexive: "1 \ x\<^sup>\" by (metis add_left_divisibility circ_right_unfold) lemma circ_add_2: "(x + y)\<^sup>\ \ (x\<^sup>\ ; y\<^sup>\)\<^sup>\" by (metis add_least_upper_bound circ_increasing circ_isotone circ_reflexive mult_isotone mult_left_one mult_right_one) lemma mult_zero_circ: "(x ; 0)\<^sup>\ = 1 + x ; 0" by (metis circ_mult mult_associative mult_left_zero) lemma mult_zero_add_circ: "(x + y ; 0)\<^sup>\ = x\<^sup>\ ; (y ; 0)\<^sup>\" by (metis circ_add_1 mult_associative mult_left_zero) lemma mult_zero_add_circ_2: "(x + y ; 0)\<^sup>\ = x\<^sup>\ + x\<^sup>\ ; y ; 0" by (metis mult_associative mult_left_dist_add mult_right_one mult_zero_add_circ mult_zero_circ) lemma circ_plus_same: "x\<^sup>\ ; x = x ; x\<^sup>\" by (metis circ_slide mult_left_one mult_right_one) lemma circ_plus_one: "x\<^sup>\ = 1 + x\<^sup>\" by (metis less_eq_def circ_reflexive) lemma circ_rtc_2: "1 + x + x\<^sup>\ ; x\<^sup>\ = x\<^sup>\" by (metis add_associative circ_increasing circ_plus_one circ_transitive_equal less_eq_def) lemma circ_unfold_sum: "(x + y)\<^sup>\ = x\<^sup>\ + x\<^sup>\ ; y ; (x + y)\<^sup>\" by (smt circ_add_1 circ_mult mult_associative mult_left_dist_add mult_right_one) lemma circ_loop_fixpoint: "y ; (y\<^sup>\ ; z) + z = y\<^sup>\ ; z" by (metis add_commutative circ_left_unfold mult_associative mult_left_one mult_right_dist_add) lemma left_plus_below_circ: "x ; x\<^sup>\ \ x\<^sup>\" by (metis add_right_upper_bound circ_left_unfold) lemma right_plus_below_circ: "x\<^sup>\ ; x \ x\<^sup>\" by (metis circ_plus_same left_plus_below_circ) lemma circ_add_upper_bound: "x \ z\<^sup>\ \ y \ z\<^sup>\ \ x + y \ z\<^sup>\" by (metis add_least_upper_bound) lemma circ_mult_upper_bound: "x \ z\<^sup>\ \ y \ z\<^sup>\ \ x ; y \ z\<^sup>\" by (metis mult_isotone circ_transitive_equal) lemma circ_sub_dist: "x\<^sup>\ \ (x + y)\<^sup>\" by (metis add_left_upper_bound circ_isotone) lemma circ_sub_dist_1: "x \ (x + y)\<^sup>\" by (metis add_least_upper_bound circ_increasing) lemma circ_sub_dist_2: "x ; y \ (x + y)\<^sup>\" by (metis add_commutative circ_mult_upper_bound circ_sub_dist_1) lemma circ_sub_dist_3: "x\<^sup>\ ; y\<^sup>\ \ (x + y)\<^sup>\" by (metis add_commutative circ_mult_upper_bound circ_sub_dist) lemma circ_sup_one_left_unfold: "1 \ x \ x ; x\<^sup>\ = x\<^sup>\" by (metis antisym less_eq_def mult_left_one mult_right_subdist_add_left left_plus_below_circ) lemma circ_sup_one_right_unfold: "1 \ x \ x\<^sup>\ ; x = x\<^sup>\" by (metis antisym less_eq_def mult_left_subdist_add_left mult_right_one right_plus_below_circ) lemma circ_decompose_4: "(x\<^sup>\ ; y\<^sup>\)\<^sup>\ = x\<^sup>\ ; (y\<^sup>\ ; x\<^sup>\)\<^sup>\" by (smt circ_add circ_increasing circ_plus_one circ_slide circ_transitive_equal less_eq_def mult_associative mult_left_subdist_add_left mult_right_one) lemma circ_decompose_5: "(x\<^sup>\ ; y\<^sup>\)\<^sup>\ = (y\<^sup>\ ; x\<^sup>\)\<^sup>\" by (metis add_associative add_commutative circ_add circ_decompose_4 circ_slide circ_zero mult_right_one) lemma circ_decompose_6: "x\<^sup>\ ; (y ; x\<^sup>\)\<^sup>\ = y\<^sup>\ ; (x ; y\<^sup>\)\<^sup>\" by (metis add_commutative circ_add_1) lemma circ_decompose_7: "(x + y)\<^sup>\ = x\<^sup>\ ; y\<^sup>\ ; (x + y)\<^sup>\" by (metis add_commutative circ_add circ_slide circ_transitive_equal mult_associative) lemma circ_decompose_8: "(x + y)\<^sup>\ = (x + y)\<^sup>\ ; x\<^sup>\ ; y\<^sup>\" by (metis antisym eq_refl mult_associative mult_isotone mult_right_one circ_mult_upper_bound circ_reflexive circ_sub_dist_3) lemma circ_decompose_9: "(x\<^sup>\ ; y\<^sup>\)\<^sup>\ = x\<^sup>\ ; y\<^sup>\ ; (x\<^sup>\ ; y\<^sup>\)\<^sup>\" by (metis circ_decompose_4 mult_associative) lemma circ_decompose_10: "(x\<^sup>\ ; y\<^sup>\)\<^sup>\ = (x\<^sup>\ ; y\<^sup>\)\<^sup>\ ; x\<^sup>\ ; y\<^sup>\" by (metis circ_decompose_9 circ_plus_same mult_associative) lemma circ_add_mult_zero: "x\<^sup>\ ; y = (x + y ; 0)\<^sup>\ ; y" by (smt mult_associative mult_left_zero mult_right_one circ_add circ_slide circ_zero) lemma circ_back_loop_fixpoint: "(z ; y\<^sup>\) ; y + z = z ; y\<^sup>\" by (metis add_commutative mult_associative mult_left_dist_add mult_right_one circ_plus_same circ_left_unfold) lemma circ_loop_is_fixpoint: "is_fixpoint (\x . y ; x + z) (y\<^sup>\ ; z)" by (metis circ_loop_fixpoint is_fixpoint_def) lemma circ_back_loop_is_fixpoint: "is_fixpoint (\x . x ; y + z) (z ; y\<^sup>\)" by (metis circ_back_loop_fixpoint is_fixpoint_def) lemma circ_circ_add: "(1 + x)\<^sup>\ = x\<^sup>\\<^sup>\" by (metis add_commutative circ_add_1 circ_decompose_4 circ_zero mult_right_one) lemma circ_circ_mult_sub: "x\<^sup>\ ; 1\<^sup>\ \ x\<^sup>\\<^sup>\" by (metis circ_increasing circ_isotone circ_mult_upper_bound circ_reflexive) lemma right_plus_circ: "(x\<^sup>\ ; x)\<^sup>\ = x\<^sup>\" by (metis add_idempotent circ_add circ_mult circ_right_unfold circ_slide) lemma left_plus_circ: "(x ; x\<^sup>\)\<^sup>\ = x\<^sup>\" by (metis circ_plus_same right_plus_circ) lemma circ_add_sub_add_one: "x ; x\<^sup>\ ; (x + y) \ x ; x\<^sup>\ ; (1 + y)" by (smt add_least_upper_bound add_left_upper_bound add_right_upper_bound circ_plus_same mult_associative mult_isotone mult_left_dist_add mult_right_one right_plus_below_circ) lemma circ_elimination: "x ; y = 0 \ x ; y\<^sup>\ \ x" by (metis add_left_zero circ_back_loop_fixpoint circ_plus_same le_less mult_associative mult_left_zero) lemma circ_square: "(x ; x)\<^sup>\ \ x\<^sup>\" by (metis circ_increasing circ_isotone left_plus_circ mult_right_isotone) lemma circ_mult_sub_add: "(x ; y)\<^sup>\ \ (x + y)\<^sup>\" by (metis add_left_upper_bound add_right_upper_bound circ_isotone circ_square mult_isotone order_trans) end class itering_1 = itering_0 + assumes circ_simulate: "z ; x \ y ; z \ z ; x\<^sup>\ \ y\<^sup>\ ; z" begin lemma circ_circ_mult: "1\<^sup>\ ; x\<^sup>\ = x\<^sup>\\<^sup>\" by (metis antisym circ_circ_add circ_reflexive circ_simulate circ_sub_dist_3 circ_sup_one_left_unfold circ_transitive_equal mult_left_one order_refl) lemma sub_mult_one_circ: "x ; 1\<^sup>\ \ 1\<^sup>\ ; x" by (metis circ_simulate mult_left_one mult_right_one order_refl) end class itering_2 = itering_1 + assumes circ_simulate_right: "z ; x \ y ; z + w \ z ; x\<^sup>\ \ y\<^sup>\ ; (z + w ; x\<^sup>\)" assumes circ_simulate_left: "x ; z \ z ; y + w \ x\<^sup>\ ; z \ (z + x\<^sup>\ ; w) ; y\<^sup>\" begin lemma circ_simulate_right_1: "z ; x \ y ; z \ z ; x\<^sup>\ \ y\<^sup>\ ; z" by (metis add_right_zero circ_simulate_right mult_left_zero) lemma circ_simulate_left_1: "x ; z \ z ; y \ x\<^sup>\ ; z \ z ; y\<^sup>\ + x\<^sup>\ ; 0" by (smt add_right_zero circ_simulate_left mult_associative mult_left_zero mult_right_dist_add) lemma circ_simulate_1: "y ; x \ x ; y \ y\<^sup>\ ; x\<^sup>\ \ x\<^sup>\ ; y\<^sup>\" by (smt add_associative add_right_zero circ_loop_fixpoint circ_simulate circ_simulate_left_1 mult_associative mult_left_zero mult_zero_add_circ_2) lemma circ_separate_1: "y ; x \ x ; y \ (x + y)\<^sup>\ = x\<^sup>\ ; y\<^sup>\" proof - have "y ; x \ x ; y \ y\<^sup>\ ; x ; y\<^sup>\ \ x ; y\<^sup>\ + y\<^sup>\ ; 0" by (smt circ_simulate_left_1 circ_transitive_equal mult_associative mult_left_isotone mult_left_zero mult_right_dist_add) thus ?thesis by (smt add_commutative circ_add_1 circ_simulate_right circ_sub_dist_3 less_eq_def mult_associative mult_left_zero zero_right_mult_decreasing) qed lemma circ_circ_mult_1: "x\<^sup>\ ; 1\<^sup>\ = x\<^sup>\\<^sup>\" by (metis add_commutative circ_circ_add circ_separate_1 mult_left_one mult_right_one order_refl) lemma atomicity_refinement: "s = s ; q \ x = q ; x \ q ; b = 0 \ r ; b \ b ; r \ r ; l \ l ; r \ x ; l \ l ; x \ b ; l \ l ; b \ q ; l \ l ; q \ r\<^sup>\ ; q \ q ; r\<^sup>\ \ q \ 1 \ s ; (x + b + r + l)\<^sup>\ ; q \ s ; (x ; b\<^sup>\ ; q + r + l)\<^sup>\" proof assume 1: "s = s ; q \ x = q ; x \ q ; b = 0 \ r ; b \ b ; r \ r ; l \ l ; r \ x ; l \ l ; x \ b ; l \ l ; b \ q ; l \ l ; q \ r\<^sup>\ ; q \ q ; r\<^sup>\ \ q \ 1" hence "s ; (x + b + r + l)\<^sup>\ ; q = s ; l\<^sup>\ ; (x + b + r)\<^sup>\ ; q" using [[ smt_timeout = 120 ]] by (smt add_commutative add_least_upper_bound circ_separate_1 mult_associative mult_left_subdist_add_right mult_right_dist_add order_trans) also have "... = s ; l\<^sup>\ ; b\<^sup>\ ; r\<^sup>\ ; q ; (x ; b\<^sup>\ ; r\<^sup>\ ; q)\<^sup>\" using 1 by (smt add_associative add_commutative circ_add_1 circ_separate_1 circ_slide mult_associative) also have "... \ s ; l\<^sup>\ ; b\<^sup>\ ; r\<^sup>\ ; q ; (x ; b\<^sup>\ ; q ; r\<^sup>\)\<^sup>\" using 1 by (metis circ_isotone mult_associative mult_right_isotone) also have "... \ s ; q ; l\<^sup>\ ; b\<^sup>\ ; r\<^sup>\ ; (x ; b\<^sup>\ ; q ; r\<^sup>\)\<^sup>\" using 1 by (metis mult_left_isotone mult_right_isotone mult_right_one) also have "... \ s ; l\<^sup>\ ; q ; b\<^sup>\ ; r\<^sup>\ ; (x ; b\<^sup>\ ; q ; r\<^sup>\)\<^sup>\" using 1 by (metis circ_simulate mult_associative mult_left_isotone mult_right_isotone) also have "... \ s ; l\<^sup>\ ; r\<^sup>\ ; (x ; b\<^sup>\ ; q ; r\<^sup>\)\<^sup>\" using 1 by (metis add_left_zero circ_back_loop_fixpoint circ_plus_same mult_associative mult_left_zero mult_left_isotone mult_right_isotone mult_right_one) also have "... \ s ; (x ; b\<^sup>\ ; q + r + l)\<^sup>\" using 1 by (metis add_commutative circ_add_1 circ_sub_dist_3 mult_associative mult_right_isotone) finally show "s ; (x + b + r + l)\<^sup>\ ; q \ s ; (x ; b\<^sup>\ ; q + r + l)\<^sup>\" . qed end class itering_3 = itering_2 + assumes circ_simulate_right_plus: "z ; x \ y ; y\<^sup>\ ; z + w \ z ; x\<^sup>\ \ y\<^sup>\ ; (z + w ; x\<^sup>\)" assumes circ_simulate_left_plus: "x ; z \ z ; y\<^sup>\ + w \ x\<^sup>\ ; z \ (z + x\<^sup>\ ; w) ; y\<^sup>\" begin lemma circ_simulate_right_plus_1: "z ; x \ y ; y\<^sup>\ ; z \ z ; x\<^sup>\ \ y\<^sup>\ ; z" by (metis add_right_zero circ_simulate_right_plus mult_left_zero) lemma circ_simulate_left_plus_1: "x ; z \ z ; y\<^sup>\ \ x\<^sup>\ ; z \ z ; y\<^sup>\ + x\<^sup>\ ; 0" by (smt add_right_zero circ_simulate_left_plus mult_associative mult_left_zero mult_right_dist_add) lemma circ_simulate_2: "y ; x\<^sup>\ \ x\<^sup>\ ; y\<^sup>\ \ y\<^sup>\ ; x\<^sup>\ \ x\<^sup>\ ; y\<^sup>\" by (rule iffI, smt add_associative add_right_zero circ_loop_fixpoint circ_simulate_left_plus_1 mult_associative mult_left_zero mult_zero_add_circ_2, metis circ_increasing mult_left_isotone order_trans) lemma circ_simulate_absorb: "y ; x \ x \ y\<^sup>\ ; x \ x + y\<^sup>\ ; 0" by (metis circ_simulate_left_plus_1 circ_zero mult_right_one) lemma circ_simulate_3: "y ; x\<^sup>\ \ x\<^sup>\ \ y\<^sup>\ ; x\<^sup>\ \ x\<^sup>\ ; y\<^sup>\" by (metis add_least_upper_bound circ_reflexive circ_simulate_2 less_eq_def mult_right_isotone mult_right_one) lemma circ_square_2: "(x ; x)\<^sup>\ ; (x + 1) \ x\<^sup>\" by (metis add_least_upper_bound circ_increasing circ_mult_upper_bound circ_reflexive circ_simulate_right_plus_1 mult_left_one mult_right_isotone mult_right_one) lemma circ_separate_mult_1: "y ; x \ x ; y \ (x ; y)\<^sup>\ \ x\<^sup>\ ; y\<^sup>\" by (metis circ_mult_sub_add circ_separate_1) lemma circ_extra_circ: "(y ; x\<^sup>\)\<^sup>\ = (y ; y\<^sup>\ ; x\<^sup>\)\<^sup>\" proof - have "y ; y\<^sup>\ ; x\<^sup>\ \ y ; x\<^sup>\ ; (y ; x\<^sup>\)\<^sup>\" by (metis add_commutative circ_add_1 circ_sub_dist_3 mult_associative mult_right_isotone) hence "(y ; y\<^sup>\ ; x\<^sup>\)\<^sup>\ \ (y ; x\<^sup>\)\<^sup>\" by (metis circ_simulate_right_plus_1 mult_left_one mult_right_one) thus ?thesis by (metis antisym circ_back_loop_fixpoint circ_isotone mult_right_subdist_add_right) qed lemma circ_separate_unfold: "(y ; x\<^sup>\)\<^sup>\ = y\<^sup>\ + y\<^sup>\ ; y ; x ; x\<^sup>\ ; (y ; x\<^sup>\)\<^sup>\" by (smt add_commutative circ_add circ_left_unfold circ_loop_fixpoint mult_associative mult_left_dist_add mult_right_one) lemma separation: "y ; x \ x ; y\<^sup>\ \ (x + y)\<^sup>\ = x\<^sup>\ ; y\<^sup>\" proof - have "y ; x \ x ; y\<^sup>\ \ y\<^sup>\ ; x ; y\<^sup>\ \ x ; y\<^sup>\ + y\<^sup>\ ; 0" by (smt circ_simulate_left_plus_1 circ_transitive_equal mult_associative mult_left_isotone mult_left_zero mult_right_dist_add) thus ?thesis by (smt add_commutative circ_add_1 circ_simulate_right circ_sub_dist_3 less_eq_def mult_associative mult_left_zero zero_right_mult_decreasing) qed lemma circ_simulate_4: "y ; x \ x ; x\<^sup>\ ; (1 + y) \ y\<^sup>\ ; x\<^sup>\ \ x\<^sup>\ ; y\<^sup>\" proof - have "y ; x \ x ; x\<^sup>\ ; (1 + y) \ (1 + y) ; x \ x ; x\<^sup>\ ; (1 + y)" by (smt add_associative add_commutative add_left_upper_bound circ_back_loop_fixpoint less_eq_def mult_left_dist_add mult_left_one mult_right_dist_add mult_right_one) thus ?thesis by (smt add_least_upper_bound circ_increasing circ_reflexive circ_simulate_2 circ_simulate_right_plus_1 mult_right_isotone mult_right_subdist_add_right order_trans) qed lemma circ_simulate_5: "y ; x \ x ; x\<^sup>\ ; (x + y) \ y\<^sup>\ ; x\<^sup>\ \ x\<^sup>\ ; y\<^sup>\" by (metis circ_add_sub_add_one circ_simulate_4 order_trans) lemma circ_simulate_6: "y ; x \ x ; (x + y) \ y\<^sup>\ ; x\<^sup>\ \ x\<^sup>\ ; y\<^sup>\" by (metis add_commutative circ_back_loop_fixpoint circ_simulate_5 mult_right_subdist_add_left order_trans) lemma circ_separate_4: "y ; x \ x ; x\<^sup>\ ; (1 + y) \ (x + y)\<^sup>\ = x\<^sup>\ ; y\<^sup>\" proof assume 1: "y ; x \ x ; x\<^sup>\ ; (1 + y)" hence "y ; x ; x\<^sup>\ \ x ; x\<^sup>\ + x ; x\<^sup>\ ; y ; x\<^sup>\" by (smt circ_transitive_equal less_eq_def mult_associative mult_left_dist_add mult_right_dist_add mult_right_one) also have "... \ x ; x\<^sup>\ + x ; x\<^sup>\ ; x\<^sup>\ ; y\<^sup>\" using 1 by (metis add_right_isotone circ_simulate_2 circ_simulate_4 mult_associative mult_right_isotone) finally have "y ; x ; x\<^sup>\ \ x ; x\<^sup>\ ; y\<^sup>\" by (metis circ_reflexive circ_transitive_equal less_eq_def mult_associative mult_right_isotone mult_right_one) hence "y\<^sup>\ ; (y\<^sup>\ ; x)\<^sup>\ \ x\<^sup>\ ; (y\<^sup>\ + y\<^sup>\ ; 0 ; (y\<^sup>\ ; x)\<^sup>\)" by (smt add_right_upper_bound circ_back_loop_fixpoint circ_simulate_left_plus_1 circ_simulate_right_plus circ_transitive_equal mult_associative order_trans) thus "(x + y)\<^sup>\ = x\<^sup>\ ; y\<^sup>\" by (smt add_commutative antisym circ_add_1 circ_slide circ_sub_dist_3 circ_transitive_equal less_eq_def mult_associative mult_left_zero mult_right_subdist_add_right zero_right_mult_decreasing) qed lemma circ_separate_5: "y ; x \ x ; x\<^sup>\ ; (x + y) \ (x + y)\<^sup>\ = x\<^sup>\ ; y\<^sup>\" by (metis circ_add_sub_add_one circ_separate_4 order_trans) lemma circ_separate_6: "y ; x \ x ; (x + y) \ (x + y)\<^sup>\ = x\<^sup>\ ; y\<^sup>\" by (metis add_commutative circ_back_loop_fixpoint circ_separate_5 mult_right_subdist_add_left order_trans) end class itering_T = semiring_T + itering_3 begin lemma circ_top: "T\<^sup>\ = T" by (metis add_right_top antisym circ_left_unfold mult_left_subdist_add_left mult_right_one top_greatest) lemma circ_right_top: "x\<^sup>\ ; T = T" by (metis add_right_top circ_loop_fixpoint) lemma circ_left_top: "T ; x\<^sup>\ = T" by (metis add_right_top circ_add circ_right_top circ_top) lemma mult_top_circ: "(x ; T)\<^sup>\ = 1 + x ; T" by (metis circ_left_top circ_mult mult_associative) (* lemma "1 = (x ; 0)\<^sup>\" nitpick lemma "1 + x ; 0 = x\<^sup>\" nitpick lemma "x = x ; x\<^sup>\" nitpick lemma "x ; x\<^sup>\ = x\<^sup>\" nitpick lemma "x\<^sup>\ = x\<^sup>\ ; 1\<^sup>\" nitpick lemma "x\<^sup>\ ; y\<^sup>\ = (x + y)\<^sup>\" nitpick [card = 6, timeout = 120] lemma "(x + y)\<^sup>\ = (x\<^sup>\ ; y\<^sup>\)\<^sup>\" nitpick lemma "z + y ; x = x \ y\<^sup>\ ; z \ x" nitpick lemma "y ; x = x \ y\<^sup>\ ; x \ x" nitpick lemma "z + x ; y = x \ z ; y\<^sup>\ \ x" nitpick lemma "x ; y = x \ x ; y\<^sup>\ \ x" nitpick lemma "x = z + y ; x \ x \ y\<^sup>\ ; z" nitpick lemma "x = y ; x \ x \ y\<^sup>\" nitpick lemma "x ; z = z ; y \ x\<^sup>\ ; z \ z ; y\<^sup>\" nitpick -- can the following be proved? lemma "x\<^sup>\ = (x ; x)\<^sup>\ ; (x + 1)" lemma "y\<^sup>\ ; x\<^sup>\ \ x\<^sup>\ ; y\<^sup>\ \ (x + y)\<^sup>\ = x\<^sup>\ ; y\<^sup>\" lemma "y ; x \ (1 + x) ; y\<^sup>\ \ (x + y)\<^sup>\ = x\<^sup>\ ; y\<^sup>\" lemma "y ; x \ x \ y\<^sup>\ ; x \ 1\<^sup>\ ; x" *) end class itering_L = itering_3 + fixes L :: "'a" assumes L_def: "L = 1\<^sup>\ ; 0" begin lemma one_circ_split: "1\<^sup>\ = L + 1" by (metis L_def add_commutative antisym circ_add_upper_bound circ_reflexive circ_simulate_absorb mult_right_one order_refl zero_right_mult_decreasing) lemma one_circ_mult_split: "1\<^sup>\ ; x = L + x" by (metis L_def add_commutative circ_loop_fixpoint mult_associative mult_left_zero mult_zero_circ one_circ_split) lemma one_circ_circ_split: "1\<^sup>\\<^sup>\ = L + 1" by (metis circ_one one_circ_split) lemma one_circ_mult_split_2: "1\<^sup>\ ; x = x ; 1\<^sup>\ + L" by (smt L_def add_associative add_commutative circ_left_unfold less_eq_def mult_left_subdist_add_left mult_right_one one_circ_mult_split sub_mult_one_circ) lemma sub_mult_one_circ_split: "x ; 1\<^sup>\ \ x + L" by (metis add_commutative one_circ_mult_split sub_mult_one_circ) lemma sub_mult_one_circ_split_2: "x ; 1\<^sup>\ \ x + 1\<^sup>\" by (metis L_def add_right_isotone order_trans sub_mult_one_circ_split zero_right_mult_decreasing) lemma L_split: "x ; L \ x ; 0 + L" by (smt L_def mult_associative mult_left_isotone mult_right_dist_add sub_mult_one_circ_split_2) lemma L_left_zero: "L ; x = L" by (metis L_def mult_associative mult_left_zero) lemma one_circ_L: "1\<^sup>\ ; L = L" by (metis add_idempotent one_circ_mult_split) lemma circ_circ_split: "x\<^sup>\\<^sup>\ = L + x\<^sup>\" by (metis circ_circ_mult one_circ_mult_split) lemma circ_left_induct_mult_L: "L \ x \ x ; y \ x \ x ; y\<^sup>\ \ x" by (metis circ_one circ_simulate less_eq_def one_circ_mult_split) lemma circ_left_induct_mult_iff_L: "L \ x \ x ; y \ x \ x ; y\<^sup>\ \ x" by (smt add_least_upper_bound circ_back_loop_fixpoint circ_left_induct_mult_L less_eq_def) lemma circ_left_induct_L: "L \ x \ x ; y + z \ x \ z ; y\<^sup>\ \ x" by (metis add_least_upper_bound circ_left_induct_mult_L less_eq_def mult_right_dist_add) lemma mult_L_circ: "(x ; L)\<^sup>\ = 1 + x ; L" by (metis L_left_zero circ_mult mult_associative) lemma mult_L_circ_mult: "(x ; L)\<^sup>\ ; y = y + x ; L" by (metis L_left_zero mult_L_circ mult_associative mult_left_one mult_right_dist_add) lemma circ_L: "L\<^sup>\ = L + 1" by (metis L_left_zero add_commutative circ_left_unfold) lemma L_below_one_circ: "L \ 1\<^sup>\" by (metis add_left_upper_bound one_circ_split) lemma circ_add_6: "L + (x + y)\<^sup>\ = (x\<^sup>\ ; y\<^sup>\)\<^sup>\" by (metis add_associative add_commutative circ_add_1 circ_circ_add circ_circ_split circ_decompose_4) end (* end theory While imports Iteration Tests begin *) class while = itering_1 + tests begin lemma wnf_lemma_5: "(-p + -q) ; (-q ; x + --q ; y) = -q ; x + --q ; -p ; y" by (smt mult_absorb mult_associative mult_compl_intro mult_idempotent mult_left_dist_add plus_def sub_comm) lemma test_case_split_left_equal: "-z ; x = -z ; y \ --z ; x = --z ; y \ x = y" by (metis case_split_left_equal plus_compl) lemma preserves_equation: "-y ; x \ x ; -y \ -y ; x = -y ; x ; -y" by (smt antisym mult_associative mult_left_isotone mult_left_one mult_right_isotone mult_right_one mult_idempotent one_greatest) lemma preserve_test: "-y ; x \ x ; -y \ -y ; x\<^sup>\ = -y ; x\<^sup>\ ; -y" by (metis circ_simulate preserves_equation) lemma import_test: "-y ; x \ x ; -y \ -y ; x\<^sup>\ = -y ; (-y ; x)\<^sup>\" by (rule, rule antisym, metis circ_simulate circ_slide mult_associative mult_idempotent preserves_equation, metis circ_isotone mult_left_isotone mult_left_one mult_right_isotone one_greatest) definition ite :: "'a \ 'a \ 'a \ 'a" ("_ \ _ \ _" [58,58,58] 57) where "x \ p \ y = p ; x + -p ; y" definition it :: "'a \ 'a \ 'a" ("_ \ _" [58,58] 57) where "p \ x = p ; x + -p" definition while :: "'a \ 'a \ 'a" (infixr "\" 59) where "p \ y = (p ; y)\<^sup>\ ; -p" definition assigns :: "'a \ 'a \ 'a \ bool" where "assigns x p q \ x = x ; (p ; q + -p ; -q)" definition preserves :: "'a \ 'a \ bool" where "preserves x p \ p ; x \ x ; p \ -p ; x \ x ; -p" lemma ite_neg: "x \ -p \ y = y \ --p \ x" by (metis add_commutative double_negation ite_def) lemma ite_import_true: "x \ -p \ y = -p ; x \ -p \ y" by (metis ite_def mult_associative mult_idempotent) lemma ite_import_false: "x \ -p \ y = x \ -p \ --p ; y" by (metis ite_def mult_associative mult_idempotent) lemma ite_import_true_false: "x \ -p \ y = -p ; x \ -p \ --p ; y" by (metis ite_import_false ite_import_true) lemma ite_context_true: "-p ; (x \ -p \ y) = -p ; x" by (metis add_right_zero ite_def mult_associative mult_compl mult_idempotent mult_left_dist_add mult_left_zero) lemma ite_context_false: "--p ; (x \ -p \ y) = --p ; y" by (metis ite_neg ite_context_true) lemma ite_context_import: "-p ; (x \ -q \ y) = -p ; (x \ -p ; -q \ y)" by (smt ite_def mult_associative mult_compl_intro mult_deMorgan mult_idempotent mult_left_dist_add) lemma ite_conjunction: "(x \ -q \ y) \ -p \ y = x \ -p ; -q \ y" by (smt add_associative add_commutative ite_def mult_associative mult_deMorgan mult_left_dist_add mult_right_dist_add plus_compl_intro) lemma ite_disjunction: "x \ -p \ (x \ -q \ y) = x \ -p + -q \ y" by (smt add_associative double_negation ite_def mult_associative mult_compl_intro mult_deMorgan mult_left_dist_add mult_right_dist_add plus_deMorgan) lemma wnf_lemma_6: "(-p + -q) ; (x \ --p ; -q \ y) = (-p + -q) ; (y \ -p \ x)" by (smt add_commutative double_negation ite_def mult_associative mult_compl mult_deMorgan mult_idempotent mult_left_dist_add plus_compl_intro sub_comm) lemma it_ite: "-p \ x = x \ -p \ 1" by (metis it_def ite_def mult_right_one) lemma it_neg: "--p \ x = 1 \ -p \ x" by (metis it_ite ite_neg) lemma it_import_true: "-p \ x = -p \ -p ; x" by (metis it_ite ite_import_true) lemma it_context_true: "-p ; (-p \ x) = -p ; x" by (metis it_ite ite_context_true) lemma it_context_false: "--p ; (-p \ x) = --p" by (metis it_ite ite_context_false mult_right_one) lemma while_unfold_it: "-p \ x = -p \ x ; (-p \ x)" by (metis circ_loop_fixpoint it_def mult_associative while_def) lemma while_context_false: "--p ; (-p \ x) = --p" by (metis it_context_false while_unfold_it) lemma while_context_true: "-p ; (-p \ x) = -p ; x ; (-p \ x)" by (metis it_context_true mult_associative while_unfold_it) lemma while_zero: "0 \ x = 1" by (metis circ_zero mult_left_one mult_left_zero one_def while_def) lemma wnf_lemma_7: "1 ; (0 \ 1) = 1" by (metis mult_left_one while_zero) lemma while_import_condition: "-p \ x = -p \ -p ; x" by (metis mult_associative mult_idempotent while_def) lemma while_import_condition_2: "-p ; -q \ x = -p ; -q \ -p ; x" by (metis mult_associative mult_idempotent sub_comm while_def) lemma wnf_lemma_8: "-r ; (-p + --p ; -q) \ (x \ --p ; -q \ y) = -r ; (-p + -q) \ (y \ -p \ x)" by (metis add_commutative double_negation mult_associative plus_compl_intro while_def wnf_lemma_6) lemma split_merge_loops: "--p ; y \ y ; --p \ -p + -q \ (x \ -p \ y) = (-p \ x) ; (-q \ y)" proof - have "-p + -q \ (x \ -p \ y) = (-p ; x + --p ; -q ; y)\<^sup>\ ; --p ; --q" by (smt ite_def mult_associative plus_comm plus_deMorgan while_def wnf_lemma_5) thus ?thesis by (smt circ_add_1 circ_slide import_test mult_associative preserves_equation sub_comm while_context_false while_def) qed (* Theorem 31 on page 329 of Back & von Wright, Acta Informatica 36:295-334, 1999 *) lemma assigns_same: "assigns x (-p) (-p)" by (metis assigns_def mult_idempotent mult_right_one plus_compl) lemma preserves_equation_test: "preserves x (-p) \ -p ; x = -p ; x ; -p \ --p ; x = --p ; x ; --p" by (metis preserves_equation preserves_def) lemma preserves_test: "preserves (-q) (-p)" by (metis order_refl preserves_def sub_comm) lemma preserves_zero: "preserves 0 (-p)" by (metis one_compl preserves_test) lemma preserves_one: "preserves 1 (-p)" by (metis one_def preserves_test) lemma preserves_add: "preserves x (-p) \ preserves y (-p) \ preserves (x + y) (-p)" by (smt mult_left_dist_add mult_right_dist_add preserves_equation_test) lemma preserves_mult: "preserves x (-p) \ preserves y (-p) \ preserves (x ; y) (-p)" by (smt mult_associative preserves_equation_test) lemma preserves_ite: "preserves x (-p) \ preserves y (-p) \ preserves (x \ -q \ y) (-p)" by (metis ite_def preserves_add preserves_mult preserves_test) lemma preserves_it: "preserves x (-p) \ preserves (-q \ x) (-p)" by (metis it_def preserves_add preserves_mult preserves_test) lemma preserves_circ: "preserves x (-p) \ preserves (x\<^sup>\) (-p)" by (metis circ_simulate preserves_def) lemma preserves_while: "preserves x (-p) \ preserves (-q \ x) (-p)" by (metis preserves_circ preserves_mult preserves_test while_def) lemma preserves_test_neg: "preserves x (-p) \ preserves x (--p)" by (metis double_negation preserves_def) lemma preserves_import_circ: "preserves x (-p) \ -p ; x\<^sup>\ = -p ; (-p ; x)\<^sup>\" by (metis import_test preserves_def) lemma preserves_simulate: "preserves x (-p) \ -p ; x\<^sup>\ = -p ; x\<^sup>\ ; -p" by (metis preserves_circ preserves_equation_test) lemma preserves_import_ite: "preserves z (-p) \ z ; (x \ -p \ y) = z ; x \ -p \ z ; y" proof - have 1: "preserves z (-p) \ -p ; z ; (x \ -p \ y) = -p ; (z ; x \ -p \ z ; y)" by (metis add_right_zero ite_def mult_associative mult_compl mult_idempotent mult_left_dist_add mult_left_zero preserves_equation_test) have "preserves z (-p) \ --p ; z ; (x \ -p \ y) = --p ; (z ; x \ -p \ z ; y)" by (smt add_left_zero ite_def mult_associative mult_compl mult_idempotent mult_left_dist_add mult_left_zero preserves_equation_test sub_comm) thus ?thesis using 1 by (metis test_case_split_left_equal mult_associative) qed lemma preserves_while_context: "preserves x (-p) \ -p ; (-q \ x) = -p ; (-p ; -q \ x)" by (smt mult_associative mult_compl_intro mult_deMorgan preserves_import_circ preserves_mult preserves_simulate preserves_test while_def) lemma while_ite_context_false: "preserves y (-p) \ --p ; (-p + -q \ (x \ -p \ y)) = --p ; (-q \ y)" proof - have "preserves y (-p) \ --p ; (-p + -q \ (x \ -p \ y)) = --p ; (--p ; -q ; y)\<^sup>\ ; -(-p + -q)" by (smt import_test double_negation ite_context_false mult_associative mult_compl_intro plus_def preserves_equation preserves_equation_test sub_comm while_def) thus ?thesis by (smt import_test circ_simulate mult_associative plus_deMorgan preserves_def preserves_equation preserves_test while_def) qed lemma while_ite_norm: "assigns z (-p) (-q) \ preserves x1 (-q) \ preserves x2 (-q) \ preserves y1 (-q) \ preserves y2 (-q) \ z ; (x1 ; (-r1 \ y1) \ -p \ x2 ; (-r2 \ y2)) = z ; (x1 \ -q \ x2) ; ((-q ; -r1 + --q ; -r2) \ (y1 \ -q \ y2))" proof assume 1: "assigns z (-p) (-q) \ preserves x1 (-q) \ preserves x2 (-q) \ preserves y1 (-q) \ preserves y2 (-q)" have 2: "(-p ; -q + --p ; --q) ; (x1 \ -q \ x2) = -p ; -q ; x1 + --p ; --q ; x2" by (smt ite_def mult_associative mult_left_dist_add wnf_lemma_2 wnf_lemma_4) have 3: "(-q ; -r1 + --q ; -r2) ; (y1 \ -q \ y2) = -q ; -r1 ; y1 + --q ; -r2 ; y2" by (smt ite_def mult_associative mult_idempotent mult_left_dist_add wnf_lemma_1 wnf_lemma_3) have 4: "-(-q ; -r1 + --q ; -r2) = -q ; --r1 + --q ; --r2" by (smt mult_absorb mult_idempotent mult_right_dist_add plus_compl_intro plus_deMorgan plus_def sub_comm) have "-p ; -q ; x1 ; (-q ; -r1 ; y1 + --q ; -r2 ; y2)\<^sup>\ ; (-q ; --r1 + --q ; --r2) = -p ; -q ; x1 ; -q ; (-q ; (-q ; -r1 ; y1 + --q ; -r2 ; y2))\<^sup>\ ; (-q ; --r1 + --q ; --r2)" using 1 by (smt mult_associative preserves_add preserves_equation_test preserves_import_circ preserves_mult preserves_test) also have "... = -p ; -q ; x1 ; -q ; (-q ; -r1 ; y1)\<^sup>\ ; (-q ; --r1 + --q ; --r2)" by (smt add_commutative add_left_zero mult_associative mult_compl mult_idempotent mult_left_dist_add mult_left_zero) finally have 5: "-p ; -q ; x1 ; (-q ; -r1 ; y1 + --q ; -r2 ; y2)\<^sup>\ ; (-q ; --r1 + --q ; --r2) = -p ; -q ; x1 ; (-r1 ; y1)\<^sup>\ ; --r1" using 1 by (smt ite_context_true ite_def mult_associative preserves_equation_test preserves_import_circ preserves_mult preserves_simulate preserves_test) have "--p ; --q ; x2 ; (-q ; -r1 ; y1 + --q ; -r2 ; y2)\<^sup>\ ; (-q ; --r1 + --q ; --r2) = --p ; --q ; x2 ; --q ; (--q ; (-q ; -r1 ; y1 + --q ; -r2 ; y2))\<^sup>\ ; (-q ; --r1 + --q ; --r2)" using 1 by (smt mult_associative preserves_add preserves_equation_test preserves_import_circ preserves_mult preserves_test preserves_test_neg) also have "... = --p ; --q ; x2 ; --q ; (--q ; -r2 ; y2)\<^sup>\ ; (-q ; --r1 + --q ; --r2)" by (smt add_commutative add_right_zero mult_associative mult_compl mult_idempotent mult_left_dist_add mult_left_zero sub_comm) finally have "--p ; --q ; x2 ; (-q ; -r1 ; y1 + --q ; -r2 ; y2)\<^sup>\ ; (-q ; --r1 + --q ; --r2) = --p ; --q ; x2 ; (-r2 ; y2)\<^sup>\ ; --r2" using 1 by (smt ite_context_false ite_def mult_associative preserves_equation_test preserves_import_circ preserves_mult preserves_simulate preserves_test preserves_test_neg) thus "z ; (x1 ; (-r1 \ y1) \ -p \ x2 ; (-r2 \ y2)) = z ; (x1 \ -q \ x2) ; ((-q ; -r1 + --q ; -r2) \ (y1 \ -q \ y2))" using 1 2 3 4 5 by (smt assigns_def ite_def mult_associative mult_left_dist_add mult_right_dist_add wnf_lemma_1 wnf_lemma_3 while_def) qed lemma while_it_norm: "assigns z (-p) (-q) \ preserves x (-q) \ preserves y (-q) \ z ; (-p \ x ; (-r \ y)) = z ; (-q \ x) ; (-q ; -r \ y)" by (metis add_right_zero bs_mult_right_zero it_context_true it_ite one_compl preserves_one while_import_condition_2 while_ite_norm wnf_lemma_7) lemma while_else_norm: "assigns z (-p) (-q) \ preserves x (-q) \ preserves y (-q) \ z ; (1 \ -p \ x ; (-r \ y)) = z ; (1 \ -q \ x) ; (--q ; -r \ y)" by (metis add_left_zero bs_mult_right_zero ite_context_false one_compl preserves_one while_import_condition_2 while_ite_norm wnf_lemma_7) lemma while_while_pre_norm: "-p \ x ; (-q \ y) = -p \ x ; (-p + -q \ (y \ -q \ x))" by (smt add_commutative circ_add_1 circ_left_unfold circ_slide it_def ite_def mult_associative mult_left_one mult_right_dist_add plus_deMorgan while_def wnf_lemma_5) lemma while_while_norm: "assigns z (-p) (-r) \ preserves x (-r) \ preserves y (-r) \ z ; (-p \ x ; (-q \ y)) = z ; (-r \ x) ; (-r ; (-p + -q) \ (y \ -q \ x))" by (smt double_negation mult_deMorgan plus_deMorgan preserves_ite while_it_norm while_while_pre_norm) lemma while_seq_replace: "assigns z (-p) (-q) \ z ; (-p \ x ; z) ; y = z ; (-q \ x ; z) ; y" by (smt assigns_def circ_slide mult_associative wnf_lemma_1 wnf_lemma_2 wnf_lemma_3 wnf_lemma_4 while_def) lemma while_ite_replace: "assigns z (-p) (-q) \ z ; (x \ -p \ y) = z ; (x \ -q \ y)" by (smt assigns_def ite_def mult_associative mult_left_dist_add sub_comm wnf_lemma_1 wnf_lemma_3) lemma while_post_norm_an: "preserves y (-p) \ (-p \ x) ; y = y \ --p \ (-p \ x ; (--p \ y))" proof assume 1: "preserves y (-p)" have "-p ; (-p ; x ; (--p ; y + -p))\<^sup>\ ; --p = -p ; x ; ((--p ; y + -p) ; -p ; x)\<^sup>\ ; (--p ; y + -p) ; --p" by (smt add_left_zero circ_left_unfold circ_slide mult_associative mult_compl mult_idempotent mult_left_dist_add mult_right_dist_add mult_right_one) also have "... = -p ; x ; (--p ; y ; 0 + -p ; x)\<^sup>\ ; --p ; y" using 1 by (smt add_right_zero mult_associative mult_compl mult_idempotent mult_left_zero mult_right_dist_add preserves_equation_test sub_comm) finally have "-p ; (-p ; x ; (--p ; y + -p))\<^sup>\ ; --p = -p ; x ; (-p ; x)\<^sup>\ ; --p ; y" by (smt add_commutative circ_slide circ_zero mult_associative mult_left_zero mult_right_one mult_zero_add_circ) thus "(-p \ x) ; y = y \ --p \ (-p \ x ; (--p \ y))" by (smt circ_left_unfold double_negation it_def ite_def mult_associative mult_left_one mult_right_dist_add while_def) qed lemma while_post_norm: "preserves y (-p) \ (-p \ x) ; y = -p \ x ; (1 \ -p \ y) \ -p \ y" by (metis it_neg ite_neg while_post_norm_an) lemma wnf_lemma_9: "assigns z (-p) (-q) \ preserves x1 (-q) \ preserves y1 (-q) \ preserves x2 (-q) \ preserves y2 (-q) \ preserves x2 (-p) \ preserves y2 (-p) \ z ; (x1 \ -q \ x2) ; (-q ; -p + -r \ (y1 \ -q ; -p \ y2)) = z ; (x1 \ -p \ x2) ; (-p + -r \ (y1 \ -p \ y2))" proof assume 1: "assigns z (-p) (-q) \ preserves x1 (-q) \ preserves y1 (-q) \ preserves x2 (-q) \ preserves y2 (-q) \ preserves x2 (-p) \ preserves y2 (-p)" hence "z ; --p ; --q ; (x1 \ -q \ x2) ; (-q ; -p + -r \ (y1 \ -q ; -p \ y2)) = z ; --p ; --q ; x2 ; --q ; (--q ; (-q ; -p + -r) \ (y1 \ -q ; -p \ y2))" by (smt double_negation ite_context_false mult_associative mult_deMorgan plus_deMorgan preserves_equation_test preserves_ite preserves_while_context) also have "... = z ; --p ; --q ; x2 ; --q ; (--q ; -r \ --q ; y2)" by (smt add_left_zero double_negation ite_conjunction ite_context_false mult_associative mult_compl mult_left_dist_add mult_left_zero while_import_condition_2) also have "... = z ; --p ; --q ; x2 ; (-r \ y2)" using 1 by (smt mult_associative preserves_equation_test preserves_test_neg preserves_while_context while_import_condition_2) finally have 2: "z ; --p ; --q ; (x1 \ -q \ x2) ; (-q ; -p + -r \ (y1 \ -q ; -p \ y2)) = z ; --p ; --q ; (x1 \ -q \ x2) ; (-p + -r \ (y1 \ -p \ y2))" using 1 by (smt ite_context_false mult_associative preserves_equation_test sub_comm while_ite_context_false) have "z ; -p ; -q ; (x1 \ -q \ x2) ; (-q ; -p + -r \ (y1 \ -q ; -p \ y2)) = z ; -p ; -q ; (x1 \ -q \ x2) ; -q ; (-q ; (-p + -r) \ -q ; (y1 \ -p \ y2))" using 1 by (smt double_negation ite_context_import mult_associative mult_deMorgan mult_idempotent mult_left_dist_add plus_deMorgan preserves_equation_test preserves_ite preserves_while_context while_import_condition_2) hence "z ; -p ; -q ; (x1 \ -q \ x2) ; (-q ; -p + -r \ (y1 \ -q ; -p \ y2)) = z ; -p ; -q ; (x1 \ -q \ x2) ; (-p + -r \ (y1 \ -p \ y2))" using 1 by (smt double_negation mult_associative mult_deMorgan mult_idempotent preserves_equation_test preserves_ite preserves_while_context while_import_condition_2) thus "z ; (x1 \ -q \ x2) ; (-q ; -p + -r \ (y1 \ -q ; -p \ y2)) = z ; (x1 \ -p \ x2) ; (-p + -r \ (y1 \ -p \ y2))" using 1 2 by (smt assigns_def mult_associative mult_left_dist_add mult_right_dist_add while_ite_replace) qed lemma while_seq_norm: "assigns z1 (-r1) (-q) \ preserves x2 (-q) \ preserves y2 (-q) \ preserves z2 (-q) \ z1 ; z2 = z2 ; z1 \ assigns z2 (-q) (-r) \ preserves y1 (-r) \ preserves z1 (-r) \ preserves x2 (-r) \ preserves y2 (-r) \ x1 ; z1 ; z2 ; (-r1 \ y1 ; z1) ; x2 ; (-r2 \ y2) = x1 ; z1 ; z2 ; (y1 ; z1 ; (1 \ -q \ x2) \ -q \ x2) ; (-q + -r2 \ (y1 ; z1 ; (1 \ -q \ x2) \ -q \ y2))" proof assume 1: "assigns z1 (-r1) (-q) \ preserves x2 (-q) \ preserves y2 (-q) \ preserves z2 (-q) \ z1 ; z2 = z2 ; z1 \ assigns z2 (-q) (-r) \ preserves y1 (-r) \ preserves z1 (-r) \ preserves x2 (-r) \ preserves y2 (-r)" have "x1 ; z1 ; z2 ; (-r1 \ y1 ; z1) ; x2 ; (-r2 \ y2) = x1 ; z1 ; z2 ; (-q \ y1 ; z1) ; x2 ; (-r2 \ y2)" using 1 by (smt mult_associative while_seq_replace) also have "... = x1 ; z1 ; z2 ; (-q \ y1 ; z1 ; (1 \ -q \ x2 ; (-r2 \ y2)) \ -q \ x2 ; (-r2 \ y2))" using 1 by (smt mult_associative preserves_mult preserves_while while_post_norm) also have "... = x1 ; z1 ; (z2 ; (-q \ y1 ; z1 ; (1 \ -q \ x2) ; (--q ; -r2 \ y2)) \ -q \ z2 ; x2 ; (-r2 \ y2))" using 1 by (smt assigns_same mult_associative preserves_import_ite while_else_norm) also have "... = x1 ; z1 ; (z2 ; (-r \ y1 ; z1 ; (1 \ -q \ x2)) ; (-r ; (-q + -r2) \ (y1 ; z1 ; (1 \ -q \ x2) \ -q \ y2)) \ -q \ z2 ; x2 ; (-r2 \ y2))" using 1 by (smt double_negation mult_deMorgan plus_deMorgan preserves_ite preserves_mult preserves_one while_while_norm wnf_lemma_8) also have "... = x1 ; z1 ; z2 ; ((-r \ y1 ; z1 ; (1 \ -q \ x2)) ; (-r ; (-q + -r2) \ (y1 ; z1 ; (1 \ -q \ x2) \ -q \ y2)) \ -r \ x2 ; (-r2 \ y2))" using 1 by (smt mult_associative preserves_import_ite while_ite_replace) also have "... = x1 ; z1 ; z2 ; (-r ; y1 ; z1 ; (1 \ -q \ x2) ; -r ; (-q + -r2 \ (y1 ; z1 ; (1 \ -q \ x2) \ -q \ y2)) \ -r \ x2 ; (-r2 \ y2))" using 1 by (smt double_negation it_context_true ite_import_true mult_associative mult_deMorgan mult_idempotent plus_deMorgan preserves_equation_test preserves_ite preserves_mult preserves_one preserves_while_context) also have "... = x1 ; z1 ; z2 ; (y1 ; z1 ; (1 \ -q \ x2) ; (-q + -r2 \ (y1 ; z1 ; (1 \ -q \ x2) \ -q \ y2)) \ -q \ x2 ; (-r2 \ y2))" using 1 by (smt double_negation ite_import_true mult_associative mult_idempotent preserves_equation_test preserves_ite preserves_one while_ite_replace) also have "... = x1 ; z1 ; z2 ; (y1 ; z1 ; (1 \ -q \ x2) \ -r \ x2) ; ((-r ; (-q + -r2) + --r ; -r2) \ ((y1 ; z1 ; (1 \ -q \ x2) \ -q \ y2) \ -r \ y2))" using 1 by (smt double_negation mult_associative mult_deMorgan plus_deMorgan preserves_ite preserves_mult preserves_one while_ite_norm) also have "... = x1 ; z1 ; z2 ; (y1 ; z1 ; (1 \ -q \ x2) \ -q \ x2) ; (-q + -r2 \ (y1 ; z1 ; (1 \ -q \ x2) \ -q \ y2))" using 1 by (smt add_associative ite_conjunction mult_associative mult_left_dist_add mult_left_one mult_right_dist_add plus_compl preserves_ite preserves_mult preserves_one wnf_lemma_9) finally show "x1 ; z1 ; z2 ; (-r1 \ y1 ; z1) ; x2 ; (-r2 \ y2) = x1 ; z1 ; z2 ; (y1 ; z1 ; (1 \ -q \ x2) \ -q \ x2) ; (-q + -r2 \ (y1 ; z1 ; (1 \ -q \ x2) \ -q \ y2))" . qed end (* end theory Omega imports Iteration begin *) class kleene_algebra = semiring + fixes star :: "'a \ 'a" ("_\<^sup>\" [100] 100) assumes star_left_unfold : "1 + y ; y\<^sup>\ \ y\<^sup>\" assumes star_left_induct : "z + y ; x \ x \ y\<^sup>\ ; z \ x" assumes star_right_induct: "z + x ; y \ x \ z ; y\<^sup>\ \ x" begin lemma star_left_unfold_equal: "1 + x ; x\<^sup>\ = x\<^sup>\" by (smt add_least_upper_bound antisym_conv mult_right_isotone mult_right_one order_refl order_trans star_left_induct star_left_unfold) lemma star_unfold_slide: "(x ; y)\<^sup>\ = 1 + x ; (y ; x)\<^sup>\ ; y" by (smt antisym mult_associative mult_left_dist_add mult_left_one mult_right_dist_add mult_right_isotone mult_right_one order_refl star_left_induct star_left_unfold_equal) lemma star_decompose: "(x + y)\<^sup>\ = (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" apply (rule antisym) apply (smt add_least_upper_bound add_left_upper_bound add_right_upper_bound mult_associative mult_left_dist_add mult_left_one mult_right_dist_add mult_right_one star_left_induct star_left_unfold_equal) by (smt add_least_upper_bound less_eq_def mult_left_subdist_add_left mult_right_one star_left_induct star_left_unfold star_right_induct) lemma star_simulation_right: "z ; x \ y ; z \ z ; x\<^sup>\ \ y\<^sup>\ ; z" by (smt add_least_upper_bound less_eq_def mult_associative mult_left_dist_add mult_left_one mult_right_subdist_add_left star_left_induct star_left_unfold star_right_induct) end sublocale kleene_algebra < star!: itering_1 where circ = star by (unfold_locales, metis star_unfold_slide, metis star_decompose, metis star_simulation_right) context kleene_algebra begin text {* Most lemmas in this class are taken from Georg Struth's theories. *} lemma star_sub_one: "x \ 1 \ x\<^sup>\ = 1" by (metis add_least_upper_bound eq_iff mult_left_one star.circ_reflexive star_right_induct) lemma star_one: "1\<^sup>\ = 1" by (metis eq_iff star_sub_one) lemma star_left_induct_mult: "x ; y \ y \ x\<^sup>\ ; y \ y" by (metis add_commutative less_eq_def order_refl star_left_induct) lemma star_left_induct_mult_iff: "x ; y \ y \ x\<^sup>\ ; y \ y" by (smt mult_associative mult_left_isotone mult_left_one mult_right_isotone order_trans star_left_induct_mult star.circ_reflexive star.left_plus_below_circ) lemma star_involutive: "x\<^sup>\ = x\<^sup>\\<^sup>\" by (smt antisym less_eq_def mult_left_subdist_add_left mult_right_one star_left_induct star.circ_plus_one star.left_plus_below_circ star.circ_transitive_equal) lemma star_sup_one: "(1 + x)\<^sup>\ = x\<^sup>\" by (smt add_commutative less_eq_def mult_left_dist_add mult_left_one mult_right_dist_add mult_right_one star_involutive star.circ_plus_one star.circ_sub_dist star.left_plus_below_circ) lemma star_left_induct_equal: "z + x ; y = y \ x\<^sup>\ ; z \ y" by (metis order_refl star_left_induct) lemma star_left_induct_mult_equal: "x ; y = y \ x\<^sup>\ ; y \ y" by (metis order_refl star_left_induct_mult) lemma star_star_upper_bound: "x\<^sup>\ \ z\<^sup>\ \ x\<^sup>\\<^sup>\ \ z\<^sup>\" by (metis star_involutive) lemma star_simulation_left: "x ; z \ z ; y \ x\<^sup>\ ; z \ z ; y\<^sup>\" by (smt add_commutative add_least_upper_bound mult_right_dist_add less_eq_def mult_associative mult_right_one star.left_plus_below_circ star.circ_increasing star_left_induct star_involutive star.circ_isotone star.circ_reflexive mult_left_subdist_add_left) lemma quasicomm_1: "y ; x \ x ; (x + y)\<^sup>\ \ y\<^sup>\ ; x \ x ; (x + y)\<^sup>\" by (smt mult_isotone order_refl order_trans star.circ_increasing star_involutive star_simulation_left) lemma star_rtc_3: "1 + x + y ; y = y \ x\<^sup>\ \ y" by (metis add_least_upper_bound less_eq_def mult_left_subdist_add_left mult_right_one star_left_induct_mult_iff star.circ_sub_dist) lemma star_decompose_1: "(x + y)\<^sup>\ = (x\<^sup>\ ; y\<^sup>\)\<^sup>\" by (smt add_least_upper_bound antisym mult_isotone mult_left_one mult_right_one star.circ_increasing star_involutive star.circ_isotone star.circ_reflexive star.circ_sub_dist_3) lemma star_sum: "(x + y)\<^sup>\ = (x\<^sup>\ + y\<^sup>\)\<^sup>\" by (metis star_decompose_1 star_involutive) lemma star_decompose_3: "(x\<^sup>\ ; y\<^sup>\)\<^sup>\ = x\<^sup>\ ; (y ; x\<^sup>\)\<^sup>\" by (metis star_decompose_1 star.circ_add_1) lemma star_right_induct_mult: "y ; x \ y \ y ; x\<^sup>\ \ y" by (metis add_commutative less_eq_def order_refl star_right_induct) lemma star_right_induct_mult_iff: "y ; x \ y \ y ; x\<^sup>\ \ y" by (metis mult_right_isotone order_trans star.circ_increasing star_right_induct_mult) lemma star_simulation_right_equal: "z ; x = y ; z \ z ; x\<^sup>\ = y\<^sup>\ ; z" by (metis eq_iff star_simulation_left star_simulation_right) lemma star_simulation_star: "x ; y \ y ; x \ x\<^sup>\ ; y\<^sup>\ \ y\<^sup>\ ; x\<^sup>\" by (metis star_simulation_left star_simulation_right) lemma star_right_induct_equal: "z + y ; x = y \ z ; x\<^sup>\ \ y" by (metis order_refl star_right_induct) lemma star_right_induct_mult_equal: "y ; x = y \ y ; x\<^sup>\ \ y" by (metis order_refl star_right_induct_mult) lemma star_loop_least_fixpoint: "y ; x + z = x \ y\<^sup>\ ; z \ x" by (metis add_commutative star_left_induct_equal) lemma star_back_loop_least_fixpoint: "x ; y + z = x \ z ; y\<^sup>\ \ x" by (metis add_commutative star_right_induct_equal) lemma star_loop_is_least_fixpoint: "is_least_fixpoint (\x . y ; x + z) (y\<^sup>\ ; z)" by (smt is_least_fixpoint_def star.circ_loop_fixpoint star_loop_least_fixpoint) lemma star_loop_mu: "\ (\x . y ; x + z) = y\<^sup>\ ; z" by (metis least_fixpoint_same star_loop_is_least_fixpoint) lemma star_back_loop_is_least_fixpoint: "is_least_fixpoint (\x . x ; y + z) (z ; y\<^sup>\)" by (smt is_least_fixpoint_def star.circ_back_loop_fixpoint star_back_loop_least_fixpoint) lemma star_back_loop_mu: "\ (\x . x ; y + z) = z ; y\<^sup>\" by (metis least_fixpoint_same star_back_loop_is_least_fixpoint) lemma star_square: "x\<^sup>\ = (1 + x) ; (x ; x)\<^sup>\" proof - let ?f = "\y . y ; x + 1" have 1: "isotone ?f" by (smt add_left_isotone isotone_def mult_left_isotone) have 2: "?f \ ?f = (\y . y ; (x ; x) + (1 + x))" by (simp add: add_associative add_commutative mult_associative mult_left_one mult_right_dist_add o_def) thus ?thesis using 1 by (metis mu_square mult_left_one star_back_loop_mu has_least_fixpoint_def star_back_loop_is_least_fixpoint) qed lemma star_square_2: "x\<^sup>\ = (x ; x)\<^sup>\ ; (x + 1)" by (smt add_commutative mult_left_dist_add mult_right_dist_add mult_right_one star.circ_decompose_5 star_involutive star_one star.circ_slide star_square) lemma star_circ_simulate_right_plus: "z ; x \ y ; y\<^sup>\ ; z + w \ z ; x\<^sup>\ \ y\<^sup>\ ; (z + w ; x\<^sup>\)" proof assume 1: "z ; x \ y ; y\<^sup>\ ; z + w" have "y\<^sup>\ ; (z + w ; x\<^sup>\) ; x \ y\<^sup>\ ; z ; x + y\<^sup>\ ; w ; x\<^sup>\" by (smt add_left_upper_bound add_right_isotone mult_associative mult_left_dist_add mult_right_dist_add star.circ_back_loop_fixpoint) also have "... \ y\<^sup>\ ; y ; z + y\<^sup>\ ; w + y\<^sup>\ ; w ; x\<^sup>\" using 1 by (smt add_left_isotone less_eq_def mult_associative mult_left_dist_add star.circ_plus_same star.circ_transitive_equal) also have "... \ y\<^sup>\ ; (z + w ; x\<^sup>\)" by (smt add_associative add_idempotent add_left_isotone mult_associative mult_left_dist_add mult_right_one mult_right_subdist_add_right star.circ_plus_one star.circ_plus_same star.circ_transitive_equal star.circ_unfold_sum) finally show "z ; x\<^sup>\ \ y\<^sup>\ ; (z + w ; x\<^sup>\)" by (smt add_least_upper_bound add_right_divisibility star.circ_loop_fixpoint star_right_induct) qed lemma star_circ_simulate_left_plus: "x ; z \ z ; y\<^sup>\ + w \ x\<^sup>\ ; z \ (z + x\<^sup>\ ; w) ; y\<^sup>\" proof assume 1: "x ; z \ z ; y\<^sup>\ + w" have "x ; ((z + x\<^sup>\ ; w) ; y\<^sup>\) \ x ; z ; y\<^sup>\ + x\<^sup>\ ; w ; y\<^sup>\" by (smt add_right_isotone mult_associative mult_left_dist_add mult_right_dist_add mult_right_subdist_add_left star.circ_loop_fixpoint) also have "... \ (z + w + x\<^sup>\ ; w) ; y\<^sup>\" using 1 by (smt add_left_divisibility add_left_isotone mult_associative mult_right_dist_add star.circ_transitive_equal) also have "... = (z + x\<^sup>\ ; w) ; y\<^sup>\" by (metis add_associative add_right_upper_bound less_eq_def star.circ_loop_fixpoint) finally show "x\<^sup>\ ; z \ (z + x\<^sup>\ ; w) ; y\<^sup>\" by (metis add_least_upper_bound mult_left_subdist_add_left mult_right_one star.circ_right_unfold star_left_induct) qed end sublocale kleene_algebra < star!: itering_3 where circ = star apply unfold_locales apply (smt add_associative add_commutative add_left_upper_bound mult_associative mult_left_dist_add order_trans star.circ_loop_fixpoint star_circ_simulate_right_plus) apply (smt add_commutative add_right_isotone mult_right_isotone order_trans star.circ_increasing star_circ_simulate_left_plus) apply (rule star_circ_simulate_right_plus) by (rule star_circ_simulate_left_plus) class kleene_itering = kleene_algebra + itering_3 begin lemma star_below_circ: "x\<^sup>\ \ x\<^sup>\" by (metis circ_right_unfold mult_left_one order_refl star_right_induct) lemma star_zero_below_circ_mult: "x\<^sup>\ ; 0 \ x\<^sup>\ ; y" by (metis mult_isotone star_below_circ zero_least) lemma star_mult_circ: "x\<^sup>\ ; x\<^sup>\ = x\<^sup>\" by (metis add_right_divisibility antisym circ_left_unfold star_left_induct_mult star.circ_loop_fixpoint) lemma circ_mult_star: "x\<^sup>\ ; x\<^sup>\ = x\<^sup>\" by (metis circ_slide mult_left_one mult_right_one star_mult_circ star_simulation_right_equal) lemma circ_star: "x\<^sup>\\<^sup>\ = x\<^sup>\" by (metis circ_reflexive circ_transitive_equal less_eq_def mult_left_one star_one star_simulation_right_equal star_square) lemma star_circ: "x\<^sup>\\<^sup>\ = x\<^sup>\\<^sup>\" by (metis antisym circ_circ_add circ_sub_dist less_eq_def star.circ_rtc_2 star_below_circ) lemma circ_add_3: "(x\<^sup>\ ; y\<^sup>\)\<^sup>\ \ (x + y)\<^sup>\" by (metis circ_add_1 circ_isotone circ_left_unfold circ_star mult_left_subdist_add_left mult_right_isotone mult_right_one star.circ_isotone) lemma circ_isolate: "x\<^sup>\ = x\<^sup>\ ; 0 + x\<^sup>\" by (metis add_commutative antisym circ_add_upper_bound circ_mult_star circ_simulate_absorb star.left_plus_below_circ star_below_circ zero_right_mult_decreasing) lemma circ_isolate_mult: "x\<^sup>\ ; y = x\<^sup>\ ; 0 + x\<^sup>\ ; y" by (metis circ_isolate mult_associative mult_left_zero mult_right_dist_add) lemma circ_isolate_mult_sub: "x\<^sup>\ ; y \ x\<^sup>\ + x\<^sup>\ ; y" by (metis add_left_isotone circ_isolate_mult zero_right_mult_decreasing) lemma circ_sub_decompose: "(x\<^sup>\ ; y)\<^sup>\ \ (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" by (smt add_commutative add_least_upper_bound add_right_upper_bound circ_back_loop_fixpoint circ_isolate_mult mult_zero_add_circ_2 zero_right_mult_decreasing) lemma circ_add_4: "(x + y)\<^sup>\ = (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" by (smt antisym circ_add circ_isotone circ_sub_decompose circ_transitive_equal mult_associative mult_left_isotone star_below_circ) lemma circ_add_5: "(x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\ = (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" by (metis circ_add circ_add_4) lemma plus_circ: "(x\<^sup>\ ; x)\<^sup>\ = x\<^sup>\" by (smt add_idempotent circ_add_4 circ_decompose_7 circ_star star.circ_decompose_5 star.right_plus_circ) (* lemma "(x\<^sup>\ ; y ; x\<^sup>\)\<^sup>\ = (x\<^sup>\ ; y)\<^sup>\" nitpick *) end class kleene_algebra_T = semiring_T + kleene_algebra sublocale kleene_algebra_T < star!: itering_T where circ = star .. class omega_algebra_T = kleene_algebra_T + fixes omega :: "'a \ 'a" ("_\<^sup>\" [100] 100) assumes omega_unfold: "y\<^sup>\ = y ; y\<^sup>\" assumes omega_induct: "x \ z + y ; x \ x \ y\<^sup>\ + y\<^sup>\ ; z" begin text {* Most lemmas in this class are taken from Georg Struth's theories. *} lemma star_zero_below_omega: "x\<^sup>\ ; 0 \ x\<^sup>\" by (metis add_left_zero omega_unfold star_left_induct_equal) lemma star_zero_below_omega_zero: "x\<^sup>\ ; 0 \ x\<^sup>\ ; 0" by (metis add_left_zero mult_associative omega_unfold star_left_induct_equal) lemma omega_induct_mult: "y \ x ; y \ y \ x\<^sup>\" by (metis add_commutative add_left_zero less_eq_def omega_induct star_zero_below_omega) lemma omega_sub_dist: "x\<^sup>\ \ (x+y)\<^sup>\" by (metis mult_right_subdist_add_left omega_induct_mult omega_unfold) lemma omega_isotone: "x \ y \ x\<^sup>\ \ y\<^sup>\" by (metis less_eq_def omega_sub_dist) lemma omega_induct_equal: "y = z + x ; y \ y \ x\<^sup>\ + x\<^sup>\ ; z" by (metis omega_induct order_refl) lemma omega_zero: "0\<^sup>\ = 0" by (metis mult_left_zero omega_unfold) lemma omega_one_greatest: "x \ 1\<^sup>\" by (metis mult_left_one omega_induct_mult order_refl) lemma omega_one: "1\<^sup>\ = T" by (metis add_left_top less_eq_def omega_one_greatest) lemma star_mult_omega: "x\<^sup>\ ; x\<^sup>\ = x\<^sup>\" by (metis antisym_conv mult_isotone omega_unfold star.circ_increasing star_left_induct_mult_equal star_left_induct_mult_iff) lemma star_omega_top: "x\<^sup>\\<^sup>\ = T" by (metis add_left_top less_eq_def omega_one omega_sub_dist star.circ_plus_one) lemma omega_sub_vector: "x\<^sup>\ ; y \ x\<^sup>\" by (metis mult_associative omega_induct_mult omega_unfold order_refl) lemma omega_vector: "x\<^sup>\ ; T = x\<^sup>\" by (metis add_commutative less_eq_def omega_sub_vector top_right_mult_increasing) lemma omega_simulation: "z ; x \ y ; z \ z ; x\<^sup>\ \ y\<^sup>\ " by (smt less_eq_def mult_associative mult_right_subdist_add_left omega_induct_mult omega_unfold) lemma omega_omega: "x\<^sup>\\<^sup>\ \ x\<^sup>\" by (metis omega_sub_vector omega_unfold) lemma left_plus_omega: "(x ; x\<^sup>\)\<^sup>\ = x\<^sup>\" by (metis antisym mult_associative mult_right_isotone mult_right_one omega_induct_mult omega_unfold star_mult_omega star_one star.circ_reflexive star.circ_right_unfold star.circ_plus_same star_sum star_sup_one) lemma omega_slide: "x ; (y ; x)\<^sup>\ = (x ; y)\<^sup>\" by (metis antisym mult_associative mult_right_isotone omega_simulation omega_unfold order_refl) lemma omega_simulation_2: "y ; x \ x ; y \ (x ; y)\<^sup>\ \ x\<^sup>\" by (metis less_eq_def mult_right_isotone omega_induct_mult omega_slide omega_sub_dist) lemma wagner: "(x + y)\<^sup>\ = x ; (x + y)\<^sup>\ + z \ (x + y)\<^sup>\ = x\<^sup>\ + x\<^sup>\ ; z" by (metis add_commutative add_least_upper_bound eq_iff omega_induct omega_sub_dist star_left_induct) lemma right_plus_omega: "(x\<^sup>\ ; x)\<^sup>\ = x\<^sup>\" by (metis left_plus_omega star.circ_plus_same) lemma omega_sub_dist_1: "(x ; y\<^sup>\)\<^sup>\ \ (x + y)\<^sup>\" by (metis add_least_upper_bound left_plus_omega mult_isotone mult_left_one mult_right_dist_add omega_isotone order_refl star_decompose_1 star.circ_increasing star.circ_plus_one) lemma omega_sub_dist_2: "(x\<^sup>\ ; y)\<^sup>\ \ (x + y)\<^sup>\" by (metis add_commutative mult_isotone omega_slide omega_sub_dist_1 star_mult_omega star.circ_sub_dist) lemma omega_star: "(x\<^sup>\)\<^sup>\ = 1 + x\<^sup>\" by (metis mult_associative omega_unfold omega_vector star.circ_plus_same star_left_unfold_equal star_omega_top) lemma omega_mult_omega_star: "x\<^sup>\ ; x\<^sup>\\<^sup>\ = x\<^sup>\" by (metis mult_associative omega_unfold omega_vector star.circ_plus_same star_omega_top) lemma omega_sum_unfold_1: "(x + y)\<^sup>\ = x\<^sup>\ + x\<^sup>\ ; y ; (x + y)\<^sup>\" by (metis mult_associative mult_right_dist_add omega_unfold wagner) lemma omega_sum_unfold_2: "(x + y)\<^sup>\ \ (x\<^sup>\ ; y)\<^sup>\ + (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" by (metis omega_induct_equal omega_sum_unfold_1) lemma omega_sum_unfold_3: "(x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\ \ (x + y)\<^sup>\" by (metis omega_sum_unfold_1 star_left_induct_equal) lemma omega_decompose: "(x + y)\<^sup>\ = (x\<^sup>\ ; y)\<^sup>\ + (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" by (metis add_least_upper_bound antisym omega_sub_dist_2 omega_sum_unfold_2 omega_sum_unfold_3) lemma omega_loop_fixpoint: "y ; (y\<^sup>\ + y\<^sup>\ ; z) + z = y\<^sup>\ + y\<^sup>\ ; z" by (metis add_associative mult_left_dist_add omega_unfold star.circ_loop_fixpoint) lemma omega_loop_greatest_fixpoint: "y ; x + z = x \ x \ y\<^sup>\ + y\<^sup>\ ; z" by (metis add_commutative omega_induct_equal) lemma omega_square: "x\<^sup>\ = (x ; x)\<^sup>\" by (smt antisym mult_associative omega_induct_mult omega_slide omega_sub_vector omega_unfold omega_vector top_mult_top) (* proof - let ?f = "\y . x ; y" have 1: "isotone ?f" by (smt isotone_def mult_right_isotone) have 2: "?f \ ?f = (\y . x ; x ; y)" by (simp add: mult_associative o_def) thus ?thesis using 1 by (metis has_greatest_fixpoint_def nu_square omega_loop_zero_is_greatest_fixpoint omega_loop_zero_nu) qed *) lemma mult_top_omega: "(x ; T)\<^sup>\ \ x ; T" by (metis mult_right_isotone omega_slide top_greatest) lemma mult_zero_omega: "(x ; 0)\<^sup>\ = x ; 0" by (metis mult_left_zero omega_slide) lemma mult_zero_add_omega: "(x + y ; 0)\<^sup>\ = x\<^sup>\ + x\<^sup>\ ; y ; 0" by (smt add_associative add_commutative add_idempotent mult_associative mult_left_one mult_left_zero mult_right_dist_add mult_zero_omega star.mult_zero_circ omega_decompose) lemma omega_mult_star: "x\<^sup>\ ; x\<^sup>\ = x\<^sup>\" by (metis mult_associative omega_vector star.circ_left_top) lemma omega_loop_is_greatest_fixpoint: "is_greatest_fixpoint (\x . y ; x + z) (y\<^sup>\ + y\<^sup>\ ; z)" by (smt is_greatest_fixpoint_def omega_loop_fixpoint omega_loop_greatest_fixpoint) lemma omega_loop_nu: "\ (\x . y ; x + z) = y\<^sup>\ + y\<^sup>\ ; z" by (metis greatest_fixpoint_same omega_loop_is_greatest_fixpoint) lemma omega_loop_zero_is_greatest_fixpoint: "is_greatest_fixpoint (\x . y ; x) (y\<^sup>\)" by (metis is_greatest_fixpoint_def omega_induct_mult omega_unfold order_refl) lemma omega_loop_zero_nu: "\ (\x . y ; x) = y\<^sup>\" by (metis greatest_fixpoint_same omega_loop_zero_is_greatest_fixpoint) lemma omega_separate_unfold: "(x\<^sup>\ ; y)\<^sup>\ = y\<^sup>\ + y\<^sup>\ ; x ; (x\<^sup>\ ; y)\<^sup>\" by (metis add_commutative mult_associative omega_slide omega_sum_unfold_1 star.circ_loop_fixpoint) lemma omega_circ_simulate_right_plus: "z ; x \ y ; (y\<^sup>\ ; 0 + y\<^sup>\) ; z + w \ z ; (x\<^sup>\ ; 0 + x\<^sup>\) \ (y\<^sup>\ ; 0 + y\<^sup>\) ; (z + w ; (x\<^sup>\ ; 0 + x\<^sup>\))" proof assume "z ; x \ y ; (y\<^sup>\ ; 0 + y\<^sup>\) ; z + w" hence 1: "z ; x \ y\<^sup>\ ; 0 + y ; y\<^sup>\ ; z + w" by (metis mult_associative mult_left_dist_add mult_left_zero mult_right_dist_add omega_unfold) hence "(y\<^sup>\ ; 0 + y\<^sup>\ ; z + y\<^sup>\ ; w ; x\<^sup>\ ; 0 + y\<^sup>\ ; w ; x\<^sup>\) ; x \ y\<^sup>\ ; 0 + y\<^sup>\ ; (y\<^sup>\ ; 0 + y ; y\<^sup>\ ; z + w) + y\<^sup>\ ; w ; x\<^sup>\ ; 0 + y\<^sup>\ ; w ; x\<^sup>\" by (smt add_associative add_left_upper_bound add_right_upper_bound less_eq_def mult_associative mult_left_dist_add mult_left_zero mult_right_dist_add star.circ_back_loop_fixpoint) also have "... = y\<^sup>\ ; 0 + y\<^sup>\ ; y ; y\<^sup>\ ; z + y\<^sup>\ ; w ; x\<^sup>\ ; 0 + y\<^sup>\ ; w ; x\<^sup>\" by (smt add_associative add_right_upper_bound less_eq_def mult_associative mult_left_dist_add star.circ_back_loop_fixpoint star_mult_omega) finally have "z + (y\<^sup>\ ; 0 + y\<^sup>\ ; z + y\<^sup>\ ; w ; x\<^sup>\ ; 0 + y\<^sup>\ ; w ; x\<^sup>\) ; x \ y\<^sup>\ ; 0 + y\<^sup>\ ; z + y\<^sup>\ ; w ; x\<^sup>\ ; 0 + y\<^sup>\ ; w ; x\<^sup>\" by (smt add_least_upper_bound add_left_isotone add_left_upper_bound mult_left_isotone order_trans star.circ_loop_fixpoint star.circ_plus_same star.circ_transitive_equal star.left_plus_below_circ) hence 2: "z ; x\<^sup>\ \ y\<^sup>\ ; 0 + y\<^sup>\ ; z + y\<^sup>\ ; w ; x\<^sup>\ ; 0 + y\<^sup>\ ; w ; x\<^sup>\" by (metis star_right_induct) have "z ; x\<^sup>\ ; 0 \ (y\<^sup>\ ; 0 + y ; y\<^sup>\ ; z + w) ; x\<^sup>\ ; 0" using 1 by (smt add_left_divisibility mult_associative mult_right_subdist_add_left omega_unfold) hence "z ; x\<^sup>\ ; 0 \ y\<^sup>\ + y\<^sup>\ ; (y\<^sup>\ ; 0 + w ; x\<^sup>\ ; 0)" by (smt add_associative add_commutative left_plus_omega mult_associative mult_left_zero mult_right_dist_add omega_induct star.left_plus_circ) thus "z ; (x\<^sup>\ ; 0 + x\<^sup>\) \ (y\<^sup>\ ; 0 + y\<^sup>\) ; (z + w ; (x\<^sup>\ ; 0 + x\<^sup>\))" using 2 by (smt add_associative add_commutative less_eq_def mult_associative mult_left_dist_add mult_left_zero mult_right_dist_add omega_unfold omega_zero star_mult_omega zero_right_mult_decreasing) qed lemma omega_circ_simulate_left_plus: "x ; z \ z ; (y\<^sup>\ ; 0 + y\<^sup>\) + w \ (x\<^sup>\ ; 0 + x\<^sup>\) ; z \ (z + (x\<^sup>\ ; 0 + x\<^sup>\) ; w) ; (y\<^sup>\ ; 0 + y\<^sup>\)" proof assume 1: "x ; z \ z ; (y\<^sup>\ ; 0 + y\<^sup>\) + w" have "x ; (z ; y\<^sup>\ ; 0 + z ; y\<^sup>\ + x\<^sup>\ ; 0 + x\<^sup>\ ; w ; y\<^sup>\ ; 0 + x\<^sup>\ ; w ; y\<^sup>\) \ x ; z ; y\<^sup>\ ; 0 + x ; z ; y\<^sup>\ + x\<^sup>\ ; 0 + x\<^sup>\ ; w ; y\<^sup>\ ; 0 + x\<^sup>\ ; w ; y\<^sup>\" by (smt add_associative add_right_upper_bound less_eq_def mult_associative mult_left_dist_add omega_unfold star.circ_loop_fixpoint) also have "... \ (z ; y\<^sup>\ ; 0 + z ; y\<^sup>\ + w) ; y\<^sup>\ ; 0 + (z ; y\<^sup>\ ; 0 + z ; y\<^sup>\ + w) ; y\<^sup>\ + x\<^sup>\ ; 0 + x\<^sup>\ ; w ; y\<^sup>\ ; 0 + x\<^sup>\ ; w ; y\<^sup>\" using 1 by (metis add_left_isotone mult_associative mult_left_dist_add mult_left_isotone) also have "... = z ; y\<^sup>\ ; 0 + z ; y\<^sup>\ + x\<^sup>\ ; 0 + x\<^sup>\ ; w ; y\<^sup>\ ; 0 + x\<^sup>\ ; w ; y\<^sup>\" by (smt add_associative add_commutative add_idempotent mult_associative mult_left_zero mult_right_dist_add star.circ_loop_fixpoint star.circ_transitive_equal star_mult_omega) finally have "(x\<^sup>\ ; 0 + x\<^sup>\) ; z \ z ; y\<^sup>\ ; 0 + z ; y\<^sup>\ + x\<^sup>\ ; 0 + x\<^sup>\ ; w ; y\<^sup>\ ; 0 + x\<^sup>\ ; w ; y\<^sup>\" by (smt add_least_upper_bound add_left_upper_bound mult_associative mult_left_zero mult_right_dist_add star.circ_back_loop_fixpoint star_left_induct) thus "(x\<^sup>\ ; 0 + x\<^sup>\) ; z \ (z + (x\<^sup>\ ; 0 + x\<^sup>\) ; w) ; (y\<^sup>\ ; 0 + y\<^sup>\)" by (smt add_associative mult_associative mult_left_dist_add mult_left_zero mult_right_dist_add) qed end sublocale omega_algebra_T < comb0!: itering_T where circ = "(\x . x\<^sup>\ ; 0 + x\<^sup>\)" apply unfold_locales apply (smt add_associative add_commutative mult_associative mult_left_dist_add mult_left_zero mult_right_dist_add omega_slide star.circ_mult) apply (smt add_associative add_commutative star.circ_add mult_associative mult_left_dist_add mult_left_zero mult_right_dist_add star.mult_zero_add_circ_2 mult_zero_add_omega omega_decompose) apply (smt add_isotone star.circ_simulate mult_associative mult_left_dist_add mult_left_isotone mult_left_zero mult_right_dist_add omega_simulation) apply (smt add_commutative add_left_isotone mult_left_isotone mult_left_subdist_add_left mult_right_one omega_circ_simulate_right_plus order_trans star.circ_plus_one) apply (smt add_commutative add_right_isotone mult_left_subdist_add_left mult_right_isotone omega_circ_simulate_left_plus order_trans star.circ_increasing) apply (metis omega_circ_simulate_right_plus) by (metis omega_circ_simulate_left_plus) class omega_itering = omega_algebra_T + itering_T begin subclass kleene_itering .. lemma circ_below_omega_star: "x\<^sup>\ \ x\<^sup>\ + x\<^sup>\" by (metis circ_left_unfold mult_right_one omega_induct order_refl) lemma omega_mult_circ: "x\<^sup>\ ; x\<^sup>\ = x\<^sup>\" by (smt add_commutative circ_reflexive less_eq_def mult_left_dist_add mult_right_one omega_sub_vector) lemma circ_mult_omega: "x\<^sup>\ ; x\<^sup>\ = x\<^sup>\" by (metis antisym circ_left_unfold circ_slide le_less mult_left_one mult_right_one mult_right_subdist_add_left omega_simulation) lemma circ_omega: "x\<^sup>\\<^sup>\ = T" by (metis circ_star star_omega_top) lemma omega_circ: "x\<^sup>\\<^sup>\ = 1 + x\<^sup>\" by (metis circ_left_unfold circ_star mult_associative omega_vector star.circ_left_top) end class Omega = fixes Omega :: "'a \ 'a" ("_\<^sup>\" [100] 100) class dra = kleene_algebra_T + Omega + assumes Omega_unfold : "y\<^sup>\ = 1 + y ; y\<^sup>\" assumes Omega_isolate : "y\<^sup>\ = y\<^sup>\ ; 0 + y\<^sup>\" assumes Omega_induct : "x \ z + y ; x \ x \ y\<^sup>\ ; z" begin lemma Omega_mult: "(x ; y)\<^sup>\ = 1 + x ; (y ; x)\<^sup>\ ; y" by (smt Omega_induct Omega_unfold antisym mult_associative mult_left_dist_add mult_left_one mult_right_dist_add mult_right_isotone mult_right_one order_refl) lemma Omega_add_1: "(x + y)\<^sup>\ = x\<^sup>\ ; (y ; x\<^sup>\)\<^sup>\" by (smt Omega_induct Omega_unfold add_associative add_commutative add_right_isotone antisym mult_associative mult_left_one mult_right_dist_add mult_right_isotone mult_right_one order_refl) lemma Omega_add: "(x + y)\<^sup>\ = (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" by (smt Omega_add_1 Omega_mult mult_associative mult_left_dist_add mult_left_one mult_right_dist_add mult_right_one) lemma Omega_simulate: "z ; x \ y ; z \ z ; x\<^sup>\ \ y\<^sup>\ ; z" by (smt Omega_induct Omega_unfold add_right_isotone mult_associative mult_left_dist_add mult_left_isotone mult_right_one) end sublocale dra < Omega!: itering_1 where circ = Omega apply unfold_locales apply (metis Omega_mult) apply (metis Omega_add) by (metis Omega_simulate) context dra begin lemma star_below_Omega: "x\<^sup>\ \ x\<^sup>\" by (metis Omega_isolate add_commutative add_left_divisibility) lemma Omega_sum_unfold_1: "(x + y)\<^sup>\ = y\<^sup>\ + y\<^sup>\ ; x ; (x + y)\<^sup>\" by (smt Omega.circ_add Omega.circ_loop_fixpoint Omega_isolate add_associative add_commutative mult_associative mult_left_zero mult_right_dist_add) lemma Omega_add_3: "(x + y)\<^sup>\ = (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" by (smt Omega.circ_add Omega.circ_isotone Omega_induct Omega_sum_unfold_1 add_commutative antisym mult_left_isotone order_refl star_below_Omega) lemma Omega_one: "1\<^sup>\ = T" by (metis Omega.circ_transitive_equal Omega_induct add_left_top add_right_upper_bound less_eq_def mult_left_one) lemma top_left_zero: "T ; x = T" by (metis Omega_induct Omega_one add_left_top add_right_upper_bound less_eq_def mult_left_one) lemma star_mult_Omega: "x\<^sup>\ = x\<^sup>\ ; x\<^sup>\" by (metis Omega.circ_plus_one Omega.circ_transitive_equal Omega_isolate add_commutative less_eq_def order_refl star.circ_add_mult_zero star.circ_increasing star.circ_plus_same star_involutive star_left_induct star_square) lemma Omega_separate_2: "y ; x \ x ; (x + y) \ (x + y)\<^sup>\ = x\<^sup>\ ; y\<^sup>\" by (smt Omega.circ_sub_dist_3 Omega_induct Omega_sum_unfold_1 add_right_isotone antisym mult_associative mult_left_isotone star_mult_Omega star_simulation_left) lemma Omega_circ_simulate_right_plus: "z ; x \ y ; y\<^sup>\ ; z + w \ z ; x\<^sup>\ \ y\<^sup>\ ; (z + w ; x\<^sup>\)" by (smt Omega.circ_back_loop_fixpoint Omega.circ_plus_same Omega.left_plus_circ Omega_induct add_associative add_commutative add_right_isotone less_eq_def mult_associative mult_right_dist_add) lemma Omega_circ_simulate_left_plus: "x ; z \ z ; y\<^sup>\ + w \ x\<^sup>\ ; z \ (z + x\<^sup>\ ; w) ; y\<^sup>\" proof assume 1: "x ; z \ z ; y\<^sup>\ + w" hence "x ; ((z + x\<^sup>\ ; w) ; y\<^sup>\) \ z ; y\<^sup>\ ; y\<^sup>\ + w ; y\<^sup>\ + x\<^sup>\ ; w ; y\<^sup>\" by (smt Omega.left_plus_below_circ add_left_isotone add_right_isotone mult_associative mult_left_dist_add mult_left_isotone mult_right_dist_add order_trans) hence "x ; ((z + x\<^sup>\ ; w) ; y\<^sup>\) \ (z + x\<^sup>\ ; w) ; y\<^sup>\" by (metis Omega.circ_transitive_equal mult_associative Omega.circ_reflexive add_associative less_eq_def mult_left_one mult_right_dist_add) thus "x\<^sup>\ ; z \ (z + x\<^sup>\ ; w) ; y\<^sup>\" by (smt Omega.circ_back_loop_fixpoint Omega_isolate add_least_upper_bound mult_associative mult_left_zero mult_right_dist_add mult_right_subdist_add_left mult_right_subdist_add_right star_left_induct) qed end sublocale dra < Omega!: itering_T where circ = Omega apply unfold_locales apply (smt Omega.circ_loop_fixpoint Omega_circ_simulate_right_plus add_associative add_commutative add_left_upper_bound mult_associative mult_left_dist_add order_trans) apply (smt Omega.circ_increasing Omega_circ_simulate_left_plus add_commutative add_right_isotone mult_right_isotone order_trans) apply (metis Omega_circ_simulate_right_plus) by (metis Omega_circ_simulate_left_plus) class dra_omega = omega_algebra_T + Omega + assumes top_left_zero: "T ; x = T" assumes Omega_def: "x\<^sup>\ = x\<^sup>\ + x\<^sup>\" begin lemma omega_left_zero: "x\<^sup>\ ; y = x\<^sup>\" by (metis mult_associative omega_vector top_left_zero) lemma Omega_mult: "(x ; y)\<^sup>\ = 1 + x ; (y ; x)\<^sup>\ ; y" by (smt add_associative add_commutative Omega_def mult_left_dist_add mult_right_dist_add omega_left_zero omega_slide star_unfold_slide) lemma Omega_add: "(x + y)\<^sup>\ = (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" proof - have "(x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\ = (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\ + (x\<^sup>\ ; y)\<^sup>\ + (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\\<^sup>\ ; x\<^sup>\" by (smt add_commutative Omega_def mult_associative mult_right_dist_add mult_zero_add_omega omega_left_zero star.circ_add_1) thus ?thesis by (smt add_associative add_commutative Omega_def mult_associative mult_left_dist_add omega_decompose omega_left_zero star.circ_add_1 star.circ_loop_fixpoint star.circ_slide) qed lemma Omega_simulate: "z ; x \ y ; z \ z ; x\<^sup>\ \ y\<^sup>\ ; z" by (smt add_isotone Omega_def mult_left_dist_add mult_right_dist_add omega_left_zero omega_simulation star_simulation_right) subclass dra apply unfold_locales apply (metis Omega_def comb0.circ_left_unfold omega_left_zero) apply (smt Omega_def add_associative less_eq_def mult_right_dist_add omega_left_zero zero_right_mult_decreasing) by (metis Omega_def mult_right_dist_add omega_induct omega_left_zero) end (* end theory ExtendedDesigns imports While Omega Domain begin *) class semiring_aL = antidomain_semiring + fixes L :: "'a" assumes d_zero_mult_L: "d(x ; 0) ; L \ x" assumes d_L_zero : "d(L ; 0) = 1" assumes mult_L : "x ; L \ x ; 0 + L" begin lemma L_left_zero: "L ; x = L" by (metis d_L_zero d_zero_mult_L less_def less_le mult_associative mult_left_one mult_left_zero zero_right_mult_decreasing) lemma d_mult_L: "d(x) ; L \ x ; L" by (metis d_L_zero d_mult_d d_zero_mult_L mult_associative mult_right_one) lemma mult_L_split: "x ; L = x ; 0 + d(x) ; L" by (rule antisym, smt d_restrict_equals less_eq_def mult_L mult_associative mult_left_dist_add, metis add_least_upper_bound d_mult_L mult_right_isotone zero_least) lemma d_L_split: "x ; d(y) ; L = x ; 0 + d(x ; y) ; L" by (metis d_commutative d_mult_d d_zero mult_L_split mult_associative mult_left_zero) lemma d_mult_mult_L: "d(x ; y) ; L \ x ; d(y) ; L" by (metis add_right_divisibility d_L_split) end class ed = omega_algebra_T + semiring_aL + Omega + assumes Omega_def: "x\<^sup>\ = d(x\<^sup>\) ; L + x\<^sup>\" begin lemma mult_L_star: "(x ; L)\<^sup>\ = 1 + x ; L" by (metis L_left_zero mult_associative star_unfold_slide) lemma mult_L_omega: "(x ; L)\<^sup>\ = x ; L" by (metis L_left_zero omega_slide) lemma mult_L_add_star: "(x ; L + y)\<^sup>\ = y\<^sup>\ + y\<^sup>\ ; x ; L" by (metis L_left_zero add_commutative mult_L_star mult_associative mult_left_dist_add mult_right_one star.circ_add_1) lemma mult_L_add_omega: "(x ; L + y)\<^sup>\ = y\<^sup>\ + y\<^sup>\ ; x ; L" by (smt L_left_zero add_commutative add_left_upper_bound less_eq_def mult_L_omega mult_L_star mult_associative mult_left_one mult_right_dist_add omega_decompose) lemma mult_L_add_circ: "(x ; L + y)\<^sup>\ = d(y\<^sup>\) ; L + y\<^sup>\ + y\<^sup>\ ; x ; L" by (smt L_left_zero Omega_def add_associative add_commutative d_dist_add d_mult_L less_eq_def mult_L_add_omega mult_L_add_star mult_associative mult_right_dist_add) lemma circ_add_d: "(x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\ = d((x\<^sup>\ ; y)\<^sup>\) ; L + ((x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\ + (x\<^sup>\ ; y)\<^sup>\ ; d(x\<^sup>\) ; L)" by (smt L_left_zero add_associative add_commutative Omega_def mult_L_add_circ mult_associative mult_left_dist_add mult_right_dist_add) lemma d_Omega_circ_simulate_right_plus: "z ; x \ y ; y\<^sup>\ ; z + w \ z ; x\<^sup>\ \ y\<^sup>\ ; (z + w ; x\<^sup>\)" proof assume "z ; x \ y ; y\<^sup>\ ; z + w" hence 1: "z ; x \ d(y\<^sup>\) ; L + y ; y\<^sup>\ ; z + w" by (smt L_left_zero Omega_def add_associative add_commutative add_left_zero mult_associative mult_left_dist_add mult_right_dist_add d_L_split omega_unfold) hence "(d(y\<^sup>\) ; L + y\<^sup>\ ; z + y\<^sup>\ ; w ; d(x\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\) ; x \ d(y\<^sup>\) ; L + y\<^sup>\ ; (d(y\<^sup>\) ; L + y ; y\<^sup>\ ; z + w) + y\<^sup>\ ; w ; d(x\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\" by (smt L_left_zero add_associative add_left_upper_bound add_right_upper_bound less_eq_def mult_associative mult_left_dist_add mult_right_dist_add star.circ_back_loop_fixpoint) also have "... = d(y\<^sup>\) ; L + y\<^sup>\ ; y ; y\<^sup>\ ; z + y\<^sup>\ ; w ; d(x\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\" by (smt add_associative add_commutative add_idempotent mult_associative mult_left_dist_add d_L_split star.circ_back_loop_fixpoint star_mult_omega) also have "... \ d(y\<^sup>\) ; L + y\<^sup>\ ; z + y\<^sup>\ ; w ; d(x\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\" by (metis add_left_isotone add_right_isotone mult_left_isotone star.circ_plus_same star.circ_transitive_equal star.left_plus_below_circ) finally have 2: "z ; x\<^sup>\ \ d(y\<^sup>\) ; L + y\<^sup>\ ; z + y\<^sup>\ ; w ; d(x\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\" by (smt add_least_upper_bound add_left_upper_bound star.circ_loop_fixpoint star_right_induct) have "z ; x ; x\<^sup>\ \ y ; y\<^sup>\ ; z ; x\<^sup>\ + d(y\<^sup>\) ; L + w ; x\<^sup>\" using 1 by (smt L_left_zero add_commutative mult_associative mult_left_isotone mult_right_dist_add) hence "z ; x\<^sup>\ \ y\<^sup>\ + y\<^sup>\ ; d(y\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\" by (smt add_associative add_commutative left_plus_omega mult_associative mult_left_dist_add omega_induct omega_unfold star.left_plus_circ) hence "z ; x\<^sup>\ \ y\<^sup>\ + y\<^sup>\ ; w ; x\<^sup>\" by (metis add_commutative d_mult_L less_eq_def mult_associative mult_right_isotone omega_sub_vector order_trans star_mult_omega) hence "d(z ; x\<^sup>\) ; L \ d(y\<^sup>\) ; L + y\<^sup>\ ; w ; d(x\<^sup>\) ; L" by (smt add_associative add_commutative d_L_split d_dist_add less_eq_def mult_right_dist_add) hence "z ; d(x\<^sup>\) ; L \ z ; 0 + d(y\<^sup>\) ; L + y\<^sup>\ ; w ; d(x\<^sup>\) ; L" by (metis add_associative add_right_isotone d_L_split) hence "z ; d(x\<^sup>\) ; L \ d(y\<^sup>\) ; L + y\<^sup>\ ; z + y\<^sup>\ ; w ; d(x\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\" by (smt add_commutative add_left_isotone add_left_upper_bound order_trans star.circ_loop_fixpoint zero_right_mult_decreasing) thus "z ; x\<^sup>\ \ y\<^sup>\ ; (z + w ; x\<^sup>\)" using 2 by (smt L_left_zero Omega_def add_associative less_eq_def mult_associative mult_left_dist_add mult_right_dist_add) qed lemma d_Omega_circ_simulate_left_plus: "x ; z \ z ; y\<^sup>\ + w \ x\<^sup>\ ; z \ (z + x\<^sup>\ ; w) ; y\<^sup>\" proof assume 1: "x ; z \ z ; y\<^sup>\ + w" have "x ; (z ; d(y\<^sup>\) ; L + z ; y\<^sup>\ + d(x\<^sup>\) ; L + x\<^sup>\ ; w ; d(y\<^sup>\) ; L + x\<^sup>\ ; w ; y\<^sup>\) = x ; z ; d(y\<^sup>\) ; L + x ; z ; y\<^sup>\ + d(x\<^sup>\) ; L + x ; x\<^sup>\ ; w ; d(y\<^sup>\) ; L + x ; x\<^sup>\ ; w ; y\<^sup>\" by (smt add_associative add_commutative mult_associative mult_left_dist_add d_L_split omega_unfold) also have "... \ (z ; d(y\<^sup>\) ; L + z ; y\<^sup>\ + w) ; d(y\<^sup>\) ; L + (z ; d(y\<^sup>\) ; L + z ; y\<^sup>\ + w) ; y\<^sup>\ + d(x\<^sup>\) ; L + x\<^sup>\ ; w ; d(y\<^sup>\) ; L + x\<^sup>\ ; w ; y\<^sup>\" using 1 by (smt Omega_def add_associative add_right_upper_bound less_eq_def mult_associative mult_left_dist_add mult_right_dist_add star.circ_loop_fixpoint) also have "... = z ; d(y\<^sup>\) ; L + z ; y\<^sup>\ ; d(y\<^sup>\) ; L + w ; d(y\<^sup>\) ; L + z ; y\<^sup>\ + w ; y\<^sup>\ + d(x\<^sup>\) ; L + x\<^sup>\ ; w ; d(y\<^sup>\) ; L + x\<^sup>\ ; w ; y\<^sup>\" by (smt L_left_zero add_associative add_commutative add_idempotent mult_associative mult_right_dist_add star.circ_transitive_equal) also have "... = z ; d(y\<^sup>\) ; L + w ; d(y\<^sup>\) ; L + z ; y\<^sup>\ + w ; y\<^sup>\ + d(x\<^sup>\) ; L + x\<^sup>\ ; w ; d(y\<^sup>\) ; L + x\<^sup>\ ; w ; y\<^sup>\" by (smt add_associative add_commutative add_idempotent less_eq_def mult_associative d_L_split star_mult_omega zero_right_mult_decreasing) finally have "x ; (z ; d(y\<^sup>\) ; L + z ; y\<^sup>\ + d(x\<^sup>\) ; L + x\<^sup>\ ; w ; d(y\<^sup>\) ; L + x\<^sup>\ ; w ; y\<^sup>\) \ z ; d(y\<^sup>\) ; L + z ; y\<^sup>\ + d(x\<^sup>\) ; L + x\<^sup>\ ; w ; d(y\<^sup>\) ; L + x\<^sup>\ ; w ; y\<^sup>\" by (smt add_associative add_commutative add_idempotent mult_associative star.circ_loop_fixpoint) thus "x\<^sup>\ ; z \ (z + x\<^sup>\ ; w) ; y\<^sup>\" by (smt L_left_zero Omega_def add_associative add_least_upper_bound add_left_upper_bound mult_associative mult_left_dist_add mult_right_dist_add star.circ_back_loop_fixpoint star_left_induct) qed end sublocale ed < ed_omega!: omega_itering where circ = Omega apply unfold_locales apply (smt L_left_zero add_associative add_commutative add_left_zero Omega_def mult_associative mult_left_dist_add mult_right_dist_add d_L_split omega_slide star_unfold_slide) apply (smt add_associative add_commutative add_left_zero circ_add_d Omega_def mult_left_dist_add mult_right_dist_add d_L_split d_dist_add omega_decompose star.circ_add_1 star.circ_slide) apply (smt L_left_zero add_associative add_commutative add_isotone add_left_zero Omega_def mult_associative mult_left_dist_add mult_left_isotone mult_right_dist_add d_L_split d_isotone omega_simulation star_simulation_right) apply (smt d_Omega_circ_simulate_right_plus Omega_def add_left_isotone add_right_upper_bound mult_left_isotone mult_right_isotone order_trans star.circ_back_loop_fixpoint) apply (smt Omega_def add_commutative add_least_upper_bound add_right_isotone mult_right_isotone d_Omega_circ_simulate_left_plus order_trans star.circ_increasing) apply (metis d_Omega_circ_simulate_right_plus) by (metis d_Omega_circ_simulate_left_plus) sublocale ed < ed_omega!: while where circ = Omega .. sublocale ed < ed_star!: omega_itering where circ = star .. (* end theory AbortingFiniteInfinite imports While Omega begin *) class nL = fixes n :: "'a \ 'a" fixes L :: "'a" class semiring_nL = semiring_T + nL + assumes n_zero : "n(0) = 0" assumes n_top : "n(T) = 1" assumes n_dist_add : "n(x + y) = n(x) + n(y)" assumes n_export : "n(n(x) ; y) = n(x) ; n(y)" assumes n_sub_mult_zero: "n(x) = n(x ; 0) ; n(x)" assumes n_L_split : "x ; n(y) ; L = x ; 0 + n(x ; y) ; L" assumes n_split : "x \ x ; 0 + n(x ; L) ; T" begin lemma n_sub_one: "n(x) \ 1" by (metis add_left_top add_right_upper_bound n_dist_add n_top) lemma n_isotone: "x \ y \ n(x) \ n(y)" by (metis less_eq_def n_dist_add) lemma n_mult_idempotent: "n(x) ; n(x) = n(x)" by (metis mult_associative mult_right_one n_export n_sub_mult_zero n_top) lemma n_mult_zero: "n(x) = n(x ; 0)" by (smt add_commutative add_left_top add_right_zero mult_left_dist_add mult_right_one n_dist_add n_sub_mult_zero n_top) lemma n_mult_left_upper_bound: "n(x) \ n(x ; y)" by (metis mult_right_isotone n_isotone n_mult_zero zero_least) lemma n_mult_right_zero: "n(x) ; 0 = 0" by (metis add_left_top add_left_zero mult_left_one mult_right_one n_export n_dist_add n_sub_mult_zero n_top n_zero) lemma n_mult_n: "n(x ; n(y)) = n(x)" by (metis mult_associative n_mult_right_zero n_mult_zero) lemma n_mult_left_absorb_add: "n(x) ; (n(x) + n(y)) = n(x)" by (metis add_left_top mult_left_dist_add mult_right_one n_dist_add n_mult_idempotent n_top) lemma n_mult_right_absorb_add: "(n(x) + n(y)) ; n(y) = n(y)" by (smt add_commutative add_left_top mult_left_one mult_right_dist_add n_dist_add n_mult_idempotent n_top) lemma n_add_left_absorb_mult: "n(x) + n(x) ; n(y) = n(x)" by (metis add_left_top mult_left_dist_add mult_right_one n_dist_add n_top) lemma n_add_right_absorb_mult: "n(x) ; n(y) + n(y) = n(y)" by (metis less_eq_def mult_left_one mult_right_dist_add n_sub_one) lemma n_mult_commutative: "n(x) ; n(y) = n(y) ; n(x)" by (smt add_commutative mult_left_dist_add mult_right_dist_add n_add_left_absorb_mult n_add_right_absorb_mult n_export n_mult_idempotent) lemma n_add_left_dist_mult: "n(x) + n(y) ; n(z) = (n(x) + n(y)) ; (n(x) + n(z))" by (metis add_associative mult_left_dist_add mult_right_dist_add n_add_right_absorb_mult n_mult_commutative n_mult_left_absorb_add) lemma n_add_right_dist_mult: "n(x) ; n(y) + n(z) = (n(x) + n(z)) ; (n(y) + n(z))" by (metis add_commutative n_add_left_dist_mult) lemma n_order: "n(x) \ n(y) \ n(x) ; n(y) = n(x)" by (metis less_eq_def n_add_right_absorb_mult n_mult_left_absorb_add) lemma n_mult_left_lower_bound: "n(x) ; n(y) \ n(x)" by (metis add_right_upper_bound n_add_left_absorb_mult) lemma n_mult_right_lower_bound: "n(x) ; n(y) \ n(y)" by (metis n_mult_commutative n_mult_left_lower_bound) lemma n_mult_least_upper_bound: "n(x) \ n(y) \ n(x) \ n(z) \ n(x) \ n(y) ; n(z)" by (smt mult_associative n_export n_mult_left_lower_bound n_order) lemma n_mult_left_divisibility: "n(x) \ n(y) \ (\z . n(x) = n(y) ; n(z))" by (metis n_mult_commutative n_mult_left_lower_bound n_order) lemma n_mult_right_divisibility: "n(x) \ n(y) \ (\z . n(x) = n(z) ; n(y))" by (metis n_mult_commutative n_mult_left_divisibility) lemma n_one: "n(1) = 0" by (metis mult_left_one n_mult_zero n_zero) lemma n_split_equal: "x + n(x ; L) ; T = x ; 0 + n(x ; L) ; T" by (smt add_associative add_commutative less_eq_def n_split zero_right_mult_decreasing) lemma n_split_top: "x ; T \ x ; 0 + n(x ; L) ; T" by (smt mult_associative mult_left_isotone mult_left_zero mult_right_dist_add n_split top_mult_top) lemma n_L: "n(L) = 1" by (metis add_left_zero antisym mult_left_one n_export n_isotone n_mult_commutative n_split_top n_sub_one n_top) lemma n_split_L: "x ; L = x ; 0 + n(x ; L) ; L" by (metis mult_right_one n_L n_L_split) lemma n_n_L: "n(n(x) ; L) = n(x)" by (metis mult_right_one n_export n_L) lemma n_L_decreasing: "n(x) ; L \ x" by (metis add_left_isotone add_left_zero less_eq_def mult_associative mult_left_zero mult_right_isotone mult_right_one n_mult_zero n_split_L order_trans) lemma n_galois: "n(x) \ n(y) \ n(x) ; L \ y" by (metis less_eq_def mult_left_one mult_right_subdist_add_left n_export n_isotone n_L n_L_decreasing n_mult_commutative order_trans) lemma split_L: "x ; L \ x ; 0 + L" by (metis add_commutative add_left_isotone n_galois n_L n_split_L n_sub_one) lemma L_left_zero: "L ; x = L" by (metis add_right_zero less_eq_def mult_associative mult_left_one mult_left_subdist_add_right mult_left_zero mult_right_one n_L n_mult_left_upper_bound n_order n_split_L) lemma n_mult: "n(x ; n(y) ; L) = n(x ; y)" by (metis less_eq_def n_dist_add n_mult_left_upper_bound n_mult_zero n_n_L n_L_split) lemma n_mult_top: "n(x ; n(y) ; T) = n(x ; y)" by (metis mult_right_one n_mult n_top) lemma n_top_L: "n(x ; T) = n(x ; L)" by (metis mult_right_one n_L n_mult_top) lemma n_top_split: "x ; n(y) ; T \ x ; 0 + n(x ; y) ; T" by (metis mult_associative n_mult n_mult_right_zero n_split_top) lemma n_mult_right_upper_bound: "n(x ; y) \ n(z) \ n(x) \ n(z) \ x ; n(y) ; L \ x ; 0 + n(z) ; L" by (rule iffI, metis add_right_isotone eq_iff mult_isotone n_L_split n_mult_left_upper_bound order_trans, smt add_least_upper_bound less_eq_def mult_left_one n_export n_dist_add n_galois n_L n_L_split n_mult_commutative n_mult_zero) lemma n_preserves_equation: "n(y) ; x \ x ; n(y) \ n(y) ; x = n(y) ; x ; n(y)" by (smt antisym mult_associative mult_left_isotone mult_left_one mult_right_isotone mult_right_one n_mult_idempotent n_sub_one) definition ni :: "'a \ 'a" where "ni x = n(x) ; L" lemma ni_zero: "ni(0) = 0" by (metis mult_left_zero n_zero ni_def) lemma ni_one: "ni(1) = 0" by (metis mult_left_zero n_one ni_def) lemma ni_L: "ni(L) = L" by (metis mult_left_one n_L ni_def) lemma ni_top: "ni(T) = L" by (metis mult_left_one n_top ni_def) lemma ni_dist_add: "ni(x + y) = ni(x) + ni(y)" by (metis mult_right_dist_add n_dist_add ni_def) lemma ni_mult_zero: "ni(x) = ni(x ; 0)" by (metis n_mult_zero ni_def) lemma ni_split: "x ; ni(y) = x ; 0 + ni(x ; y)" by (metis mult_associative n_L_split ni_def) lemma ni_decreasing: "ni(x) \ x" by (metis n_L_decreasing ni_def) lemma ni_isotone: "x \ y \ ni(x) \ ni(y)" by (metis less_eq_def ni_dist_add) lemma ni_mult_left_upper_bound: "ni(x) \ ni(x ; y)" by (metis n_galois n_mult_left_upper_bound n_n_L ni_def) lemma ni_idempotent: "ni(ni(x)) = ni(x)" by (metis n_n_L ni_def) lemma ni_below_L: "ni(x) \ L" by (metis n_L n_galois n_sub_one ni_def) lemma ni_left_zero: "ni(x) ; y = ni(x)" by (metis L_left_zero mult_associative ni_def) lemma ni_split_L: "x ; L = x ; 0 + ni(x ; L)" by (metis n_split_L ni_def) lemma ni_top_L: "ni(x ; T) = ni(x ; L)" by (metis n_top_L ni_def) lemma ni_galois: "ni(x) \ ni(y) \ ni(x) \ y" by (metis n_galois n_n_L ni_def) lemma ni_mult: "ni(x ; ni(y)) = ni(x ; y)" by (metis mult_associative n_mult ni_def) lemma ni_n_order: "ni(x) \ ni(y) \ n(x) \ n(y)" by (metis n_galois n_n_L ni_def) lemma ni_n_equal: "ni(x) = ni(y) \ n(x) = n(y)" by (metis n_n_L ni_def) lemma ni_mult_right_upper_bound: "ni(x ; y) \ ni(z) \ ni(x) \ ni(z) \ x ; ni(y) \ x ; 0 + ni(z)" by (smt mult_associative n_mult_right_upper_bound ni_def ni_n_order) lemma n_ni: "n(ni(x)) = n(x)" by (metis n_n_L ni_def) lemma ni_n: "ni(n(x)) = 0" by (metis n_mult_right_zero ni_mult_zero ni_zero) lemma ni_n_galois: "n(x) \ n(y) \ ni(x) \ y" by (metis n_galois ni_def) lemma n_mult_ni: "n(x ; ni(y)) = n(x ; y)" by (metis mult_associative n_mult ni_def) lemma ni_mult_n: "ni(x ; n(y)) = ni(x)" by (metis n_mult_n ni_def) lemma ni_export: "ni(n(x) ; y) = n(x) ; ni(y)" by (metis mult_associative n_export ni_def) lemma ni_mult_top: "ni(x ; n(y) ; T) = ni(x ; y)" by (metis n_mult_top ni_def) lemma ni_n_zero: "ni(x) = 0 \ n(x) = 0" by (metis mult_left_zero n_ni n_zero ni_def) lemma ni_n_L: "ni(x) = L \ n(x) = 1" by (metis mult_left_one n_L n_n_L ni_def) end class itering_nL = itering_T + semiring_nL begin lemma mult_L_circ: "(x ; L)\<^sup>\ = 1 + x ; L" by (metis L_left_zero circ_mult mult_associative) lemma mult_L_circ_mult: "(x ; L)\<^sup>\ ; y = y + x ; L" by (metis L_left_zero mult_L_circ mult_associative mult_left_one mult_right_dist_add) lemma circ_L: "L\<^sup>\ = L + 1" by (metis L_left_zero add_commutative circ_left_unfold) lemma circ_n_L: "x\<^sup>\ ; n(x) ; L = x\<^sup>\ ; 0" by (smt antisym circ_increasing circ_transitive_equal mult_associative mult_right_isotone n_galois n_isotone n_mult_zero zero_least) lemma n_circ_left_unfold: "n(x\<^sup>\) = n(x ; x\<^sup>\)" by (metis circ_n_L circ_plus_same n_mult n_mult_zero) lemma ni_circ: "ni(x)\<^sup>\ = 1 + ni(x)" by (metis mult_L_circ ni_def) lemma circ_ni: "x\<^sup>\ ; ni(x) = x\<^sup>\ ; 0" by (metis circ_n_L mult_associative ni_def) lemma ni_circ_left_unfold: "ni(x\<^sup>\) = ni(x ; x\<^sup>\)" by (metis n_circ_left_unfold ni_def) lemma n_circ_import: "n(y) ; x \ x ; n(y) \ n(y) ; x\<^sup>\ = n(y) ; (n(y) ; x)\<^sup>\" by (rule, rule antisym, metis circ_simulate circ_slide mult_associative n_mult_idempotent n_preserves_equation, metis circ_isotone mult_left_isotone mult_left_one mult_right_isotone n_sub_one) end class omega_itering_nL = omega_itering + itering_nL + assumes circ_circ: "x\<^sup>\\<^sup>\ = L + x\<^sup>\" begin lemma L_below_one_circ: "L \ 1\<^sup>\" by (metis add_left_divisibility circ_circ circ_one) lemma circ_below_L_add_star: "x\<^sup>\ \ L + x\<^sup>\" by (metis circ_circ circ_increasing) lemma L_add_circ_add_star: "L + x\<^sup>\ = L + x\<^sup>\" by (smt add_associative add_commutative circ_below_L_add_star less_eq_def star_below_circ) lemma circ_one_L: "1\<^sup>\ = L + 1" by (metis L_add_circ_add_star L_below_one_circ less_eq_def star_one) lemma one_circ_zero: "L = 1\<^sup>\ ; 0" by (metis L_left_zero circ_L circ_ni circ_one_L circ_plus_same ni_L) lemma circ_not_simulate: "(\x y z . x ; z \ z ; y \ x\<^sup>\ ; z \ z ; y\<^sup>\) \ 1 = 0" by (metis L_left_zero circ_one_L eq_iff mult_left_one mult_left_zero mult_right_subdist_add_left n_L n_zero zero_least) lemma star_circ_L: "x\<^sup>\\<^sup>\ = L + x\<^sup>\" by (smt L_add_circ_add_star L_left_zero add_commutative circ_add_1 circ_mult_star circ_one_L circ_star star.circ_loop_fixpoint star.circ_plus_one star_sup_one) lemma circ_circ_2: "x\<^sup>\\<^sup>\ = L + x\<^sup>\" by (metis circ_star star_circ_L) lemma circ_add_6: "L + (x + y)\<^sup>\ = (x\<^sup>\ ; y\<^sup>\)\<^sup>\" using [[ smt_timeout = 120 ]] by (smt add_least_upper_bound add_left_upper_bound antisym circ_circ_2 circ_add_2 circ_add_3 circ_isotone circ_reflexive mult_left_isotone mult_left_one order_trans star.circ_increasing) lemma circ_add_7: "(x\<^sup>\ ; y\<^sup>\)\<^sup>\ = L + (x + y)\<^sup>\" by (metis L_add_circ_add_star circ_add_6) end class omega_algebra_nL = omega_algebra_T + semiring_nL + Omega + assumes Omega_def: "x\<^sup>\ = n(x\<^sup>\) ; L + x\<^sup>\" begin lemma mult_L_star: "(x ; L)\<^sup>\ = 1 + x ; L" by (metis L_left_zero mult_associative star_unfold_slide) lemma mult_L_omega: "(x ; L)\<^sup>\ = x ; L" by (metis L_left_zero omega_slide) lemma mult_L_add_star: "(x ; L + y)\<^sup>\ = y\<^sup>\ + y\<^sup>\ ; x ; L" by (metis L_left_zero add_commutative mult_L_star mult_associative mult_left_dist_add mult_right_one star.circ_add_1) lemma mult_L_add_omega: "(x ; L + y)\<^sup>\ = y\<^sup>\ + y\<^sup>\ ; x ; L" by (smt L_left_zero add_commutative add_left_upper_bound less_eq_def mult_L_omega mult_L_star mult_associative mult_left_one mult_right_dist_add omega_decompose) lemma mult_L_add_circ: "(x ; L + y)\<^sup>\ = n(y\<^sup>\) ; L + y\<^sup>\ + y\<^sup>\ ; x ; L" by (smt add_associative add_commutative Omega_def less_eq_def mult_L_add_omega mult_L_add_star mult_right_dist_add n_L_decreasing n_dist_add) lemma circ_add_n: "(x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\ = n((x\<^sup>\ ; y)\<^sup>\) ; L + ((x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\ + (x\<^sup>\ ; y)\<^sup>\ ; n(x\<^sup>\) ; L)" by (smt L_left_zero add_associative add_commutative Omega_def mult_L_add_circ mult_associative mult_left_dist_add mult_right_dist_add) lemma n_omega_induct: "n(y) \ n(x ; y + z) \ n(y) \ n(x\<^sup>\ + x\<^sup>\ ; z)" by (smt add_commutative mult_associative n_dist_add n_galois n_mult omega_induct) lemma n_Omega_circ_simulate_right_plus: "z ; x \ y ; y\<^sup>\ ; z + w \ z ; x\<^sup>\ \ y\<^sup>\ ; (z + w ; x\<^sup>\)" proof assume "z ; x \ y ; y\<^sup>\ ; z + w" hence 1: "z ; x \ n(y\<^sup>\) ; L + y ; y\<^sup>\ ; z + w" by (smt L_left_zero Omega_def add_associative add_commutative add_left_zero mult_associative mult_left_dist_add mult_right_dist_add n_L_split omega_unfold) hence "(n(y\<^sup>\) ; L + y\<^sup>\ ; z + y\<^sup>\ ; w ; n(x\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\) ; x \ n(y\<^sup>\) ; L + y\<^sup>\ ; (n(y\<^sup>\) ; L + y ; y\<^sup>\ ; z + w) + y\<^sup>\ ; w ; n(x\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\" by (smt L_left_zero add_associative add_left_upper_bound add_right_upper_bound less_eq_def mult_associative mult_left_dist_add mult_right_dist_add star.circ_back_loop_fixpoint) also have "... = n(y\<^sup>\) ; L + y\<^sup>\ ; y ; y\<^sup>\ ; z + y\<^sup>\ ; w ; n(x\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\" by (smt add_associative add_commutative add_idempotent mult_associative mult_left_dist_add n_L_split star.circ_back_loop_fixpoint star_mult_omega) also have "... \ n(y\<^sup>\) ; L + y\<^sup>\ ; z + y\<^sup>\ ; w ; n(x\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\" by (metis add_left_isotone add_right_isotone mult_left_isotone star.circ_plus_same star.circ_transitive_equal star.left_plus_below_circ) finally have 2: "z ; x\<^sup>\ \ n(y\<^sup>\) ; L + y\<^sup>\ ; z + y\<^sup>\ ; w ; n(x\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\" by (smt add_least_upper_bound add_left_upper_bound star.circ_loop_fixpoint star_right_induct) have "n(z ; x ; x\<^sup>\) \ n(y ; y\<^sup>\ ; z ; x\<^sup>\ + n(y\<^sup>\) ; L + w ; x\<^sup>\)" using 1 by (smt L_left_zero add_commutative mult_associative mult_left_isotone mult_right_dist_add n_isotone) hence "n(z ; x\<^sup>\) \ n(y\<^sup>\ + y\<^sup>\ ; w ; x\<^sup>\)" by (smt add_associative add_commutative left_plus_omega less_eq_def mult_associative mult_left_dist_add n_L_decreasing n_omega_induct omega_unfold star.left_plus_circ star_mult_omega) hence "n(z ; x\<^sup>\) ; L \ n(y\<^sup>\) ; L + y\<^sup>\ ; w ; n(x\<^sup>\) ; L" by (smt add_right_isotone eq_iff mult_right_dist_add n_dist_add n_galois n_mult order_trans) hence "z ; n(x\<^sup>\) ; L \ z ; 0 + n(y\<^sup>\) ; L + y\<^sup>\ ; w ; n(x\<^sup>\) ; L" by (metis add_associative add_right_isotone n_L_split) hence "z ; n(x\<^sup>\) ; L \ n(y\<^sup>\) ; L + y\<^sup>\ ; z + y\<^sup>\ ; w ; n(x\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\" by (smt add_commutative add_left_isotone add_left_upper_bound order_trans star.circ_loop_fixpoint zero_right_mult_decreasing) thus "z ; x\<^sup>\ \ y\<^sup>\ ; (z + w ; x\<^sup>\)" using 2 by (smt L_left_zero Omega_def add_associative less_eq_def mult_associative mult_left_dist_add mult_right_dist_add) qed lemma n_Omega_circ_simulate_left_plus: "x ; z \ z ; y\<^sup>\ + w \ x\<^sup>\ ; z \ (z + x\<^sup>\ ; w) ; y\<^sup>\" proof assume 1: "x ; z \ z ; y\<^sup>\ + w" have "x ; (z ; n(y\<^sup>\) ; L + z ; y\<^sup>\ + n(x\<^sup>\) ; L + x\<^sup>\ ; w ; n(y\<^sup>\) ; L + x\<^sup>\ ; w ; y\<^sup>\) = x ; z ; n(y\<^sup>\) ; L + x ; z ; y\<^sup>\ + n(x\<^sup>\) ; L + x ; x\<^sup>\ ; w ; n(y\<^sup>\) ; L + x ; x\<^sup>\ ; w ; y\<^sup>\" by (smt add_associative add_commutative mult_associative mult_left_dist_add n_L_split omega_unfold) also have "... \ (z ; n(y\<^sup>\) ; L + z ; y\<^sup>\ + w) ; n(y\<^sup>\) ; L + (z ; n(y\<^sup>\) ; L + z ; y\<^sup>\ + w) ; y\<^sup>\ + n(x\<^sup>\) ; L + x\<^sup>\ ; w ; n(y\<^sup>\) ; L + x\<^sup>\ ; w ; y\<^sup>\" using 1 by (smt Omega_def add_associative add_right_upper_bound less_eq_def mult_associative mult_left_dist_add mult_right_dist_add star.circ_loop_fixpoint) also have "... = z ; n(y\<^sup>\) ; L + z ; y\<^sup>\ ; n(y\<^sup>\) ; L + w ; n(y\<^sup>\) ; L + z ; y\<^sup>\ + w ; y\<^sup>\ + n(x\<^sup>\) ; L + x\<^sup>\ ; w ; n(y\<^sup>\) ; L + x\<^sup>\ ; w ; y\<^sup>\" by (smt L_left_zero add_associative add_commutative add_idempotent mult_associative mult_right_dist_add star.circ_transitive_equal) also have "... = z ; n(y\<^sup>\) ; L + w ; n(y\<^sup>\) ; L + z ; y\<^sup>\ + w ; y\<^sup>\ + n(x\<^sup>\) ; L + x\<^sup>\ ; w ; n(y\<^sup>\) ; L + x\<^sup>\ ; w ; y\<^sup>\" by (smt add_associative add_commutative add_idempotent less_eq_def mult_associative n_L_split star_mult_omega zero_right_mult_decreasing) finally have "x ; (z ; n(y\<^sup>\) ; L + z ; y\<^sup>\ + n(x\<^sup>\) ; L + x\<^sup>\ ; w ; n(y\<^sup>\) ; L + x\<^sup>\ ; w ; y\<^sup>\) \ z ; n(y\<^sup>\) ; L + z ; y\<^sup>\ + n(x\<^sup>\) ; L + x\<^sup>\ ; w ; n(y\<^sup>\) ; L + x\<^sup>\ ; w ; y\<^sup>\" by (smt add_associative add_commutative add_idempotent mult_associative star.circ_loop_fixpoint) thus "x\<^sup>\ ; z \ (z + x\<^sup>\ ; w) ; y\<^sup>\" by (smt L_left_zero Omega_def add_associative add_least_upper_bound add_left_upper_bound mult_associative mult_left_dist_add mult_right_dist_add star.circ_back_loop_fixpoint star_left_induct) qed end sublocale omega_algebra_nL < nL_omega!: omega_itering_nL where circ = Omega apply unfold_locales apply (smt L_left_zero add_associative add_commutative add_left_zero Omega_def mult_associative mult_left_dist_add mult_right_dist_add n_L_split omega_slide star_unfold_slide) apply (smt add_associative add_commutative add_left_zero circ_add_n Omega_def mult_left_dist_add mult_right_dist_add n_L_split n_dist_add omega_decompose star.circ_add_1 star.circ_slide) apply (smt L_left_zero add_associative add_commutative add_isotone add_left_zero Omega_def mult_associative mult_left_dist_add mult_left_isotone mult_right_dist_add n_L_split n_isotone omega_simulation star_simulation_right) apply (smt n_Omega_circ_simulate_right_plus Omega_def add_left_isotone add_right_upper_bound mult_left_isotone mult_right_isotone order_trans star.circ_back_loop_fixpoint) apply (smt Omega_def add_commutative add_least_upper_bound add_right_isotone mult_right_isotone n_Omega_circ_simulate_left_plus order_trans star.circ_increasing) apply (metis n_Omega_circ_simulate_right_plus) apply (metis n_Omega_circ_simulate_left_plus) by (smt Omega_def add_associative add_commutative less_eq_def mult_L_add_star mult_left_one n_L_split n_top ni_below_L ni_def star_involutive star_mult_omega star_omega_top zero_right_mult_decreasing) sublocale omega_algebra_nL < nL_star!: omega_itering where circ = star .. context omega_algebra_nL begin lemma circ_add_8: "n((x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\) ; L \ (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" by (metis add_left_upper_bound nL_omega.circ_add_4 Omega_def mult_left_isotone n_isotone omega_sum_unfold_3 order_trans) lemma n_split_omega_omega: "x\<^sup>\ \ x\<^sup>\ ; 0 + n(x\<^sup>\) ; T" by (metis n_split n_top_L omega_vector) lemma n_star_below_n_omega: "n(x\<^sup>\) \ n(x\<^sup>\)" by (metis n_mult_left_upper_bound star_mult_omega) lemma n_below_n_omega: "n(x) \ n(x\<^sup>\)" by (metis n_mult_left_upper_bound omega_unfold) lemma star_n_L: "x\<^sup>\ ; n(x) ; L = x\<^sup>\ ; 0" by (smt antisym mult_associative mult_right_isotone n_galois n_isotone n_mult_zero star.circ_increasing star.circ_transitive_equal zero_least) lemma star_L_split: "y \ z \ x ; z ; L \ x ; 0 + z ; L \ x\<^sup>\ ; y ; L \ x\<^sup>\ ; 0 + z ; L" by (smt add_least_upper_bound add_left_isotone star.left_plus_below_circ mult_associative mult_left_dist_add mult_left_isotone order_trans star.circ_increasing star_left_induct) lemma star_L_split_same: "x ; y ; L \ x ; 0 + y ; L \ x\<^sup>\ ; y ; L = x\<^sup>\ ; 0 + y ; L" by (smt add_associative add_left_zero antisym less_eq_def mult_associative mult_left_dist_add mult_left_one mult_right_subdist_add_left order_refl star_L_split star.circ_right_unfold) lemma star_n_L_split_equal: "n(x ; y) \ n(y) \ x\<^sup>\ ; n(y) ; L = x\<^sup>\ ; 0 + n(y) ; L" by (metis n_mult_right_upper_bound star_L_split_same) lemma n_star_mult: "n(x ; y) \ n(y) \ n(x\<^sup>\ ; y) = n(x\<^sup>\) + n(y)" by (metis n_dist_add n_mult n_mult_zero n_n_L star_n_L_split_equal) lemma n_omega_mult: "n(x\<^sup>\ ; y) = n(x\<^sup>\)" by (smt add_commutative less_eq_def n_dist_add n_mult_left_upper_bound omega_sub_vector) lemma n_star_left_unfold: "n(x\<^sup>\) = n(x ; x\<^sup>\)" by (metis n_mult n_mult_zero star.circ_plus_same star_n_L) lemma ni_star_below_ni_omega: "ni(x\<^sup>\) \ ni(x\<^sup>\)" by (metis n_star_below_n_omega ni_n_order) lemma ni_below_ni_omega: "ni(x) \ ni(x\<^sup>\)" by (metis n_below_n_omega ni_n_order) lemma ni_star: "ni(x)\<^sup>\ = 1 + ni(x)" by (metis mult_L_star ni_def) lemma ni_omega: "ni(x)\<^sup>\ = ni(x)" by (metis mult_L_omega ni_def) lemma ni_omega_induct: "ni(y) \ ni(x ; y + z) \ ni(y) \ ni(x\<^sup>\ + x\<^sup>\ ; z)" by (metis n_omega_induct ni_n_order) lemma star_ni: "x\<^sup>\ ; ni(x) = x\<^sup>\ ; 0" by (metis mult_associative ni_def star_n_L) lemma star_ni_split_equal: "ni(x ; y) \ ni(y) \ x\<^sup>\ ; ni(y) = x\<^sup>\ ; 0 + ni(y)" by (metis mult_associative ni_def ni_n_order star_n_L_split_equal) lemma ni_star_mult: "ni(x ; y) \ ni(y) \ ni(x\<^sup>\ ; y) = ni(x\<^sup>\) + ni(y)" by (metis n_dist_add n_star_mult ni_dist_add ni_n_equal ni_n_order) lemma ni_omega_mult: "ni(x\<^sup>\ ; y) = ni(x\<^sup>\)" by (metis n_omega_mult ni_def) lemma ni_star_left_unfold: "ni(x\<^sup>\) = ni(x ; x\<^sup>\)" by (metis n_star_left_unfold ni_def) lemma n_star_import: "n(y) ; x \ x ; n(y) \ n(y) ; x\<^sup>\ = n(y) ; (n(y) ; x)\<^sup>\" apply (rule impI, rule antisym) defer apply (metis mult_left_isotone mult_left_one mult_right_isotone n_sub_one star.circ_isotone) proof - assume "n(y) ; x \ x ; n(y)" hence "n(y) ; (n(y) ; x)\<^sup>\ ; x \ n(y) ; (n(y) ; x)\<^sup>\" by (smt mult_associative mult_isotone n_order order_refl order_trans star.right_plus_below_circ star.circ_isotone star.circ_slide) thus "n(y) ; x\<^sup>\ \ n(y) ; (n(y) ; x)\<^sup>\" by (smt add_associative less_eq_def mult_left_dist_add mult_right_one star.circ_plus_one star_right_induct) qed lemma n_omega_export: "n(y) ; x \ x ; n(y) \ n(y) ; x\<^sup>\ = (n(y) ; x)\<^sup>\" apply (rule impI, rule antisym) apply (metis mult_associative mult_right_isotone n_mult_idempotent omega_simulation) by (metis mult_right_isotone mult_right_one n_sub_one omega_isotone omega_slide) lemma n_omega_import: "n(y) ; x \ x ; n(y) \ n(y) ; x\<^sup>\ = n(y) ; (n(y) ; x)\<^sup>\" by (metis mult_associative n_order n_omega_export order_refl) lemma star_n_omega_top: "x\<^sup>\ ; n(x\<^sup>\) ; T = x\<^sup>\ ; 0 + n(x\<^sup>\) ; T" by (smt add_least_upper_bound add_right_divisibility antisym mult_associative nL_star.circ_mult_omega nL_star.star_zero_below_circ_mult n_top_split star.circ_loop_fixpoint) end class anL = nL + fixes an :: "'a \ 'a" class semiring_anL = semiring_T + anL + neg + assumes an_complement: "an(x) + n(x) = 1" assumes an_dist_add : "an(x + y) = an(x) ; an(y)" assumes an_export : "an(an(x) ; y) = n(x) + an(y)" assumes an_mult_zero : "an(x) = an(x ; 0)" assumes an_L_split : "x ; n(y) ; L = x ; 0 + n(x ; y) ; L" assumes an_split : "an(x ; L) ; x \ x ; 0" assumes an_uminus : "-x = an(x ; L)" begin lemma n_an_def: "n(x) = an(an(x) ; L)" by (metis add_right_zero an_export an_split antisym mult_left_one mult_right_one zero_least) lemma an_complement_zero: "an(x) ; n(x) = 0" by (smt add_commutative an_dist_add an_split antisym mult_left_zero n_an_def zero_least) lemma an_n_def: "an(x) = n(an(x) ; L)" by (smt add_commutative an_complement an_complement_zero mult_left_dist_add mult_right_dist_add mult_right_one n_an_def) lemma an_case_split_left: "an(z) ; x \ y \ n(z) ; x \ y \ x \ y" by (metis add_least_upper_bound an_complement mult_left_one mult_right_dist_add) lemma an_case_split_right: "x ; an(z) \ y \ x ; n(z) \ y \ x \ y" by (metis add_least_upper_bound an_complement mult_right_one mult_left_dist_add) subclass semiring_nL by (unfold_locales, metis add_left_zero an_complement_zero an_dist_add n_an_def, metis add_left_top an_complement an_dist_add an_export mult_associative n_an_def, metis an_dist_add an_export mult_associative n_an_def, metis an_dist_add an_export an_n_def mult_right_dist_add n_an_def, metis add_idempotent an_dist_add an_mult_zero n_an_def, metis an_L_split, smt add_left_upper_bound add_right_upper_bound an_case_split_left an_split mult_right_isotone order_trans top_greatest) lemma n_complement_zero: "n(x) ; an(x) = 0" by (metis an_complement_zero an_n_def n_an_def) lemma an_zero: "an(0) = 1" by (metis add_right_zero an_complement n_zero) lemma an_one: "an(1) = 1" by (metis add_right_zero an_complement n_one) lemma an_L: "an(L) = 0" by (metis mult_left_one n_L n_complement_zero) lemma an_top: "an(T) = 0" by (metis mult_left_one n_complement_zero n_top) lemma an_export_n: "an(n(x) ; y) = an(x) + an(y)" by (metis an_export an_n_def n_an_def) lemma n_export_an: "n(an(x) ; y) = an(x) ; n(y)" by (metis an_n_def n_export) lemma n_an_mult_commutative: "n(x) ; an(y) = an(y) ; n(x)" by (metis add_commutative an_dist_add n_an_def) lemma an_mult_commutative: "an(x) ; an(y) = an(y) ; an(x)" by (metis add_commutative an_dist_add) lemma an_mult_idempotent: "an(x) ; an(x) = an(x)" by (metis add_idempotent an_dist_add) lemma an_sub_one: "an(x) \ 1" by (metis add_left_upper_bound an_complement) lemma an_antitone: "x \ y \ an(y) \ an(x)" by (metis an_dist_add an_sub_one less_eq_def mult_right_isotone mult_right_one) lemma an_mult_left_upper_bound: "an(x ; y) \ an(x)" by (metis an_antitone an_mult_zero mult_right_isotone zero_least) lemma an_mult_right_zero: "an(x) ; 0 = 0" by (metis an_n_def n_mult_right_zero) lemma n_mult_an: "n(x ; an(y)) = n(x)" by (metis an_n_def n_mult_n) lemma an_mult_n: "an(x ; n(y)) = an(x)" by (metis an_n_def n_an_def n_mult_n) lemma an_mult_an: "an(x ; an(y)) = an(x)" by (metis an_mult_n an_n_def) lemma an_mult_left_absorb_add: "an(x) ; (an(x) + an(y)) = an(x)" by (metis an_n_def n_mult_left_absorb_add) lemma an_mult_right_absorb_add: "(an(x) + an(y)) ; an(y) = an(y)" by (metis add_commutative an_export_n an_mult_commutative an_mult_left_absorb_add) lemma an_add_left_absorb_mult: "an(x) + an(x) ; an(y) = an(x)" by (metis an_n_def n_add_left_absorb_mult) lemma an_add_right_absorb_mult: "an(x) ; an(y) + an(y) = an(y)" by (metis add_commutative an_add_left_absorb_mult an_mult_commutative) lemma an_add_left_dist_mult: "an(x) + an(y) ; an(z) = (an(x) + an(y)) ; (an(x) + an(z))" by (metis an_dist_add an_export_n mult_left_dist_add) lemma an_add_right_dist_mult: "an(x) ; an(y) + an(z) = (an(x) + an(z)) ; (an(y) + an(z))" by (metis add_commutative an_add_left_dist_mult) lemma an_n_order: "an(x) \ an(y) \ n(y) \ n(x)" by (smt add_commutative an_dist_add an_mult_left_absorb_add an_n_def less_eq_def n_an_def n_dist_add) lemma an_order: "an(x) \ an(y) \ an(x) ; an(y) = an(x)" by (metis an_add_right_absorb_mult an_mult_left_absorb_add less_eq_def) lemma an_mult_left_lower_bound: "an(x) ; an(y) \ an(x)" by (metis add_left_upper_bound an_antitone an_dist_add) lemma an_mult_right_lower_bound: "an(x) ; an(y) \ an(y)" by (metis an_add_right_absorb_mult less_eq_def) lemma an_n_mult_left_lower_bound: "an(x) ; n(y) \ an(x)" by (metis an_mult_left_lower_bound n_an_def) lemma an_n_mult_right_lower_bound: "an(x) ; n(y) \ n(y)" by (metis an_mult_right_lower_bound n_an_def) lemma n_an_mult_left_lower_bound: "n(x) ; an(y) \ n(x)" by (metis an_mult_left_lower_bound n_an_def) lemma n_an_mult_right_lower_bound: "n(x) ; an(y) \ an(y)" by (metis an_mult_right_lower_bound n_an_def) lemma an_mult_least_upper_bound: "an(x) \ an(y) \ an(x) \ an(z) \ an(x) \ an(y) ; an(z)" by (smt an_dist_add an_mult_left_lower_bound an_order mult_associative) lemma an_mult_left_divisibility: "an(x) \ an(y) \ (\z . an(x) = an(y) ; an(z))" by (metis an_mult_commutative an_mult_left_lower_bound an_order) lemma an_mult_right_divisibility: "an(x) \ an(y) \ (\z . an(x) = an(z) ; an(y))" by (metis an_mult_commutative an_mult_left_divisibility) lemma an_split_top: "an(x ; L) ; x ; T \ x ; 0" by (metis an_split mult_associative mult_left_isotone mult_left_zero) lemma an_n_L: "an(n(x) ; L) = an(x)" by (metis an_n_def n_an_def) lemma an_galois: "an(y) \ an(x) \ n(x) ; L \ y" by (metis an_n_order n_galois) lemma an_mult: "an(x ; n(y) ; L) = an(x ; y)" by (metis an_n_L n_mult) lemma n_mult_top: "an(x ; n(y) ; T) = an(x ; y)" by (metis an_n_L n_mult_top) lemma an_n_equal: "an(x) = an(y) \ n(x) = n(y)" by (metis an_n_L n_an_def) lemma an_top_L: "an(x ; T) = an(x ; L)" by (metis an_n_equal n_top_L) lemma an_case_split_left_equal: "an(z) ; x = an(z) ; y \ n(z) ; x = n(z) ; y \ x = y" by (metis an_complement case_split_left_equal) lemma an_case_split_right_equal: "x ; an(z) = y ; an(z) \ x ; n(z) = y ; n(z) \ x = y" by (metis an_complement case_split_right_equal) lemma an_equal_complement: "n(x) + an(y) = 1 \ n(x) ; an(y) = 0 \ an(x) = an(y)" by (metis add_commutative an_complement an_dist_add mult_left_one mult_right_dist_add n_complement_zero) lemma n_equal_complement: "n(x) + an(y) = 1 \ n(x) ; an(y) = 0 \ n(x) = n(y)" by (metis an_equal_complement n_an_def) lemma an_shunting: "an(z) ; x \ y \ x \ y + n(z) ; T" by (rule iffI, smt add_left_upper_bound add_right_upper_bound an_case_split_left mult_right_isotone order_trans top_greatest, metis add_right_zero an_case_split_left an_complement_zero mult_associative mult_left_dist_add mult_left_zero mult_right_isotone order_refl order_trans) lemma an_shunting_an: "an(z) ; an(x) \ an(y) \ an(x) \ n(z) + an(y)" by (smt add_left_upper_bound add_left_zero add_right_upper_bound an_case_split_left an_complement_zero mult_left_dist_add mult_right_isotone n_an_mult_left_lower_bound order_trans) lemma an_L_zero: "an(x ; L) ; x = an(x ; L) ; x ; 0" by (smt an_order an_split antisym mult_associative mult_right_isotone order_refl zero_right_mult_decreasing) lemma n_plus_complement_intro_n: "n(x) + an(x) ; n(y) = n(x) + n(y)" by (metis add_commutative an_complement an_n_def mult_right_one n_add_right_dist_mult n_an_mult_commutative) lemma n_plus_complement_intro_an: "n(x) + an(x) ; an(y) = n(x) + an(y)" by (metis an_n_def n_plus_complement_intro_n) lemma an_plus_complement_intro_n: "an(x) + n(x) ; n(y) = an(x) + n(y)" by (metis an_n_def n_an_def n_plus_complement_intro_n) lemma an_plus_complement_intro_an: "an(x) + n(x) ; an(y) = an(x) + an(y)" by (metis an_n_def an_plus_complement_intro_n) lemma n_mult_complement_intro_n: "n(x) ; (an(x) + n(y)) = n(x) ; n(y)" by (metis add_left_zero mult_left_dist_add n_complement_zero) lemma n_mult_complement_intro_an: "n(x) ; (an(x) + an(y)) = n(x) ; an(y)" by (metis add_left_zero mult_left_dist_add n_complement_zero) lemma an_mult_complement_intro_n: "an(x) ; (n(x) + n(y)) = an(x) ; n(y)" by (metis add_left_zero an_complement_zero mult_left_dist_add) lemma an_mult_complement_intro_an: "an(x) ; (n(x) + an(y)) = an(x) ; an(y)" by (metis add_left_zero an_complement_zero mult_left_dist_add) lemma an_preserves_equation: "an(y) ; x \ x ; an(y) \ an(y) ; x = an(y) ; x ; an(y)" by (metis an_n_def n_preserves_equation) (* lemma wnf_lemma_1: "(n(p;L) ; n(q;L) + an(p;L) ; an(r;L)) ; n(p;L) = n(p;L) ; n(q;L)" by (smt add_commutative an_n_def n_add_left_absorb_mult n_add_right_dist_mult n_export n_mult_commutative n_mult_complement_intro_n) lemma wnf_lemma_2: "(n(p;L) ; n(q;L) + an(r;L) ; an(q;L)) ; n(q;L) = n(p;L) ; n(q;L)" by (metis an_mult_commutative n_mult_commutative wnf_lemma_1) lemma wnf_lemma_3: "(n(p;L) ; n(r;L) + an(p;L) ; an(q;L)) ; an(p;L) = an(p;L) ; an(q;L)" by (smt an_add_right_dist_mult an_n_def n_add_left_absorb_mult n_an_def n_an_mult_commutative n_export n_mult_complement_intro_n n_plus_complement_intro_an) lemma wnf_lemma_4: "(n(r;L) ; n(q;L) + an(p;L) ; an(q;L)) ; an(q;L) = an(p;L) ; an(q;L)" by (metis an_mult_commutative n_mult_commutative wnf_lemma_3) lemma wnf_lemma_5: "n(p+q) ; (n(q) ; x + an(q) ; y) = n(q) ; x + an(q) ; n(p) ; y" by (smt add_right_zero mult_associative mult_left_dist_add n_an_mult_commutative n_complement_zero n_dist_add n_mult_right_absorb_add) *) definition ani :: "'a \ 'a" where "ani x = an(x) ; L" lemma ani_zero: "ani(0) = L" by (metis an_zero ani_def mult_left_one) lemma ani_one: "ani(1) = L" by (metis an_one ani_def mult_left_one) lemma ani_L: "ani(L) = 0" by (metis an_L ani_def mult_left_zero) lemma ani_top: "ani(T) = 0" by (metis an_top ani_def mult_left_zero) lemma ani_complement: "ani(x) + ni(x) = L" by (metis an_complement ani_def mult_right_dist_add n_top ni_def ni_top) lemma ani_mult_zero: "ani(x) = ani(x ; 0)" by (metis an_mult_zero ani_def) lemma ani_antitone: "y \ x \ ani(x) \ ani(y)" by (metis an_antitone ani_def mult_left_isotone) lemma ani_mult_left_upper_bound: "ani(x ; y) \ ani(x)" by (metis an_mult_left_upper_bound ani_def mult_left_isotone) lemma ani_involutive: "ani(ani(x)) = ni(x)" by (metis ani_def n_an_def ni_def) lemma ani_below_L: "ani(x) \ L" by (metis add_left_upper_bound ani_complement) lemma ani_left_zero: "ani(x) ; y = ani(x)" by (metis L_left_zero ani_def mult_associative) lemma ani_top_L: "ani(x ; T) = ani(x ; L)" by (metis an_top_L ani_def) lemma ani_ni_order: "ani(x) \ ani(y) \ ni(y) \ ni(x)" by (metis an_galois an_n_L an_n_def ani_def mult_left_isotone n_isotone ni_def) lemma ani_ni_equal: "ani(x) = ani(y) \ ni(x) = ni(y)" by (metis ani_ni_order antisym order_refl) lemma ni_ani: "ni(ani(x)) = ani(x)" by (metis an_n_def ani_def ni_def) lemma ani_ni: "ani(ni(x)) = ani(x)" by (metis ani_ni_equal ni_idempotent) lemma ani_mult: "ani(x ; ni(y)) = ani(x ; y)" by (metis ani_ni_equal ni_mult) lemma ani_an_order: "ani(x) \ ani(y) \ an(x) \ an(y)" by (metis an_n_order ani_ni_order ni_n_order) lemma ani_an_equal: "ani(x) = ani(y) \ an(x) = an(y)" by (metis an_n_def ani_def) lemma n_mult_ani: "n(x) ; ani(x) = 0" by (smt an_complement an_export_n an_zero ani_def ani_ni_equal n_an_def ni_ani ni_export ni_zero) lemma an_mult_ni: "an(x) ; ni(x) = 0" by (metis an_n_def ani_def n_an_def n_mult_ani ni_def) lemma n_mult_ni: "n(x) ; ni(x) = ni(x)" by (metis n_export n_order ni_def ni_export order_refl) lemma an_mult_ani: "an(x) ; ani(x) = ani(x)" by (metis an_n_def ani_def n_mult_ni ni_def) lemma ani_ni_meet: "x \ ani(y) \ x \ ni(y) \ x = 0" by (metis an_case_split_left an_mult_ni antisym less_eq_def mult_left_subdist_add_left n_mult_ani zero_least) lemma ani_galois: "ani(x) \ y \ ni(x + y) = L" by (metis add_commutative an_L an_complement an_dist_add an_n_def an_shunting_an ani_def less_eq_def mult_left_one n_an_def ni_def ni_n_galois zero_least) lemma an_ani: "an(ani(x)) = n(x)" by (metis ani_def n_an_def) lemma n_ani: "n(ani(x)) = an(x)" by (metis an_n_def ani_def) lemma an_ni: "an(ni(x)) = an(x)" by (metis an_n_L ni_def) lemma ani_an: "ani(an(x)) = L" by (metis an_mult_right_zero an_mult_zero an_zero ani_def mult_left_one) lemma ani_n: "ani(n(x)) = L" by (metis an_ani ani_an) lemma ni_an: "ni(an(x)) = 0" by (metis n_ani ni_n) lemma ani_mult_n: "ani(x ; n(y)) = ani(x)" by (metis an_mult_n ani_an_equal) lemma ani_mult_an: "ani(x ; an(y)) = ani(x)" by (metis an_mult_an ani_def) lemma ani_export_n: "ani(n(x) ; y) = ani(x) + ani(y)" by (metis an_export_n ani_def mult_right_dist_add) lemma ani_export_an: "ani(an(x) ; y) = ni(x) + ani(y)" by (metis an_export ani_def mult_right_dist_add ni_def) lemma ni_export_an: "ni(an(x) ; y) = an(x) ; ni(y)" by (metis an_n_def ni_export) lemma ani_mult_top: "ani(x ; n(y) ; T) = ani(x ; y)" by (metis ani_ni_equal ni_mult_top) lemma ani_an_zero: "ani(x) = 0 \ an(x) = 0" by (metis ani_def mult_left_zero n_ani n_zero) lemma ani_an_L: "ani(x) = L \ an(x) = 1" by (metis ani_def mult_left_one n_L n_ani) subclass tests apply unfold_locales apply (metis mult_associative) apply (metis an_mult_commutative an_uminus) apply (smt an_add_left_dist_mult an_export_n an_n_L an_uminus n_an_def n_complement_zero n_export) apply (metis an_dist_add an_n_def an_uminus n_an_def) apply (rule the_equality[THEN sym], metis an_complement_zero an_uminus n_an_def, metis an_L an_uminus mult_left_one mult_left_zero) apply (metis an_uminus an_zero mult_left_zero) apply (metis an_export_n an_n_L an_uminus n_an_def n_export) apply (metis an_order an_uminus) by (metis less_def) end class itering_anL = itering_nL + semiring_anL begin subclass while .. lemma an_circ_left_unfold: "an(x\<^sup>\) = an(x ; x\<^sup>\)" by (metis an_dist_add an_one circ_left_unfold mult_left_one) lemma an_circ_x_n_circ: "an(x\<^sup>\) ; x ; n(x\<^sup>\) \ x ; 0" by (metis an_circ_left_unfold an_mult an_split mult_associative n_mult_right_zero) lemma an_circ_invariant: "an(x\<^sup>\) ; x \ x ; an(x\<^sup>\)" by (smt add_left_zero an_case_split_left an_case_split_right an_circ_x_n_circ less_eq_def mult_isotone order_refl order_trans) lemma ani_circ: "ani(x)\<^sup>\ = 1 + ani(x)" by (metis ani_left_zero circ_plus_same circ_right_unfold) lemma ani_circ_left_unfold: "ani(x\<^sup>\) = ani(x ; x\<^sup>\)" by (metis an_circ_left_unfold ani_def) lemma an_circ_import: "an(y) ; x \ x ; an(y) \ an(y) ; x\<^sup>\ = an(y) ; (an(y) ; x)\<^sup>\" by (metis an_n_def n_circ_import) lemma preserves_L: "preserves L (-p)" by (metis L_left_zero mult_associative preserves_equation_test) end class omega_algebra_anL = omega_algebra_nL + semiring_anL begin lemma an_split_omega_omega: "an(x\<^sup>\) ; x\<^sup>\ \ x\<^sup>\ ; 0" by (metis an_split an_top_L omega_vector) lemma an_omega_below_an_star: "an(x\<^sup>\) \ an(x\<^sup>\)" by (metis an_n_order n_star_below_n_omega) lemma an_omega_below_an: "an(x\<^sup>\) \ an(x)" by (metis an_n_order n_below_n_omega) lemma an_omega_induct: "an(x ; y + z) \ an(y) \ an(x\<^sup>\ + x\<^sup>\ ; z) \ an(y)" by (metis an_n_order n_omega_induct) lemma an_star_mult: "an(y) \ an(x ; y) \ an(x\<^sup>\ ; y) = an(x\<^sup>\) ; an(y)" by (smt an_dist_add an_export_n an_n_equal less_eq_def n_dist_add n_export n_mult_left_lower_bound n_star_mult) lemma an_omega_mult: "an(x\<^sup>\ ; y) = an(x\<^sup>\)" by (metis an_n_equal n_omega_mult) lemma an_star_left_unfold: "an(x\<^sup>\) = an(x ; x\<^sup>\)" by (metis an_n_equal n_star_left_unfold) lemma an_star_x_n_star: "an(x\<^sup>\) ; x ; n(x\<^sup>\) \ x ; 0" by (metis add_right_zero an_case_split_left an_complement_zero mult_associative mult_left_zero n_export_an n_mult n_mult_right_zero n_split n_star_left_unfold order_refl order_trans) lemma an_star_invariant: "an(x\<^sup>\) ; x \ x ; an(x\<^sup>\)" by (smt add_left_zero an_case_split_left an_case_split_right an_star_x_n_star less_eq_def mult_isotone order_refl order_trans) lemma n_an_star_unfold_invariant: "n(an(x\<^sup>\) ; x\<^sup>\) \ an(x) ; n(x ; an(x\<^sup>\) ; x\<^sup>\)" proof - have "n(an(x\<^sup>\) ; x\<^sup>\) \ an(x)" by (metis an_antitone an_n_mult_left_lower_bound n_export_an order_trans star.circ_increasing) thus ?thesis by (smt an_star_invariant less_eq_def mult_associative mult_right_dist_add n_isotone n_order omega_unfold) qed lemma ani_omega_below_ani_star: "ani(x\<^sup>\) \ ani(x\<^sup>\)" by (metis an_omega_below_an_star ani_an_order) lemma ani_omega_below_ani: "ani(x\<^sup>\) \ ani(x)" by (metis an_omega_below_an ani_an_order) lemma ani_star: "ani(x)\<^sup>\ = 1 + ani(x)" by (metis mult_L_star ani_def) lemma ani_omega: "ani(x)\<^sup>\ = ani(x) ; L" by (metis mult_L_omega ani_def ani_left_zero) lemma ani_omega_induct: "ani(x ; y + z) \ ani(y) \ ani(x\<^sup>\ + x\<^sup>\ ; z) \ ani(y)" by (metis an_omega_induct ani_an_order) lemma ani_omega_mult: "ani(x\<^sup>\ ; y) = ani(x\<^sup>\)" by (metis an_omega_mult ani_def) lemma ani_star_left_unfold: "ani(x\<^sup>\) = ani(x ; x\<^sup>\)" by (metis an_star_left_unfold ani_def) lemma an_star_import: "an(y) ; x \ x ; an(y) \ an(y) ; x\<^sup>\ = an(y) ; (an(y) ; x)\<^sup>\" by (metis an_n_def n_star_import) lemma an_omega_export: "an(y) ; x \ x ; an(y) \ an(y) ; x\<^sup>\ = (an(y) ; x)\<^sup>\" by (metis an_n_def n_omega_export) lemma an_omega_import: "an(y) ; x \ x ; an(y) \ an(y) ; x\<^sup>\ = an(y) ; (an(y) ; x)\<^sup>\" by (metis an_n_def n_omega_import) end sublocale omega_algebra_anL < nL_omega!: itering_anL where circ = Omega .. context omega_algebra_anL begin lemma preserves_star: "nL_omega.preserves x (-p) \ nL_omega.preserves (x\<^sup>\) (-p)" by (smt omega_algebra_anL_class.nL_omega.preserves_def kleene_algebra_class.star.circ_simulate) end (* end theory Modal imports AbortingFiniteInfinite begin *) class diamond_semiring_nL = semiring_nL + fixes ndiamond :: "'a \ 'a \ 'a" ("| _ > _" [50,90] 95) assumes ndiamond_def: "|x>y = n(x ; y ; L)" begin lemma diamond_x_0: "|x>0 = n(x)" by (metis n_mult n_mult_zero n_zero ndiamond_def) lemma diamond_x_1: "|x>1 = n(x ; L)" by (metis n_L n_mult ndiamond_def) lemma diamond_x_L: "|x>L = n(x ; L)" by (metis L_left_zero mult_associative ndiamond_def) lemma diamond_x_top: "|x>T = n(x ; L)" by (metis mult_associative n_top_L ndiamond_def top_mult_top) lemma diamond_x_n: "|x>n(y) = n(x ; y)" by (metis n_mult ndiamond_def) lemma diamond_0_y: "|0>y = 0" by (metis mult_left_zero n_n_L n_one ndiamond_def) lemma diamond_1_y: "|1>y = n(y ; L)" by (metis mult_left_one ndiamond_def) lemma diamond_1_n: "|1>n(y) = n(y)" by (metis diamond_1_y n_n_L) lemma diamond_L_y: "|L>y = 1" by (metis L_left_zero n_L ndiamond_def) lemma diamond_top_y: "|T>y = 1" by (metis add_left_top add_right_top diamond_L_y mult_right_dist_add n_dist_add n_top ndiamond_def) lemma diamond_n_y: "|n(x)>y = n(x) ; n(y ; L)" by (metis mult_associative n_export ndiamond_def) lemma diamond_n_0: "|n(x)>0 = 0" by (metis diamond_x_n n_mult_right_zero n_zero) lemma diamond_n_1: "|n(x)>1 = n(x)" by (metis diamond_x_1 n_n_L) lemma diamond_n_n: "|n(x)>n(y) = n(x) ; n(y)" by (metis diamond_x_n n_export) lemma diamond_n_n_same: "|n(x)>n(x) = n(x)" by (metis diamond_n_n n_mult_idempotent) lemma diamond_left_dist_add: "|x + y>z = |x>z + |y>z" by (metis mult_right_dist_add n_dist_add ndiamond_def) lemma diamond_right_dist_add: "|x>(y + z) = |x>y + |x>z" by (metis mult_left_dist_add mult_right_dist_add n_dist_add ndiamond_def) lemma diamond_associative: "|x ; y>z = |x>(y ; z)" by (metis mult_associative ndiamond_def) lemma diamond_left_mult: "|x ; y>z = |x>|y>z" by (metis diamond_x_n mult_associative ndiamond_def) lemma diamond_right_mult: "|x>(y ; z) = |x>|y>z" by (metis diamond_associative diamond_left_mult) lemma diamond_n_export: "|n(x) ; y>z = n(x) ; |y>z" by (metis diamond_associative diamond_n_y ndiamond_def) lemma diamond_diamond_export: "||x>y>z = |x>y ; |z>1" by (metis diamond_n_y diamond_x_1 ndiamond_def) lemma diamond_left_isotone: "x \ y \ |x>z \ |y>z" by (metis diamond_left_dist_add less_eq_def) lemma diamond_right_isotone: "y \ z \ |x>y \ |x>z" by (metis diamond_right_dist_add less_eq_def) lemma diamond_isotone: "w \ y \ x \ z \ |w>x \ |y>z" by (metis diamond_left_isotone diamond_right_isotone order_trans) definition ndiamond_L :: "'a \ 'a \ 'a" ("\ _ \ _" [50,90] 95) where "\x\y = n(x ; y) ; L" lemma ndiamond_to_L: "\x\y = |x>n(y) ; L" by (metis diamond_x_n ndiamond_L_def) lemma ndiamond_from_L: "|x>y = n(\x\(y ; L))" by (metis mult_associative n_n_L ndiamond_L_def ndiamond_def) lemma diamond_L_ni: "\x\y = ni(x ; y)" by (metis ndiamond_L_def ni_def) lemma diamond_L_associative: "\x ; y\z = \x\(y ; z)" by (metis mult_associative diamond_L_ni) lemma diamond_L_left_mult: "\x ; y\z = \x\\y\z" by (metis diamond_L_associative diamond_L_ni ni_mult) lemma diamond_L_right_mult: "\x\(y ; z) = \x\\y\z" by (metis diamond_L_associative diamond_L_left_mult) lemma diamond_L_left_dist_add: "\x + y\z = \x\z + \y\z" by (metis mult_right_dist_add diamond_L_ni ni_dist_add) lemma diamond_L_x_ni: "\x\ni(y) = ni(x ; y)" by (metis diamond_L_ni ni_mult) lemma diamond_L_left_isotone: "x \ y \ \x\z \ \y\z" by (metis diamond_L_left_dist_add less_eq_def) lemma diamond_L_right_isotone: "y \ z \ \x\y \ \x\z" by (metis mult_right_isotone ndiamond_L_def ni_def ni_isotone) lemma diamond_L_isotone: "w \ y \ x \ z \ \w\x \ \y\z" by (metis mult_isotone ndiamond_L_def ni_def ni_isotone) end class box_semiring_nL = diamond_semiring_nL + semiring_anL + fixes nbox :: "'a \ 'a \ 'a" ("| _ ] _" [50,90] 95) assumes nbox_def: "|x]y = an(x ; an(y ; L) ; L)" begin lemma box_diamond: "|x]y = an( |x>an(y ; L) ; L)" by (metis an_n_L nbox_def ndiamond_def) lemma diamond_box: "|x>y = an( |x]an(y ; L) ; L)" by (metis diamond_associative diamond_right_mult diamond_x_n n_an_def nbox_def ndiamond_def) lemma box_x_0: "|x]0 = an(x ; L)" by (metis an_L mult_right_one n_L n_an_def nbox_def) lemma box_x_1: "|x]1 = an(x)" by (metis an_L an_n_L box_diamond diamond_x_0 n_L) lemma box_x_L: "|x]L = an(x)" by (metis L_left_zero an_L an_n_L box_diamond diamond_x_0) lemma box_x_top: "|x]T = an(x)" by (metis an_n_L an_top an_top_L box_diamond diamond_x_n n_mult_zero n_zero top_mult_top) lemma box_x_n: "|x]n(y) = an(x ; an(y) ; L)" by (metis an_n_L nbox_def) lemma box_x_an: "|x]an(y) = an(x ; y)" by (metis an_n_L box_diamond diamond_x_n n_an_def) lemma box_0_y: "|0]y = 1" by (metis an_zero box_diamond diamond_0_y mult_left_zero) lemma box_1_y: "|1]y = n(y ; L)" by (metis mult_left_one n_an_def nbox_def) lemma box_1_n: "|1]n(y) = n(y)" by (metis box_1_y n_n_L) lemma box_1_an: "|1]an(y) = an(y)" by (metis an_n_def box_1_y) lemma box_L_y: "|L]y = 0" by (metis an_L box_1_an box_diamond box_x_an diamond_L_y) lemma box_top_y: "|T]y = 0" by (metis an_L box_1_an box_diamond box_x_an diamond_top_y) lemma box_n_y: "|n(x)]y = an(x) + n(y ; L)" by (metis an_export_n mult_associative n_an_def nbox_def) lemma box_an_y: "|an(x)]y = n(x) + n(y ; L)" by (metis an_n_def box_n_y n_an_def) lemma box_n_0: "|n(x)]0 = an(x)" by (metis an_n_L box_x_0) lemma box_an_0: "|an(x)]0 = n(x)" by (metis box_x_0 n_an_def) lemma box_n_1: "|n(x)]1 = 1" by (metis an_zero box_x_an n_mult_right_zero) lemma box_an_1: "|an(x)]1 = 1" by (metis an_mult_right_zero an_zero box_x_an) lemma box_n_n: "|n(x)]n(y) = an(x) + n(y)" by (metis box_n_y n_n_L) lemma box_an_n: "|an(x)]n(y) = n(x) + n(y)" by (metis an_n_def box_n_n n_an_def) lemma box_n_an: "|n(x)]an(y) = an(x) + an(y)" by (metis an_export_n box_x_an) lemma box_an_an: "|an(x)]an(y) = n(x) + an(y)" by (metis an_export box_x_an) lemma box_n_n_same: "|n(x)]n(x) = 1" by (metis an_complement box_n_n) lemma box_an_an_same: "|an(x)]an(x) = 1" by (metis an_equal_complement box_an_an) lemma box_left_dist_add: "|x + y]z = |x]z ; |y]z" by (metis an_dist_add mult_right_dist_add nbox_def) lemma box_right_dist_add: "|x](y + z) = an(x ; an(y ; L) ; an(z ; L) ; L)" by (metis an_dist_add mult_associative mult_right_dist_add nbox_def) lemma box_associative: "|x ; y]z = an(x ; y ; an(z ; L) ; L)" by (metis nbox_def) lemma box_left_mult: "|x ; y]z = |x]|y]z" by (metis box_x_an mult_associative nbox_def) lemma box_right_mult: "|x](y ; z) = an(x ; an(y ; z ; L) ; L)" by (metis nbox_def) lemma box_right_mult_n_n: "|x](n(y) ; n(z)) = |x]n(y) ; |x]n(z)" by (smt an_dist_add an_export_n an_n_L mult_associative mult_left_dist_add mult_right_dist_add nbox_def) lemma box_right_mult_an_n: "|x](an(y) ; n(z)) = |x]an(y) ; |x]n(z)" by (metis an_n_def box_right_mult_n_n) lemma box_right_mult_n_an: "|x](n(y) ; an(z)) = |x]n(y) ; |x]an(z)" by (metis an_n_def box_right_mult_n_n) lemma box_right_mult_an_an: "|x](an(y) ; an(z)) = |x]an(y) ; |x]an(z)" by (metis an_dist_add box_x_an mult_left_dist_add) lemma box_n_export: "|n(x) ; y]z = an(x) + |y]z" by (metis box_1_y box_left_mult box_n_y mult_left_one) lemma box_an_export: "|an(x) ; y]z = n(x) + |y]z" by (metis box_an_y box_left_mult box_n_an box_n_y n_an_def nbox_def) lemma box_left_antitone: "y \ x \ |x]z \ |y]z" by (smt an_mult_commutative an_order box_diamond box_left_dist_add less_eq_def) lemma box_right_isotone: "y \ z \ |x]y \ |x]z" by (metis an_antitone mult_left_isotone mult_right_isotone nbox_def) lemma box_antitone_isotone: "y \ w \ x \ z \ |w]x \ |y]z" by (metis box_left_antitone box_right_isotone order_trans) definition nbox_L :: "'a \ 'a \ 'a" ("\ _ \ _" [50,90] 95) where "\x\y = an(x ; an(y) ; L) ; L" lemma nbox_to_L: "\x\y = |x]n(y) ; L" by (metis box_x_n nbox_L_def) lemma nbox_from_L: "|x]y = n(\x\(y ; L))" by (metis an_n_def nbox_L_def nbox_def) lemma diamond_x_an: "|x>an(y) = n(x ; an(y) ; L)" by (metis ndiamond_def) lemma diamond_1_an: "|1>an(y) = an(y)" by (metis an_n_def diamond_1_y) lemma diamond_an_y: "|an(x)>y = an(x) ; n(y ; L)" by (metis mult_associative n_export_an ndiamond_def) lemma diamond_an_0: "|an(x)>0 = 0" by (metis an_mult_right_zero diamond_x_n n_zero) lemma diamond_an_1: "|an(x)>1 = an(x)" by (metis an_n_def diamond_x_1) lemma diamond_an_n: "|an(x)>n(y) = an(x) ; n(y)" by (metis n_export_an n_mult ndiamond_def) lemma diamond_n_an: "|n(x)>an(y) = n(x) ; an(y)" by (metis an_n_def diamond_n_y) lemma diamond_an_an: "|an(x)>an(y) = an(x) ; an(y)" by (metis an_n_def diamond_an_n) lemma diamond_an_an_same: "|an(x)>an(x) = an(x)" by (metis an_mult_idempotent an_n_def ndiamond_def) lemma diamond_an_export: "|an(x) ; y>z = an(x) ; |y>z" by (metis mult_associative n_export_an ndiamond_def) lemma box_ani: "|x]y = an(x ; ani(y ; L))" by (metis ani_def mult_associative nbox_def) lemma box_x_n_ani: "|x]n(y) = an(x ; ani(y))" by (metis an_ani box_x_an) lemma box_L_ani: "\x\y = ani(x ; ani(y))" by (metis ani_def mult_associative nbox_L_def) lemma box_L_left_mult: "\x ; y\z = \x\\y\z" by (metis ani_def ani_mult mult_associative n_an_def nbox_L_def ni_def) lemma diamond_x_an_ani: "|x>an(y) = n(x ; ani(y))" by (metis diamond_x_n n_ani) lemma box_L_left_antitone: "y \ x \ \x\z \ \y\z" by (metis ani_antitone ani_def mult_left_isotone nbox_L_def) lemma box_L_right_isotone: "y \ z \ \x\y \ \x\z" by (metis ani_antitone ani_def mult_associative mult_right_isotone nbox_L_def) lemma box_L_antitone_isotone: "y \ w \ x \ z \ \w\x \ \y\z" by (metis box_L_left_antitone box_L_right_isotone order_trans) end class box_omega_algebra_nL = box_semiring_nL + omega_algebra_anL begin lemma diamond_omega: "|x\<^sup>\>y = |x\<^sup>\>z" by (metis mult_associative n_omega_mult ndiamond_def) lemma box_omega: "|x\<^sup>\]y = |x\<^sup>\]z" by (metis box_diamond diamond_omega) lemma an_box_omega_induct: "|x]an(y) ; n(z ; L) \ an(y) \ |x\<^sup>\ + x\<^sup>\]z \ an(y)" by (smt an_dist_add an_omega_induct an_omega_mult box_left_dist_add box_x_an mult_associative n_an_def nbox_def) lemma n_box_omega_induct: "|x]n(y) ; n(z ; L) \ n(y) \ |x\<^sup>\ + x\<^sup>\]z \ n(y)" by (metis an_box_omega_induct n_an_def) lemma an_box_omega_induct_an: "|x]an(y) ; an(z) \ an(y) \ |x\<^sup>\ + x\<^sup>\]an(z) \ an(y)" by (metis an_box_omega_induct an_n_def) lemma n_box_omega_induct_n: "|x]n(y) ; n(z) \ n(y) \ |x\<^sup>\ + x\<^sup>\]n(z) \ n(y)" by (metis n_box_omega_induct n_n_L) lemma n_diamond_omega_induct: "n(y) \ |x>n(y) + n(z ; L) \ n(y) \ |x\<^sup>\ + x\<^sup>\>z" by (smt n_dist_add n_omega_induct n_omega_mult diamond_left_dist_add diamond_x_n mult_associative ndiamond_def) lemma an_diamond_omega_induct: "an(y) \ |x>an(y) + n(z ; L) \ an(y) \ |x\<^sup>\ + x\<^sup>\>z" by (metis n_diamond_omega_induct an_n_def) lemma n_diamond_omega_induct_n: "n(y) \ |x>n(y) + n(z) \ n(y) \ |x\<^sup>\ + x\<^sup>\>n(z)" by (metis n_diamond_omega_induct n_n_L) lemma an_diamond_omega_induct_an: "an(y) \ |x>an(y) + an(z) \ an(y) \ |x\<^sup>\ + x\<^sup>\>an(z)" by (metis an_diamond_omega_induct an_n_def) lemma box_segerberg_an: "|x\<^sup>\ + x\<^sup>\]an(y) = an(y) ; |x\<^sup>\ + x\<^sup>\](n(y) + |x]an(y))" proof (rule antisym) have "|x\<^sup>\ + x\<^sup>\]an(y) \ |x\<^sup>\ + x\<^sup>\]|x]an(y)" by (smt box_left_dist_add box_left_mult box_omega add_right_isotone box_left_antitone mult_right_dist_add star.right_plus_below_circ) hence "|x\<^sup>\ + x\<^sup>\]an(y) \ |x\<^sup>\ + x\<^sup>\](n(y) + |x]an(y))" by (smt add_right_upper_bound box_right_isotone order_trans) thus"|x\<^sup>\ + x\<^sup>\]an(y) \ an(y) ; |x\<^sup>\ + x\<^sup>\](n(y) + |x]an(y))" by (metis add_least_upper_bound box_1_an box_left_antitone order_refl star_left_unfold_equal an_mult_least_upper_bound nbox_def) next have "an(y) ; |x](n(y) + |x\<^sup>\ + x\<^sup>\]an(y)) ; (n(y) + |x]an(y)) = |x]( |x\<^sup>\ + x\<^sup>\]an(y) ; an(y)) ; an(y)" by (smt add_left_zero an_export an_mult_commutative box_right_mult_an_an mult_associative mult_right_dist_add n_complement_zero nbox_def) hence 1: "an(y) ; |x](n(y) + |x\<^sup>\ + x\<^sup>\]an(y)) ; (n(y) + |x]an(y)) \ n(y) + |x\<^sup>\ + x\<^sup>\]an(y)" by (smt add_associative add_commutative add_right_upper_bound box_1_an box_left_dist_add box_left_mult mult_left_dist_add omega_unfold star_left_unfold_equal star.circ_plus_one) have "n(y) ; |x](n(y) + |x\<^sup>\ + x\<^sup>\]an(y)) ; (n(y) + |x]an(y)) \ n(y) + |x\<^sup>\ + x\<^sup>\]an(y)" by (smt add_left_upper_bound an_n_def mult_left_isotone n_an_mult_left_lower_bound n_mult_left_absorb_add nbox_def order_trans) thus "an(y) ; |x\<^sup>\ + x\<^sup>\](n(y) + |x]an(y)) \ |x\<^sup>\ + x\<^sup>\]an(y)" using 1 by (smt an_case_split_left an_shunting_an mult_associative n_box_omega_induct_n n_dist_add nbox_def nbox_from_L) qed lemma box_segerberg_n: "|x\<^sup>\ + x\<^sup>\]n(y) = n(y) ; |x\<^sup>\ + x\<^sup>\](an(y) + |x]n(y))" by (smt an_n_def box_segerberg_an n_an_def) lemma diamond_segerberg_an: "|x\<^sup>\ + x\<^sup>\>an(y) = an(y) + |x\<^sup>\ + x\<^sup>\>(n(y) ; |x>an(y))" by (smt an_export an_n_L box_diamond box_segerberg_an diamond_box mult_associative n_an_def) lemma diamond_segerberg_n: "|x\<^sup>\ + x\<^sup>\>n(y) = n(y) + |x\<^sup>\ + x\<^sup>\>(an(y) ; |x>n(y))" by (smt an_export an_n_L box_diamond box_segerberg_an diamond_box mult_associative n_an_def) lemma diamond_star_unfold_n: "|x\<^sup>\>n(y) = n(y) + |an(y) ; x>|x\<^sup>\>n(y)" proof - have "|x\<^sup>\>n(y) = n(y) + n(y) ; |x ; x\<^sup>\>n(y) + |an(y) ; x ; x\<^sup>\>n(y)" by (smt add_associative add_commutative add_right_zero an_complement an_complement_zero diamond_an_n diamond_left_dist_add diamond_n_export diamond_n_n_same mult_associative mult_left_one mult_right_dist_add star_left_unfold_equal) thus ?thesis by (metis diamond_left_mult diamond_x_n n_add_left_absorb_mult) qed lemma diamond_star_unfold_an: "|x\<^sup>\>an(y) = an(y) + |n(y) ; x>|x\<^sup>\>an(y)" by (metis an_n_def diamond_star_unfold_n n_an_def) lemma box_star_unfold_n: "|x\<^sup>\]n(y) = n(y) ; |n(y) ; x]|x\<^sup>\]n(y)" by (smt an_export an_n_L box_diamond diamond_box diamond_star_unfold_an n_an_def n_export) lemma box_star_unfold_an: "|x\<^sup>\]an(y) = an(y) ; |an(y) ; x]|x\<^sup>\]an(y)" by (metis an_n_def box_star_unfold_n) lemma diamond_omega_unfold_n: "|x\<^sup>\ + x\<^sup>\>n(y) = n(y) + |an(y) ; x>|x\<^sup>\ + x\<^sup>\>n(y)" by (smt add_associative add_commutative diamond_an_export diamond_left_dist_add diamond_right_dist_add diamond_star_unfold_n diamond_x_n n_omega_mult n_plus_complement_intro_n omega_unfold) lemma diamond_omega_unfold_an: "|x\<^sup>\ + x\<^sup>\>an(y) = an(y) + |n(y) ; x>|x\<^sup>\ + x\<^sup>\>an(y)" by (metis an_n_def diamond_omega_unfold_n n_an_def) lemma box_omega_unfold_n: "|x\<^sup>\ + x\<^sup>\]n(y) = n(y) ; |n(y) ; x]|x\<^sup>\ + x\<^sup>\]n(y)" by (smt an_export an_n_L box_diamond diamond_box diamond_omega_unfold_an n_an_def n_export) lemma box_omega_unfold_an: "|x\<^sup>\ + x\<^sup>\]an(y) = an(y) ; |an(y) ; x]|x\<^sup>\ + x\<^sup>\]an(y)" by (metis an_n_def box_omega_unfold_n) lemma box_cut_iteration_an: "|x\<^sup>\ + x\<^sup>\]an(y) = |(an(y) ; x)\<^sup>\ + (an(y) ; x)\<^sup>\]an(y)" by (smt add_isotone an_box_omega_induct_an an_case_split_left an_mult_commutative antisym box_left_antitone box_omega_unfold_an nbox_def omega_isotone order_refl star.circ_isotone) lemma box_cut_iteration_n: "|x\<^sup>\ + x\<^sup>\]n(y) = |(n(y) ; x)\<^sup>\ + (n(y) ; x)\<^sup>\]n(y)" by (metis n_an_def box_cut_iteration_an) lemma diamond_cut_iteration_an: "|x\<^sup>\ + x\<^sup>\>an(y) = |(n(y) ; x)\<^sup>\ + (n(y) ; x)\<^sup>\>an(y)" by (metis box_cut_iteration_n diamond_box n_an_def) lemma diamond_cut_iteration_n: "|x\<^sup>\ + x\<^sup>\>n(y) = |(an(y) ; x)\<^sup>\ + (an(y) ; x)\<^sup>\>n(y)" by (metis an_n_def diamond_cut_iteration_an n_an_def) lemma ni_diamond_omega_induct: "ni(y) \ \x\ni(y) + ni(z) \ ni(y) \ \x\<^sup>\ + x\<^sup>\\z" by (metis diamond_L_left_dist_add diamond_L_x_ni diamond_L_ni ni_dist_add ni_omega_induct ni_omega_mult) lemma ani_diamond_omega_induct: "ani(y) \ \x\ani(y) + ni(z) \ ani(y) \ \x\<^sup>\ + x\<^sup>\\z" by (metis ni_ani ni_diamond_omega_induct) lemma n_diamond_omega_L: "|n(x\<^sup>\) ; L>y = |x\<^sup>\>y" by (metis L_left_zero mult_associative n_n_L n_omega_mult ndiamond_def) lemma n_diamond_loop: "|x\<^sup>\>y = |x\<^sup>\ + x\<^sup>\>y" by (metis Omega_def diamond_left_dist_add n_diamond_omega_L) lemma cut_iteration_loop: "|x\<^sup>\>n(y) = |(an(y) ; x)\<^sup>\>n(y)" by (metis n_diamond_loop diamond_cut_iteration_n) lemma cut_iteration_while_loop: "|x\<^sup>\>n(y) = |(an(y) ; x)\<^sup>\ ; n(y)>n(y)" by (metis cut_iteration_loop diamond_left_mult diamond_n_n_same) lemma modal_while: "-q ; -p ; L \ x ; -p ; L \ -p \ -q + -r \ -p \ |n((-q ; x)\<^sup>\) ; L + (-q ; x)\<^sup>\ ; --q>(-r)" proof - have "-p \ -q + -r \ --q ; -p \ |-q ; x>(-p) + --q ; -r" by (smt add_associative add_commutative greatest_lower_bound leq_mult_zero less_eq_def lower_bound_right mult_associative plus_def sub_comm sub_mult_closed) hence "-q ; -p ; L \ x ; -p ; L \ -p \ -q + -r \ -p \ |-q ; x>(-p) + --q ; -r" using [[ smt_timeout = 120 ]] by (smt add_left_upper_bound an_mult an_uminus greatest_lower_bound leq_cases mult_associative n_an_def n_isotone ndiamond_def order_refl order_trans plus_closed sub_mult_closed) thus ?thesis by (smt L_left_zero an_diamond_omega_induct_an an_uminus diamond_left_dist_add mult_associative n_n_L n_omega_mult ndiamond_def sub_mult_closed) qed lemma modal_while_loop: "-q ; -p ; L \ x ; -p ; L \ -p \ -q + -r \ -p \ |(-q ; x)\<^sup>\ ; --q>(-r)" by (metis L_left_zero Omega_def modal_while mult_associative mult_right_dist_add) lemma modal_while_2: "-p ; L \ x ; -p ; L \ -p \ |n((-q ; x)\<^sup>\) ; L + (-q ; x)\<^sup>\ ; --q>(--q)" proof - have "-p ; L \ x ; -p ; L \ -p \ |-q ; x>(-p) + --q" by (metis an_uminus double_negation n_an_def n_isotone ndiamond_def diamond_an_export add_associative add_commutative less_eq_def plus_compl_intro) thus ?thesis by (smt L_left_zero an_diamond_omega_induct_an an_uminus diamond_left_dist_add mult_associative mult_idempotent n_n_L n_omega_mult ndiamond_def) qed end class modal_omega_algebra_nL = box_omega_algebra_nL + assumes n_star_induct: "n(x ; y) \ n(y) \ n(x\<^sup>\ ; y) \ n(y)" begin lemma n_star_induct_add: "n(z + x ; y) \ n(y) \ n(x\<^sup>\ ; z) \ n(y)" by (metis an_dist_add an_mult_least_upper_bound an_n_order n_mult_right_upper_bound n_star_induct star_L_split) lemma n_star_induct_star: "n(x ; y) \ n(y) \ n(x\<^sup>\) \ n(y)" by (metis n_mult_right_upper_bound n_star_induct) lemma n_star_induct_iff: "n(x ; y) \ n(y) \ n(x\<^sup>\ ; y) \ n(y)" by (metis mult_left_isotone n_isotone n_star_induct order_trans star.circ_increasing) lemma n_star_zero: "n(x) = 0 \ n(x\<^sup>\) = 0" by (metis add_right_zero less_eq_def mult_right_one n_one n_star_induct_iff) lemma n_diamond_star_induct: "|x>n(y) \ n(y) \ |x\<^sup>\>n(y) \ n(y)" by (metis diamond_x_n n_star_induct) lemma n_diamond_star_induct_add: "|x>n(y) + n(z) \ n(y) \ |x\<^sup>\>n(z) \ n(y)" by (metis add_commutative diamond_x_n n_dist_add n_star_induct_add) lemma n_diamond_star_induct_iff: "|x>n(y) \ n(y) \ |x\<^sup>\>n(y) \ n(y)" by (metis n_mult n_star_induct_iff ndiamond_def) lemma an_star_induct: "an(y) \ an(x ; y) \ an(y) \ an(x\<^sup>\ ; y)" by (metis an_n_order n_star_induct) lemma an_star_induct_add: "an(y) \ an(z + x ; y) \ an(y) \ an(x\<^sup>\ ; z)" by (metis an_n_order n_star_induct_add) lemma an_star_induct_star: "an(y) \ an(x ; y) \ an(y) \ an(x\<^sup>\)" by (metis an_n_order n_star_induct_star) lemma an_star_induct_iff: "an(y) \ an(x ; y) \ an(y) \ an(x\<^sup>\ ; y)" by (metis an_n_order n_star_induct_iff) lemma an_star_one: "an(x) = 1 \ an(x\<^sup>\) = 1" by (metis an_n_equal an_zero n_star_zero n_zero) lemma an_box_star_induct: "an(y) \ |x]an(y) \ an(y) \ |x\<^sup>\]an(y)" by (metis an_star_induct box_x_an) lemma an_box_star_induct_add: "an(y) \ |x]an(y) ; an(z) \ an(y) \ |x\<^sup>\]an(z)" by (metis add_commutative an_dist_add an_star_induct_add box_x_an) lemma an_box_star_induct_iff: "an(y) \ |x]an(y) \ an(y) \ |x\<^sup>\]an(y)" by (metis an_star_induct_iff box_x_an) lemma box_star_segerberg_an: "|x\<^sup>\]an(y) = an(y) ; |x\<^sup>\](n(y) + |x]an(y))" proof (rule antisym) show "|x\<^sup>\]an(y) \ an(y) ; |x\<^sup>\](n(y) + |x]an(y))" by (metis add_right_upper_bound box_1_an box_left_dist_add box_left_mult box_right_isotone mult_right_isotone star.circ_right_unfold) next have "an(y) ; |x\<^sup>\](n(y) + |x]an(y)) \ an(y) ; |x]an(y)" by (metis add_left_zero an_complement_zero box_an_an box_left_antitone box_x_an mult_left_dist_add mult_left_one mult_right_isotone star.circ_reflexive) thus "an(y) ; |x\<^sup>\](n(y) + |x]an(y)) \ |x\<^sup>\]an(y)" by (smt an_box_star_induct_add an_case_split_left an_dist_add an_mult_least_upper_bound box_left_antitone box_left_mult box_right_mult_an_an star.left_plus_below_circ nbox_def) qed lemma box_star_segerberg_n: "|x\<^sup>\]n(y) = n(y) ; |x\<^sup>\](an(y) + |x]n(y))" by (metis box_diamond box_n_export box_star_segerberg_an box_x_an n_an_def nbox_def ndiamond_def) lemma diamond_segerberg_an: "|x\<^sup>\>an(y) = an(y) + |x\<^sup>\>(n(y) ; |x>an(y))" by (smt an_export an_n_L box_diamond box_star_segerberg_an diamond_box mult_associative n_an_def) lemma diamond_star_segerberg_n: "|x\<^sup>\>n(y) = n(y) + |x\<^sup>\>(an(y) ; |x>n(y))" by (smt an_export an_n_L box_diamond box_star_segerberg_an diamond_box mult_associative n_an_def) lemma box_cut_star_iteration_an: "|x\<^sup>\]an(y) = |(an(y) ; x)\<^sup>\]an(y)" by (smt an_box_star_induct_add an_mult_commutative an_mult_complement_intro_an antisym box_an_export box_star_unfold_an nbox_def order_refl) lemma box_cut_star_iteration_n: "|x\<^sup>\]n(y) = |(n(y) ; x)\<^sup>\]n(y)" by (metis box_cut_star_iteration_an n_an_def) lemma diamond_cut_star_iteration_an: "|x\<^sup>\>an(y) = |(n(y) ; x)\<^sup>\>an(y)" by (metis box_cut_star_iteration_n diamond_box n_an_def) lemma diamond_cut_star_iteration_n: "|x\<^sup>\>n(y) = |(an(y) ; x)\<^sup>\>n(y)" by (metis an_n_def diamond_cut_star_iteration_an n_an_def) lemma ni_star_induct: "ni(x ; y) \ ni(y) \ ni(x\<^sup>\ ; y) \ ni(y)" by (metis n_star_induct ni_n_order) lemma ni_star_induct_add: "ni(z + x ; y) \ ni(y) \ ni(x\<^sup>\ ; z) \ ni(y)" by (metis n_star_induct_add ni_n_order) lemma ni_star_induct_star: "ni(x ; y) \ ni(y) \ ni(x\<^sup>\) \ ni(y)" by (metis n_star_induct_star ni_n_order) lemma ni_star_induct_iff: "ni(x ; y) \ ni(y) \ ni(x\<^sup>\ ; y) \ ni(y)" by (metis n_star_induct_iff ni_n_order) lemma ni_star_zero: "ni(x) = 0 \ ni(x\<^sup>\) = 0" by (metis n_star_zero ni_n_zero) lemma ni_diamond_star_induct: "\x\ni(y) \ ni(y) \ \x\<^sup>\\ni(y) \ ni(y)" by (metis diamond_L_x_ni ni_star_induct) lemma ni_diamond_star_induct_add: "\x\ni(y) + ni(z) \ ni(y) \ \x\<^sup>\\ni(z) \ ni(y)" by (metis add_commutative diamond_L_x_ni ni_dist_add ni_star_induct_add) lemma ni_diamond_star_induct_iff: "\x\ni(y) \ ni(y) \ \x\<^sup>\\ni(y) \ ni(y)" by (metis diamond_L_x_ni ni_star_induct_iff) lemma ani_star_induct: "ani(y) \ ani(x ; y) \ ani(y) \ ani(x\<^sup>\ ; y)" by (metis an_star_induct ani_an_order) lemma ani_star_induct_add: "ani(y) \ ani(z + x ; y) \ ani(y) \ ani(x\<^sup>\ ; z)" by (metis an_star_induct_add ani_an_order) lemma ani_star_induct_star: "ani(y) \ ani(x ; y) \ ani(y) \ ani(x\<^sup>\)" by (metis an_star_induct_star ani_an_order) lemma ani_star_induct_iff: "ani(y) \ ani(x ; y) \ ani(y) \ ani(x\<^sup>\ ; y)" by (metis an_star_induct_iff ani_an_order) lemma ani_star_L: "ani(x) = L \ ani(x\<^sup>\) = L" by (metis an_star_one ani_an_L) lemma ani_box_star_induct: "ani(y) \ \x\ani(y) \ ani(y) \ \x\<^sup>\\ani(y)" by (metis an_ani ani_def ani_star_induct_iff n_ani box_L_ani) lemma ani_box_star_induct_iff: "ani(y) \ \x\ani(y) \ ani(y) \ \x\<^sup>\\ani(y)" by (smt an_ani ani_def ani_star_induct_iff n_ani box_L_ani) lemma ani_box_star_induct_add: "ani(y) \ \x\ani(y) \ ani(y) \ ani(z) \ ani(y) \ \x\<^sup>\\ani(z)" by (smt ani_box_star_induct_iff box_L_right_isotone order_trans) end (* end theory Recursion imports AbortingFiniteInfinite begin *) class semiring_apx = semiring_nL + fixes apx :: "'a \ 'a \ bool" (infix "\" 50) assumes apx_def: "x \ y \ x \ y + n(x) ; L \ y \ x + n(x) ; T" begin definition apx_isotone :: "('a \ 'a) \ bool" where "apx_isotone f \ (\x y . x \ y \ f(x) \ f(y))" lemma apx_reflexive: "x \ x" by (metis add_left_upper_bound apx_def) lemma apx_antisymmetric: "x \ y \ y \ x \ x = y" by (smt add_least_upper_bound antisym apx_def eq_refl less_eq_def n_add_left_absorb_mult n_export n_dist_add n_galois) lemma apx_L_least: "L \ x" by (metis add_right_top add_right_upper_bound apx_def mult_left_one n_L top_greatest) lemma apx_transitive: "x \ y \ y \ z \ x \ z" proof assume 1: "x \ y \ y \ z" hence "n(y) ; L \ n(x) ; L" by (metis apx_def mult_left_isotone n_add_left_absorb_mult n_export n_dist_add n_isotone) hence 2: "x \ z + n(x) ; L" using 1 by (smt add_associative add_right_divisibility apx_def less_eq_def) have "z \ x + n(x) ; T" using 1 by (smt add_associative add_idempotent add_isotone apx_def mult_left_isotone n_add_left_absorb_mult n_export n_dist_add n_isotone order_trans) thus "x \ z" using 2 by (metis apx_def) qed lemma add_apx_right_isotone: "x \ y \ z + x \ z + y" by (smt add_associative add_right_isotone apx_def mult_right_subdist_add_right n_dist_add order_trans) lemma add_apx_left_isotone: "x \ y \ x + z \ y + z" by (metis add_commutative add_apx_right_isotone) lemma mult_apx_left_isotone: "x \ y \ x ; z \ y ; z" proof assume 1: "x \ y" hence 2: "x ; z \ y ; z + n(x ; z) ; L" by (smt add_right_isotone apx_def L_left_zero mult_associative mult_left_isotone mult_right_dist_add n_mult_left_upper_bound order_trans) have "y ; z \ x ; z + n(x) ; T ; z" using 1 by (metis apx_def mult_left_isotone mult_right_dist_add) hence "y ; z \ x ; z + n(x ; z) ; T" by (smt add_right_isotone mult_associative mult_isotone n_mult_left_upper_bound order_trans top_greatest) thus "x ; z \ y ; z" using 2 by (metis apx_def) qed lemma mult_apx_right_isotone: "x \ y \ z ; x \ z ; y" by (smt add_associative add_least_upper_bound add_left_isotone add_left_upper_bound add_right_zero apx_def mult_associative mult_left_dist_add mult_right_isotone n_L_split n_top_split order_trans) lemma ni_apx_isotone: "x \ y \ ni(x) \ ni(y)" by (smt apx_def less_eq_def n_dist_add n_galois n_n_L ni_def) definition is_apx_prefixpoint :: "('a \ 'a) \ 'a \ bool" where "is_apx_prefixpoint f x \ f(x) \ x" definition is_apx_least_fixpoint :: "('a \ 'a) \ 'a \ bool" where "is_apx_least_fixpoint f x \ f(x) = x \ (\y . f(y) = y \ x \ y)" definition is_apx_least_prefixpoint :: "('a \ 'a) \ 'a \ bool" where "is_apx_least_prefixpoint f x \ f(x) \ x \ (\y . f(y) \ y \ x \ y)" definition has_apx_prefixpoint :: "('a \ 'a) \ bool" where "has_apx_prefixpoint f \ (\x . is_apx_prefixpoint f x)" definition has_apx_least_fixpoint :: "('a \ 'a) \ bool" where "has_apx_least_fixpoint f \ (\x . is_apx_least_fixpoint f x)" definition has_apx_least_prefixpoint :: "('a \ 'a) \ bool" where "has_apx_least_prefixpoint f \ (\x . is_apx_least_prefixpoint f x)" definition the_apx_least_fixpoint :: "('a \ 'a) \ 'a" ("\ _" [201] 200) where "\ f = (THE x . is_apx_least_fixpoint f x)" definition the_apx_least_prefixpoint :: "('a \ 'a) \ 'a" ("p\ _" [201] 200) where "p\ f = (THE x . is_apx_least_prefixpoint f x)" lemma apx_least_fixpoint_unique: "has_apx_least_fixpoint f \ (\!x . is_apx_least_fixpoint f x)" by (smt apx_antisymmetric has_apx_least_fixpoint_def is_apx_least_fixpoint_def) lemma apx_least_prefixpoint_unique: "has_apx_least_prefixpoint f \ (\!x . is_apx_least_prefixpoint f x)" by (smt apx_antisymmetric has_apx_least_prefixpoint_def is_apx_least_prefixpoint_def) lemma apx_least_fixpoint: "has_apx_least_fixpoint f \ is_apx_least_fixpoint f (\ f)" proof assume "has_apx_least_fixpoint f" hence "is_apx_least_fixpoint f (THE x . is_apx_least_fixpoint f x)" by (smt apx_least_fixpoint_unique theI') thus "is_apx_least_fixpoint f (\ f)" by (simp add: is_apx_least_fixpoint_def the_apx_least_fixpoint_def) qed lemma apx_least_prefixpoint: "has_apx_least_prefixpoint f \ is_apx_least_prefixpoint f (p\ f)" proof assume "has_apx_least_prefixpoint f" hence "is_apx_least_prefixpoint f (THE x . is_apx_least_prefixpoint f x)" by (smt apx_least_prefixpoint_unique theI') thus "is_apx_least_prefixpoint f (p\ f)" by (simp add: is_apx_least_prefixpoint_def the_apx_least_prefixpoint_def) qed lemma apx_least_fixpoint_same: "is_apx_least_fixpoint f x \ x = \ f" by (metis apx_least_fixpoint apx_least_fixpoint_unique has_apx_least_fixpoint_def) lemma apx_least_prefixpoint_same: "is_apx_least_prefixpoint f x \ x = p\ f" by (metis apx_least_prefixpoint apx_least_prefixpoint_unique has_apx_least_prefixpoint_def) lemma apx_least_fixpoint_char: "is_apx_least_fixpoint f x \ has_apx_least_fixpoint f \ x = \ f" by (metis apx_least_fixpoint_same has_apx_least_fixpoint_def) lemma apx_least_prefixpoint_char: "is_apx_least_prefixpoint f x \ has_apx_least_prefixpoint f \ x = p\ f" by (metis apx_least_prefixpoint_same has_apx_least_prefixpoint_def) lemma apx_least_prefixpoint_fixpoint: "has_apx_least_prefixpoint f \ apx_isotone f \ is_apx_least_fixpoint f (p\ f)" by (smt apx_antisymmetric apx_isotone_def apx_reflexive is_apx_least_fixpoint_def is_apx_least_prefixpoint_def apx_least_prefixpoint) lemma pxi_xi: "has_apx_least_prefixpoint f \ apx_isotone f \ p\ f = \ f" by (smt has_apx_least_fixpoint_def is_apx_least_fixpoint_def apx_least_fixpoint_unique apx_least_prefixpoint_fixpoint apx_least_fixpoint) definition lifted_apx_less_eq :: "('a \ 'a) \ ('a \ 'a) \ bool" ("(_ \\ _)" [51, 51] 50) where "f \\ g \ (\x . f(x) \ g(x))" lemma lifted_reflexive: "f = g \ f \\ g" by (metis lifted_apx_less_eq_def apx_reflexive) lemma lifted_transitive: "f \\ g \ g \\ h \ f \\ h" by (smt lifted_apx_less_eq_def apx_transitive) lemma lifted_antisymmetric: "f \\ g \ g \\ f \ f = g" by (metis apx_antisymmetric ext lifted_apx_less_eq_def) lemma pxi_isotone: "has_apx_least_prefixpoint f \ has_apx_least_prefixpoint g \ f \\ g \ p\ f \ p\ g" by (metis is_apx_least_prefixpoint_def apx_transitive apx_least_prefixpoint lifted_apx_less_eq_def) lemma xi_isotone: "has_apx_least_prefixpoint f \ has_apx_least_prefixpoint g \ apx_isotone f \ apx_isotone g \ f \\ g \ \ f \ \ g" by (metis pxi_isotone pxi_xi) lemma xi_square: "apx_isotone f \ has_apx_least_fixpoint f \ has_apx_least_fixpoint (f \ f) \ \ f = \ (f \ f)" by (metis apx_antisymmetric is_apx_least_fixpoint_def apx_isotone_def apx_least_fixpoint_char apx_least_fixpoint_unique o_apply) lemma mu_below_xi: "has_least_fixpoint f \ has_apx_least_fixpoint f \ \ f \ \ f" by (metis apx_least_fixpoint is_apx_least_fixpoint_def is_least_fixpoint_def least_fixpoint) lemma xi_below_nu: "has_greatest_fixpoint f \ has_apx_least_fixpoint f \ \ f \ \ f" by (metis apx_least_fixpoint greatest_fixpoint is_apx_least_fixpoint_def is_greatest_fixpoint_def) lemma xi_apx_below_mu: "has_least_fixpoint f \ has_apx_least_fixpoint f \ \ f \ \ f" by (metis apx_least_fixpoint is_apx_least_fixpoint_def is_least_fixpoint_def least_fixpoint) lemma xi_apx_below_nu: "has_greatest_fixpoint f \ has_apx_least_fixpoint f \ \ f \ \ f" by (metis apx_least_fixpoint greatest_fixpoint is_apx_least_fixpoint_def is_greatest_fixpoint_def) definition is_apx_meet :: "'a \ 'a \ 'a \ bool" where "is_apx_meet x y z \ z \ x \ z \ y \ (\w . w \ x \ w \ y \ w \ z)" definition has_apx_meet :: "'a \ 'a \ bool" where "has_apx_meet x y \ (\z . is_apx_meet x y z)" definition the_apx_meet :: "'a \ 'a \ 'a" (infixl "\" 66) where "x \ y = (THE z . is_apx_meet x y z)" lemma apx_meet_unique: "has_apx_meet x y \ (\!z . is_apx_meet x y z)" by (smt apx_antisymmetric has_apx_meet_def is_apx_meet_def) lemma apx_meet: "has_apx_meet x y \ is_apx_meet x y (x \ y)" proof assume "has_apx_meet x y" hence "is_apx_meet x y (THE z . is_apx_meet x y z)" by (smt apx_meet_unique theI') thus "is_apx_meet x y (x \ y)" by (simp add: is_apx_meet_def the_apx_meet_def) qed lemma apx_greatest_lower_bound: "has_apx_meet x y \ (w \ x \ w \ y \ w \ x \ y)" by (smt apx_meet apx_transitive is_apx_meet_def) lemma apx_meet_same: "is_apx_meet x y z \ z = x \ y" by (metis apx_meet apx_meet_unique has_apx_meet_def) lemma apx_meet_char: "is_apx_meet x y z \ has_apx_meet x y \ z = x \ y" by (metis apx_meet_same has_apx_meet_def) definition xi_apx_meet :: "('a \ 'a) \ bool" where "xi_apx_meet f \ has_apx_least_fixpoint f \ has_apx_meet (\ f) (\ f) \ \ f = \ f \ \ f" definition xi_mu_nu :: "('a \ 'a) \ bool" where "xi_mu_nu f \ has_apx_least_fixpoint f \ \ f = \ f + n(\ f) ; L" definition nu_below_mu_nu :: "('a \ 'a) \ bool" where "nu_below_mu_nu f \ \ f \ \ f + n(\ f) ; T" definition mu_nu_apx_nu :: "('a \ 'a) \ bool" where "mu_nu_apx_nu f \ \ f + n(\ f) ; L \ \ f" definition mu_nu_apx_meet :: "('a \ 'a) \ bool" where "mu_nu_apx_meet f \ has_apx_meet (\ f) (\ f) \ \ f \ \ f = \ f + n(\ f) ; L" definition apx_meet_below_nu :: "('a \ 'a) \ bool" where "apx_meet_below_nu f \ has_apx_meet (\ f) (\ f) \ \ f \ \ f \ \ f" lemma mu_below_l: "\ f \ \ f + n(\ f) ; L" by (metis add_left_upper_bound) lemma l_below_nu: "has_least_fixpoint f \ has_greatest_fixpoint f \ \ f + n(\ f) ; L \ \ f" by (metis add_least_upper_bound mu_below_nu n_L_decreasing) lemma n_l_nu: "has_least_fixpoint f \ has_greatest_fixpoint f \ n(\ f + n(\ f) ; L) = n(\ f)" by (metis less_eq_def mu_below_nu n_dist_add n_n_L) lemma l_apx_mu: "has_least_fixpoint f \ has_greatest_fixpoint f \ \ f + n(\ f) ; L \ \ f" by (smt add_associative add_left_upper_bound apx_def n_l_nu order_refl) lemma nu_below_mu_nu_mu_nu_apx_nu: "has_least_fixpoint f \ has_greatest_fixpoint f \ nu_below_mu_nu f \ mu_nu_apx_nu f" by (smt add_associative add_commutative add_left_isotone add_left_top apx_def mu_below_nu mu_nu_apx_nu_def mult_left_dist_add n_l_nu nu_below_mu_nu_def) lemma mu_nu_apx_nu_mu_nu_apx_meet: "has_least_fixpoint f \ has_greatest_fixpoint f \ mu_nu_apx_nu f \ mu_nu_apx_meet f" proof let ?l = "\ f + n(\ f) ; L" assume "has_least_fixpoint f \ has_greatest_fixpoint f \ mu_nu_apx_nu f" hence "is_apx_meet (\ f) (\ f) ?l" by (smt add_associative add_commutative add_left_upper_bound apx_def is_apx_meet_def l_below_nu mu_nu_apx_nu_def n_l_nu order_refl order_trans) thus "mu_nu_apx_meet f" by (smt apx_meet_char mu_nu_apx_meet_def) qed lemma mu_nu_apx_meet_apx_meet_below_nu: "has_least_fixpoint f \ has_greatest_fixpoint f \ mu_nu_apx_meet f \ apx_meet_below_nu f" by (metis apx_meet_below_nu_def l_below_nu mu_nu_apx_meet_def) lemma apx_meet_below_nu_nu_below_mu_nu: "apx_meet_below_nu f \ nu_below_mu_nu f" proof - have "\m . m \ \ f \ m \ \ f \ m \ \ f \ \ f \ \ f + n(m) ; T" by (smt add_associative add_left_isotone add_right_top apx_def mult_left_dist_add order_trans) thus ?thesis by (smt add_right_isotone apx_greatest_lower_bound apx_meet_below_nu_def apx_reflexive mult_left_isotone n_isotone nu_below_mu_nu_def order_trans) qed lemma has_apx_least_fixpoint_xi_apx_meet: "has_least_fixpoint f \ has_greatest_fixpoint f \ has_apx_least_fixpoint f \ xi_apx_meet f" proof assume 1: "has_least_fixpoint f \ has_greatest_fixpoint f \ has_apx_least_fixpoint f" hence "\w . w \ \ f \ w \ \ f \ w \ \ f" by (smt add_left_isotone apx_def mu_below_xi order_trans xi_below_nu) thus "xi_apx_meet f" using 1 by (smt apx_meet_char is_apx_meet_def xi_apx_below_mu xi_apx_below_nu xi_apx_meet_def) qed lemma xi_apx_meet_apx_meet_below_nu: "has_greatest_fixpoint f \ xi_apx_meet f \ apx_meet_below_nu f" by (metis apx_meet_below_nu_def xi_apx_meet_def xi_below_nu) lemma apx_meet_below_nu_xi_mu_nu: "has_least_fixpoint f \ has_greatest_fixpoint f \ isotone f \ apx_isotone f \ apx_meet_below_nu f \ xi_mu_nu f" proof let ?l = "\ f + n(\ f) ; L" assume 1: "has_least_fixpoint f \ has_greatest_fixpoint f \ isotone f \ apx_isotone f \ apx_meet_below_nu f" hence 2: "?l \ \ f" by (metis apx_meet_below_nu_nu_below_mu_nu mu_nu_apx_nu_def nu_below_mu_nu_mu_nu_apx_nu) hence 3: "?l \ f(?l)" using 1 by (smt add_left_isotone add_left_upper_bound apx_def greatest_fixpoint is_greatest_fixpoint_def is_least_fixpoint_def isotone_def l_below_nu least_fixpoint n_l_nu order_trans) have "f(?l) \ ?l" using 1 2 by (smt apx_isotone_def apx_meet_char greatest_fixpoint is_apx_meet_def is_greatest_fixpoint_def is_least_fixpoint_def least_fixpoint mu_nu_apx_meet_def mu_nu_apx_nu_def mu_nu_apx_nu_mu_nu_apx_meet) thus "xi_mu_nu f" using 1 2 3 by (smt add_left_isotone apx_antisymmetric apx_def apx_least_fixpoint_char greatest_fixpoint is_apx_least_fixpoint_def is_greatest_fixpoint_def is_least_fixpoint_def least_fixpoint n_l_nu order_trans xi_mu_nu_def) qed lemma xi_mu_nu_has_apx_least_fixpoint: "xi_mu_nu f \ has_apx_least_fixpoint f" by (metis xi_mu_nu_def) lemma nu_below_mu_nu_xi_mu_nu: "has_least_fixpoint f \ has_greatest_fixpoint f \ isotone f \ apx_isotone f \ nu_below_mu_nu f \ xi_mu_nu f" by (metis apx_meet_below_nu_xi_mu_nu mu_nu_apx_meet_apx_meet_below_nu mu_nu_apx_nu_mu_nu_apx_meet nu_below_mu_nu_mu_nu_apx_nu) lemma xi_mu_nu_nu_below_mu_nu: "has_least_fixpoint f \ has_greatest_fixpoint f \ xi_mu_nu f \ nu_below_mu_nu f" by (metis apx_meet_below_nu_nu_below_mu_nu has_apx_least_fixpoint_xi_apx_meet xi_apx_meet_apx_meet_below_nu xi_mu_nu_has_apx_least_fixpoint) definition xi_mu_nu_ni :: "('a \ 'a) \ bool" where "xi_mu_nu_ni f \ has_apx_least_fixpoint f \ \ f = \ f + ni(\ f)" lemma xi_mu_nu_ni_xi_mu_nu: "xi_mu_nu_ni f \ xi_mu_nu f" by (metis ni_def xi_mu_nu_def xi_mu_nu_ni_def) lemma nu_below_mu_nu_xi_mu_nu_ni: "has_least_fixpoint f \ has_greatest_fixpoint f \ isotone f \ apx_isotone f \ nu_below_mu_nu f \ xi_mu_nu_ni f" by (metis nu_below_mu_nu_xi_mu_nu xi_mu_nu_ni_xi_mu_nu) lemma xi_mu_nu_ni_nu_below_mu_nu: "has_least_fixpoint f \ has_greatest_fixpoint f \ xi_mu_nu_ni f \ nu_below_mu_nu f" by (metis xi_mu_nu_ni_xi_mu_nu xi_mu_nu_nu_below_mu_nu) end class itering_apx = itering_nL + semiring_apx begin lemma circ_apx_isotone: "x \ y \ x\<^sup>\ \ y\<^sup>\" proof assume "x \ y" hence 1: "x \ y + n(x) ; L \ y \ x + n(x) ; T" by (metis apx_def) hence "y\<^sup>\ \ x\<^sup>\ + x\<^sup>\ ; n(x) ; T" by (metis circ_isotone circ_left_top circ_unfold_sum mult_associative) hence 2: "y\<^sup>\ \ x\<^sup>\ + n(x\<^sup>\) ; T" by (smt add_least_upper_bound mult_left_isotone n_isotone n_top_split order_refl order_trans right_plus_below_circ zero_right_mult_decreasing) have "x\<^sup>\ \ y\<^sup>\ + y\<^sup>\ ; n(x) ; L" using 1 by (metis L_left_zero circ_isotone circ_unfold_sum mult_associative) also have "... = y\<^sup>\ + n(y\<^sup>\ ; x) ; L" by (metis add_associative add_right_zero mult_associative mult_zero_add_circ_2 n_L_split n_mult_right_zero) also have "... \ y\<^sup>\ + n(x\<^sup>\ ; x) ; L + n(x\<^sup>\) ; n(T ; x) ; L" using 2 by (metis add_associative add_right_isotone mult_associative mult_left_isotone mult_right_dist_add n_dist_add n_export n_isotone) finally have "x\<^sup>\ \ y\<^sup>\ + n(x\<^sup>\) ; L" by (metis add_associative circ_plus_same n_add_left_absorb_mult n_circ_left_unfold n_dist_add n_export ni_def ni_dist_add) thus "x\<^sup>\ \ y\<^sup>\" using 2 by (metis apx_def) qed end class omega_algebra_apx = omega_algebra_nL + semiring_apx sublocale omega_algebra_apx < star!: itering_apx where circ = star .. sublocale omega_algebra_apx < nL_omega!: itering_apx where circ = Omega .. context omega_algebra_apx begin lemma omega_apx_isotone: "x \ y \ x\<^sup>\ \ y\<^sup>\" proof assume "x \ y" hence 1: "x \ y + n(x) ; L \ y \ x + n(x) ; T" by (metis apx_def) hence "y\<^sup>\ \ x\<^sup>\ ; n(x) ; T ; (x\<^sup>\ ; n(x) ; T)\<^sup>\ + x\<^sup>\ + x\<^sup>\ ; n(x) ; T ; (x\<^sup>\ ; n(x) ; T)\<^sup>\ ; x\<^sup>\" by (smt add_associative mult_associative mult_left_one mult_right_dist_add omega_decompose omega_isotone omega_unfold star_left_unfold_equal) also have "... \ n(x\<^sup>\ ; x) ; T + x\<^sup>\" by (smt add_least_upper_bound add_left_isotone mult_associative mult_right_isotone n_top_split order_trans star_zero_below_omega top_greatest) finally have 2: "y\<^sup>\ \ x\<^sup>\ + n(x\<^sup>\) ; T" by (metis add_commutative add_right_isotone mult_left_isotone n_star_below_n_omega n_star_left_unfold order_trans star.circ_plus_same) have "x\<^sup>\ \ y\<^sup>\ + y\<^sup>\ ; 0 + n(y\<^sup>\ ; x) ; L" using 1 by (metis add_right_upper_bound less_eq_def nL_omega.mult_L_circ nL_omega.mult_L_circ_mult mult_L_omega mult_L_star mult_associative omega_decompose omega_isotone add_associative mult_associative ni_def ni_split) also have "... \ y\<^sup>\ + n(x\<^sup>\ ; x) ; L + n(x\<^sup>\) ; n(T ; x) ; L" using 1 by (metis add_right_isotone add_right_zero apx_def mult_associative mult_left_dist_add mult_left_isotone mult_right_dist_add n_dist_add n_export n_isotone star.circ_apx_isotone star_mult_omega add_associative) finally have "x\<^sup>\ \ y\<^sup>\ + n(x\<^sup>\) ; L" by (metis add_associative add_isotone mult_right_dist_add n_add_left_absorb_mult n_star_left_unfold ni_def ni_star_below_ni_omega order_refl order_trans star.circ_plus_same) thus "x\<^sup>\ \ y\<^sup>\" using 2 by (metis apx_def) qed end class omega_algebra_apx_extra = omega_algebra_apx + assumes n_split_omega: "x\<^sup>\ \ x\<^sup>\ ; 0 + n(x\<^sup>\) ; T" begin lemma omega_n_star: "x\<^sup>\ + n(x\<^sup>\) ; T \ x\<^sup>\ ; n(x\<^sup>\) ; T" by (smt add_least_upper_bound mult_associative mult_left_isotone mult_left_one mult_right_isotone n_split_omega n_star_below_n_omega order_trans star.circ_reflexive zero_least) lemma n_omega_zero: "n(x\<^sup>\) = 0 \ n(x\<^sup>\) = 0 \ x\<^sup>\ \ x\<^sup>\ ; 0" by (metis add_right_zero eq_iff mult_left_zero n_mult_zero n_split_omega star_zero_below_omega) lemma n_split_nu_mu: "y\<^sup>\ + y\<^sup>\ ; z \ y\<^sup>\ ; z + n(y\<^sup>\ + y\<^sup>\ ; z) ; T" by (smt add_least_upper_bound mult_isotone n_isotone n_split_omega order_refl order_trans zero_least) lemma loop_exists: "\ (\x . y ; x + z) \ \ (\x . y ; x + z) + n(\ (\x . y ; x + z)) ; T" by (metis n_split_nu_mu omega_loop_nu star_loop_mu) lemma loop_isotone: "isotone (\x . y ; x + z)" by (smt add_commutative add_right_isotone isotone_def mult_right_isotone) lemma loop_apx_isotone: "apx_isotone (\x . y ; x + z)" by (smt add_apx_left_isotone apx_isotone_def mult_apx_right_isotone) lemma loop_has_least_fixpoint: "has_least_fixpoint (\x . y ; x + z)" by (metis has_least_fixpoint_def star_loop_is_least_fixpoint) lemma loop_has_greatest_fixpoint: "has_greatest_fixpoint (\x . y ; x + z)" by (metis has_greatest_fixpoint_def omega_loop_is_greatest_fixpoint) lemma loop_apx_least_fixpoint: "is_apx_least_fixpoint (\x . y ; x + z) (\ (\x . y ; x + z) + n(\ (\x . y ; x + z)) ; L)" by (metis apx_least_fixpoint_char loop_apx_isotone loop_exists loop_has_greatest_fixpoint loop_has_least_fixpoint loop_isotone nu_below_mu_nu_def nu_below_mu_nu_xi_mu_nu xi_mu_nu_def) lemma loop_has_apx_least_fixpoint: "has_apx_least_fixpoint (\x . y ; x + z)" by (metis has_apx_least_fixpoint_def loop_apx_least_fixpoint) lemma loop_semantics: "\ (\x . y ; x + z) = \ (\x . y ; x + z) + n(\ (\x . y ; x + z)) ; L" by (metis apx_least_fixpoint_char loop_apx_least_fixpoint) lemma loop_apx_least_fixpoint_ni: "is_apx_least_fixpoint (\x . y ; x + z) (\ (\x . y ; x + z) + ni(\ (\x . y ; x + z)))" by (metis loop_apx_least_fixpoint ni_def) lemma loop_semantics_ni: "\ (\x . y ; x + z) = \ (\x . y ; x + z) + ni(\ (\x . y ; x + z))" by (metis loop_semantics ni_def) lemma loop_semantics_xi_mu_nu: "\ (\x . y ; x + z) = n(y\<^sup>\) ; L + y\<^sup>\ ; z" proof - have "\ (\x . y ; x + z) = y\<^sup>\ ; z + n(y\<^sup>\ + y\<^sup>\ ; z) ; L" by (metis loop_semantics omega_loop_nu star_loop_mu) thus ?thesis by (smt add_associative add_commutative less_eq_def mult_right_dist_add n_L_decreasing n_dist_add) qed end (* end *) end