(* Walter Guttmann, 2012.04.17 *) (* use with Isabelle2011 *) theory ULSC 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 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 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 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 Domain imports Semiring 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) lemma d_mult_below: "d(x) ; y \ y" by (metis add_left_divisibility d_plus_one mult_left_one mult_right_dist_add) lemma d_preserves_equation: "d(y) ; x \ x ; d(y) \ d(y) ; x = d(y) ; x ; d(y)" by (smt antisym d_below_one d_idempotent mult_associative mult_left_isotone mult_left_one mult_right_isotone mult_right_one) 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 ExtendedDesigns imports Omega Domain begin *) class semiring_dL_below = domain_semiring + fixes L :: "'a" assumes L_left_zero_below: "L ; x \ L" assumes mult_L_split: "x ; L = x ; 0 + d(x) ; L" begin lemma d_zero_mult_L: "d(x ; 0) ; L \ x" by (metis add_least_upper_bound mult_L_split mult_associative mult_left_zero zero_right_mult_decreasing) lemma mult_L: "x ; L \ x ; 0 + L" by (metis add_right_isotone d_mult_below mult_L_split) lemma d_mult_L: "d(x) ; L \ x ; L" by (metis add_right_divisibility mult_L_split) 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) lemma L_L: "L ; L = L" by (metis d_restrict_equals less_eq_def mult_L_split zero_right_mult_decreasing) end class ed_below = omega_algebra_T + semiring_dL_below + Omega + assumes Omega_def: "x\<^sup>\ = d(x\<^sup>\) ; L + x\<^sup>\" begin lemma Omega_isotone: "x \ y \ x\<^sup>\ \ y\<^sup>\" by (metis Omega_def add_isotone d_isotone mult_left_isotone omega_isotone star.circ_isotone) lemma star_below_Omega: "x\<^sup>\ \ x\<^sup>\" by (metis Omega_def add_right_upper_bound) lemma one_below_Omega: "1 \ x\<^sup>\" by (metis add_least_upper_bound star.circ_plus_one star_below_Omega) lemma L_left_zero_star: "L ; x\<^sup>\ = L" by (metis L_left_zero_below add_right_upper_bound antisym star.circ_back_loop_fixpoint) lemma L_left_zero_Omega: "L ; x\<^sup>\ = L" by (metis L_left_zero_below L_left_zero_star Omega_def less_eq_def mult_left_dist_add) lemma mult_L_star: "(x ; L)\<^sup>\ = 1 + x ; L" by (metis L_left_zero_star mult_associative star.circ_left_unfold) lemma mult_L_omega_below: "(x ; L)\<^sup>\ \ x ; L" by (metis L_left_zero_below mult_right_isotone omega_slide) lemma mult_L_add_star: "(x ; L + y)\<^sup>\ = y\<^sup>\ + y\<^sup>\ ; x ; L" by (metis L_left_zero_star add_commutative mult_associative star.circ_unfold_sum) lemma mult_L_add_omega_below: "(x ; L + y)\<^sup>\ \ y\<^sup>\ + y\<^sup>\ ; x ; L" proof - have "(x ; L + y)\<^sup>\ = (y\<^sup>\ ; x ; L)\<^sup>\ + (y\<^sup>\ ; x ; L)\<^sup>\ ; y\<^sup>\" by (metis add_commutative mult_associative omega_decompose) also have "... \ y\<^sup>\ ; x ; L + (y\<^sup>\ ; x ; L)\<^sup>\ ; y\<^sup>\" by (metis add_left_isotone mult_L_omega_below) also have "... = y\<^sup>\ ; x ; L + y\<^sup>\ ; x ; L ; y\<^sup>\ + y\<^sup>\" by (smt L_left_zero_star add_associative add_commutative mult_associative star.circ_loop_fixpoint) also have "... \ y\<^sup>\ + y\<^sup>\ ; x ; L" by (metis L_left_zero_star add_commutative eq_refl mult_associative star.circ_back_loop_fixpoint) finally show ?thesis . qed lemma mult_L_add_circ: "(x ; L + y)\<^sup>\ = d(y\<^sup>\) ; L + y\<^sup>\ + y\<^sup>\ ; x ; L" proof - have "(x ; L + y)\<^sup>\ = d((x ; L + y)\<^sup>\) ; L + (x ; L + y)\<^sup>\" by (metis Omega_def) also have "... \ d(y\<^sup>\ + y\<^sup>\ ; x ; L) ; L + (x ; L + y)\<^sup>\" by (metis add_left_isotone d_isotone mult_L_add_omega_below mult_left_isotone) also have "... = d(y\<^sup>\) ; L + d(y\<^sup>\ ; x ; L) ; L + (x ; L + y)\<^sup>\" by (metis d_dist_add mult_right_dist_add) also have "... \ d(y\<^sup>\) ; L + y\<^sup>\ ; x ; L ; L + (x ; L + y)\<^sup>\" by (metis add_left_isotone add_right_isotone d_mult_L) also have "... = d(y\<^sup>\) ; L + y\<^sup>\ + y\<^sup>\ ; x ; L" by (smt L_L add_associative add_commutative less_eq_def mult_L_add_star mult_associative order_refl) finally have 1: "(x ; L + y)\<^sup>\ \ d(y\<^sup>\) ; L + y\<^sup>\ + y\<^sup>\ ; x ; L" . have 2: "d(y\<^sup>\) ; L \ (x ; L + y)\<^sup>\" by (metis Omega_def add_left_upper_bound add_right_upper_bound d_isotone mult_left_isotone omega_isotone order_trans) have "y\<^sup>\ + y\<^sup>\ ; x ; L \ (x ; L + y)\<^sup>\" by (metis Omega_def add_right_upper_bound mult_L_add_star) hence "d(y\<^sup>\) ; L + y\<^sup>\ + y\<^sup>\ ; x ; L \ (x ; L + y)\<^sup>\" using 2 by (metis Omega_def add_least_upper_bound add_right_upper_bound mult_L_add_star) thus ?thesis using 1 by (metis antisym) qed 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)" proof - have "(x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\ = ((d(x\<^sup>\) ; L + x\<^sup>\) ; y)\<^sup>\ ; x\<^sup>\" by (metis Omega_def) also have "... = (d(x\<^sup>\) ; L ; y + x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" by (metis mult_right_dist_add) also have "... \ (d(x\<^sup>\) ; L + x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" by (metis L_left_zero_below Omega_isotone add_left_isotone mult_associative mult_left_isotone mult_right_isotone) also have "... = (d((x\<^sup>\ ; y)\<^sup>\) ; L + (x\<^sup>\ ; y)\<^sup>\ + (x\<^sup>\ ; y)\<^sup>\ ; d(x\<^sup>\) ; L) ; x\<^sup>\" by (metis mult_L_add_circ) also have "... = d((x\<^sup>\ ; y)\<^sup>\) ; L ; x\<^sup>\ + (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\ + (x\<^sup>\ ; y)\<^sup>\ ; d(x\<^sup>\) ; L ; x\<^sup>\" by (metis mult_right_dist_add) also have "... = 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_Omega mult_associative) also have "... = d((x\<^sup>\ ; y)\<^sup>\) ; L + ((x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\ + (x\<^sup>\ ; y)\<^sup>\ ; d(x\<^sup>\) ; L)" by (smt Omega_def add_associative add_commutative add_idempotent mult_associative mult_left_dist_add) finally have 1: "(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)" . have "d((x\<^sup>\ ; y)\<^sup>\) ; L \ (x\<^sup>\ ; y)\<^sup>\" by (metis Omega_def Omega_isotone add_commutative add_right_upper_bound mult_left_isotone order_trans) also have "... \ (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" by (metis mult_right_isotone mult_right_one one_below_Omega) finally have 2: "d((x\<^sup>\ ; y)\<^sup>\) ; L \ (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" . have 3: "(x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\ \ (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" by (smt Omega_isotone mult_left_isotone mult_right_isotone order_trans star_below_Omega) have "(x\<^sup>\ ; y)\<^sup>\ ; d(x\<^sup>\) ; L \ (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" by (metis Omega_def add_commutative mult_associative mult_left_subdist_add_right) also have "... \ (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" by (metis Omega_isotone mult_left_isotone order_trans star_below_Omega) finally have "d((x\<^sup>\ ; y)\<^sup>\) ; L + ((x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\ + (x\<^sup>\ ; y)\<^sup>\ ; d(x\<^sup>\) ; L) \ (x\<^sup>\ ; y)\<^sup>\ ; x\<^sup>\" using 2 3 by (smt add_associative less_eq_def) thus ?thesis using 1 by (metis antisym) qed (* lemma mult_L_omega: "(x ; L)\<^sup>\ = x ; L" nitpick lemma mult_L_add_omega: "(x ; L + y)\<^sup>\ = y\<^sup>\ + y\<^sup>\ ; x ; L" nitpick lemma d_Omega_circ_simulate_right_plus: "z ; x \ y ; y\<^sup>\ ; z + w \ z ; x\<^sup>\ \ y\<^sup>\ ; (z + w ; x\<^sup>\)" nitpick lemma d_Omega_circ_simulate_left_plus: "x ; z \ z ; y\<^sup>\ + w \ x\<^sup>\ ; z \ (z + x\<^sup>\ ; w) ; y\<^sup>\" nitpick *) end class ed = ed_below + assumes L_left_zero: "L ; x = L" begin lemma mult_L_omega: "(x ; L)\<^sup>\ = x ; L" by (metis L_left_zero omega_slide) 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 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 "z ; x \ y ; d(y\<^sup>\) ; L ; z + y ; y\<^sup>\ ; z + w" by (metis Omega_def mult_associative mult_left_dist_add mult_right_dist_add) also have "... \ y ; d(y\<^sup>\) ; L + y ; y\<^sup>\ ; z + w" by (metis L_left_zero_below add_commutative add_right_isotone mult_associative mult_right_isotone) also have "... = y ; 0 + d(y ; y\<^sup>\) ; L + y ; y\<^sup>\ ; z + w" by (metis d_L_split) also have "... = d(y\<^sup>\) ; L + y ; y\<^sup>\ ; z + w" by (smt add_associative add_commutative add_left_zero mult_associative mult_left_dist_add omega_unfold) finally have 1: "z ; x \ d(y\<^sup>\) ; L + y ; y\<^sup>\ ; z + w" . have "(d(y\<^sup>\) ; L + y\<^sup>\ ; z + y\<^sup>\ ; w ; d(x\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\) ; x = d(y\<^sup>\) ; L ; x + y\<^sup>\ ; z ; x + y\<^sup>\ ; w ; d(x\<^sup>\) ; L ; x + y\<^sup>\ ; w ; x\<^sup>\ ; x" by (metis mult_right_dist_add) also have "... \ d(y\<^sup>\) ; L + y\<^sup>\ ; z ; x + y\<^sup>\ ; w ; d(x\<^sup>\) ; L ; x + y\<^sup>\ ; w ; x\<^sup>\ ; x" by (metis L_left_zero_below add_left_isotone mult_associative mult_right_isotone) also have "... \ d(y\<^sup>\) ; L + y\<^sup>\ ; z ; x + y\<^sup>\ ; w ; d(x\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\ ; x" by (metis L_left_zero_below add_commutative add_left_isotone mult_associative mult_right_isotone) also have "... \ d(y\<^sup>\) ; L + y\<^sup>\ ; z ; x + y\<^sup>\ ; w ; d(x\<^sup>\) ; L + y\<^sup>\ ; w ; x\<^sup>\" by (metis add_left_upper_bound add_right_isotone star.circ_back_loop_fixpoint) also have "... \ 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>\" using 1 by (smt add_left_isotone add_right_isotone less_eq_def mult_associative mult_left_dist_add) 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 ; x\<^sup>\ + w ; x\<^sup>\" using 1 by (metis add_commutative mult_left_isotone mult_right_dist_add) also have "... \ y ; y\<^sup>\ ; z ; x\<^sup>\ + d(y\<^sup>\) ; L + w ; x\<^sup>\" by (metis L_left_zero_below add_commutative add_right_isotone mult_associative mult_right_isotone) finally have "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>\ ; 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_star!: omega_itering where circ = star .. (* end theory Lattice imports Semiring begin *) class meet = fixes meet :: "'a \ 'a \ 'a" (infixl "\" 65) class semiring_lattice = semiring_T + meet + assumes meet_associative : "(x \ y) \ z = x \ (y \ z)" assumes meet_commutative : "x \ y = y \ x" assumes meet_idempotent : "x \ x = x" assumes meet_left_zero : "0 \ x = 0" assumes meet_left_top : "T \ x = x" assumes meet_left_dist_add : "x \ (y + z) = (x \ y) + (x \ z)" assumes add_left_dist_meet : "x + (y \ z) = (x + y) \ (x + z)" assumes meet_absorb : "x \ (x + y) = x" assumes add_absorb : "x + (x \ y) = x" begin lemma less_eq_meet: "x \ y \ x \ y = x" by (metis add_absorb add_right_upper_bound less_eq_def meet_absorb meet_commutative) lemma meet_left_isotone: "x \ y \ x \ z \ y \ z" by (smt less_eq_def meet_commutative meet_left_dist_add) lemma meet_right_isotone: "x \ y \ z \ x \ z \ y" by (metis meet_commutative meet_left_isotone) lemma meet_isotone: "w \ y \ x \ z \ w \ x \ y \ z" by (smt less_eq_meet meet_associative meet_commutative) lemma meet_left_upper_bound: "x \ y \ x" by (metis add_absorb add_right_divisibility) lemma meet_right_upper_bound: "x \ y \ y" by (metis meet_commutative meet_left_upper_bound) lemma meet_least_upper_bound: "z \ x \ z \ y \ z \ x \ y" by (metis less_eq_meet meet_associative meet_left_upper_bound) lemma meet_left_divisibility: "y \ x \ (\z . x \ z = y)" by (metis less_eq_meet meet_commutative meet_left_upper_bound) lemma meet_right_divisibility: "y \ x \ (\z . z \ x = y)" by (metis meet_commutative meet_left_divisibility) lemma meet_right_zero: "x \ 0 = 0" by (metis meet_commutative meet_left_zero) lemma mult_left_subdist_meet_left: "x ; (y \ z) \ x ; y" by (metis meet_left_upper_bound mult_right_isotone) lemma mult_left_subdist_meet_right: "x ; (y \ z) \ x ; z" by (metis meet_commutative mult_left_subdist_meet_left) lemma mult_right_subdist_meet_left: "(x \ y) ; z \ x ; z" by (metis meet_left_upper_bound mult_left_isotone) lemma mult_right_subdist_meet_right: "(x \ y) ; z \ y ; z" by (metis meet_right_upper_bound mult_left_isotone) lemma mult_same_context:"x \ y \ z \ y \ x \ z \ x \ z = y \ z" by (metis eq_iff meet_least_upper_bound) lemma mult_right_top: "x \ T = x" by (metis meet_commutative meet_left_top) lemma vector_mult_closed: "vector x \ vector y \ vector (x \ y)" by (metis antisym meet_least_upper_bound mult_right_subdist_meet_left mult_right_subdist_meet_right top_right_mult_increasing vector_def) lemma relative_equality: "x + z = y + z \ x \ z = y \ z \ x = y" by (metis add_absorb add_commutative add_left_dist_meet) end (* end theory Common imports Domain Lattice begin *) class domain_semiring_lattice = domain_semiring + semiring_lattice begin lemma d_top: "d(T) = 1" by (metis add_left_top d_dist_add d_one d_plus_one) lemma mult_domain_top: "x ; d(y) ; T \ d(x ; y) ; T" by (smt d_mult_d d_restrict_equals mult_associative mult_right_isotone top_greatest) lemma meet_domain: "x \ d(y) ; z = d(y) ; (x \ z)" apply (rule antisym) apply (smt add_commutative add_right_divisibility d_export d_isotone d_mult_left_lower_bound d_plus_one d_restrict_equals meet_right_isotone meet_right_upper_bound mult_left_isotone mult_left_one mult_right_isotone order_trans) by (metis d_plus_one meet_least_upper_bound mult_left_one mult_left_subdist_meet_right mult_right_subdist_add_left) lemma meet_intro_domain: "x \ y = d(y) ; x \ y" by (metis d_restrict_equals meet_commutative meet_domain) lemma meet_domain_top: "x \ d(y) ; T = d(y) ; x" by (metis meet_domain mult_right_top) (* lemma "d(x) = x ; T \ 1" nitpick *) lemma d_galois: "d(x) \ d(y) \ x \ d(y) ; T" by (metis d_isotone d_least_left_preserver meet_domain_top meet_least_upper_bound) lemma vector_meet: "x ; T \ y \ d(x) ; y" by (metis d_galois d_mult_sub meet_commutative meet_domain_top meet_right_isotone) end class domain_semiring_lattice_L = domain_semiring_lattice + fixes L :: "'a" assumes l1: "x ; L = x ; 0 + d(x) ; L" assumes l2: "d(L) ; x \ x ; d(L)" assumes l3: "d(L) ; T \ L + d(L ; 0) ; T" assumes l4: "L ; T \ L" assumes l5: "x ; 0 \ L \ (x \ L) ; 0" begin lemma l8: "(x \ L) ; 0 \ x ; 0 \ L" by (metis meet_commutative meet_least_upper_bound mult_right_subdist_meet_right zero_right_mult_decreasing) lemma l9: "x ; 0 \ L \ d(x ; 0) ; L" by (metis d_restrict_equals meet_commutative meet_domain meet_right_upper_bound) lemma l10: "L ; L = L" by (metis d_restrict_equals l1 less_eq_def zero_right_mult_decreasing) lemma l11: "d(x) ; L \ x ; L" by (metis add_right_upper_bound l1) lemma l12: "d(x ; 0) ; L \ x ; 0" by (metis add_right_divisibility l1 mult_associative mult_left_zero) lemma l13: "d(x ; 0) ; L \ x" by (metis l12 order_trans zero_right_mult_decreasing) lemma l14: "x ; L \ x ; 0 + L" by (metis add_right_isotone l1 meet_domain_top meet_left_upper_bound) lemma l15: "x ; d(y) ; L = x ; 0 + d(x ; y) ; L" by (metis d_commutative d_mult_d d_zero l1 mult_associative mult_left_zero) lemma l16: "x ; T \ L \ x ; L" by (metis l11 order_trans vector_meet) lemma l17: "d(x) ; L \ d(x ; L) ; L" by (smt d_restrict_equals l11 meet_domain_top meet_least_upper_bound meet_left_divisibility order_trans) lemma l18: "d(x) ; L = d(x ; L) ; L" by (metis antisym d_mult_sub l17 mult_left_isotone) lemma l19: "d(x ; T ; 0) ; L \ d(x ; L) ; L" by (metis d_mult_sub l18 mult_associative mult_left_isotone) lemma l20: "x \ y \ x \ y + L \ x \ y + d(y ; 0) ; T" apply rule apply (metis add_absorb less_eq_meet meet_left_dist_add) by (smt add_commutative add_left_dist_meet l13 less_eq_def meet_domain_top) lemma l21: "d(x ; 0) ; L \ x ; 0 \ L" by (metis l12 meet_domain_top meet_least_upper_bound meet_left_upper_bound) lemma l22: "x ; 0 \ L = d(x ; 0) ; L" by (metis antisym l9 l21) lemma l23: "x ; T \ L = d(x) ; L" apply (rule antisym) apply (metis vector_meet) by (metis add_least_upper_bound d_mult_below l1 meet_least_upper_bound mult_right_isotone top_greatest) lemma l29: "L ; d(L) = L" by (metis d_preserves_equation d_restrict_equals l2) lemma l30: "d(L) ; x \ (x \ L) + d(L ; 0) ; x" by (metis l3 less_eq_def meet_domain_top meet_left_dist_add) lemma l31: "d(L) ; x = (x \ L) + d(L ; 0) ; x" by (smt add_least_upper_bound antisym d_mult_sub d_restrict_equals l30 meet_domain mult_left_isotone mult_left_subdist_meet_left) lemma l40: "L ; x \ L" by (metis add_right_top l4 mult_left_subdist_add_left order_trans) lemma l41: "L ; T = L" by (metis antisym l4 top_right_mult_increasing) lemma l50: "x ; 0 \ L = (x \ L) ; 0" by (metis eq_iff l5 l8) lemma l51: "d(x ; 0) ; L = (x \ L) ; 0" by (metis l22 l50) lemma l90: "L ; T ; L = L" by (metis add_commutative d_restrict_equals d_top l1 l51 l31 meet_absorb meet_commutative mult_associative mult_left_dist_add mult_left_zero mult_right_one) lemma l91: "x = x ; T \ d(L ; 0) ; x \ d(x ; 0) ; T" proof - have "d(L ; 0) ; x \ d(d(L ; 0) ; x) ; T" by (metis d_galois order_refl) also have "... = d(d(L ; 0) ; d(x)) ; T" by (metis d_mult_d) also have "... = d(d(x) ; L ; 0) ; T" by (metis d_commutative d_mult_d mult_associative) also have "... \ d(x ; L ; 0) ; T" by (metis d_isotone l11 mult_left_isotone) also have "... \ d(x ; T ; 0) ; T" by (metis d_isotone mult_left_isotone mult_right_isotone top_greatest) finally show ?thesis by metis qed lemma l92: "x = x ; T \ d(L ; 0) ; x \ d((x \ L) ; 0) ; T" proof assume 1: "x = x ; T" have "d(L ; 0) ; x = d(L) ; d(L ; 0) ; x" by (metis d_commutative d_mult_sub d_order) also have "... \ d(L) ; d(x ; 0) ; T" using 1 by (metis eq_iff l91 mult_associative mult_isotone) also have "... = d(d(x ; 0) ; L) ; T" by (metis d_commutative d_export) also have "... \ d((x \ L) ; 0) ; T" by (metis l51 order_refl) finally show "d(L ; 0) ; x \ d((x \ L) ; 0) ; T" by metis qed end (* end theory CommonIteration imports Common Omega begin *) class domain_itering_lattice_L = itering_T + domain_semiring_lattice_L begin lemma mult_L_circ: "(x ; L)\<^sup>\ = 1 + x ; L" by (metis circ_back_loop_fixpoint circ_mult l40 less_eq_def mult_associative) lemma mult_L_circ_mult_below: "(x ; L)\<^sup>\ ; y \ y + x ; L" by (smt add_right_isotone l40 mult_L_circ mult_associative mult_left_one mult_right_dist_add mult_right_isotone) lemma circ_L: "L\<^sup>\ = L + 1" by (metis add_commutative l10 mult_L_circ) lemma circ_d0_L: "x\<^sup>\ ; d(x ; 0) ; L = x\<^sup>\ ; 0" by (metis add_right_zero circ_loop_fixpoint circ_plus_same d_zero l15 mult_associative mult_left_zero) lemma d0_circ_left_unfold: "d(x\<^sup>\ ; 0) = d(x ; x\<^sup>\ ; 0)" by (metis add_commutative add_left_zero circ_loop_fixpoint mult_associative) lemma d_circ_import: "d(y) ; x \ x ; d(y) \ d(y) ; x\<^sup>\ = d(y) ; (d(y) ; x)\<^sup>\" by (rule, rule antisym, metis circ_simulate circ_slide mult_associative d_idempotent d_preserves_equation, metis circ_isotone mult_left_isotone mult_left_one mult_right_isotone d_below_one) end class domain_omega_algebra_lattice_L = omega_algebra_T + domain_semiring_lattice_L begin lemma mult_L_star: "(x ; L)\<^sup>\ = 1 + x ; L" by (metis l40 less_eq_def mult_associative star.circ_back_loop_fixpoint star.circ_mult) lemma mult_L_omega: "(x ; L)\<^sup>\ \ x ; L" by (smt l41 less_eq_def mult_associative mult_left_dist_add omega_unfold top_greatest) lemma mult_L_add_star: "(x ; L + y)\<^sup>\ = y\<^sup>\ + y\<^sup>\ ; x ; L" proof (rule antisym) have "(x ; L + y) ; (y\<^sup>\ + y\<^sup>\ ; x ; L) = x ; L ; (y\<^sup>\ + y\<^sup>\ ; x ; L) + y ; (y\<^sup>\ + y\<^sup>\ ; x ; L)" by (metis mult_associative mult_right_dist_add) also have "... \ x ; L + y ; (y\<^sup>\ + y\<^sup>\ ; x ; L)" by (metis add_left_isotone l40 mult_associative mult_right_isotone) also have "... \ x ; L + y ; y\<^sup>\ + y\<^sup>\ ; x ; L" by (smt add_associative add_commutative add_right_upper_bound mult_associative mult_left_dist_add star.circ_loop_fixpoint) also have "... \ x ; L + y\<^sup>\ + y\<^sup>\ ; x ; L" by (metis add_left_isotone add_right_isotone star.left_plus_below_circ) also have "... = y\<^sup>\ + y\<^sup>\ ; x ; L" by (metis add_associative add_commutative mult_associative star.circ_loop_fixpoint star.circ_reflexive star.circ_sup_one_right_unfold star_involutive) finally have "1 + (x ; L + y) ; (y\<^sup>\ + y\<^sup>\ ; x ; L) \ y\<^sup>\ + y\<^sup>\ ; x ; L" by (metis add_commutative add_least_upper_bound add_right_divisibility star.circ_left_unfold) thus "(x ; L + y)\<^sup>\ \ y\<^sup>\ + y\<^sup>\ ; x ; L" by (metis mult_right_one star_left_induct) next show "y\<^sup>\ + y\<^sup>\ ; x ; L \ (x ; L + y)\<^sup>\" by (metis add_commutative add_least_upper_bound mult_associative star.circ_increasing star.circ_mult_upper_bound star.circ_sub_dist) qed lemma mult_L_add_omega: "(x ; L + y)\<^sup>\ \ y\<^sup>\ + y\<^sup>\ ; x ; L" proof - have 1: "(y\<^sup>\ ; x ; L)\<^sup>\ \ y\<^sup>\ + y\<^sup>\ ; x ; L" by (metis add_least_upper_bound add_right_isotone mult_L_omega) have "(y\<^sup>\ ; x ; L)\<^sup>\ ; y\<^sup>\ \ y\<^sup>\ + y\<^sup>\ ; x ; L" by (metis add_right_isotone l40 mult_associative mult_right_isotone star_left_induct) thus ?thesis using 1 by (smt add_associative add_commutative less_eq_def mult_associative omega_decompose) qed end sublocale domain_omega_algebra_lattice_L < dL_star!: omega_itering where circ = star .. sublocale domain_omega_algebra_lattice_L < dL_star!: domain_itering_lattice_L where circ = star .. context domain_omega_algebra_lattice_L begin lemma d0_star_below_d0_omega: "d(x\<^sup>\ ; 0) \ d(x\<^sup>\ ; 0)" by (metis d_isotone star_zero_below_omega_zero) lemma d0_below_d0_omega: "d(x ; 0) \ d(x\<^sup>\ ; 0)" by (metis d0_star_below_d0_omega d_isotone mult_left_isotone order_trans star.circ_increasing) lemma star_d0_L: "x\<^sup>\ ; d(x ; 0) ; L = x\<^sup>\ ; 0" by (metis dL_star.circ_d0_L) 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_d_L_split_equal: "d(x ; y) \ d(y) \ x\<^sup>\ ; d(y) ; L = x\<^sup>\ ; 0 + d(y) ; L" by (metis add_right_isotone l15 less_eq_def mult_right_subdist_add_left star_L_split_same) lemma d0_omega_mult: "d(x\<^sup>\ ; y ; 0) = d(x\<^sup>\ ; 0)" by (smt antisym mult_associative mult_left_isotone mult_right_isotone omega_sub_vector zero_least) lemma d_star_left_unfold: "d(x\<^sup>\ ; 0) = d(x ; x\<^sup>\ ; 0)" by (metis dL_star.d0_circ_left_unfold) lemma d_star_import: "d(y) ; x \ x ; d(y) \ d(y) ; x\<^sup>\ = d(y) ; (d(y) ; x)\<^sup>\" by (metis dL_star.d_circ_import) lemma d_omega_export: "d(y) ; x \ x ; d(y) \ d(y) ; x\<^sup>\ = (d(y) ; x)\<^sup>\" apply (rule impI, rule antisym) apply (metis d_preserves_equation omega_simulation order_refl) by (smt less_eq_def mult_left_dist_add omega_simulation_2 omega_slide) lemma d_omega_import: "d(y) ; x \ x ; d(y) \ d(y) ; x\<^sup>\ = d(y) ; (d(y) ; x)\<^sup>\" by (metis d_idempotent d_omega_export mult_associative omega_slide) lemma star_d_omega_top: "x\<^sup>\ ; d(x\<^sup>\) ; T = x\<^sup>\ ; 0 + d(x\<^sup>\) ; T" apply (rule antisym) apply (metis add_right_upper_bound dL_star.circ_mult_omega mult_domain_top order_trans) by (metis add_commutative add_least_upper_bound add_left_divisibility dL_star.star_zero_below_circ_mult mult_associative star.circ_loop_fixpoint) lemma omega_meet_L: "x\<^sup>\ \ L = d(x\<^sup>\) ; L" by (metis l23 omega_vector) (* nitpick has no counterexamples: lemma d_star_mult: "d(x ; y) \ d(y) \ d(x\<^sup>\ ; y) = d(x\<^sup>\ ; 0) + d(y)" *) (* nitpick has counterexamples: lemma d0_split_omega_omega: "x\<^sup>\ \ x\<^sup>\ ; 0 + d(x\<^sup>\ \ L) ; T" *) end (* end theory Recursion imports CommonIteration begin *) class domain_semiring_lattice_apx = domain_semiring_lattice_L + fixes apx :: "'a \ 'a \ bool" (infix "\" 50) assumes apx_def: "x \ y \ x \ y + L \ d(L) ; y \ x + d(x ; 0) ; 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_least_upper_bound add_left_upper_bound apx_def d_plus_one mult_left_one mult_right_dist_add) lemma apx_L_least: "L \ x" by (metis add_right_upper_bound apx_def l3 mult_right_isotone order_trans top_greatest) lemma apx_transitive: "x \ y \ y \ z \ x \ z" proof assume 1: "x \ y \ y \ z" hence 2: "x \ z + L" by (smt add_associative add_commutative apx_def less_eq_def) have "d(d(L) ; y ; 0) ; T \ d((x + d(x ; 0) ; T) ; 0) ; T" using 1 by (metis apx_def d_isotone mult_left_isotone) also have "... \ d(x ; 0) ; T" by (metis add_least_upper_bound d_galois mult_left_isotone mult_right_dist_add order_refl zero_right_mult_decreasing) finally have 3: "d(d(L) ; y ; 0) ; T \ d(x ; 0) ; T" by metis have "d(L) ; z = d(L) ; (d(L) ; z)" by (metis d_idempotent mult_associative) also have "... \ d(L) ; y + d(d(L) ; y ; 0) ; T" using 1 by (metis apx_def calculation d_export less_eq_meet meet_domain mult_associative mult_left_dist_add) also have "... \ x + d(x ; 0) ; T" using 1 3 by (smt add_least_upper_bound add_right_upper_bound apx_def order_trans) finally show "x \ z" using 2 by (metis apx_def) qed lemma apx_meet_L: "y \ x \ x \ L \ y \ L" proof assume 1: "y \ x" have "x \ L = d(L) ; x \ L" by (metis d_restrict_equals meet_commutative meet_domain) also have "... \ (y + d(y ; 0) ; T) \ L" using 1 by (metis apx_def meet_left_isotone) also have "... \ y" by (metis add_least_upper_bound l13 meet_commutative meet_domain meet_left_dist_add meet_right_upper_bound mult_right_top) finally show "x \ L \ y \ L" by (metis meet_associative meet_idempotent meet_left_isotone) qed lemma apx_antisymmetric: "x \ y \ y \ x \ x = y" by (metis add_same_context antisym apx_def apx_meet_L relative_equality) lemma add_apx_left_isotone: "x \ y \ x + z \ y + z" proof assume 1: "x \ y" hence 2: "x + z \ y + z + L" by (smt add_associative add_commutative add_left_isotone apx_def) have "d(L) ; (y + z) = d(L) ; y + d(L) ; z" by (metis mult_left_dist_add) also have "... \ d(L) ; y + z" by (metis add_commutative add_least_upper_bound add_right_upper_bound d_below_one mult_left_dist_add mult_left_isotone mult_left_one) also have "... \ x + d(x ; 0) ; T + z" using 1 by (metis add_left_isotone apx_def) also have "... \ x + z + d((x + z) ; 0) ; T" by (smt add_associative add_commutative add_right_isotone d_isotone mult_left_isotone mult_right_subdist_add_left) finally show "x + z \ y + z" using 2 by (metis apx_def) qed lemma add_apx_right_isotone: "x \ y \ z + x \ z + y" by (metis add_commutative add_apx_left_isotone) lemma add_apx_isotone: "w \ y \ x \ z \ w + x \ y + z" by (metis add_apx_left_isotone add_apx_right_isotone apx_transitive) lemma mult_apx_left_isotone: "x \ y \ x ; z \ y ; z" proof assume 1: "x \ y" hence "x ; z \ y ; z + L ; z" by (metis apx_def mult_left_isotone mult_right_dist_add) hence 2: "x ; z \ y ; z + L" by (metis add_commutative add_left_isotone l40 order_trans) have "d(L) ; y ; z \ x ; z + d(x ; 0) ; T ; z" using 1 by (metis apx_def mult_left_isotone mult_right_dist_add) also have "... \ x ; z + d(x ; z ; 0) ; T" by (metis add_right_isotone d_isotone mult_associative mult_isotone mult_right_isotone top_greatest zero_least) finally show "x ; z \ y ; z" using 2 by (metis apx_def mult_associative) qed lemma mult_apx_right_isotone: "x \ y \ z ; x \ z ; y" proof assume 1: "x \ y" hence "z ; x \ z ; y + z ; L" by (metis apx_def mult_left_dist_add mult_right_isotone) also have "... \ z ; y + z ; 0 + L" by (metis add_associative add_right_isotone l14) finally have 2: "z ; x \ z ; y + L" by (metis add_right_zero mult_left_dist_add) have "d(L) ; z ; y \ z ; d(L) ; y" by (metis l2 mult_left_isotone) also have "... \ z ; (x + d(x ; 0) ; T)" using 1 by (metis apx_def mult_associative mult_right_isotone) also have "... = z ; x + z ; d(x ; 0) ; T" by (metis mult_associative mult_left_dist_add) also have "... \ z ; x + d(z ; x ; 0) ; T" by (metis add_right_isotone mult_associative mult_domain_top) finally show "z ; x \ z ; y" using 2 by (metis apx_def mult_associative) qed lemma mult_apx_isotone: "w \ y \ x \ z \ w ; x \ y ; z" by (metis apx_transitive mult_apx_left_isotone mult_apx_right_isotone) lemma meet_L_apx_isotone: "x \ y \ x \ L \ y \ L" by (smt add_absorb add_commutative apx_def apx_meet_L d_restrict_equals l20 meet_commutative meet_domain meet_left_upper_bound) 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 + (\ f \ L)" definition nu_below_mu_nu :: "('a \ 'a) \ bool" where "nu_below_mu_nu f \ d(L) ; \ f \ \ f + (\ f \ L) + d(\ f ; 0) ; T" definition nu_below_mu_nu_2 :: "('a \ 'a) \ bool" where "nu_below_mu_nu_2 f \ d(L) ; \ f \ \ f + (\ f \ L) + d((\ f + (\ f \ L)) ; 0) ; T" definition mu_nu_apx_nu :: "('a \ 'a) \ bool" where "mu_nu_apx_nu f \ \ f + (\ 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 + (\ 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 + (\ f \ L)" by (metis add_left_upper_bound) lemma l_below_nu: "has_least_fixpoint f \ has_greatest_fixpoint f \ \ f + (\ f \ L) \ \ f" by (metis add_least_upper_bound meet_left_upper_bound mu_below_nu) lemma n_l_nu: "has_least_fixpoint f \ has_greatest_fixpoint f \ (\ f + (\ f \ L)) \ L = \ f \ L" by (smt add_commutative add_left_dist_meet less_eq_def meet_absorb meet_associative meet_commutative mu_below_nu) lemma l_apx_mu: "\ f + (\ f \ L) \ \ f" by (metis add_right_isotone apx_def meet_absorb meet_domain_top meet_least_upper_bound meet_left_upper_bound meet_right_upper_bound) lemma nu_below_mu_nu_nu_below_mu_nu_2: "nu_below_mu_nu f \ nu_below_mu_nu_2 f" proof assume 1: "nu_below_mu_nu f" have "d(L) ; \ f = d(L) ; (d(L) ; \ f)" by (metis d_idempotent mult_associative) also have "... \ d(L) ; (\ f + (\ f \ L) + d(\ f ; 0) ; T)" using 1 by (metis mult_right_isotone nu_below_mu_nu_def) also have "... = d(L) ; (\ f + (\ f \ L)) + d(L) ; d(\ f ; 0) ; T" by (metis mult_associative mult_left_dist_add) also have "... \ \ f + (\ f \ L) + d(L) ; d(\ f ; 0) ; T" by (metis add_left_isotone meet_domain_top meet_left_upper_bound) also have "... = \ f + (\ f \ L) + d(d(\ f ; 0) ; L) ; T" by (smt d_commutative d_export) also have "... = \ f + (\ f \ L) + d((\ f \ L) ; 0) ; T" by (metis l51) also have "... \ \ f + (\ f \ L) + d((\ f + (\ f \ L)) ; 0) ; T" by (metis add_right_isotone add_right_upper_bound d_dist_add mult_right_dist_add) finally show "nu_below_mu_nu_2 f" by (metis nu_below_mu_nu_2_def) qed lemma nu_below_mu_nu_2_nu_below_mu_nu: "has_least_fixpoint f \ has_greatest_fixpoint f \ nu_below_mu_nu_2 f \ nu_below_mu_nu f" proof assume 1: "has_least_fixpoint f \ has_greatest_fixpoint f \ nu_below_mu_nu_2 f" hence "d(L) ; \ f \ \ f + (\ f \ L) + d((\ f + (\ f \ L)) ; 0) ; T" by (metis nu_below_mu_nu_2_def) also have "... \ \ f + (\ f \ L) + d(\ f ; 0) ; T" using 1 by (smt add_absorb add_associative add_commutative d_dist_add l_below_nu less_eq_def meet_absorb mult_right_dist_add) finally show "nu_below_mu_nu f" by (metis nu_below_mu_nu_def) qed lemma nu_below_mu_nu_equivalent: "has_least_fixpoint f \ has_greatest_fixpoint f \ (nu_below_mu_nu f \ nu_below_mu_nu_2 f)" by (metis nu_below_mu_nu_2_nu_below_mu_nu nu_below_mu_nu_nu_below_mu_nu_2) lemma nu_below_mu_nu_2_mu_nu_apx_nu: "has_least_fixpoint f \ has_greatest_fixpoint f \ nu_below_mu_nu_2 f \ mu_nu_apx_nu f" proof assume 1: "has_least_fixpoint f \ has_greatest_fixpoint f \ nu_below_mu_nu_2 f" hence "\ f + (\ f \ L) \ \ f + L" by (metis add_commutative add_right_upper_bound l_below_nu order_trans) thus "mu_nu_apx_nu f" using 1 by (metis apx_def mu_nu_apx_nu_def nu_below_mu_nu_2_def) qed 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 + (\ 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_apx_left_isotone add_commutative apx_meet_L is_apx_meet_def l_apx_mu less_eq_def meet_least_upper_bound mu_nu_apx_nu_def) 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_2: "apx_meet_below_nu f \ nu_below_mu_nu_2 f" proof - let ?l = "\ f + (\ f \ L)" have "\m . m \ \ f \ m \ \ f \ m \ \ f \ d(L) ; \ f \ ?l + d(?l ; 0) ; T" proof fix m show "m \ \ f \ m \ \ f \ m \ \ f \ d(L) ; \ f \ ?l + d(?l ; 0) ; T" proof assume 1: "m \ \ f \ m \ \ f \ m \ \ f" hence "m \ ?l" by (smt add_commutative add_left_dist_meet add_left_upper_bound apx_def less_eq_meet meet_least_upper_bound) hence "m + d(m ; 0) ; T \ ?l + d(?l ; 0) ; T" by (metis add_isotone d_dist_add less_eq_def mult_right_dist_add) thus "d(L) ; \ f \ ?l + d(?l ; 0) ; T" using 1 by (smt apx_def order_trans) qed qed thus ?thesis by (smt apx_meet_below_nu_def apx_meet_same apx_meet_unique is_apx_meet_def nu_below_mu_nu_2_def) 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 mult_right_isotone 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 + (\ f \ L)" let ?m = "\ f \ \ f" assume 1: "has_least_fixpoint f \ has_greatest_fixpoint f \ isotone f \ apx_isotone f \ apx_meet_below_nu f" hence 2: "?m = ?l" by (metis apx_meet_below_nu_nu_below_mu_nu_2 mu_nu_apx_meet_def mu_nu_apx_nu_mu_nu_apx_meet nu_below_mu_nu_2_mu_nu_apx_nu) have 3: "?l \ f(?l) + L" proof - have "?l \ \ f + L" by (metis add_right_isotone meet_right_upper_bound) also have "... = f(\ f) + L" using 1 by (metis is_least_fixpoint_def least_fixpoint) also have "... \ f(?l) + L" using 1 by (metis add_left_isotone add_left_upper_bound isotone_def) finally show "?l \ f(?l) + L" by metis qed have "d(L) ; f(?l) \ ?l + d(?l ; 0) ; T" proof - have "d(L) ; f(?l) \ d(L) ; f(\ f)" using 1 2 by (metis apx_meet_below_nu_def isotone_def mult_right_isotone) also have "... = d(L) ; \ f" using 1 by (metis greatest_fixpoint is_greatest_fixpoint_def) also have "... \ ?l + d(?l ; 0) ; T" using 1 by (metis apx_meet_below_nu_nu_below_mu_nu_2 nu_below_mu_nu_2_def) finally show "d(L) ; f(?l) \ ?l + d(?l ; 0) ; T" by metis qed hence 4: "?l \ f(?l)" using 3 by (metis apx_def) have 5: "f(?l) \ \ f" proof - have "?l \ \ f" by (metis l_apx_mu) thus "f(?l) \ \ f" using 1 by (metis apx_isotone_def is_least_fixpoint_def least_fixpoint) qed have 6: "f(?l) \ \ f" proof - have "?l \ \ f" using 1 2 by (metis apx_greatest_lower_bound apx_meet_below_nu_def apx_reflexive) thus "f(?l) \ \ f" using 1 by (metis apx_isotone_def greatest_fixpoint is_greatest_fixpoint_def) qed hence "f(?l) \ ?l" using 1 2 5 by (metis apx_greatest_lower_bound apx_meet_below_nu_def) hence 7: "f(?l) = ?l" using 4 by (metis apx_antisymmetric) have "\y . f(y) = y \ ?l \ y" proof fix y show "f(y) = y \ ?l \ y" proof assume 8: "f(y) = y" hence 9: "?l \ y + L" using 1 by (metis add_isotone is_least_fixpoint_def least_fixpoint meet_right_upper_bound) have "y \ \ f" using 1 8 by (metis greatest_fixpoint is_greatest_fixpoint_def) hence "d(L) ; y \ ?l + d(?l ; 0) ; T" using 4 6 by (smt apx_def apx_transitive mult_right_isotone order_trans) thus "?l \ y" using 9 by (metis apx_def) qed qed thus "xi_mu_nu f" using 1 2 7 by (smt apx_least_fixpoint_same has_apx_least_fixpoint_def is_apx_least_fixpoint_def 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_nu_below_mu_nu_2 nu_below_mu_nu_2_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_2 has_apx_least_fixpoint_xi_apx_meet nu_below_mu_nu_2_nu_below_mu_nu xi_apx_meet_apx_meet_below_nu xi_mu_nu_has_apx_least_fixpoint) definition xi_mu_nu_L :: "('a \ 'a) \ bool" where "xi_mu_nu_L f \ has_apx_least_fixpoint f \ \ f = \ f + d(\ f ; 0) ; L" definition nu_below_mu_nu_L :: "('a \ 'a) \ bool" where "nu_below_mu_nu_L f \ d(L) ; \ f \ \ f + d(\ f ; 0) ; T" definition mu_nu_apx_nu_L :: "('a \ 'a) \ bool" where "mu_nu_apx_nu_L f \ \ f + d(\ f ; 0) ; L \ \ f" definition mu_nu_apx_meet_L :: "('a \ 'a) \ bool" where "mu_nu_apx_meet_L f \ has_apx_meet (\ f) (\ f) \ \ f \ \ f = \ f + d(\ f ; 0) ; L" lemma n_below_l: "x + d(y ; 0) ; L \ x + (y \ L)" by (metis add_right_isotone d_mult_below l13 meet_least_upper_bound) lemma n_equal_l: "nu_below_mu_nu_L f \ \ f + d(\ f ; 0) ; L = \ f + (\ f \ L)" proof assume "nu_below_mu_nu_L f" hence "\ f \ L \ (\ f + d(\ f ; 0) ; T) \ L" by (smt meet_associative meet_intro_domain meet_right_divisibility nu_below_mu_nu_L_def) also have "... \ \ f + d(\ f ; 0) ; L" by (smt add_left_dist_meet add_right_divisibility meet_commutative meet_domain_top meet_left_isotone) finally have "\ f + (\ f \ L) \ \ f + d(\ f ; 0) ; L" by (metis add_least_upper_bound add_left_upper_bound) thus "\ f + d(\ f ; 0) ; L = \ f + (\ f \ L)" by (metis antisym n_below_l) qed lemma nu_below_mu_nu_L_nu_below_mu_nu: "nu_below_mu_nu_L f \ nu_below_mu_nu f" by (metis add_associative add_right_top mult_left_dist_add n_equal_l nu_below_mu_nu_L_def nu_below_mu_nu_def) lemma nu_below_mu_nu_L_xi_mu_nu_L: "has_least_fixpoint f \ has_greatest_fixpoint f \ isotone f \ apx_isotone f \ nu_below_mu_nu_L f \ xi_mu_nu_L f" by (metis n_equal_l nu_below_mu_nu_L_nu_below_mu_nu nu_below_mu_nu_xi_mu_nu xi_mu_nu_L_def xi_mu_nu_def) lemma nu_below_mu_nu_L_mu_nu_apx_nu_L: "has_least_fixpoint f \ has_greatest_fixpoint f \ nu_below_mu_nu_L f \ mu_nu_apx_nu_L f" by (metis mu_nu_apx_nu_L_def mu_nu_apx_nu_def n_equal_l nu_below_mu_nu_2_mu_nu_apx_nu nu_below_mu_nu_L_nu_below_mu_nu nu_below_mu_nu_nu_below_mu_nu_2) lemma nu_below_mu_nu_L_mu_nu_apx_meet_L: "has_least_fixpoint f \ has_greatest_fixpoint f \ nu_below_mu_nu_L f \ mu_nu_apx_meet_L f" by (metis mu_nu_apx_meet_L_def mu_nu_apx_meet_def mu_nu_apx_nu_mu_nu_apx_meet n_equal_l nu_below_mu_nu_2_mu_nu_apx_nu nu_below_mu_nu_L_nu_below_mu_nu nu_below_mu_nu_nu_below_mu_nu_2) lemma mu_nu_apx_nu_L_nu_below_mu_nu_L: "has_least_fixpoint f \ has_greatest_fixpoint f \ mu_nu_apx_nu_L f \ nu_below_mu_nu_L f" proof let ?n = "\ f + d(\ f ; 0) ; L" let ?l = "\ f + (\ f \ L)" assume 1: "has_least_fixpoint f \ has_greatest_fixpoint f \ mu_nu_apx_nu_L f" hence "d(L) ; \ f \ ?n + d(?n ; 0) ; T" by (metis apx_def mu_nu_apx_nu_L_def) also have "... \ ?n + d(?l ; 0) ; T" by (metis add_right_isotone d_isotone mult_left_isotone n_below_l) also have "... \ ?n + d(\ f ; 0) ; T" using 1 by (metis add_right_isotone d_isotone l_below_nu mult_left_isotone) finally show "nu_below_mu_nu_L f" by (metis add_associative add_right_top mult_left_dist_add nu_below_mu_nu_L_def) qed lemma xi_mu_nu_L_mu_nu_apx_nu_L: "has_greatest_fixpoint f \ xi_mu_nu_L f \ mu_nu_apx_nu_L f" by (metis mu_nu_apx_nu_L_def xi_apx_below_nu xi_mu_nu_L_def) lemma mu_nu_apx_meet_L_mu_nu_apx_nu_L: "mu_nu_apx_meet_L f \ mu_nu_apx_nu_L f" by (metis apx_meet_same has_apx_meet_def is_apx_meet_def mu_nu_apx_meet_L_def mu_nu_apx_nu_L_def) lemma xi_mu_nu_L_nu_below_mu_nu_L: "has_least_fixpoint f \ has_greatest_fixpoint f \ xi_mu_nu_L f \ nu_below_mu_nu_L f" by (metis mu_nu_apx_nu_L_nu_below_mu_nu_L xi_mu_nu_L_mu_nu_apx_nu_L) end class itering_apx = domain_itering_lattice_L + domain_semiring_lattice_apx begin lemma circ_apx_isotone: "x \ y \ x\<^sup>\ \ y\<^sup>\" proof assume "x \ y" hence 1: "x \ y + L \ d(L) ; y \ x + d(x ; 0) ; T" by (metis apx_def) have "d(L) ; y\<^sup>\ \ (d(L) ; y)\<^sup>\" by (smt circ_reflexive circ_transitive_equal d_below_one d_circ_import l2 mult_left_isotone order_trans) also have "... \ x\<^sup>\ ; (d(x ; 0) ; T ; x\<^sup>\)\<^sup>\" using 1 by (metis circ_add_1 circ_isotone) also have "... = x\<^sup>\ + x\<^sup>\ ; d(x ; 0) ; T" by (metis circ_left_top mult_associative mult_left_dist_add mult_right_one mult_top_circ) also have "... \ x\<^sup>\ + d(x\<^sup>\ ; x ; 0) ; T" by (metis add_right_isotone mult_associative mult_domain_top) finally have 2: "d(L) ; y\<^sup>\ \ x\<^sup>\ + d(x\<^sup>\ ; 0) ; T" by (metis circ_plus_same d0_circ_left_unfold) have "x\<^sup>\ \ y\<^sup>\ ; L\<^sup>\" using 1 by (metis circ_add_1 circ_back_loop_fixpoint circ_isotone l40 less_eq_def mult_associative) also have "... = y\<^sup>\ + y\<^sup>\ ; L" by (metis add_commutative circ_L mult_left_dist_add mult_right_one) also have "... \ y\<^sup>\ + y\<^sup>\ ; 0 + L" by (metis add_associative add_right_isotone l14) finally have "x\<^sup>\ \ y\<^sup>\ + L" by (metis add_commutative less_eq_def zero_right_mult_decreasing) thus "x\<^sup>\ \ y\<^sup>\" using 2 by (metis apx_def) qed end class omega_algebra_apx = domain_omega_algebra_lattice_L + domain_semiring_lattice_apx sublocale omega_algebra_apx < star!: itering_apx where circ = star .. context omega_algebra_apx begin lemma omega_apx_isotone: "x \ y \ x\<^sup>\ \ y\<^sup>\" proof assume "x \ y" hence 1: "x \ y + L \ d(L) ; y \ x + d(x ; 0) ; T" by (metis apx_def) have "d(L) ; y\<^sup>\ = (d(L) ; y)\<^sup>\" by (metis d_omega_export l2) also have "... \ (x + d(x ; 0) ; T)\<^sup>\" using 1 by (metis omega_isotone) also have "... = (x\<^sup>\ ; d(x ; 0) ; T)\<^sup>\ + (x\<^sup>\ ; d(x ; 0) ; T)\<^sup>\ ; x\<^sup>\" by (metis mult_associative omega_decompose) also have "... \ x\<^sup>\ ; d(x ; 0) ; T + (x\<^sup>\ ; d(x ; 0) ; T)\<^sup>\ ; x\<^sup>\" by (metis add_left_isotone mult_top_omega) also have "... = x\<^sup>\ ; d(x ; 0) ; T + (1 + x\<^sup>\ ; d(x ; 0) ; T ; (x\<^sup>\ ; d(x ; 0) ; T)\<^sup>\) ; x\<^sup>\" by (metis mult_associative star.circ_left_top star.mult_top_circ) also have "... \ x\<^sup>\ + x\<^sup>\ ; d(x ; 0) ; T" by (smt add_isotone add_least_upper_bound mult_associative mult_left_one mult_right_dist_add mult_right_isotone order_refl top_greatest) also have "... \ x\<^sup>\ + d(x\<^sup>\ ; x ; 0) ; T" by (metis add_right_isotone mult_associative mult_domain_top) also have "... \ x\<^sup>\ + d(x\<^sup>\ ; 0) ; T" by (metis dL_star.d0_circ_left_unfold eq_refl star.circ_plus_same) finally have 2: "d(L) ; y\<^sup>\ \ x\<^sup>\ + d(x\<^sup>\ ; 0) ; T" by (smt add_right_isotone d0_star_below_d0_omega mult_left_isotone order_trans) have "x\<^sup>\ \ (y + L)\<^sup>\" using 1 by (metis omega_isotone) also have "... = (y\<^sup>\ ; L)\<^sup>\ + (y\<^sup>\ ; L)\<^sup>\ ; y\<^sup>\" by (metis omega_decompose) also have "... = y\<^sup>\ ; L ; (y\<^sup>\ ; L)\<^sup>\ + (y\<^sup>\ ; L)\<^sup>\ ; y\<^sup>\" by (metis omega_unfold) also have "... \ y\<^sup>\ ; L + (y\<^sup>\ ; L)\<^sup>\ ; y\<^sup>\" by (metis add_left_isotone l40 mult_associative mult_right_isotone) also have "... = y\<^sup>\ ; L + (1 + y\<^sup>\ ; L ; (y\<^sup>\ ; L)\<^sup>\) ; y\<^sup>\" by (metis star.circ_left_unfold) also have "... \ y\<^sup>\ ; L + y\<^sup>\" by (metis add_commutative add_least_upper_bound add_right_upper_bound dL_star.mult_L_circ_mult_below mult_associative star.circ_mult star.circ_slide) also have "... \ y\<^sup>\ ; 0 + L + y\<^sup>\" by (metis add_left_isotone l14) finally have "x\<^sup>\ \ y\<^sup>\ + L" by (metis add_associative add_commutative less_eq_def star_zero_below_omega) thus "x\<^sup>\ \ y\<^sup>\" using 2 by (metis apx_def) qed lemma combined_apx_isotone: "x \ y \ (x\<^sup>\ \ L) + x\<^sup>\ ; z \ (y\<^sup>\ \ L) + y\<^sup>\ ; z" by (metis add_apx_isotone mult_apx_left_isotone omega_apx_isotone star.circ_apx_isotone meet_L_apx_isotone) lemma d_split_nu_mu: "d(L) ; (y\<^sup>\ + y\<^sup>\ ; z) \ y\<^sup>\ ; z + ((y\<^sup>\ + y\<^sup>\ ; z) \ L) + d((y\<^sup>\ + y\<^sup>\ ; z) ; 0) ; T" proof - have "d(L) ; y\<^sup>\ \ (y\<^sup>\ \ L) + d(y\<^sup>\ ; 0) ; T" by (metis add_right_isotone l31 l91 omega_vector) hence "d(L) ; (y\<^sup>\ + y\<^sup>\ ; z) \ y\<^sup>\ ; z + (y\<^sup>\ \ L) + d(y\<^sup>\ ; 0) ; T" by (smt add_associative add_commutative add_isotone d_mult_below mult_left_dist_add) thus ?thesis by (smt add_commutative add_isotone add_right_isotone add_right_upper_bound d_isotone meet_commutative meet_right_isotone mult_left_isotone order_trans) qed lemma loop_exists: "d(L) ; \ (\x . y ; x + z) \ \ (\x . y ; x + z) + (\ (\x . y ; x + z) \ L) + d(\ (\x . y ; x + z) ; 0) ; T" by (metis d_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) + (\ (\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) + (\ (\x . y ; x + z) \ L)" by (metis apx_least_fixpoint_char loop_apx_least_fixpoint) lemma loop_semantics_xi_mu_nu: "\ (\x . y ; x + z) = (y\<^sup>\ \ L) + y\<^sup>\ ; z" proof - have "\ (\x . y ; x + z) = y\<^sup>\ ; z + ((y\<^sup>\ + y\<^sup>\ ; z) \ L)" by (metis loop_semantics omega_loop_nu star_loop_mu) thus ?thesis by (smt add_absorb add_associative add_commutative add_left_dist_meet) qed lemma loop_semantics_xi_mu_nu_domain: "\ (\x . y ; x + z) = d(y\<^sup>\) ; L + y\<^sup>\ ; z" by (metis loop_semantics_xi_mu_nu omega_meet_L) lemma loop_semantics_apx_isotone: "w \ y \ \ (\x . w ; x + z) \ \ (\x . y ; x + z)" by (metis loop_semantics_xi_mu_nu combined_apx_isotone) end (* end theory BinaryIteration imports Semiring Fixpoint begin *) class while = fixes while :: "'a \ 'a \ 'a" (infixr "\" 60) class binary_itering = semiring + while + assumes while_productstar: "(x ; y) \ z = z + x ; ((y ; x) \ (y ; z))" assumes while_sumstar: "(x + y) \ z = (x \ y) \ (x \ z)" assumes while_left_dist_add: "x \ (y + z) = (x \ y) + (x \ z)" assumes while_sub_associative: "(x \ y) ; z \ x \ (y ; z)" assumes while_simulate_left_plus: "x ; z \ z ; (y \ 1) + w \ x \ (z ; v) \ z ; (y \ v) + (x \ (w ; (y \ v)))" assumes while_simulate_right_plus: "z ; x \ y ; (y \ z) + w \ z ; (x \ v) \ y \ (z ; v + w ; (x \ v))" begin lemma while_zero: "0 \ x = x" by (metis add_right_zero mult_left_zero while_productstar) lemma while_mult_increasing: "x ; y \ x \ y" by (metis add_least_upper_bound mult_left_one order_refl while_productstar) lemma while_one_increasing: "x \ x \ 1" by (metis mult_right_one while_mult_increasing) lemma while_increasing: "y \ x \ y" by (metis add_left_divisibility mult_left_one while_productstar) lemma while_right_isotone: "y \ z \ x \ y \ x \ z" by (metis less_eq_def while_left_dist_add) lemma while_left_isotone: "x \ y \ x \ z \ y \ z" by (metis less_eq_def while_increasing while_sumstar) lemma while_isotone: "w \ x \ y \ z \ w \ y \ x \ z" by (smt order_trans while_left_isotone while_right_isotone) lemma while_left_unfold: "x \ y = y + x ; (x \ y)" by (metis mult_left_one mult_right_one while_productstar) lemma while_simulate_left_plus_1: "x ; z \ z ; (y \ 1) \ x \ (z ; w) \ z ; (y \ w) + (x \ 0)" by (metis add_right_zero mult_left_zero while_simulate_left_plus) lemma while_simulate_absorb: "y ; x \ x \ y \ x \ x + (y \ 0)" by (metis while_simulate_left_plus_1 while_zero mult_right_one) lemma while_transitive: "x \ (x \ y) = x \ y" by (metis add_right_upper_bound add_right_zero antisym while_increasing while_left_dist_add while_left_unfold while_simulate_absorb) lemma while_slide: "(x ; y) \ (x ; z) = x ; ((y ; x) \ z)" by (metis mult_associative mult_left_dist_add while_left_unfold while_productstar) lemma while_zero_2: "(x ; 0) \ y = x ; 0 + y" by (metis add_commutative mult_associative mult_left_zero while_left_unfold) lemma while_mult_star_exchange: "x ; (x \ y) = x \ (x ; y)" by (metis mult_left_one while_slide) lemma while_right_unfold: "x \ y = y + (x \ (x ; y))" by (metis while_left_unfold while_mult_star_exchange) lemma while_one_mult_below: "(x \ 1) ; y \ x \ y" by (metis mult_left_one while_sub_associative) lemma while_plus_one: "x \ y = y + (x \ y)" by (metis less_eq_def while_increasing) lemma while_rtc_2: "y + x ; y + (x \ (x \ y)) = x \ y" by (metis add_associative less_eq_def while_mult_increasing while_plus_one while_transitive) lemma while_left_plus_below: "x ; (x \ y) \ x \ y" by (metis add_right_divisibility while_left_unfold) lemma while_right_plus_below: "x \ (x ; y) \ x \ y" by (metis while_left_plus_below while_mult_star_exchange) lemma while_right_plus_below_2: "(x \ x) ; y \ x \ y" by (smt order_trans while_right_plus_below while_sub_associative) lemma while_mult_transitive: "x \ z \ y \ y \ z \ w \ x \ z \ w" by (smt order_trans while_right_isotone while_transitive) lemma while_mult_upper_bound: "x \ z \ 1 \ y \ z \ w \ x ; y \ z \ w" by (metis less_eq_def mult_right_subdist_add_left order_trans while_mult_transitive while_one_mult_below) lemma while_sub_dist: "x \ z \ (x + y) \ z" by (metis add_left_upper_bound while_left_isotone) lemma while_sub_dist_1: "x ; z \ (x + y) \ z" by (metis order_trans while_mult_increasing while_sub_dist) lemma while_sub_dist_2: "x ; y ; z \ (x + y) \ z" by (smt mult_associative mult_right_subdist_add_right order_trans while_mult_increasing while_mult_transitive while_sub_dist_1) lemma while_sub_dist_3: "x \ (y \ z) \ (x + y) \ z" by (metis add_right_upper_bound while_left_isotone while_mult_transitive while_sub_dist) lemma while_absorb_2: "x \ y \ y \ (x \ z) = y \ z" by (metis add_commutative less_eq_def while_left_dist_add while_plus_one while_sub_dist_3) lemma while_simulate_right_plus_1: "z ; x \ y ; (y \ z) \ z ; (x \ w) \ y \ (z ; w)" by (metis add_right_zero mult_left_zero while_simulate_right_plus) lemma while_sumstar_1_below: "x \ ((y ; (x \ 1)) \ z) \ ((x \ 1) ; y) \ (x \ z)" proof - have 1: "x ; (((x \ 1) ; y) \ (x \ z)) \ ((x \ 1) ; y) \ (x \ z)" by (smt add_isotone add_right_upper_bound mult_associative mult_left_dist_add mult_right_subdist_add_right while_left_unfold) have "x \ ((y ; (x \ 1)) \ z) \ (x \ z) + (x \ (y ; (((x \ 1) ; y) \ ((x \ 1) ; z))))" by (metis eq_refl while_left_dist_add while_productstar) also have "... \ (x \ z) + (x \ ((x \ 1) ; y ; (((x \ 1) ; y) \ ((x \ 1) ; z))))" by (metis add_right_isotone mult_associative mult_left_one mult_right_subdist_add_left while_left_unfold while_right_isotone) also have "... \ (x \ z) + (x \ (((x \ 1) ; y) \ ((x \ 1) ; z)))" by (metis add_right_isotone add_right_upper_bound while_left_unfold while_right_isotone) also have "... \ x \ (((x \ 1) ; y) \ (x \ z))" by (smt add_associative add_left_upper_bound less_eq_def mult_left_one while_left_dist_add while_left_unfold while_sub_associative) also have "... \ (((x \ 1) ; y) \ (x \ z)) + (x \ 0)" using 1 by (metis while_simulate_absorb) also have "... = ((x \ 1) ; y) \ (x \ z)" by (smt add_associative add_commutative add_left_zero while_left_dist_add while_left_unfold) finally show ?thesis . qed lemma while_sumstar_2_below: "((x \ 1) ; y) \ (x \ z) \ (x \ y) \ (x \ z)" by (metis mult_left_one while_left_isotone while_sub_associative) lemma while_add_1_below: "x \ ((y ; (x \ 1)) \ z) \ (x + y) \ z" proof - have "((x \ 1) ; y) \ ((x \ 1) ; z) \ (x + y) \ z" by (metis while_isotone while_one_mult_below while_sumstar) hence "(y ; (x \ 1)) \ z \ z + y ; ((x + y) \ z)" by (metis add_right_isotone mult_right_isotone while_productstar) also have "... \ (x + y) \ z" by (metis add_right_isotone add_right_upper_bound mult_left_isotone while_left_unfold) finally show ?thesis by (metis add_commutative add_right_upper_bound while_isotone while_transitive) qed lemma while_while_while: "((x \ 1) \ 1) \ y = (x \ 1) \ y" by (smt add_commutative less_eq_def mult_right_one while_left_plus_below while_mult_star_exchange while_plus_one while_sumstar while_transitive) lemma while_one: "(1 \ 1) \ y = 1 \ y" by (metis while_while_while while_zero) lemma while_add_below: "x + y \ x \ (y \ 1)" by (smt add_commutative add_isotone case_split_right order_trans while_increasing while_left_plus_below while_mult_increasing while_plus_one) lemma while_add_2: "(x + y) \ z \ (x \ (y \ 1)) \ z" by (metis while_add_below while_left_isotone) lemma while_sup_one_left_unfold: "1 \ x \ x ; (x \ y) = x \ y" by (metis less_eq_def mult_left_one mult_right_dist_add while_mult_star_exchange while_right_unfold while_transitive) lemma while_sup_one_right_unfold: "1 \ x \ x \ (x ; y) = x \ y" by (metis while_mult_star_exchange while_sup_one_left_unfold) lemma while_decompose_7: "(x + y) \ z = x \ (y \ ((x + y) \ z))" by (metis eq_iff order_trans while_increasing while_sub_dist_3 while_transitive) lemma while_decompose_8: "(x + y) \ z = (x + y) \ (x \ (y \ z))" by (metis add_commutative while_sumstar while_transitive) lemma while_decompose_9: "(x \ (y \ 1)) \ z = x \ (y \ ((x \ (y \ 1)) \ z))" by (smt add_commutative less_eq_def order_trans while_add_below while_increasing while_sub_dist_3) lemma while_decompose_10: "(x \ (y \ 1)) \ z = (x \ (y \ 1)) \ (x \ (y \ z))" proof - have 1: "(x \ (y \ 1)) \ z \ (x \ (y \ 1)) \ (x \ (y \ z))" by (metis add_associative less_eq_def while_left_dist_add while_plus_one) have "x + (y \ 1) \ x \ (y \ 1)" by (metis add_least_upper_bound while_add_below while_increasing) hence "(x \ (y \ 1)) \ (x \ (y \ z)) \ (x \ (y \ 1)) \ z" by (smt antisym while_decompose_9 while_increasing while_mult_transitive while_right_isotone) thus ?thesis using 1 by (metis antisym) qed lemma while_back_loop_fixpoint: "z ; (y \ (y ; x)) + z ; x = z ; (y \ x)" by (metis add_commutative mult_left_dist_add while_right_unfold) lemma while_back_loop_prefixpoint: "z ; (y \ 1) ; y + z \ z ; (y \ 1)" by (metis add_least_upper_bound mult_associative mult_right_isotone mult_right_one order_refl while_increasing while_mult_upper_bound while_one_increasing) lemma while_loop_is_fixpoint: "is_fixpoint (\x . y ; x + z) (y \ z)" by (smt add_commutative is_fixpoint_def while_left_unfold) lemma while_back_loop_is_prefixpoint: "is_prefixpoint (\x . x ; y + z) (z ; (y \ 1))" by (metis is_prefixpoint_def while_back_loop_prefixpoint) lemma while_while_add: "(1 + x) \ y = (x \ 1) \ y" by (metis add_commutative while_decompose_10 while_sumstar while_zero) lemma while_while_mult_sub: "x \ (1 \ y) \ (x \ 1) \ y" by (metis add_commutative while_sub_dist_3 while_while_add) lemma while_right_plus: "(x \ x) \ y = x \ y" by (metis add_idempotent while_plus_one while_sumstar while_transitive) lemma while_left_plus: "(x ; (x \ 1)) \ y = x \ y" by (metis mult_right_one while_mult_star_exchange while_right_plus) lemma while_below_while_one: "x \ x \ x \ 1" by (metis while_one_increasing while_right_plus) lemma while_below_while_one_mult: "x ; (x \ x) \ x ; (x \ 1)" by (metis mult_right_isotone while_below_while_one) lemma while_add_sub_add_one: "x \ (x + y) \ x \ (1 + y)" by (metis add_left_isotone while_below_while_one while_left_dist_add) lemma while_add_sub_add_one_mult: "x ; (x \ (x + y)) \ x ; (x \ (1 + y))" by (metis mult_right_isotone while_add_sub_add_one) lemma while_elimination: "x ; y = 0 \ x ; (y \ z) = x ; z" by (metis add_right_zero mult_associative mult_left_dist_add mult_left_zero while_left_unfold) lemma while_square: "(x ; x) \ y \ x \ y" by (metis while_left_isotone while_mult_increasing while_right_plus) lemma while_mult_sub_add: "(x ; y) \ z \ (x + y) \ z" by (metis while_increasing while_isotone while_mult_increasing while_sumstar) lemma while_absorb_1: "x \ y \ x \ (y \ z) = y \ z" by (metis antisym less_eq_def while_increasing while_sub_dist_3) lemma while_absorb_3: "x \ y \ x \ (y \ z) = y \ (x \ z)" by (metis while_absorb_1 while_absorb_2) lemma while_square_2: "(x ; x) \ ((x + 1) ; y) \ x \ y" by (smt add_least_upper_bound while_increasing while_mult_transitive while_mult_upper_bound while_one_increasing while_square) lemma while_separate_unfold_below: "(y ; (x \ 1)) \ z \ (y \ z) + (y \ (y ; x ; (x \ ((y ; (x \ 1)) \ z))))" proof - have "(y ; (x \ 1)) \ z = (y \ (y ; x ; (x \ 1))) \ (y \ z)" by (metis mult_associative mult_left_dist_add mult_right_one while_left_unfold while_sumstar) hence "(y ; (x \ 1)) \ z = (y \ z) + (y \ (y ; x ; (x \ 1))) ; ((y ; (x \ 1)) \ z)" by (metis while_left_unfold) also have "... \ (y \ z) + (y \ (y ; x ; (x \ 1)) ; ((y ; (x \ 1)) \ z))" by (metis add_right_isotone while_sub_associative) also have "... \ (y \ z) + (y \ (y ; x ; (x \ ((y ; (x \ 1)) \ z))))" by (smt add_right_isotone mult_associative mult_right_isotone while_one_mult_below while_right_isotone) finally show ?thesis . qed lemma while_mult_zero_add: "(x + y ; 0) \ z = x \ ((y ; 0) \ z)" proof - have "(x + y ; 0) \ z = (x \ (y ; 0)) \ (x \ z)" by (metis while_sumstar) also have "... = (x \ z) + (x \ (y ; 0)) ; ((x \ (y ; 0)) \ (x \ z))" by (metis while_left_unfold) also have "... \ (x \ z) + (x \ (y ; 0))" by (metis add_right_isotone mult_associative mult_left_zero while_sub_associative) also have "... = x \ ((y ; 0) \ z)" by (metis add_commutative while_left_dist_add while_zero_2) finally show ?thesis by (metis le_neq_trans less_def while_sub_dist_3) qed lemma while_add_mult_zero: "(x + y ; 0) \ y = x \ y" by (metis less_eq_def while_mult_zero_add while_zero_2 zero_right_mult_decreasing) lemma while_mult_zero_add_2: "(x + y ; 0) \ z = (x \ z) + (x \ (y ; 0))" by (metis add_commutative while_left_dist_add while_mult_zero_add while_zero_2) lemma while_add_zero_star: "(x + y ; 0) \ z = x \ (y ; 0 + z)" by (metis while_mult_zero_add while_zero_2) lemma while_unfold_sum: "(x + y) \ z = (x \ z) + (x \ (y ; ((x + y) \ z)))" apply (rule antisym) apply (smt add_associative less_eq_def while_absorb_1 while_increasing while_mult_star_exchange while_right_unfold while_sub_associative while_sumstar) by (metis add_least_upper_bound while_decompose_7 while_mult_increasing while_right_isotone while_sub_dist) lemma while_simulate_left: "x ; z \ z ; y + w \ x \ (z ; v) \ z ; (y \ v) + (x \ (w ; (y \ v)))" by (smt add_commutative add_right_isotone mult_right_isotone order_trans while_one_increasing while_simulate_left_plus) lemma while_simulate_right: "z ; x \ y ; z + w \ z ; (x \ v) \ y \ (z ; v + w ; (x \ v))" proof - have "y ; z + w \ y ; (y \ z) + w" by (metis add_left_isotone mult_right_isotone while_increasing) thus ?thesis by (smt order_trans while_simulate_right_plus) qed lemma while_simulate: "z ; x \ y ; z \ z ; (x \ v) \ y \ (z ; v)" by (metis add_right_zero mult_left_zero while_simulate_right) lemma while_while_mult: "1 \ (x \ y) = (x \ 1) \ y" proof - have "(x \ 1) \ y \ (x \ 1) ; ((x \ 1) \ y)" by (metis order_refl while_increasing while_sup_one_left_unfold) also have "... \ 1 \ ((x \ 1) ; y)" by (metis mult_left_one order_refl while_mult_upper_bound while_simulate) also have "... \ 1 \ (x \ y)" by (metis while_one_mult_below while_right_isotone) finally show ?thesis by (metis antisym while_sub_dist_3 while_while_add) qed lemma while_simulate_left_1: "x ; z \ z ; y \ x \ (z ; v) \ z ; (y \ v) + (x \ 0)" by (metis add_right_zero mult_left_zero while_simulate_left) lemma while_associative_1: "1 \ z \ x \ (y ; z) = (x \ y) ; z" proof assume 1: "1 \ z" have "x \ (y ; z) \ x \ ((x \ y) ; z)" by (metis less_eq_def mult_right_dist_add while_plus_one while_right_isotone) also have "... \ (x \ y) ; (0 \ z) + (x \ 0)" by (metis mult_associative mult_right_subdist_add_right while_left_unfold while_simulate_absorb while_zero) also have "... \ (x \ y) ; z + (x \ 0) ; z" using 1 by (metis add_least_upper_bound add_left_upper_bound add_right_upper_bound case_split_right while_plus_one while_zero) also have "... = (x \ y) ; z" by (metis add_right_zero mult_right_dist_add while_left_dist_add) finally show "x \ (y ; z) = (x \ y) ; z" by (metis antisym while_sub_associative) qed lemma while_associative_while_1: "x \ (y ; (z \ 1)) = (x \ y) ; (z \ 1)" by (metis while_associative_1 while_increasing) lemma while_one_while: "(x \ 1) ; (y \ 1) = x \ (y \ 1)" by (metis mult_left_one while_associative_while_1) lemma while_decompose_5_below: "(x \ (y \ 1)) \ z \ (y \ (x \ 1)) \ z" by (smt add_commutative mult_left_dist_add mult_right_one while_increasing while_left_unfold while_mult_star_exchange while_one_while while_plus_one while_sumstar) lemma while_decompose_5: "(x \ (y \ 1)) \ z = (y \ (x \ 1)) \ z" by (metis antisym while_decompose_5_below) lemma while_decompose_4: "(x \ (y \ 1)) \ z = x \ ((y \ (x \ 1)) \ z)" by (metis while_decompose_5 while_decompose_9 while_transitive) lemma while_simulate_2: "y ; (x \ 1) \ x \ (y \ 1) \ y \ (x \ 1) \ x \ (y \ 1)" proof (rule iffI) assume "y ; (x \ 1) \ x \ (y \ 1)" hence "y ; (x \ 1) \ (x \ 1) ; (y \ 1)" by (metis while_one_while) hence "y \ ((x \ 1) ; 1) \ (x \ 1) ; (y \ 1) + (y \ 0)" by (metis while_simulate_left_plus_1) hence "y \ (x \ 1) \ (x \ (y \ 1)) + (y \ 0)" by (metis mult_right_one while_one_while) also have "... = x \ (y \ 1)" by (metis add_commutative less_eq_def order_trans while_increasing while_right_isotone zero_least) finally show "y \ (x \ 1) \ x \ (y \ 1)" . next assume "y \ (x \ 1) \ x \ (y \ 1)" thus "y ; (x \ 1) \ x \ (y \ 1)" by (metis order_trans while_mult_increasing) qed lemma while_simulate_1: "y ; x \ x ; y \ y \ (x \ 1) \ x \ (y \ 1)" by (smt mult_right_one order_trans while_one_increasing while_right_isotone while_simulate while_simulate_2) lemma while_simulate_3: "y ; (x \ 1) \ x \ 1 \ y \ (x \ 1) \ x \ (y \ 1)" by (metis add_idempotent case_split_right while_increasing while_mult_upper_bound while_simulate_2) lemma while_extra_while: "(y ; (x \ 1)) \ z = (y ; (y \ (x \ 1))) \ z" proof - have "y ; (y \ (x \ 1)) \ y ; (x \ 1) ; (y ; (x \ 1) \ 1)" by (smt add_commutative add_left_upper_bound mult_right_one order_trans while_back_loop_prefixpoint while_left_isotone while_mult_star_exchange) hence 1: "(y ; (y \ (x \ 1))) \ z \ (y ; (x \ 1)) \ z" by (metis while_simulate_right_plus_1 mult_left_one) have "(y ; (x \ 1)) \ z \ (y ; (y \ (x \ 1))) \ z" by (metis while_increasing while_left_isotone while_mult_star_exchange) thus ?thesis using 1 by (metis antisym) qed lemma while_separate_4: "y ; x \ x ; (x \ (1 + y)) \ (x + y) \ z = x \ (y \ z)" proof assume 1: "y ; x \ x ; (x \ (1 + y))" hence "(1 + y) ; x \ x ; (x \ (1 + y))" by (smt add_associative add_least_upper_bound mult_left_one mult_left_subdist_add_left mult_right_dist_add mult_right_one while_left_unfold) hence 2: "(1 + y) ; (x \ 1) \ x \ (1 + y)" by (metis mult_right_one while_simulate_right_plus_1) have "y ; x ; (x \ 1) \ x ; (x \ ((1 + y) ; (x \ 1)))" using 1 by (smt less_eq_def mult_associative mult_right_dist_add while_associative_1 while_increasing) also have "... \ x ; (x \ (1 + y))" using 2 by (smt less_eq_def mult_left_dist_add order_refl while_absorb_2 while_left_dist_add) also have "... \ x ; (x \ 1) ; (y \ 1)" by (metis add_least_upper_bound mult_associative mult_right_isotone while_increasing while_one_increasing while_one_while while_right_isotone) finally have "y \ (x ; (x \ 1)) \ x ; (x \ 1) ; (y \ 1) + (y \ 0)" by (metis mult_associative mult_right_one while_simulate_left_plus_1) hence "(y \ 1) ; (y \ x) \ x ; (x \ y \ 1) + (y \ 0)" by (smt less_eq_def mult_associative mult_right_one order_refl order_trans while_absorb_2 while_left_dist_add while_mult_star_exchange while_one_mult_below while_one_while while_plus_one) hence "(y \ 1) ; ((y \ x) \ (y \ z)) \ x \ ((y \ 1) ; (y \ z) + (y \ 0) ; ((y \ x) \ (y \ z)))" by (metis while_simulate_right_plus) also have "... \ x \ ((y \ z) + (y \ 0))" by (metis add_isotone mult_left_zero order_refl while_absorb_2 while_one_mult_below while_right_isotone while_sub_associative) also have "... = x \ y \ z" by (metis add_right_zero while_left_dist_add) finally show "(x + y) \ z = x \ (y \ z)" by (smt add_commutative less_eq_def mult_left_one mult_right_dist_add while_plus_one while_sub_associative while_sumstar) qed lemma while_separate_5: "y ; x \ x ; (x \ (x + y)) \ (x + y) \ z = x \ (y \ z)" by (smt order_trans while_add_sub_add_one_mult while_separate_4) lemma while_separate_6: "y ; x \ x ; (x + y) \ (x + y) \ z = x \ (y \ z)" by (smt order_trans while_increasing while_mult_star_exchange while_separate_5) lemma while_separate_1: "y ; x \ x ; y \ (x + y) \ z = x \ (y \ z)" by (metis add_least_upper_bound less_eq_def mult_left_subdist_add_right while_separate_6) lemma while_separate_mult_1: "y ; x \ x ; y \ (x ; y) \ z \ x \ (y \ z)" by (metis while_mult_sub_add while_separate_1) lemma separation: "y ; x \ x ; (y \ 1) \ (x + y) \ z = x \ (y \ z)" proof assume "y ; x \ x ; (y \ 1)" hence "y \ x \ x ; (y \ 1) + (y \ 0)" by (metis mult_right_one while_simulate_left_plus_1) also have "... \ x ; (x \ y \ 1) + (y \ 0)" by (metis add_left_isotone while_increasing while_mult_star_exchange) finally have "(y \ 1) ; (y \ x) \ x ; (x \ y \ 1) + (y \ 0)" by (metis order_refl order_trans while_absorb_2 while_one_mult_below) hence "(y \ 1) ; ((y \ x) \ (y \ z)) \ x \ ((y \ 1) ; (y \ z) + (y \ 0) ; ((y \ x) \ (y \ z)))" by (metis while_simulate_right_plus) also have "... \ x \ ((y \ z) + (y \ 0))" by (metis add_isotone mult_left_zero order_refl while_absorb_2 while_one_mult_below while_right_isotone while_sub_associative) also have "... = x \ y \ z" by (metis add_right_zero while_left_dist_add) finally show "(x + y) \ z = x \ (y \ z)" by (smt add_commutative less_eq_def mult_left_one mult_right_dist_add while_plus_one while_sub_associative while_sumstar) qed lemma while_separate_left: "y ; x \ x ; (y \ 1) \ y \ (x \ z) \ x \ (y \ z)" by (metis add_commutative separation while_sub_dist_3) lemma while_simulate_4: "y ; x \ x ; (x \ (1 + y)) \ y \ (x \ z) \ x \ (y \ z)" by (metis add_commutative while_separate_4 while_sub_dist_3) lemma while_simulate_5: "y ; x \ x ; (x \ (x + y)) \ y \ (x \ z) \ x \ (y \ z)" by (smt order_trans while_add_sub_add_one_mult while_simulate_4) lemma while_simulate_6: "y ; x \ x ; (x + y) \ y \ (x \ z) \ x \ (y \ z)" by (smt order_trans while_increasing while_mult_star_exchange while_simulate_5) lemma while_simulate_7: "y ; x \ x ; y \ y \ (x \ z) \ x \ (y \ z)" by (metis add_commutative mult_left_subdist_add_left order_trans while_simulate_6) lemma while_while_mult_1: "x \ (1 \ y) = 1 \ (x \ y)" by (metis add_commutative mult_left_one mult_right_one order_refl while_separate_1) lemma while_while_mult_2: "x \ (1 \ y) = (x \ 1) \ y" by (metis while_while_mult while_while_mult_1) lemma while_import: "p \ p ; p \ p \ 1 \ p ; x \ x ; p \ p ; (x \ y) = p ; ((p ; x) \ y)" proof assume 1: "p \ p ; p \ p \ 1 \ p ; x \ x ; p" hence "p ; (x \ y) \ (p ; x) \ (p ; y)" by (smt add_commutative less_eq_def mult_associative mult_left_dist_add mult_right_one while_simulate) also have "... \ (p ; x) \ y" using 1 by (metis less_eq_def mult_left_one mult_right_dist_add while_right_isotone) finally have 2: "p ; (x \ y) \ p ; ((p ; x) \ y)" using 1 by (smt add_commutative less_eq_def mult_associative mult_left_dist_add mult_right_one) have "p ; ((p ; x) \ y) \ p ; (x \ y)" using 1 by (metis mult_left_isotone mult_left_one mult_right_isotone while_left_isotone) thus "p ; (x \ y) = p ; ((p ; x) \ y)" using 2 by (metis antisym) qed lemma while_preserve: "p \ p ; p \ p \ 1 \ p ; x \ x ; p \ p ; (x \ y) = p ; (x \ (p ; y))" apply (rule, rule antisym) apply (smt mult_associative mult_left_isotone mult_right_isotone order_trans while_simulate) by (metis mult_left_isotone mult_left_one mult_right_isotone while_right_isotone) lemma while_plus_below_while: "(x \ 1) ; x \ x \ 1" by (metis order_refl while_mult_upper_bound while_one_increasing) lemma while_01: "(w ; (x \ 1)) \ (y ; z) \ (x \ w) \ ((x \ y) ; z)" proof - have "(w ; (x \ 1)) \ (y ; z) = y ; z + w ; (((x \ 1) ; w) \ ((x \ 1) ; y ; z))" by (metis mult_associative while_productstar) also have "... \ y ; z + w ; ((x \ w) \ ((x \ y) ; z))" by (metis add_right_isotone mult_left_isotone mult_right_isotone while_isotone while_one_mult_below) also have "... \ (x \ y) ; z + (x \ w) ; ((x \ w) \ ((x \ y) ; z))" by (metis add_isotone mult_right_subdist_add_left while_left_unfold) finally show ?thesis by (metis while_left_unfold) qed lemma while_while_sub_associative: "x \ (y \ z) \ ((x \ y) \ z) + (x \ z)" proof - have 1: "x ; (x \ 1) \ (x \ 1) ; ((x \ y) \ 1)" by (metis add_least_upper_bound order_trans while_back_loop_prefixpoint while_left_plus_below) have "x \ (y \ z) \ x \ ((x \ 1) ; (y \ z))" by (metis mult_left_isotone mult_left_one while_increasing while_right_isotone) also have "... \ (x \ 1) ; ((x \ y) \ (y \ z)) + (x \ 0)" using 1 by (metis while_simulate_left_plus_1) also have "... \ (x \ 1) ; ((x \ y) \ z) + (x \ z)" by (metis add_isotone order_refl while_absorb_2 while_increasing while_right_isotone zero_least) also have "... = (x \ 1) ; z + (x \ 1) ; (x \ y) ; ((x \ y) \ z) + (x \ z)" by (metis mult_associative mult_left_dist_add while_left_unfold) also have "... = (x \ y) ; ((x \ y) \ z) + (x \ z)" by (smt add_associative add_commutative less_eq_def mult_left_one mult_right_dist_add order_refl while_absorb_1 while_plus_one while_sub_associative) also have "... \ ((x \ y) \ z) + (x \ z)" by (metis add_left_isotone while_left_plus_below) finally show ?thesis . qed (* nitpick has no counterexamples: lemma while_sumstar_4_below: "(x \ y) \ ((x \ 1) ; z) \ x \ ((y ; (x \ 1)) \ z)" lemma while_sumstar_2: "(x + y) \ z = x \ ((y ; (x \ 1)) \ z)" lemma while_sumstar_3: "(x + y) \ z = ((x \ 1) ; y) \ (x \ z)" lemma while_decompose_6: "x \ ((y ; (x \ 1)) \ z) = y \ ((x ; (y \ 1)) \ z)" lemma while_finite_associative: "x \ 0 = 0 \ (x \ y) ; z = x \ (y ; z)" 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 \ q \ q ; (r \ 1) \ q \ 1 \ s ; ((x + b + r + l) \ (q ; z)) \ s ; ((x ; (b \ q) + r + l) \ z)" lemma while_separate_right_plus: "y ; x \ x ; (x \ (1 + y)) + 1 \ y \ (x \ z) \ x \ (y \ z)" lemma while_square_1: "x \ 1 = (x ; x) \ (x + 1)" lemma while_absorb_below_one: "y ; x \ x \ y \ x \ 1 \ x" lemma "x ; z \ z \ y \ z \ x \ 1 \ z \ x \ y \ z" lemma "y \ (x \ 1) \ x \ (y \ 1) \ (x + y) \ 1 = x \ (y \ 1)" lemma "y ; x \ (1 + x) ; (y \ 1) \ (x + y) \ 1 = x \ (y \ 1)" *) end class binary_itering_T = semiring_T + binary_itering begin lemma while_right_top: "x \ T = T" by (metis add_left_top while_left_unfold) lemma while_left_top: "T ; (x \ 1) = T" by (metis add_right_top antisym top_greatest while_back_loop_prefixpoint) (* nitpick has counterexamples: lemma while_denest_0: "w ; (x \ (y ; z)) \ (w ; (x \ y)) \ (w ; (x \ y) ; z)" lemma while_denest_1: "w ; (x \ (y ; z)) \ (w ; (x \ y)) \ z" lemma while_mult_sub_while_while: "x \ (y ; z) \ (x \ y) \ z" lemma while_zero_zero: "(x \ 0) \ 0 = x \ 0" lemma while_mult_zero_zero: "(x ; (y \ 0)) \ 0 = x ; (y \ 0)" lemma while_denest_2: "w ; ((x \ (y ; w)) \ z) = w ; (((x \ y) ; w) \ z)" lemma while_denest_3: "(x \ w) \ (x \ 0) = (x \ w) \ 0" lemma while_02: "x \ ((x \ w) \ ((x \ y) ; z)) = (x \ w) \ ((x \ y) ; z)" lemma while_sumstar_3_below: "(x \ y) \ (x \ z) \ (x \ y) \ ((x \ 1) ; z)" lemma while_sumstar_1: "(x + y) \ z = (x \ y) \ ((x \ 1) ; z)" lemma while_denest_4: "(x \ w) \ (x \ (y ; z)) = (x \ w) \ ((x \ y) ; z)" lemma while_denest_5: "w ; ((x \ (y ; w)) \ (x \ (y ; z))) = w ; (((x \ y) ; w) \ ((x \ y) ; z))" lemma while_denest_6: "(w ; (x \ y)) \ z = z + w ; ((x + y ; w) \ (y ; z))" lemma while_sum_below_one: "y ; ((x + y) \ z) \ (y ; (x \ 1)) \ z" lemma while_separate_unfold: "(y ; (x \ 1)) \ z = (y \ z) + (y \ (y ; x ; (x \ ((y ; (x \ 1)) \ z))))" *) end class binary_itering_1 = binary_itering + assumes while_denest_0: "w ; (x \ (y ; z)) \ (w ; (x \ y)) \ (w ; (x \ y) ; z)" begin lemma while_denest_1: "w ; (x \ (y ; z)) \ (w ; (x \ y)) \ z" by (metis order_trans while_denest_0 while_right_plus_below) lemma while_mult_sub_while_while: "x \ (y ; z) \ (x \ y) \ z" by (metis mult_left_one while_denest_1) lemma while_zero_zero: "(x \ 0) \ 0 = x \ 0" by (smt less_eq_def mult_left_zero while_left_dist_add while_mult_star_exchange while_mult_sub_while_while while_mult_zero_add_2 while_plus_one while_sumstar) lemma while_mult_zero_zero: "(x ; (y \ 0)) \ 0 = x ; (y \ 0)" apply (rule antisym) apply (metis add_least_upper_bound add_right_zero mult_left_zero mult_right_isotone while_left_dist_add while_slide while_sub_associative) by (metis mult_left_zero while_denest_1) lemma while_denest_2: "w ; ((x \ (y ; w)) \ z) = w ; (((x \ y) ; w) \ z)" apply (rule antisym) apply (metis mult_associative while_denest_0 while_simulate_right_plus_1 while_slide) by (metis mult_right_isotone while_left_isotone while_sub_associative) lemma while_denest_3: "(x \ w) \ (x \ 0) = (x \ w) \ 0" by (metis while_absorb_2 while_right_isotone while_zero_zero zero_least) lemma while_02: "x \ ((x \ w) \ ((x \ y) ; z)) = (x \ w) \ ((x \ y) ; z)" proof - have "x ; ((x \ w) \ ((x \ y) ; z)) = x ; (x \ y) ; z + x ; (x \ w) ; ((x \ w) \ ((x \ y) ; z))" by (metis mult_associative mult_left_dist_add while_left_unfold) also have "... \ (x \ w) \ ((x \ y) ; z)" by (metis add_isotone mult_right_subdist_add_right while_left_unfold) finally have "x \ ((x \ w) \ ((x \ y) ; z)) \ ((x \ w) \ ((x \ y) ; z)) + (x \ 0)" by (metis while_simulate_absorb) hence "x \ ((x \ w) \ ((x \ y) ; z)) \ (x \ w) \ ((x \ y) ; z)" by (smt add_least_upper_bound order_refl order_trans while_mult_sub_while_while while_right_isotone zero_least) thus ?thesis by (metis antisym while_increasing) qed lemma while_sumstar_3_below: "(x \ y) \ (x \ z) \ (x \ y) \ ((x \ 1) ; z)" proof - have "(x \ y) \ (x \ z) = (x \ z) + ((x \ y) \ ((x \ y) ; (x \ z)))" by (metis while_right_unfold) also have "... \ (x \ z) + ((x \ y) \ (x \ (y ; (x \ z))))" by (metis add_right_isotone while_right_isotone while_sub_associative) also have "... \ (x \ z) + ((x \ y) \ (x \ ((x \ y) \ ((x \ 1) ; z))))" by (smt add_right_isotone mult_left_isotone mult_left_one order_trans while_increasing while_mult_upper_bound while_one_increasing while_right_isotone while_sumstar while_transitive) also have "... = (x \ z) + ((x \ y) \ ((x \ 1) ; z))" by (metis while_02 while_transitive) also have "... = (x \ y) \ ((x \ 1) ; z)" by (smt add_associative mult_left_one mult_right_dist_add while_02 while_left_dist_add while_plus_one) finally show ?thesis . qed lemma while_sumstar_4_below: "(x \ y) \ ((x \ 1) ; z) \ x \ ((y ; (x \ 1)) \ z)" proof - have "(x \ y) \ ((x \ 1) ; z) = (x \ 1) ; z + (x \ y) ; ((x \ y) \ ((x \ 1) ; z))" by (metis while_left_unfold) also have "... \ (x \ z) + (x \ (y ; ((x \ y) \ ((x \ 1) ; z))))" by (metis add_isotone while_one_mult_below while_sub_associative) also have "... = (x \ z) + (x \ (y ; (((x \ 1) ; y) \ ((x \ 1) ; z))))" by (metis mult_left_one while_denest_2) also have "... = x \ ((y ; (x \ 1)) \ z)" by (metis while_left_dist_add while_productstar) finally show ?thesis . qed lemma while_sumstar_1: "(x + y) \ z = (x \ y) \ ((x \ 1) ; z)" by (smt eq_iff order_trans while_add_1_below while_sumstar while_sumstar_3_below while_sumstar_4_below) lemma while_sumstar_2: "(x + y) \ z = x \ ((y ; (x \ 1)) \ z)" by (metis eq_iff while_add_1_below while_sumstar_1 while_sumstar_4_below) lemma while_sumstar_3: "(x + y) \ z = ((x \ 1) ; y) \ (x \ z)" by (metis eq_iff while_sumstar while_sumstar_1_below while_sumstar_2 while_sumstar_2_below) lemma while_decompose_6: "x \ ((y ; (x \ 1)) \ z) = y \ ((x ; (y \ 1)) \ z)" by (metis add_commutative while_sumstar_2) lemma while_denest_4: "(x \ w) \ (x \ (y ; z)) = (x \ w) \ ((x \ y) ; z)" proof - have "(x \ w) \ (x \ (y ; z)) = x \ ((w ; (x \ 1)) \ (y ; z))" by (metis while_sumstar while_sumstar_2) also have "... \ (x \ w) \ ((x \ y) ; z)" by (smt antisym while_01 while_02 while_increasing while_right_isotone) finally show ?thesis by (metis antisym while_right_isotone while_sub_associative) qed lemma while_denest_5: "w ; ((x \ (y ; w)) \ (x \ (y ; z))) = w ; (((x \ y) ; w) \ ((x \ y) ; z))" by (metis while_denest_2 while_denest_4) lemma while_denest_6: "(w ; (x \ y)) \ z = z + w ; ((x + y ; w) \ (y ; z))" by (metis while_denest_5 while_productstar while_sumstar) lemma while_sum_below_one: "y ; ((x + y) \ z) \ (y ; (x \ 1)) \ z" by (metis add_right_divisibility mult_left_one while_denest_6) lemma while_separate_unfold: "(y ; (x \ 1)) \ z = (y \ z) + (y \ (y ; x ; (x \ ((y ; (x \ 1)) \ z))))" proof - have "y \ (y ; x ; (x \ ((y ; (x \ 1)) \ z))) \ y \ (y ; ((x + y) \ z))" by (metis mult_associative mult_right_isotone while_sumstar_2 while_left_plus_below while_right_isotone) also have "... \ (y ; (x \ 1)) \ z" by (metis add_commutative add_left_upper_bound while_absorb_1 while_mult_star_exchange while_sum_below_one) finally have "(y \ z) + (y \ (y ; x ; (x \ ((y ; (x \ 1)) \ z)))) \ (y ; (x \ 1)) \ z" by (metis add_least_upper_bound mult_left_subdist_add_left mult_right_one while_left_isotone while_left_unfold) thus ?thesis by (metis antisym while_separate_unfold_below) qed lemma while_finite_associative: "x \ 0 = 0 \ (x \ y) ; z = x \ (y ; z)" by (metis while_denest_4 while_zero) 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 \ q \ q ; (r \ 1) \ q \ 1 \ s ; ((x + b + r + l) \ (q ; z)) \ s ; ((x ; (b \ q) + r + l) \ z)" 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 \ q \ q ; (r \ 1) \ q \ 1" hence 2: "(x + b + r) ; l \ l ; (x + b + r)" by (smt add_commutative add_least_upper_bound mult_left_subdist_add_right mult_right_dist_add order_trans) have "q ; ((x ; (b \ r \ 1) ; q) \ z) \ (x ; (b \ r \ 1) ; q) \ z" using 1 by (smt eq_refl order_trans while_increasing while_mult_upper_bound) also have "... \ (x ; (b \ ((r \ 1) ; q))) \ z" by (metis mult_associative mult_right_isotone while_left_isotone while_sub_associative) also have "... \ (x ; (b \ r \ q)) \ z" by (metis mult_right_isotone while_left_isotone while_one_mult_below while_right_isotone) also have "... \ (x ; (b \ (q ; (r \ 1)))) \ z" using 1 by (metis mult_right_isotone while_left_isotone while_right_isotone) finally have 3: "q ; ((x ; (b \ r \ 1) ; q) \ z) \ (x ; (b \ q) ; (r \ 1)) \ z" by (metis mult_associative while_associative_while_1) have "s ; ((x + b + r + l) \ (q ; z)) = s ; (l \ (x + b + r) \ (q ; z))" using 2 by (metis add_commutative while_separate_1) also have "... = s ; q ; (l \ b \ r \ (q ; x ; (b \ r \ 1)) \ (q ; z))" using 1 by (smt add_associative add_commutative while_sumstar_2 while_separate_1) also have "... = s ; q ; (l \ b \ r \ (q ; ((x ; (b \ r \ 1) ; q) \ z)))" by (smt mult_associative while_slide) also have "... \ s ; q ; (l \ b \ r \ (x ; (b \ q) ; (r \ 1)) \ z)" using 3 by (metis mult_right_isotone while_right_isotone) also have "... \ s ; (l \ q ; (b \ r \ (x ; (b \ q) ; (r \ 1)) \ z))" using 1 by (smt mult_associative mult_right_isotone while_simulate) also have "... = s ; (l \ q ; (r \ (x ; (b \ q) ; (r \ 1)) \ z))" using 1 by (metis while_elimination) also have "... \ s ; (l \ r \ (x ; (b \ q) ; (r \ 1)) \ z)" using 1 by (smt add_left_divisibility mult_left_one mult_right_dist_add mult_right_isotone while_right_isotone) also have "... = s ; (l \ (r + x ; (b \ q)) \ z)" by (metis while_sumstar_2) also have "... \ s ; ((x ; (b \ q) + r + l) \ z)" by (metis add_commutative mult_right_isotone while_sub_dist_3) finally show "s ; ((x + b + r + l) \ (q ; z)) \ s ; ((x ; (b \ q) + r + l) \ z)" . qed end class binary_itering_1_T = binary_itering_T + binary_itering_1 begin (* lemma while_unfold_below: "x = z + y ; x \ x \ y \ z" nitpick lemma while_unfold_below_1: "x = y ; x \ x \ y \ 1" nitpick lemma while_loop_is_greatest_postfixpoint: "is_greatest_postfixpoint (\x . y ; x + z) (y \ z)" nitpick lemma while_loop_is_greatest_fixpoint: "is_greatest_fixpoint (\x . y ; x + z) (y \ z)" nitpick lemma while_sub_mult_one: "x ; (1 \ y) \ 1 \ x" nitpick lemma while_sub_while_zero: "x \ z \ (x \ y) \ z" nitpick lemma while_while_sub_associative: "x \ (y \ z) \ (x \ y) \ z" nitpick lemma while_top: "T \ x = T" nitpick lemma while_one_top: "1 \ x = T" nitpick lemma while_mult_top: "(x ; T) \ z = z + x ; T" nitpick lemma tarski: "x \ x ; T ; x ; T" nitpick lemma tarski_mult_top_idempotent: "x ; T = x ; T ; x ; T" nitpick lemma tarski_top_omega_below: "x ; T \ (x ; T) \ 0" nitpick lemma tarski_top_omega: "x ; T = (x ; T) \ 0" nitpick lemma tarski_below_top_omega: "x \ (x ; T) \ 0" nitpick lemma tarski: "x = 0 \ T ; x ; T = T" nitpick lemma "(x + y) \ z = ((x \ 1) ; y) \ ((x \ 1) ; z)" nitpick lemma "1 = (x ; 0) \ 1" nitpick lemma while_top_2: "T \ z = T ; z" nitpick lemma while_mult_top_2: "(x ; T) \ z = z + x ; T ; z" nitpick lemma while_one_mult: "(x \ 1) ; x = x \ x" nitpick lemma "(x \ 1) ; y = x \ y" nitpick lemma while_associative: "(x \ y) ; z = x \ (y ; z)" nitpick lemma while_back_loop_is_fixpoint: "is_fixpoint (\x . x ; y + z) (z ; (y \ 1))" nitpick lemma "1 + x ; 0 = x \ 1" nitpick lemma "x = x ; (x \ 1)" nitpick lemma "x ; (x \ 1) = x \ 1" nitpick lemma "x \ 1 = x \ (1 \ 1)" nitpick lemma "(x + y) \ 1 = (x \ (y \ 1)) \ 1" nitpick lemma "z + y ; x = x \ y \ z \ x" nitpick lemma "y ; x = x \ y \ x \ x" nitpick lemma "z + x ; y = x \ z ; (y \ 1) \ x" nitpick lemma "x ; y = x \ x ; (y \ 1) \ x" nitpick lemma "x ; z = z ; y \ x \ z \ z ; (y \ 1)" nitpick *) end (* end theory BinaryIterationStrict imports BinaryIteration Iteration begin *) class strict_itering = itering_3 + while + assumes while_def: "x \ y = x\<^sup>\ ; y" begin subclass binary_itering_1 apply unfold_locales apply (metis add_commutative circ_loop_fixpoint circ_slide mult_associative while_def) apply (metis circ_add mult_associative while_def) apply (metis mult_left_dist_add while_def) apply (metis mult_associative order_refl while_def) apply (metis circ_simulate_left_plus mult_associative mult_left_isotone mult_right_dist_add mult_right_one while_def) apply (metis circ_simulate_right_plus mult_associative mult_left_isotone mult_right_dist_add while_def) by (metis add_right_divisibility circ_loop_fixpoint mult_associative while_def) lemma while_associative: "(x \ y) ; z = x \ (y ; z)" by (metis mult_associative while_def) lemma circ_import: "p \ p ; p \ p \ 1 \ p ; x \ x ; p \ p ; x\<^sup>\ = p ; (p ; x)\<^sup>\" proof assume 1: "p \ p ; p \ p \ 1 \ p ; x \ x ; p" hence "p ; x \ p ; x ; p" by (smt mult_associative mult_left_isotone mult_right_isotone order_trans) hence "p ; x\<^sup>\ \ (p ; x)\<^sup>\" using 1 by (smt circ_mult_upper_bound circ_reflexive circ_simulate order_refl order_trans) hence 2: "p ; x\<^sup>\ \ p ; (p ; x)\<^sup>\" using 1 by (smt mult_associative mult_left_isotone mult_right_isotone order_trans) have "p ; (p ; x)\<^sup>\ \ p ; x\<^sup>\" using 1 by (metis circ_isotone mult_left_isotone mult_left_one mult_right_isotone) thus "p ; x\<^sup>\ = p ; (p ; x)\<^sup>\" using 2 by (metis antisym) qed lemma while_one_mult: "(x \ 1) ; x = x \ x" by (metis mult_right_one while_def) lemma while_back_loop_is_fixpoint: "is_fixpoint (\x . x ; y + z) (z ; (y \ 1))" by (metis circ_back_loop_is_fixpoint mult_right_one while_def) lemma "x ; z \ z \ y \ z \ x \ 1 \ z \ x \ y \ z" by (metis add_commutative less_eq_def mult_left_one order_trans while_right_isotone while_simulate_absorb zero_right_mult_decreasing) lemma "(x + y) \ z = ((x \ 1) ; y) \ ((x \ 1) ; z)" by (metis mult_right_one while_def while_sumstar) lemma "(x \ 1) ; y = x \ y" by (metis mult_left_one while_associative) (* nitpick has no counterexamples: lemma "y \ (x \ 1) \ x \ (y \ 1) \ (x + y) \ 1 = x \ (y \ 1)" lemma "y ; x \ (1 + x) ; (y \ 1) \ (x + y) \ 1 = x \ (y \ 1)" lemma while_square_1: "x \ 1 = (x ; x) \ (x + 1)" lemma while_absorb_below_one: "y ; x \ x \ y \ x \ 1 \ x" *) end class strict_itering_T = itering_T + strict_itering begin subclass binary_itering_1_T .. lemma while_top_2: "T \ z = T ; z" by (metis circ_top while_def) lemma while_mult_top_2: "(x ; T) \ z = z + x ; T ; z" by (metis circ_left_top mult_associative while_def while_left_unfold) (* lemma while_unfold_below: "x = z + y ; x \ x \ y \ z" nitpick lemma while_unfold_below_1: "x = y ; x \ x \ y \ 1" nitpick lemma while_loop_is_greatest_postfixpoint: "is_greatest_postfixpoint (\x . y ; x + z) (y \ z)" nitpick lemma while_loop_is_greatest_fixpoint: "is_greatest_fixpoint (\x . y ; x + z) (y \ z)" nitpick lemma while_sub_mult_one: "x ; (1 \ y) \ 1 \ x" nitpick lemma while_sub_while_zero: "x \ z \ (x \ y) \ z" nitpick lemma while_while_sub_associative: "x \ (y \ z) \ (x \ y) \ z" nitpick lemma while_top: "T \ x = T" nitpick lemma while_one_top: "1 \ x = T" nitpick lemma while_mult_top: "(x ; T) \ z = z + x ; T" nitpick lemma tarski: "x \ x ; T ; x ; T" nitpick lemma tarski_mult_top_idempotent: "x ; T = x ; T ; x ; T" nitpick lemma tarski_top_omega_below: "x ; T \ (x ; T) \ 0" nitpick lemma tarski_top_omega: "x ; T = (x ; T) \ 0" nitpick lemma tarski_below_top_omega: "x \ (x ; T) \ 0" nitpick lemma tarski: "x = 0 \ T ; x ; T = T" nitpick lemma "1 = (x ; 0) \ 1" nitpick lemma "1 + x ; 0 = x \ 1" nitpick lemma "x = x ; (x \ 1)" nitpick lemma "x ; (x \ 1) = x \ 1" nitpick lemma "x \ 1 = x \ (1 \ 1)" nitpick lemma "(x + y) \ 1 = (x \ (y \ 1)) \ 1" nitpick lemma "z + y ; x = x \ y \ z \ x" nitpick lemma "y ; x = x \ y \ x \ x" nitpick lemma "z + x ; y = x \ z ; (y \ 1) \ x" nitpick lemma "x ; y = x \ x ; (y \ 1) \ x" nitpick lemma "x ; z = z ; y \ x \ z \ z ; (y \ 1)" nitpick *) end (* end theory BinaryIterationNonstrict imports BinaryIteration Omega begin *) class nonstrict_itering = omega_algebra_T + while + assumes while_def: "x \ y = x\<^sup>\ + x\<^sup>\ ; y" begin subclass binary_itering_T proof (unfold_locales) fix x y z show "(x ; y) \ z = z + x ; ((y ; x) \ (y ; z))" by (metis add_commutative mult_associative mult_left_dist_add omega_loop_fixpoint omega_slide star.circ_slide while_def) next fix x y z show "(x + y) \ z = (x \ y) \ (x \ z)" proof - have 1: "(x + y) \ z = (x\<^sup>\ ; y)\<^sup>\ + (x\<^sup>\ ; y)\<^sup>\ ; (x\<^sup>\ + x\<^sup>\ ; z)" by (smt add_associative mult_associative mult_left_dist_add omega_decompose star.circ_add while_def) hence 2: "(x + y) \ z \ (x \ y) \ (x \ z)" by (smt add_isotone add_right_upper_bound less_eq_def mult_left_isotone omega_sub_dist star.circ_sub_dist while_def) let ?rhs = "x\<^sup>\ ; y ; ((x\<^sup>\ + x\<^sup>\ ; y)\<^sup>\ + (x\<^sup>\ + x\<^sup>\ ; y)\<^sup>\ ; (x\<^sup>\ + x\<^sup>\ ; z)) + (x\<^sup>\ + x\<^sup>\ ; z)" have "x\<^sup>\ ; (x\<^sup>\ + x\<^sup>\ ; y)\<^sup>\ \ x\<^sup>\" by (metis omega_sub_vector) hence "x\<^sup>\ ; (x\<^sup>\ + x\<^sup>\ ; y)\<^sup>\ + x\<^sup>\ ; y ; (x\<^sup>\ + x\<^sup>\ ; y)\<^sup>\ \ ?rhs" by (smt add_commutative add_isotone add_left_upper_bound mult_left_dist_add order_trans) hence 3: "(x\<^sup>\ + x\<^sup>\ ; y)\<^sup>\ \ ?rhs" by (metis mult_right_dist_add omega_unfold) have "x\<^sup>\ ; (x\<^sup>\ + x\<^sup>\ ; y)\<^sup>\ ; (x\<^sup>\ + x\<^sup>\ ; z) \ x\<^sup>\" by (metis mult_associative omega_sub_vector) hence "x\<^sup>\ ; (x\<^sup>\ + x\<^sup>\ ; y)\<^sup>\ ; (x\<^sup>\ + x\<^sup>\ ; z) + x\<^sup>\ ; y ; (x\<^sup>\ + x\<^sup>\ ; y)\<^sup>\ ; (x\<^sup>\ + x\<^sup>\ ; z) \ ?rhs" by (smt add_commutative add_isotone add_right_upper_bound mult_associative mult_left_dist_add order_trans) hence "(x\<^sup>\ + x\<^sup>\ ; y)\<^sup>\ ; (x\<^sup>\ + x\<^sup>\ ; z) \ ?rhs" by (smt add_associative add_right_upper_bound less_eq_def mult_associative mult_right_dist_add star.circ_loop_fixpoint) hence "(x\<^sup>\ + x\<^sup>\ ; y)\<^sup>\ + (x\<^sup>\ + x\<^sup>\ ; y)\<^sup>\ ; (x\<^sup>\ + x\<^sup>\ ; z) \ ?rhs" using 3 by (metis add_least_upper_bound) hence "(x\<^sup>\ + x\<^sup>\ ; y)\<^sup>\ + (x\<^sup>\ + x\<^sup>\ ; y)\<^sup>\ ; (x\<^sup>\ + x\<^sup>\ ; z) \ (x\<^sup>\ ; y)\<^sup>\ + (x\<^sup>\ ; y)\<^sup>\ ; (x\<^sup>\ + x\<^sup>\ ; z)" by (metis add_commutative omega_induct) thus ?thesis using 1 2 by (smt antisym while_def) qed next fix x y z show "x \ (y + z) = (x \ y) + (x \ z)" by (smt add_associative add_commutative add_left_upper_bound less_eq_def mult_left_dist_add while_def) next fix x y z show "(x \ y) ; z \ x \ (y ; z)" by (metis mult_associative mult_right_dist_add omega_loop_fixpoint omega_loop_greatest_fixpoint while_def) next fix v w x y z show "x ; z \ z ; (y \ 1) + w \ x \ (z ; v) \ z ; (y \ v) + (x \ (w ; (y \ v)))" proof assume "x ; z \ z ; (y \ 1) + w" hence 1: "x ; z \ z ; y\<^sup>\ + z ; y\<^sup>\ + w" by (metis mult_left_dist_add mult_right_one while_def) let ?rhs = "z ; (y\<^sup>\ + y\<^sup>\ ; v) + x\<^sup>\ + x\<^sup>\ ; w ; (y\<^sup>\ + y\<^sup>\ ; v)" have 2: "z ; v \ ?rhs" by (metis add_least_upper_bound add_left_upper_bound mult_left_dist_add omega_loop_fixpoint) have "x ; z ; (y\<^sup>\ + y\<^sup>\ ; v) \ ?rhs" proof - have "x ; z ; (y\<^sup>\ + y\<^sup>\ ; v) \ (z ; y\<^sup>\ + z ; y\<^sup>\ + w) ; (y\<^sup>\ + y\<^sup>\ ; v)" using 1 by (metis mult_left_isotone) also have "... = z ; (y\<^sup>\ ; (y\<^sup>\ + y\<^sup>\ ; v) + y\<^sup>\ ; (y\<^sup>\ + y\<^sup>\ ; v)) + w ; (y\<^sup>\ + y\<^sup>\ ; v)" by (smt mult_associative mult_left_dist_add mult_right_dist_add) also have "... = z ; (y\<^sup>\ ; (y\<^sup>\ + y\<^sup>\ ; v) + y\<^sup>\ + y\<^sup>\ ; v) + w ; (y\<^sup>\ + y\<^sup>\ ; v)" by (smt add_associative mult_associative mult_left_dist_add star.circ_transitive_equal star_mult_omega) also have "... \ z ; (y\<^sup>\ + y\<^sup>\ ; v) + x\<^sup>\ ; w ; (y\<^sup>\ + y\<^sup>\ ; v)" by (smt add_commutative add_isotone add_left_top mult_left_dist_add mult_left_one mult_right_dist_add mult_right_subdist_add_left omega_vector order_refl star.circ_plus_one) finally show ?thesis by (smt add_associative add_commutative less_eq_def) qed hence "x ; ?rhs \ ?rhs" by (smt add_associative add_commutative add_left_upper_bound less_eq_def mult_associative mult_left_dist_add mult_right_dist_add omega_unfold star.circ_increasing star.circ_transitive_equal) hence "z ; v + x ; ?rhs \ ?rhs" using 2 by (metis add_least_upper_bound) hence "x\<^sup>\ ; z ; v \ ?rhs" by (metis mult_associative star_left_induct) hence "x\<^sup>\ + x\<^sup>\ ; z ; v \ ?rhs" by (metis add_least_upper_bound add_left_upper_bound) thus "x \ (z ; v) \ z ; (y \ v) + (x \ (w ; (y \ v)))" by (smt add_associative mult_associative mult_left_dist_add while_def) qed next fix v w x y z show "z ; x \ y ; (y \ z) + w \ z ; (x \ v) \ y \ (z ; v + w ; (x \ v))" proof assume "z ; x \ y ; (y \ z) + w" hence "z ; x \ y ; (y\<^sup>\ + y\<^sup>\ ; z) + w" by (metis while_def) hence 1: "z ; x \ y\<^sup>\ + y ; y\<^sup>\ ; z + w" by (metis mult_associative mult_left_dist_add omega_unfold) let ?rhs = "y\<^sup>\ + y\<^sup>\ ; z ; v + y\<^sup>\ ; w ; (x\<^sup>\ + x\<^sup>\ ; v)" have 2: "z ; x\<^sup>\ \ ?rhs" proof - have "z ; x\<^sup>\ \ y ; y\<^sup>\ ; z ; x\<^sup>\ + y\<^sup>\ ; x\<^sup>\ + w ; x\<^sup>\" using 1 by (smt add_commutative less_eq_def mult_associative mult_right_dist_add omega_unfold) also have "... \ y ; y\<^sup>\ ; z ; x\<^sup>\ + y\<^sup>\ + w ; x\<^sup>\" by (metis add_left_isotone add_right_isotone omega_sub_vector) also have "... = y ; y\<^sup>\ ; (z ; x\<^sup>\) + (y\<^sup>\ + w ; x\<^sup>\)" by (metis add_associative mult_associative) finally have "z ; x\<^sup>\ \ (y ; y\<^sup>\)\<^sup>\ + (y ; y\<^sup>\)\<^sup>\ ; (y\<^sup>\ + w ; x\<^sup>\)" by (metis add_commutative omega_induct) also have "... = y\<^sup>\ + y\<^sup>\ ; w ; x\<^sup>\" by (metis left_plus_omega less_eq_def mult_associative mult_left_dist_add mult_left_subdist_add_left star.left_plus_circ star_mult_omega) also have "... \ ?rhs" by (metis add_isotone add_left_upper_bound mult_left_subdist_add_left) finally show ?thesis by metis qed let ?rhs2 = "y\<^sup>\ + y\<^sup>\ ; z + y\<^sup>\ ; w ; (x\<^sup>\ + x\<^sup>\)" have "?rhs2 ; x \ ?rhs2" proof - have 3: "y\<^sup>\ ; x \ ?rhs2" by (metis add_associative less_eq_def omega_sub_vector) have "y\<^sup>\ ; z ; x \ y\<^sup>\ ; (y\<^sup>\ + y ; y\<^sup>\ ; z + w)" using 1 by (metis mult_associative mult_right_isotone) also have "... = y\<^sup>\ + y\<^sup>\ ; y ; y\<^sup>\ ; z + y\<^sup>\ ; w" by (metis mult_associative mult_left_dist_add star_mult_omega) also have "... = y\<^sup>\ + y ; y\<^sup>\ ; z + y\<^sup>\ ; w" by (metis mult_associative star.circ_transitive_equal star_simulation_right_equal) also have "... \ y\<^sup>\ + y\<^sup>\ ; z + y\<^sup>\ ; w" by (metis add_left_isotone add_right_isotone mult_left_isotone star.left_plus_below_circ) also have "... \ y\<^sup>\ + y\<^sup>\ ; z + y\<^sup>\ ; w ; x\<^sup>\" by (metis add_right_isotone add_right_upper_bound star.circ_back_loop_fixpoint) finally have 4: "y\<^sup>\ ; z ; x \ ?rhs2" by (smt add_associative add_commutative less_eq_def mult_left_dist_add) have "(x\<^sup>\ + x\<^sup>\) ; x \ x\<^sup>\ + x\<^sup>\" by (metis add_isotone mult_right_dist_add omega_sub_vector star.circ_plus_same star.left_plus_below_circ) hence "y\<^sup>\ ; w ; (x\<^sup>\ + x\<^sup>\) ; x \ ?rhs2" by (smt add_right_upper_bound mult_associative mult_right_isotone order_trans) thus ?thesis using 3 4 by (smt add_associative less_eq_def mult_right_dist_add) qed hence "z + ?rhs2 ; x \ ?rhs2" by (smt add_commutative add_least_upper_bound add_right_divisibility while_def omega_loop_fixpoint) hence 5: "z ; x\<^sup>\ \ ?rhs2" by (metis star_right_induct) have "z ; x\<^sup>\ ; v \ ?rhs" proof - have "z ; x\<^sup>\ ; v \ ?rhs2 ; v" using 5 by (metis mult_left_isotone) also have "... = y\<^sup>\ ; v + y\<^sup>\ ; z ; v + y\<^sup>\ ; w ; (x\<^sup>\ ; v + x\<^sup>\ ; v)" by (metis mult_associative mult_right_dist_add) also have "... \ y\<^sup>\ + y\<^sup>\ ; z ; v + y\<^sup>\ ; w ; (x\<^sup>\ ; v + x\<^sup>\ ; v)" by (metis add_left_isotone omega_sub_vector) also have "... \ ?rhs" by (metis add_left_isotone add_right_isotone mult_right_isotone omega_sub_vector) finally show ?thesis by metis qed hence "z ; (x\<^sup>\ + x\<^sup>\ ; v) \ ?rhs" using 2 by (smt add_associative less_eq_def mult_associative mult_left_dist_add) thus "z ; (x \ v) \ y \ (z ; v + w ; (x \ v))" by (metis add_associative mult_associative mult_left_dist_add while_def) qed qed lemma while_top: "T \ x = T" by (metis add_left_top star.circ_top star_omega_top while_def) lemma while_one_top: "1 \ x = T" by (metis add_left_top omega_one while_def) lemma while_finite_associative: "x\<^sup>\ = 0 \ (x \ y) ; z = x \ (y ; z)" by (metis add_left_zero mult_associative while_def) lemma star_below_while: "x\<^sup>\ ; y \ x \ y" by (metis add_right_upper_bound while_def) lemma while_sub_mult_one: "x ; (1 \ y) \ 1 \ x" by (metis top_greatest while_one_top) lemma while_while_one: "y \ (x \ 1) = y\<^sup>\ + y\<^sup>\ ; x\<^sup>\ + y\<^sup>\ ; x\<^sup>\" by (metis add_associative mult_left_dist_add mult_right_one while_def) lemma omega_mult_star_2: "x\<^sup>\ ; y\<^sup>\ = x\<^sup>\" by (metis add_right_upper_bound antisym omega_sub_vector star.circ_back_loop_fixpoint) lemma star_omega_absorb: "y\<^sup>\ ; (y\<^sup>\ ; x)\<^sup>\ ; y\<^sup>\ = (y\<^sup>\ ; x)\<^sup>\ ; y\<^sup>\" proof - have "y\<^sup>\ ; (y\<^sup>\ ; x)\<^sup>\ ; y\<^sup>\ = y\<^sup>\ ; y\<^sup>\ ; x ; (y\<^sup>\ ; x)\<^sup>\ ; y\<^sup>\ + y\<^sup>\ ; y\<^sup>\" by (metis add_commutative mult_associative mult_right_dist_add star.circ_back_loop_fixpoint star.circ_plus_same) thus ?thesis by (metis mult_associative star.circ_loop_fixpoint star.circ_transitive_equal star_mult_omega) qed lemma star_star_absorb: "y\<^sup>\ ; (y\<^sup>\ ; x)\<^sup>\ ; y\<^sup>\ = (y\<^sup>\ ; x)\<^sup>\ ; y\<^sup>\" by (metis add_commutative mult_associative star.circ_decompose_4 star.circ_slide star_decompose_1 star_decompose_3) lemma while_simulate_4_plus: "y ; x \ x ; (x \ (1 + y)) \ y ; x ; x\<^sup>\ \ x ; (x \ (1 + y))" proof have 1: "x ; (x \ (1 + y)) = x\<^sup>\ + x ; x\<^sup>\ + x ; x\<^sup>\ ; y" by (metis add_associative mult_associative mult_left_dist_add mult_right_one omega_unfold while_def) assume "y ; x \ x ; (x \ (1 + y))" hence "y ; x ; x\<^sup>\ \ (x\<^sup>\ + x ; x\<^sup>\ + x ; x\<^sup>\ ; y) ; x\<^sup>\" using 1 by (metis mult_left_isotone) also have "... = x\<^sup>\ ; x\<^sup>\ + x ; x\<^sup>\ ; x\<^sup>\ + x ; x\<^sup>\ ; y ; x\<^sup>\" by (metis mult_right_dist_add) also have "... = x ; x\<^sup>\ ; (y ; x ; x\<^sup>\) + x\<^sup>\ + x ; x\<^sup>\ + x ; x\<^sup>\ ; y" by (smt add_associative add_commutative mult_associative omega_mult_star_2 star.circ_back_loop_fixpoint star.circ_plus_same star.circ_transitive_equal) finally have "y ; x ; x\<^sup>\ \ x ; x\<^sup>\ ; (y ; x ; x\<^sup>\) + (x\<^sup>\ + x ; x\<^sup>\ + x ; x\<^sup>\ ; y)" by (metis add_associative) hence "y ; x ; x\<^sup>\ \ (x ; x\<^sup>\)\<^sup>\ + (x ; x\<^sup>\)\<^sup>\ ; (x\<^sup>\ + x ; x\<^sup>\ + x ; x\<^sup>\ ; y)" by (metis add_commutative omega_induct) also have "... = x\<^sup>\ + x\<^sup>\ ; (x\<^sup>\ + x ; x\<^sup>\ + x ; x\<^sup>\ ; y)" by (metis left_plus_omega star.left_plus_circ) finally show "y ; x ; x\<^sup>\ \ x ; (x \ (1 + y))" using 1 by (metis while_def while_mult_star_exchange while_transitive) qed lemma while_simulate_4_omega: "y ; x \ x ; (x \ (1 + y)) \ y ; x\<^sup>\ \ x\<^sup>\" proof have 1: "x ; (x \ (1 + y)) = x\<^sup>\ + x ; x\<^sup>\ + x ; x\<^sup>\ ; y" by (metis add_associative mult_associative mult_left_dist_add mult_right_one omega_unfold while_def) assume "y ; x \ x ; (x \ (1 + y))" hence "y ; x\<^sup>\ \ (x\<^sup>\ + x ; x\<^sup>\ + x ; x\<^sup>\ ; y) ; x\<^sup>\" using 1 by (smt less_eq_def mult_associative mult_right_dist_add omega_unfold) also have "... = x\<^sup>\ ; x\<^sup>\ + x ; x\<^sup>\ ; x\<^sup>\ + x ; x\<^sup>\ ; y ; x\<^sup>\" by (metis mult_right_dist_add) also have "... = x ; x\<^sup>\ ; (y ; x\<^sup>\) + x\<^sup>\" by (metis add_commutative less_eq_def mult_associative omega_sub_vector omega_unfold star_mult_omega) finally have "y ; x\<^sup>\ \ x ; x\<^sup>\ ; (y ; x\<^sup>\) + x\<^sup>\" by metis hence "y ; x\<^sup>\ \ (x ; x\<^sup>\)\<^sup>\ + (x ; x\<^sup>\)\<^sup>\ ; x\<^sup>\" by (metis add_commutative omega_induct) thus "y ; x\<^sup>\ \ x\<^sup>\" by (metis add_idempotent left_plus_omega star_mult_omega) qed lemma while_unfold_below: "x = z + y ; x \ x \ y \ z" by (metis omega_induct_equal while_def) lemma while_unfold_below_1: "x = y ; x \ x \ y \ 1" by (metis add_right_upper_bound omega_induct while_def) lemma while_square_1: "x \ 1 = (x ; x) \ (x + 1)" by (metis mult_right_one omega_square star_square_2 while_def) lemma while_absorb_below_one: "y ; x \ x \ y \ x \ 1 \ x" by (metis top_greatest while_one_top) lemma omega_import: "p \ p ; p \ p ; x \ x ; p \ p ; x\<^sup>\ = p ; (p ; x)\<^sup>\" proof assume 1: "p \ p ; p \ p ; x \ x ; p" hence "p ; x\<^sup>\ \ p ; (p ; x) ; x\<^sup>\" by (metis mult_associative mult_left_isotone omega_unfold) also have "... \ p ; x ; p ; x\<^sup>\" using 1 by (metis mult_associative mult_left_isotone mult_right_isotone) finally have "p ; x\<^sup>\ \ (p ; x)\<^sup>\" by (metis mult_associative omega_induct_mult) hence "p ; x\<^sup>\ \ p ; (p ; x)\<^sup>\" using 1 by (smt mult_associative mult_left_isotone mult_right_isotone order_trans) thus "p ; x\<^sup>\ = p ; (p ; x)\<^sup>\" using 1 by (metis add_left_divisibility antisym mult_right_isotone omega_induct_mult omega_slide omega_sub_dist) qed lemma star_import: "p \ p ; p \ p \ 1 \ p ; x \ x ; p \ p ; x\<^sup>\ = p ; (p ; x)\<^sup>\" proof assume 1: "p \ p ; p \ p \ 1 \ p ; x \ x ; p" hence "p ; (p ; x)\<^sup>\ ; x \ p ; (x ; p)\<^sup>\ ; x" by (smt add_right_divisibility mult_associative mult_left_isotone mult_left_subdist_add_right star.circ_simulate star.circ_slide) hence "p ; (p ; x)\<^sup>\ ; x \ (p ; x)\<^sup>\" by (metis add_right_divisibility order_trans star.circ_mult) hence 2: "p ; (p ; x)\<^sup>\ ; x \ p ; (p ; x)\<^sup>\" using 1 by (smt mult_associative mult_left_isotone mult_right_isotone order_trans) have "p \ p ; (p ; x)\<^sup>\" by (metis add_right_divisibility star.circ_back_loop_fixpoint) hence "p ; x\<^sup>\ \ p ; (p ; x)\<^sup>\" using 2 by (metis add_least_upper_bound star_right_induct) thus "p ; x\<^sup>\ = p ; (p ; x)\<^sup>\" using 1 by (metis antisym mult_left_isotone mult_left_one mult_right_isotone star.circ_isotone) qed lemma while_loop_is_greatest_postfixpoint: "is_greatest_postfixpoint (\x . y ; x + z) (y \ z)" proof - have "(y \ z) \ (\x . y ; x + z) (y \ z)" by (metis is_fixpoint_def order_refl while_loop_is_fixpoint) thus ?thesis by (smt add_commutative is_greatest_postfixpoint_def omega_induct while_def) qed lemma while_loop_is_greatest_fixpoint: "is_greatest_fixpoint (\x . y ; x + z) (y \ z)" by (metis omega_loop_is_greatest_fixpoint while_def) lemma "x ; z \ z \ y \ z \ x \ 1 \ z \ x \ y \ z" by (metis add_commutative add_least_upper_bound add_left_zero less_eq_def while_right_isotone while_simulate_absorb) (* nitpick has no counterexamples: lemma while_sumstar_4_below: "(x \ y) \ ((x \ 1) ; z) \ x \ ((y ; (x \ 1)) \ z)" lemma while_sumstar_2: "(x + y) \ z = x \ ((y ; (x \ 1)) \ z)" lemma while_sumstar_3: "(x + y) \ z = ((x \ 1) ; y) \ (x \ z)" lemma while_decompose_6: "x \ ((y ; (x \ 1)) \ z) = y \ ((x ; (y \ 1)) \ z)" lemma while_finite_associative: "x \ 0 = 0 \ (x \ y) ; z = x \ (y ; z)" 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 \ q \ q ; (r \ 1) \ q \ 1 \ s ; ((x + b + r + l) \ (q ; z)) \ s ; ((x ; (b \ q) + r + l) \ z)" lemma while_separate_right_plus: "y ; x \ x ; (x \ (1 + y)) + 1 \ y \ (x \ z) \ x \ (y \ z)" lemma "x ; z \ z \ y \ z \ x \ 1 \ z \ x \ y \ z" lemma "y \ (x \ 1) \ x \ (y \ 1) \ (x + y) \ 1 = x \ (y \ 1)" lemma "y ; x \ (1 + x) ; (y \ 1) \ (x + y) \ 1 = x \ (y \ 1)" lemma while_mult_sub_while_while: "x \ (y ; z) \ (x \ y) \ z" lemma while_zero_zero: "(x \ 0) \ 0 = x \ 0" lemma while_denest_3: "(x \ w) \ (x \ 0) = (x \ w) \ 0" lemma while_02: "x \ ((x \ w) \ ((x \ y) ; z)) = (x \ w) \ ((x \ y) ; z)" lemma while_sumstar_3_below: "(x \ y) \ (x \ z) \ (x \ y) \ ((x \ 1) ; z)" lemma while_sumstar_1: "(x + y) \ z = (x \ y) \ ((x \ 1) ; z)" lemma while_denest_4: "(x \ w) \ (x \ (y ; z)) = (x \ w) \ ((x \ y) ; z)" *) end class nonstrict_itering_zero = nonstrict_itering + assumes mult_right_zero: "x ; 0 = 0" begin lemma while_finite_associative_2: "x \ 0 = 0 \ (x \ y) ; z = x \ (y ; z)" by (metis add_left_zero add_right_zero mult_associative mult_right_zero while_def) (* nitpick has counterexamples: lemma while_denest_0: "w ; (x \ (y ; z)) \ (w ; (x \ y)) \ (w ; (x \ y) ; z)" lemma while_denest_1: "w ; (x \ (y ; z)) \ (w ; (x \ y)) \ z" lemma while_mult_zero_zero: "(x ; (y \ 0)) \ 0 = x ; (y \ 0)" lemma while_denest_2: "w ; ((x \ (y ; w)) \ z) = w ; (((x \ y) ; w) \ z)" lemma while_denest_5: "w ; ((x \ (y ; w)) \ (x \ (y ; z))) = w ; (((x \ y) ; w) \ ((x \ y) ; z))" lemma while_denest_6: "(w ; (x \ y)) \ z = z + w ; ((x + y ; w) \ (y ; z))" lemma while_sum_below_one: "y ; ((x + y) \ z) \ (y ; (x \ 1)) \ z" lemma while_separate_unfold: "(y ; (x \ 1)) \ z = (y \ z) + (y \ (y ; x ; (x \ ((y ; (x \ 1)) \ z))))" lemma while_sub_while_zero: "x \ z \ (x \ y) \ z" lemma while_while_sub_associative: "x \ (y \ z) \ (x \ y) \ z" lemma tarski: "x \ x ; T ; x ; T" lemma tarski_mult_top_idempotent: "x ; T = x ; T ; x ; T" lemma tarski_top_omega_below: "x ; T \ (x ; T)\<^sup>\" lemma tarski_top_omega: "x ; T = (x ; T)\<^sup>\" lemma tarski_below_top_omega: "x \ (x ; T)\<^sup>\" lemma tarski_mult_omega_omega: "(x ; y\<^sup>\)\<^sup>\ = x ; y\<^sup>\" lemma tarski_mult_omega_omega: "(\z . z\<^sup>\\<^sup>\ = z\<^sup>\) \ (x ; y\<^sup>\)\<^sup>\ = x ; y\<^sup>\" lemma while_mult_top: "(x ; T) \ z = z + x ; T" lemma tarski: "x = 0 \ T ; x ; T = T" *) end class nonstrict_itering_tarski = nonstrict_itering + assumes tarski: "x \ x ; T ; x ; T" begin lemma tarski_mult_top_idempotent: "x ; T = x ; T ; x ; T" by (metis add_commutative less_eq_def mult_associative star.circ_back_loop_fixpoint star.circ_left_top tarski top_mult_top) lemma tarski_top_omega_below: "x ; T \ (x ; T)\<^sup>\" by (metis mult_associative omega_induct_mult order_refl tarski_mult_top_idempotent) lemma tarski_top_omega: "x ; T = (x ; T)\<^sup>\" by (metis antisym mult_top_omega tarski_top_omega_below) lemma tarski_below_top_omega: "x \ (x ; T)\<^sup>\" by (metis tarski_top_omega top_right_mult_increasing) lemma tarski_mult_omega_omega: "(x ; y\<^sup>\)\<^sup>\ = x ; y\<^sup>\" by (metis mult_associative omega_vector tarski_top_omega) lemma tarski_omega_idempotent: "x\<^sup>\\<^sup>\ = x\<^sup>\" by (metis omega_vector tarski_top_omega) lemma while_denest_2a: "w ; ((x \ (y ; w)) \ z) = w ; (((x \ y) ; w) \ z)" proof - have "(x\<^sup>\ + x\<^sup>\ ; y ; w)\<^sup>\ = (x\<^sup>\ ; y ; w)\<^sup>\ ; x\<^sup>\ ; (((x\<^sup>\ ; y ; w)\<^sup>\ ; x\<^sup>\)\<^sup>\ + ((x\<^sup>\ ; y ; w)\<^sup>\ ; x\<^sup>\)\<^sup>\ ; (x\<^sup>\ ; y ; w)\<^sup>\) + (x\<^sup>\ ; y ; w)\<^sup>\" by (metis add_commutative omega_decompose omega_loop_fixpoint) also have "... \ (x\<^sup>\ ; y ; w)\<^sup>\ ; x\<^sup>\ + (x\<^sup>\ ; y ; w)\<^sup>\" by (metis add_left_isotone mult_associative mult_right_isotone omega_sub_vector) finally have 1: "w ; (x\<^sup>\ + x\<^sup>\ ; y ; w)\<^sup>\ \ (w ; x\<^sup>\ ; y)\<^sup>\ ; w ; x\<^sup>\ + (w ; x\<^sup>\ ; y)\<^sup>\" by (smt add_commutative less_eq_def mult_associative mult_left_dist_add while_def while_slide) have "(x\<^sup>\ + x\<^sup>\ ; y ; w)\<^sup>\ ; z = (x\<^sup>\ ; y ; w)\<^sup>\ ; x\<^sup>\ ; ((x\<^sup>\ ; y ; w)\<^sup>\ ; x\<^sup>\)\<^sup>\ ; (x\<^sup>\ ; y ; w)\<^sup>\ ; z + (x\<^sup>\ ; y ; w)\<^sup>\ ; z" by (smt add_commutative mult_associative star.circ_add star.circ_loop_fixpoint) also have "... \ (x\<^sup>\ ; y ; w)\<^sup>\ ; x\<^sup>\ + (x\<^sup>\ ; y ; w)\<^sup>\ ; z" by (smt add_commutative add_right_isotone mult_associative mult_right_isotone omega_sub_vector) finally have "w ; (x\<^sup>\ + x\<^sup>\ ; y ; w)\<^sup>\ ; z \ (w ; x\<^sup>\ ; y)\<^sup>\ ; w ; x\<^sup>\ + (w ; x\<^sup>\ ; y)\<^sup>\ ; w ; z" by (metis mult_associative mult_left_dist_add mult_right_isotone star.circ_slide) hence "w ; (x\<^sup>\ + x\<^sup>\ ; y ; w)\<^sup>\ + w ; (x\<^sup>\ + x\<^sup>\ ; y ; w)\<^sup>\ ; z \ (w ; x\<^sup>\ ; y)\<^sup>\ ; (w ; x\<^sup>\)\<^sup>\ + (w ; x\<^sup>\ ; y)\<^sup>\ + (w ; x\<^sup>\ ; y)\<^sup>\ ; w ; z" using 1 by (smt add_associative add_commutative less_eq_def mult_associative tarski_mult_omega_omega) also have "... \ (w ; x\<^sup>\ + w ; x\<^sup>\ ; y)\<^sup>\ ; (w ; x\<^sup>\ + w ; x\<^sup>\ ; y)\<^sup>\ + (w ; x\<^sup>\ + w ; x\<^sup>\ ; y)\<^sup>\ + (w ; x\<^sup>\ + w ; x\<^sup>\ ; y)\<^sup>\ ; w ; z" by (metis add_isotone add_left_upper_bound add_right_upper_bound mult_isotone mult_left_isotone omega_isotone star.circ_isotone) also have "... = (w ; x\<^sup>\ + w ; x\<^sup>\ ; y)\<^sup>\ + (w ; x\<^sup>\ + w ; x\<^sup>\ ; y)\<^sup>\ ; w ; z" by (metis add_idempotent star_mult_omega) finally have "w ; ((x\<^sup>\ + x\<^sup>\ ; y ; w)\<^sup>\ + (x\<^sup>\ + x\<^sup>\ ; y ; w)\<^sup>\ ; z) \ w ; ((x\<^sup>\ + x\<^sup>\ ; y) ; w)\<^sup>\ + w ; ((x\<^sup>\ + x\<^sup>\ ; y) ; w)\<^sup>\ ; z" by (smt mult_associative mult_left_dist_add omega_slide star.circ_slide) hence 2: "w ; ((x \ (y ; w)) \ z) \ w ; (((x \ y) ; w) \ z)" by (smt mult_associative mult_left_dist_add while_def while_slide) have "w ; (((x \ y) ; w) \ z) \ w ; ((x \ (y ; w)) \ z)" by (metis mult_right_isotone while_left_isotone while_sub_associative) thus ?thesis using 2 by (metis antisym) qed lemma while_denest_3: "(x \ w) \ x\<^sup>\ = (x \ w)\<^sup>\" proof - have 1: "(x \ w) \ x\<^sup>\ = (x \ w)\<^sup>\ + (x \ w)\<^sup>\ ; x\<^sup>\\<^sup>\" by (metis tarski_omega_idempotent while_def) also have "... \ (x \ w)\<^sup>\ + (x \ w)\<^sup>\ ; (x\<^sup>\ + x\<^sup>\ ; w)\<^sup>\" by (metis add_left_upper_bound add_right_isotone mult_right_isotone omega_isotone) also have "... = (x \ w)\<^sup>\" by (metis add_idempotent star_mult_omega while_def) finally show ?thesis using 1 by (metis add_left_upper_bound antisym_conv) qed lemma while_denest_4a: "(x \ w) \ (x \ (y ; z)) = (x \ w) \ ((x \ y) ; z)" proof - have "(x \ w) \ (x \ (y ; z)) = (x \ w)\<^sup>\ + ((x \ w) \ (x\<^sup>\ ; y ; z))" by (smt mult_associative while_denest_3 while_def while_left_dist_add) also have "... \ (x \ w)\<^sup>\ + ((x \ w) \ ((x \ y) ; z))" by (metis add_right_isotone mult_left_isotone star_below_while while_right_isotone) finally have 1: "(x \ w) \ (x \ (y ; z)) \ (x \ w) \ ((x \ y) ; z)" by (smt add_left_upper_bound less_eq_def while_def) have "(x \ w) \ ((x \ y) ; z) \ (x \ w) \ (x \ (y ; z))" by (metis while_right_isotone while_sub_associative) thus ?thesis using 1 by (metis antisym) qed subclass binary_itering_1_T apply unfold_locales by (smt mult_associative while_denest_2a while_denest_4a while_increasing while_slide) lemma while_mult_top: "(x ; T) \ z = z + x ; T" proof - have 1: "z + x ; T \ (x ; T) \ z" by (metis add_least_upper_bound while_denest_1 while_increasing while_one_top) have "(x ; T) \ z = z + x ; T ; ((x ; T) \ z)" by (metis while_left_unfold) also have "... \ z + x ; T" by (metis add_right_isotone mult_associative mult_right_isotone top_greatest) finally show ?thesis using 1 by (metis antisym) qed lemma tarski_top_omega_below_2: "x ; T \ (x ; T) \ 0" by (metis add_right_divisibility while_mult_top) lemma tarski_top_omega_2: "x ; T = (x ; T) \ 0" by (metis add_left_zero while_mult_top) lemma tarski_below_top_omega_2: "x \ (x ; T) \ 0" by (metis tarski_top_omega_2 top_right_mult_increasing) (* nitpick has counterexamples: lemma "1 = (x ; 0) \ 1" *) end class nonstrict_itering_tarski_zero = nonstrict_itering_tarski + nonstrict_itering_zero begin lemma "1 = (x ; 0) \ 1" by (metis mult_right_zero while_zero) (* nitpick has counterexamples: lemma tarski: "x = 0 \ T ; x ; T = T" lemma "(x + y) \ z = ((x \ 1) ; y) \ ((x \ 1) ; z)" lemma while_top_2: "T \ z = T ; z" lemma while_mult_top_2: "(x ; T) \ z = z + x ; T ; z" lemma while_one_mult: "(x \ 1) ; x = x \ x" lemma "(x \ 1) ; y = x \ y" lemma while_associative: "(x \ y) ; z = x \ (y ; z)" lemma while_back_loop_is_fixpoint: "is_fixpoint (\x . x ; y + z) (z ; (y \ 1))" lemma "1 + x ; 0 = x \ 1" lemma "x = x ; (x \ 1)" lemma "x ; (x \ 1) = x \ 1" lemma "x \ 1 = x \ (1 \ 1)" lemma "(x + y) \ 1 = (x \ (y \ 1)) \ 1" lemma "z + y ; x = x \ y \ z \ x" lemma "y ; x = x \ y \ x \ x" lemma "z + x ; y = x \ z ; (y \ 1) \ x" lemma "x ; y = x \ x ; (y \ 1) \ x" lemma "x ; z = z ; y \ x \ z \ z ; (y \ 1)" *) (* lemma tarski: "x = 0 \ T ; x ; T = T" nitpick lemma tarski_case: assumes t1: "x = 0 \ P x" and t2: "T ; x ; T = T \ P x" shows "P x" by (metis tarski t1 t2) lemma tarski_omega_1: "(x ; y\<^sup>\)\<^sup>\ = x ; y\<^sup>\" apply (rule tarski_case) apply (metis omega_zero) by (metis mult_associative omega_slide omega_vector star.circ_top star_omega_top) *) end context binary_itering_1_T begin (* move to BinaryItering.thy lemma "x ; ((y ; x) \ y) \ x ; ((y ; x) \ 1) ; y" nitpick *) end (* end *) end