(* Walter Guttmann, 2012.04.08 *) (* use with Isabelle2011 *) theory UCS imports Main begin (* theory Notation imports Main begin *) class mult = times begin notation times (infixl "\" 70) and times (infixl ";" 70) end class neg = uminus begin no_notation uminus ("- _" [81] 80) notation uminus ("- _" [80] 80) end (* end theory Fixpoint imports Main begin *) context order begin definition isotone :: "('a \ 'a) \ bool" where "isotone f \ (\x y . x \ y \ f(x) \ f(y))" definition is_fixpoint :: "('a \ 'a) \ 'a \ bool" where "is_fixpoint f x \ f(x) = x" definition is_prefixpoint :: "('a \ 'a) \ 'a \ bool" where "is_prefixpoint f x \ f(x) \ x" definition is_postfixpoint :: "('a \ 'a) \ 'a \ bool" where "is_postfixpoint f x \ f(x) \ x" definition is_least_fixpoint :: "('a \ 'a) \ 'a \ bool" where "is_least_fixpoint f x \ f(x) = x \ (\y . f(y) = y \ x \ y)" definition is_greatest_fixpoint :: "('a \ 'a) \ 'a \ bool" where "is_greatest_fixpoint f x \ f(x) = x \ (\y . f(y) = y \ x \ y)" definition is_least_prefixpoint :: "('a \ 'a) \ 'a \ bool" where "is_least_prefixpoint f x \ f(x) \ x \ (\y . f(y) \ y \ x \ y)" definition is_greatest_postfixpoint :: "('a \ 'a) \ 'a \ bool" where "is_greatest_postfixpoint f x \ f(x) \ x \ (\y . f(y) \ y \ x \ y)" definition has_fixpoint :: "('a \ 'a) \ bool" where "has_fixpoint f \ (\x . is_fixpoint f x)" definition has_prefixpoint :: "('a \ 'a) \ bool" where "has_prefixpoint f \ (\x . is_prefixpoint f x)" definition has_postfixpoint :: "('a \ 'a) \ bool" where "has_postfixpoint f \ (\x . is_postfixpoint f x)" definition has_least_fixpoint :: "('a \ 'a) \ bool" where "has_least_fixpoint f \ (\x . is_least_fixpoint f x)" definition has_greatest_fixpoint :: "('a \ 'a) \ bool" where "has_greatest_fixpoint f \ (\x . is_greatest_fixpoint f x)" definition has_least_prefixpoint :: "('a \ 'a) \ bool" where "has_least_prefixpoint f \ (\x . is_least_prefixpoint f x)" definition has_greatest_postfixpoint :: "('a \ 'a) \ bool" where "has_greatest_postfixpoint f \ (\x . is_greatest_postfixpoint f x)" definition the_least_fixpoint :: "('a \ 'a) \ 'a" ("\ _" [201] 200) where "\ f = (THE x . is_least_fixpoint f x)" definition the_greatest_fixpoint :: "('a \ 'a) \ 'a" ("\ _" [201] 200) where "\ f = (THE x . is_greatest_fixpoint f x)" definition the_least_prefixpoint :: "('a \ 'a) \ 'a" ("p\ _" [201] 200) where "p\ f = (THE x . is_least_prefixpoint f x)" definition the_greatest_postfixpoint :: "('a \ 'a) \ 'a" ("p\ _" [201] 200) where "p\ f = (THE x . is_greatest_postfixpoint f x)" lemma least_fixpoint_unique: "has_least_fixpoint f \ (\!x . is_least_fixpoint f x)" by (smt antisym has_least_fixpoint_def is_least_fixpoint_def) lemma greatest_fixpoint_unique: "has_greatest_fixpoint f \ (\!x . is_greatest_fixpoint f x)" by (smt antisym has_greatest_fixpoint_def is_greatest_fixpoint_def) lemma least_prefixpoint_unique: "has_least_prefixpoint f \ (\!x . is_least_prefixpoint f x)" by (smt antisym has_least_prefixpoint_def is_least_prefixpoint_def) lemma greatest_postfixpoint_unique: "has_greatest_postfixpoint f \ (\!x . is_greatest_postfixpoint f x)" by (smt antisym has_greatest_postfixpoint_def is_greatest_postfixpoint_def) lemma least_fixpoint: "has_least_fixpoint f \ is_least_fixpoint f (\ f)" proof assume "has_least_fixpoint f" hence "is_least_fixpoint f (THE x . is_least_fixpoint f x)" by (smt least_fixpoint_unique theI') thus "is_least_fixpoint f (\ f)" by (simp add: is_least_fixpoint_def the_least_fixpoint_def) qed lemma greatest_fixpoint: "has_greatest_fixpoint f \ is_greatest_fixpoint f (\ f)" proof assume "has_greatest_fixpoint f" hence "is_greatest_fixpoint f (THE x . is_greatest_fixpoint f x)" by (smt greatest_fixpoint_unique theI') thus "is_greatest_fixpoint f (\ f)" by (simp add: is_greatest_fixpoint_def the_greatest_fixpoint_def) qed lemma least_prefixpoint: "has_least_prefixpoint f \ is_least_prefixpoint f (p\ f)" proof assume "has_least_prefixpoint f" hence "is_least_prefixpoint f (THE x . is_least_prefixpoint f x)" by (smt least_prefixpoint_unique theI') thus "is_least_prefixpoint f (p\ f)" by (simp add: is_least_prefixpoint_def the_least_prefixpoint_def) qed lemma greatest_postfixpoint: "has_greatest_postfixpoint f \ is_greatest_postfixpoint f (p\ f)" proof assume "has_greatest_postfixpoint f" hence "is_greatest_postfixpoint f (THE x . is_greatest_postfixpoint f x)" by (smt greatest_postfixpoint_unique theI') thus "is_greatest_postfixpoint f (p\ f)" by (simp add: is_greatest_postfixpoint_def the_greatest_postfixpoint_def) qed lemma least_fixpoint_same: "is_least_fixpoint f x \ x = \ f" by (metis least_fixpoint least_fixpoint_unique has_least_fixpoint_def) lemma greatest_fixpoint_same: "is_greatest_fixpoint f x \ x = \ f" by (metis greatest_fixpoint greatest_fixpoint_unique has_greatest_fixpoint_def) lemma least_prefixpoint_same: "is_least_prefixpoint f x \ x = p\ f" by (metis least_prefixpoint least_prefixpoint_unique has_least_prefixpoint_def) lemma greatest_postfixpoint_same: "is_greatest_postfixpoint f x \ x = p\ f" by (metis greatest_postfixpoint greatest_postfixpoint_unique has_greatest_postfixpoint_def) lemma least_fixpoint_char: "is_least_fixpoint f x \ has_least_fixpoint f \ x = \ f" by (metis least_fixpoint_same has_least_fixpoint_def) lemma least_prefixpoint_char: "is_least_prefixpoint f x \ has_least_prefixpoint f \ x = p\ f" by (metis least_prefixpoint_same has_least_prefixpoint_def) lemma greatest_fixpoint_char: "is_greatest_fixpoint f x \ has_greatest_fixpoint f \ x = \ f" by (metis greatest_fixpoint_same has_greatest_fixpoint_def) lemma greatest_postfixpoint_char: "is_greatest_postfixpoint f x \ has_greatest_postfixpoint f \ x = p\ f" by (metis greatest_postfixpoint_same has_greatest_postfixpoint_def) lemma least_prefixpoint_fixpoint: "has_least_prefixpoint f \ isotone f \ is_least_fixpoint f (p\ f)" by (smt eq_iff is_least_fixpoint_def is_least_prefixpoint_def isotone_def least_prefixpoint) lemma pmu_mu: "has_least_prefixpoint f \ isotone f \ p\ f = \ f" by (smt has_least_fixpoint_def is_least_fixpoint_def least_fixpoint_unique least_prefixpoint_fixpoint least_fixpoint) definition lifted_less_eq :: "('a \ 'a) \ ('a \ 'a) \ bool" ("(_ \\ _)" [51, 51] 50) where "f \\ g \ (\x . f(x) \ g(x))" lemma lifted_reflexive: "f = g \ f \\ g" by (metis lifted_less_eq_def order_refl) lemma lifted_transitive: "f \\ g \ g \\ h \ f \\ h" by (smt lifted_less_eq_def order_trans) lemma lifted_antisymmetric: "f \\ g \ g \\ f \ f = g" by (metis antisym ext lifted_less_eq_def) lemma pmu_isotone: "has_least_prefixpoint f \ has_least_prefixpoint g \ f \\ g \ p\ f \ p\ g" by (smt is_least_prefixpoint_def least_prefixpoint lifted_less_eq_def order_trans) lemma mu_isotone: "has_least_prefixpoint f \ has_least_prefixpoint g \ isotone f \ isotone g \ f \\ g \ \ f \ \ g" by (metis pmu_isotone pmu_mu) lemma greatest_postfixpoint_fixpoint: "has_greatest_postfixpoint f \ isotone f \ is_greatest_fixpoint f (p\ f)" by (smt eq_iff is_greatest_fixpoint_def is_greatest_postfixpoint_def isotone_def greatest_postfixpoint) lemma pnu_nu: "has_greatest_postfixpoint f \ isotone f \ p\ f = \ f" by (smt has_greatest_fixpoint_def is_greatest_fixpoint_def greatest_fixpoint_unique greatest_postfixpoint_fixpoint greatest_fixpoint) lemma pnu_isotone: "has_greatest_postfixpoint f \ has_greatest_postfixpoint g \ f \\ g \ p\ f \ p\ g" by (smt is_greatest_postfixpoint_def lifted_less_eq_def order_trans greatest_postfixpoint) lemma nu_isotone: "has_greatest_postfixpoint f \ has_greatest_postfixpoint g \ isotone f \ isotone g \ f \\ g \ \ f \ \ g" by (metis pnu_isotone pnu_nu) lemma mu_square: "isotone f \ has_least_fixpoint f \ has_least_fixpoint (f \ f) \ \ f = \ (f \ f)" by (metis antisym is_least_fixpoint_def isotone_def least_fixpoint_char least_fixpoint_unique o_apply) lemma nu_square: "isotone f \ has_greatest_fixpoint f \ has_greatest_fixpoint (f \ f) \ \ f = \ (f \ f)" by (metis antisym is_greatest_fixpoint_def isotone_def greatest_fixpoint_char greatest_fixpoint_unique o_apply) lemma mu_roll: "isotone g \ has_least_fixpoint (f \ g) \ has_least_fixpoint (g \ f) \ \ (g \ f) = g(\ (f \ g))" apply (rule impI, rule antisym) apply (smt is_least_fixpoint_def least_fixpoint o_apply) by (smt is_least_fixpoint_def isotone_def least_fixpoint o_apply) lemma nu_roll: "isotone g \ has_greatest_fixpoint (f \ g) \ has_greatest_fixpoint (g \ f) \ \ (g \ f) = g(\ (f \ g))" apply (rule impI, rule antisym) apply (smt is_greatest_fixpoint_def greatest_fixpoint isotone_def o_apply) by (smt is_greatest_fixpoint_def greatest_fixpoint o_apply) lemma mu_below_nu: "has_least_fixpoint f \ has_greatest_fixpoint f \ \ f \ \ f" by (metis is_greatest_fixpoint_def is_least_fixpoint_def least_fixpoint greatest_fixpoint) lemma pmu_below_pnu_fix: "has_fixpoint f \ has_least_prefixpoint f \ has_greatest_postfixpoint f \ p\ f \ p\ f" by (smt has_fixpoint_def is_fixpoint_def is_greatest_postfixpoint_def is_least_prefixpoint_def le_less order_trans least_prefixpoint greatest_postfixpoint) lemma pmu_below_pnu_iso: "isotone f \ has_least_prefixpoint f \ has_greatest_postfixpoint f \ p\ f \ p\ f" by (metis has_fixpoint_def is_fixpoint_def is_least_fixpoint_def least_prefixpoint_fixpoint pmu_below_pnu_fix) definition galois :: "('a \ 'a) \ ('a \ 'a) \ bool" where "galois l u \ (\x y . l(x) \ y \ x \ u(y))" lemma galois_char: "galois l u \ (\x . x \ u(l(x))) \ (\x . l(u(x)) \ x) \ isotone l \ isotone u" apply (rule iffI) apply (smt galois_def isotone_def order_refl order_trans) by (metis galois_def isotone_def order_trans) lemma galois_closure: "galois l u \ l(x) = l(u(l(x))) \ u(x) = u(l(u(x)))" by (smt antisym galois_char isotone_def) lemma mu_fusion_1: "galois l u \ isotone h \ has_least_prefixpoint g \ has_least_fixpoint h \ l(g(u(\ h))) \ h(l(u(\ h))) \ l(p\ g) \ \ h" proof assume 1: "galois l u \ isotone h \ has_least_prefixpoint g \ has_least_fixpoint h \ l(g(u(\ h))) \ h(l(u(\ h)))" hence "l(u(\ h)) \ \ h" by (metis galois_char) hence "g(u(\ h)) \ u(\ h)" using 1 by (smt galois_def least_fixpoint_same least_fixpoint_unique is_least_fixpoint_def isotone_def order_trans) thus "l(p\ g) \ \ h" using 1 by (metis galois_def least_prefixpoint is_least_prefixpoint_def) qed lemma mu_fusion_2: "galois l u \ isotone h \ has_least_prefixpoint g \ has_least_fixpoint h \ l \ g \\ h \ l \ l(p\ g) \ \ h" by (metis lifted_less_eq_def mu_fusion_1 o_apply) lemma mu_fusion_equal_1: "galois l u \ isotone g \ isotone h \ has_least_prefixpoint g \ has_least_fixpoint h \ l(g(u(\ h))) \ h(l(u(\ h))) \ l(g(p\ g)) = h(l(p\ g)) \ \ h = l(p\ g) \ \ h = l(\ g)" by (metis antisym least_fixpoint least_prefixpoint_fixpoint is_least_fixpoint_def mu_fusion_1 pmu_mu) lemma mu_fusion_equal_2: "galois l u \ isotone h \ has_least_prefixpoint g \ has_least_prefixpoint h \ l(g(u(\ h))) \ h(l(u(\ h))) \ l(g(p\ g)) = h(l(p\ g)) \ p\ h = l(p\ g) \ \ h = l(p\ g)" by (smt antisym galois_char least_fixpoint_char least_prefixpoint least_prefixpoint_fixpoint is_least_prefixpoint_def isotone_def mu_fusion_1) lemma mu_fusion_equal_3: "galois l u \ isotone g \ isotone h \ has_least_prefixpoint g \ has_least_fixpoint h \ l \ g = h \ l \ \ h = l(p\ g) \ \ h = l(\ g)" by (smt mu_fusion_equal_1 o_apply order_refl) lemma mu_fusion_equal_4: "galois l u \ isotone h \ has_least_prefixpoint g \ has_least_prefixpoint h \ l \ g = h \ l \ p\ h = l(p\ g) \ \ h = l(p\ g)" by (smt mu_fusion_equal_2 o_apply order_refl) lemma nu_fusion_1: "galois l u \ isotone h \ has_greatest_postfixpoint g \ has_greatest_fixpoint h \ h(u(l(\ h))) \ u(g(l(\ h))) \ \ h \ u(p\ g)" proof assume 1: "galois l u \ isotone h \ has_greatest_postfixpoint g \ has_greatest_fixpoint h \ h(u(l(\ h))) \ u(g(l(\ h)))" hence "\ h \ u(l(\ h))" by (metis galois_char) hence "l(\ h) \ g(l(\ h))" using 1 by (smt galois_def greatest_fixpoint_same greatest_fixpoint_unique is_greatest_fixpoint_def isotone_def order_trans) thus "\ h \ u(p\ g)" using 1 by (metis galois_def greatest_postfixpoint is_greatest_postfixpoint_def) qed lemma nu_fusion_2: "galois l u \ isotone h \ has_greatest_postfixpoint g \ has_greatest_fixpoint h \ h \ u \\ u \ g \ \ h \ u(p\ g)" by (metis lifted_less_eq_def nu_fusion_1 o_apply) lemma nu_fusion_equal_1: "galois l u \ isotone g \ isotone h \ has_greatest_postfixpoint g \ has_greatest_fixpoint h \ h(u(l(\ h))) \ u(g(l(\ h))) \ h(u(p\ g)) = u(g(p\ g)) \ \ h = u(p\ g) \ \ h = u(\ g)" by (metis antisym greatest_fixpoint greatest_postfixpoint_fixpoint is_greatest_fixpoint_def nu_fusion_1 pnu_nu) lemma nu_fusion_equal_2: "galois l u \ isotone h \ has_greatest_postfixpoint g \ has_greatest_postfixpoint h \ h(u(l(\ h))) \ u(g(l(\ h))) \ h(u(p\ g)) = u(g(p\ g)) \ p\ h = u(p\ g) \ \ h = u(p\ g)" by (smt antisym galois_char greatest_fixpoint_char greatest_postfixpoint greatest_postfixpoint_fixpoint is_greatest_postfixpoint_def isotone_def nu_fusion_1) lemma nu_fusion_equal_3: "galois l u \ isotone g \ isotone h \ has_greatest_postfixpoint g \ has_greatest_fixpoint h \ h \ u = u \ g \ \ h = u(p\ g) \ \ h = u(\ g)" by (metis nu_fusion_equal_1 o_apply order_refl) lemma nu_fusion_equal_4: "galois l u \ isotone h \ has_greatest_postfixpoint g \ has_greatest_postfixpoint h \ h \ u = u \ g \ p\ h = u(p\ g) \ \ h = u(p\ g)" by (smt nu_fusion_equal_2 o_apply order_refl) lemma mu_exchange_1: "galois l u \ isotone g \ isotone h \ has_least_prefixpoint (l \ h) \ has_least_prefixpoint (h \ g) \ has_least_fixpoint (g \ h) \ l \ h \ g \\ g \ h \ l \ \(l \ h) \ \(g \ h)" by (smt galois_char is_least_prefixpoint_def isotone_def least_fixpoint_char least_prefixpoint least_prefixpoint_fixpoint mu_fusion_2 mu_roll o_apply o_assoc) lemma mu_exchange_2: "galois l u \ isotone g \ isotone h \ has_least_prefixpoint (l \ h) \ has_least_prefixpoint (h \ l) \ has_least_prefixpoint (h \ g) \ has_least_fixpoint (g \ h) \ has_least_fixpoint (h \ g) \ l \ h \ g \\ g \ h \ l \ \(h \ l) \ \(h \ g)" by (smt galois_char isotone_def least_fixpoint_char least_prefixpoint_fixpoint mu_exchange_1 mu_roll o_apply) lemma mu_exchange_equal: "galois l u \ galois k t \ isotone h \ has_least_prefixpoint (l \ h) \ has_least_prefixpoint (h \ l) \ has_least_prefixpoint (k \ h) \ has_least_prefixpoint (h \ k) \ l \ h \ k = k \ h \ l \ \(l \ h) = \(k \ h) \ \(h \ l) = \(h \ k)" by (smt antisym galois_char isotone_def least_fixpoint_char least_prefixpoint_fixpoint lifted_reflexive mu_exchange_1 mu_exchange_2 o_apply) lemma nu_exchange_1: "galois l u \ isotone g \ isotone h \ has_greatest_postfixpoint (u \ h) \ has_greatest_postfixpoint (h \ g) \ has_greatest_fixpoint (g \ h) \ g \ h \ u \\ u \ h \ g \ \(g \ h) \ \(u \ h)" by (smt galois_char is_greatest_postfixpoint_def isotone_def greatest_fixpoint_char greatest_postfixpoint greatest_postfixpoint_fixpoint nu_fusion_2 nu_roll o_apply o_assoc) lemma nu_exchange_2: "galois l u \ isotone g \ isotone h \ has_greatest_postfixpoint (u \ h) \ has_greatest_postfixpoint (h \ u) \ has_greatest_postfixpoint (h \ g) \ has_greatest_fixpoint (g \ h) \ has_greatest_fixpoint (h \ g) \ g \ h \ u \\ u \ h \ g \ \(h \ g) \ \(h \ u)" by (smt galois_char isotone_def greatest_fixpoint_char greatest_postfixpoint_fixpoint nu_exchange_1 nu_roll o_apply) lemma nu_exchange_equal: "galois l u \ galois k t \ isotone h \ has_greatest_postfixpoint (u \ h) \ has_greatest_postfixpoint (h \ u) \ has_greatest_postfixpoint (t \ h) \ has_greatest_postfixpoint (h \ t) \ u \ h \ t = t \ h \ u \ \(u \ h) = \(t \ h) \ \(h \ u) = \(h \ t)" by (smt antisym galois_char isotone_def greatest_fixpoint_char greatest_postfixpoint_fixpoint lifted_reflexive nu_exchange_1 nu_exchange_2 o_apply) lemma mu_commute_fixpoint_1: "isotone f \ has_least_fixpoint (f \ g) \ f \ g = g \ f \ is_fixpoint f (\(f \ g))" by (metis is_fixpoint_def mu_roll) lemma mu_commute_fixpoint_2: "isotone g \ has_least_fixpoint (f \ g) \ f \ g = g \ f \ is_fixpoint g (\(f \ g))" by (metis is_fixpoint_def mu_roll) lemma mu_commute_least_fixpoint: "isotone f \ isotone g \ has_least_fixpoint f \ has_least_fixpoint g \ has_least_fixpoint (f \ g) \ f \ g = g \ f \ (\(f \ g) = \ f \ \ g \ \ f)" by (metis is_least_fixpoint_def least_fixpoint_same least_fixpoint_unique mu_roll) (* converse claimed by [Davey & Priestley 2002, page 200, exercise 8.27(iii)] for continuous f, g on a CPO ; does it hold without additional assumptions? lemma mu_commute_least_fixpoint_converse: "isotone f \ isotone g \ has_least_prefixpoint f \ has_least_prefixpoint g \ has_least_prefixpoint (f \ g) \ f \ g = g \ f \ (\ g \ \ f \ \(f \ g) = \ f)" *) lemma nu_commute_fixpoint_1: "isotone f \ has_greatest_fixpoint (f \ g) \ f \ g = g \ f \ is_fixpoint f (\(f \ g))" by (metis is_fixpoint_def nu_roll) lemma nu_commute_fixpoint_2: "isotone g \ has_greatest_fixpoint (f \ g) \ f \ g = g \ f \ is_fixpoint g (\(f \ g))" by (metis is_fixpoint_def nu_roll) lemma nu_commute_greatest_fixpoint: "isotone f \ isotone g \ has_greatest_fixpoint f \ has_greatest_fixpoint g \ has_greatest_fixpoint (f \ g) \ f \ g = g \ f \ (\(f \ g) = \ f \ \ f \ \ g)" by (smt is_greatest_fixpoint_def greatest_fixpoint_same greatest_fixpoint_unique nu_roll) lemma mu_diagonal_1: "isotone (\x . f x x) \ (\x . isotone (\y . f x y)) \ isotone (\x . \(\y . f x y)) \ (\x . has_least_fixpoint (\y . f x y)) \ has_least_prefixpoint (\x . \(\y . f x y)) \ \(\x . f x x) = \(\x . \(\y . f x y))" by (smt is_least_fixpoint_def is_least_prefixpoint_def least_fixpoint_same least_fixpoint_unique least_prefixpoint least_prefixpoint_fixpoint) lemma mu_diagonal_2: "(\x . isotone (\y . f x y) \ isotone (\y . f y x) \ has_least_prefixpoint (\y . f x y)) \ has_least_prefixpoint (\x . \(\y . f x y)) \ \(\x . f x x) = \(\x . \(\y . f x y))" by (smt is_least_fixpoint_def is_least_prefixpoint_def isotone_def least_fixpoint_same least_prefixpoint least_prefixpoint_fixpoint) lemma nu_diagonal_1: "isotone (\x . f x x) \ (\x . isotone (\y . f x y)) \ isotone (\x . \(\y . f x y)) \ (\x . has_greatest_fixpoint (\y . f x y)) \ has_greatest_postfixpoint (\x . \(\y . f x y)) \ \(\x . f x x) = \(\x . \(\y . f x y))" by (smt is_greatest_fixpoint_def is_greatest_postfixpoint_def greatest_fixpoint_same greatest_fixpoint_unique greatest_postfixpoint greatest_postfixpoint_fixpoint) lemma nu_diagonal_2: "(\x . isotone (\y . f x y) \ isotone (\y . f y x) \ has_greatest_postfixpoint (\y . f x y)) \ has_greatest_postfixpoint (\x . \(\y . f x y)) \ \(\x . f x x) = \(\x . \(\y . f x y))" using [[ smt_timeout = 120 ]] by (smt is_greatest_fixpoint_def is_greatest_postfixpoint_def isotone_def greatest_fixpoint_same greatest_postfixpoint greatest_postfixpoint_fixpoint) end (* end theory Tests imports Notation begin *) class tests = mult + neg + one + ord + plus + zero + assumes sub_assoc: "-x ; (-y ; -z) = (-x ; -y) ; -z" assumes sub_comm: "-x ; -y = -y ; -x" assumes sub_compl: "-x = -(--x ; -y) ; -(--x ; --y)" assumes sub_mult_closed: "-x ; -y = --(-x ; -y)" assumes the_zero_def: "0 = (THE x . (\y . x = -y ; --y))" -- {* define without imposing uniqueness *} assumes one_def: "1 = - 0" assumes plus_def: "-x + -y = -(--x ; --y)" assumes leq_def: "-x \ -y \ -x ; -y = -x" assumes strict_leq_def: "-x < -y \ -x \ -y \ \ (-y \ -x)" begin -- {* uniqueness of 0, resulting in the lemma @{text zero_def} to replace the assumption @{text the_zero_def} *} lemma unique_zero: "-x ; --x = -y ; --y" by (metis sub_assoc sub_comm sub_compl) definition is_zero :: "'a \ bool" where is_zero_def: "is_zero(x) \ (\y . x = -y ; --y)" (* This is an auxiliary predicate for the following lemma. *) lemma the_zero_def_p: "0 = (THE x . is_zero(x))" by (simp only: the_zero_def is_zero_def) (* This auxiliary lemma replaces the assumption the_zero_def in the proof of the following lemma. *) lemma zero_def: "0 = -x ; --x" by (metis unique_zero the_zero_def_p is_zero_def theI') (* Metis does not terminate if the original assumption the_zero_def is used. *) -- {* consequences for meet and complement *} lemma double_negation: "-x = ---x" by (metis sub_mult_closed sub_compl) lemma compl_1: "--x = -(-x ; -y) ; -(-x ; --y)" by (metis double_negation sub_compl) lemma right_zero: "-x ; (-y ; --y) = -z ; --z" by (metis compl_1 sub_assoc sub_mult_closed zero_def) lemma right_one: "-x ; -x = -x ; -(-y ; --y)" by (metis compl_1 right_zero sub_mult_closed zero_def) lemma mult_idempotent: "-x ; -x = -x" by (metis compl_1 double_negation sub_assoc sub_mult_closed zero_def) lemma compl_2: "-x = -(-(-x ; -y) ; -(-x ; --y))" by (metis compl_1 double_negation) -- {* consequences for join *} lemma plus_idempotent: "-x + -x = -x" by (metis double_negation mult_idempotent plus_def) lemma plus_comm: "-x + -y = -y + -x" by (metis plus_def sub_comm) lemma plus_assoc: "-x + (-y + -z) = (-x + -y) + -z" by (metis plus_def sub_assoc sub_mult_closed) lemma plus_absorb: "-x ; -y + -x = -x" by (smt compl_1 mult_idempotent plus_def sub_assoc sub_mult_closed) lemma mult_cases: "-x = (-x + -y) ; (-x + --y)" by (metis compl_1 double_negation plus_def) lemma mult_deMorgan: "-(-x ; -y) = --x + --y" by (metis double_negation plus_def) lemma plus_deMorgan: "-(-x + -y) = --x ; --y" by (metis plus_def sub_mult_closed) lemma plus_cases: "-x = -x ; -y + -x ; --y" by (smt mult_deMorgan double_negation mult_cases sub_mult_closed) lemma plus_compl_intro: "(-x ; -y) + --x = -y + --x" by (smt compl_1 mult_deMorgan plus_absorb plus_cases sub_assoc sub_comm sub_mult_closed) lemma mult_absorb: "-x ; (-x + -y) = -x" by (smt plus_absorb plus_def sub_mult_closed sub_comm) lemma plus_closed: "-x + -y = --(-x + -y)" by (metis plus_def double_negation) lemma plus_distr_mult: "-x + (-y ; -z) = (-x + -y) ; (-x + -z)" by (smt mult_cases sub_mult_closed plus_closed plus_assoc plus_absorb plus_compl_intro mult_absorb sub_assoc plus_comm) lemma mult_distr_plus: "-x ; (-y + -z) = (-x ; -y) + (-x ; -z)" by (smt plus_def double_negation plus_deMorgan plus_distr_mult mult_deMorgan sub_mult_closed) lemma mult_compl_intro: "-x ; -y = -x ; (--x + -y)" by (metis sub_mult_closed mult_cases plus_absorb plus_compl_intro plus_comm) lemma case_duality: "(--x + -y) ; (-x + -z) = -x ; -y + --x ; -z" proof - have "(--x + -y) ; (-x + -z) = --(-y ; -z ; -x) + --(-y ; -x) + (--(-y ; -z ; --x) + --(--x ; -z))" by (smt mult_distr_plus plus_closed mult_compl_intro sub_comm plus_assoc plus_cases sub_mult_closed plus_comm) thus ?thesis by (smt sub_comm sub_assoc sub_mult_closed plus_absorb) qed lemma case_duality_2: "(-x + -y) ; (--x + -z) = -x ; -z + --x ; -y" by (metis case_duality double_negation plus_comm sub_mult_closed) lemma compl_cases: "(-v + -w) ; (--v + -x) + -((-v + -y) ; (--v + -z)) = (-v + -w + --y) ; (--v + -x + --z)" by (smt mult_deMorgan plus_deMorgan sub_mult_closed plus_closed double_negation case_duality sub_comm plus_assoc plus_comm mult_distr_plus case_duality_2) lemma plus_cases_2: "--x = -(-x + -y) + -(-x + --y)" by (metis mult_deMorgan plus_deMorgan double_negation mult_cases sub_mult_closed plus_closed) -- {* consequences for 0 and 1 *} lemma mult_compl: "-x ; --x = 0" by (metis zero_def) lemma plus_compl: "-x + --x = 1" by (metis one_def plus_def zero_def) lemma one_compl: "- 1 = 0" by (metis mult_compl one_def sub_mult_closed) lemma bs_mult_right_zero: "-x ; 0 = 0" by (metis right_zero zero_def) lemma bs_mult_left_zero: "0 ; -x = 0" by (metis bs_mult_right_zero one_compl sub_comm) lemma plus_right_one: "-x + 1 = 1" by (metis one_compl one_def mult_deMorgan double_negation bs_mult_right_zero) lemma plus_left_one: "1 + -x = 1" by (metis plus_right_one one_def plus_comm) lemma bs_mult_right_one: "-x ; 1 = -x" by (metis mult_compl one_def mult_idempotent right_one) lemma bs_mult_left_one: "1 ; -x = -x" by (metis one_def bs_mult_right_one sub_comm) lemma plus_right_zero: "-x + 0 = -x" by (metis mult_compl mult_cases plus_distr_mult) lemma plus_left_zero: "0 + -x = -x" by (metis plus_right_zero one_compl plus_comm) lemma one_double_compl: "-- 1 = 1" by (metis one_compl one_def) lemma zero_double_compl: "-- 0 = 0" by (metis one_compl one_def) -- {* consequences for the order *} lemma reflexive: "-x \ -x" by (metis leq_def mult_idempotent) lemma transitive: "-x \ -y \ -y \ -z \ -x \ -z" by (metis leq_def sub_assoc) lemma antisymmetric: "-x \ -y \ -y \ -x \ -x = -y" by (metis leq_def sub_comm) lemma zero_least_test: "0 \ -x" by (metis one_compl leq_def bs_mult_right_zero sub_comm) lemma one_greatest: "-x \ 1" by (metis leq_def one_def bs_mult_right_one) lemma lower_bound_left: "-x ; -y \ -x" by (metis leq_def mult_idempotent sub_assoc sub_mult_closed sub_comm) lemma lower_bound_right: "-x ; -y \ -y" by (metis leq_def mult_idempotent sub_assoc sub_mult_closed) lemma mult_iso_left: "-x \ -y \ -x ; -z \ -y ; -z" by (metis leq_def lower_bound_left sub_assoc sub_comm sub_mult_closed) lemma mult_iso_right: "-x \ -y \ -z ; -x \ -z ; -y" by (metis mult_iso_left sub_comm) lemma compl_anti: "-x \ -y \ --y \ --x" by (metis one_compl plus_compl plus_deMorgan double_negation leq_def plus_comm plus_compl_intro plus_right_zero) lemma leq_plus: "-x \ -y \ -x + -y = -y" by (metis double_negation leq_def mult_absorb plus_def sub_comm) lemma plus_compl_iso: "-x \ -y \ -(-y + -z) \ -(-x + -z)" by (metis plus_deMorgan leq_plus lower_bound_left mult_iso_left) lemma plus_iso_left: "-x \ -y \ -x + -z \ -y + -z" by (metis plus_compl_iso compl_anti double_negation plus_def) lemma plus_iso_right: "-x \ -y \ -z + -x \ -z + -y" by (metis plus_iso_left plus_comm) lemma greatest_lower_bound: "-x \ -y \ -x \ -z \ -x \ -y ; -z" by (metis leq_def plus_absorb plus_comm sub_assoc sub_mult_closed) lemma upper_bound_left: "-x \ -x + -y" by (metis one_compl plus_iso_right plus_right_zero zero_least_test) lemma upper_bound_right: "-y \ -x + -y" by (metis upper_bound_left plus_comm) lemma least_upper_bound: "-x \ -z \ -y \ -z \ -x + -y \ -z" by (metis leq_plus plus_assoc plus_def upper_bound_right) lemma leq_mult_zero: "-x \ -y \ -x ; --y = 0" proof - have "-x \ -y \ -x ; --y = 0" by (metis leq_def sub_assoc mult_compl bs_mult_right_zero) also have "-x ; --y = 0 \ -x \ -y" by (metis compl_1 one_def leq_def bs_mult_right_one sub_mult_closed) ultimately show ?thesis by metis qed lemma leq_plus_right_one: "-x \ -y \ --x + -y = 1" by (metis one_compl one_def mult_deMorgan plus_deMorgan double_negation leq_mult_zero) lemma shunting: "-x ; -y \ -z \ -y \ --x + -z" by (smt leq_mult_zero sub_assoc sub_mult_closed sub_comm plus_deMorgan double_negation mult_deMorgan) lemma shunting_right: "-x ; -y \ -z \ -x \ -z + --y" by (metis plus_comm shunting sub_comm) lemma leq_cases: "-x ; -y \ -z \ --x ; -y \ -z \ -y \ -z" by (smt least_upper_bound sub_mult_closed mult_distr_plus sub_comm plus_compl bs_mult_right_one) lemma leq_cases_2: "-x ; -y \ -x ; -z \ --x ; -y \ --x ; -z \ -y \ -z" by (metis greatest_lower_bound leq_cases sub_mult_closed) lemma leq_cases_3: "-y ; -x \ -z ; -x \ -y ; --x \ -z ; --x \ -y \ -z" by (metis leq_cases_2 sub_comm) lemma eq_cases: "-x ; -y = -x ; -z \ --x ; -y = --x ; -z \ -y = -z" by (metis plus_cases sub_comm) lemma eq_cases_2: "-y ; -x = -z ; -x \ -y ; --x = -z ; --x \ -y = -z" by (metis eq_cases sub_comm) lemma mult_distr_plus_right: "(-y + -z) ; -x = (-y ; -x) + (-z ; -x)" by (metis mult_distr_plus plus_def sub_comm) lemma wnf_lemma_1: "(-x ; -y + --x ; -z) ; -x = -x ; -y" by (smt mult_compl mult_distr_plus_right mult_idempotent plus_right_zero sub_assoc sub_comm sub_mult_closed) lemma wnf_lemma_2: "(-x ; -y + -z ; --y) ; -y = -x ; -y" by (metis sub_comm wnf_lemma_1) lemma wnf_lemma_3: "(-x ; -z + --x ; -y) ; --x = --x ; -y" by (smt mult_compl mult_distr_plus_right mult_idempotent plus_comm plus_right_zero sub_assoc sub_comm sub_mult_closed) lemma wnf_lemma_4: "(-z ; -y + -x ; --y) ; --y = -x ; --y" by (metis sub_comm wnf_lemma_3) end (* end theory Semiring imports Notation begin *) class semiring = mult + one + ord + plus + zero + assumes add_associative : "(x + y) + z = x + (y + z)" assumes add_commutative : "x + y = y + x" assumes add_idempotent : "x + x = x" assumes add_left_zero : "0 + x = x" assumes mult_associative : "(x ; y) ; z = x ; (y ; z)" assumes mult_left_one : "1 ; x = x" assumes mult_right_one : "x ; 1 = x" assumes mult_left_dist_add : "x ; (y + z) = x ; y + x ; z" assumes mult_right_dist_add: "(x + y) ; z = x ; z + y ; z" assumes mult_left_zero : "0 ; x = 0" assumes less_eq_def : "x \ y \ x + y = y" assumes less_def : "x < y \ x \ y \ \ (y \ x)" begin subclass order by unfold_locales (metis less_def, metis add_idempotent less_eq_def, metis add_associative less_eq_def, metis add_commutative less_eq_def) lemma add_left_isotone: "x \ y \ x + z \ y + z" by (smt add_associative add_commutative add_idempotent less_eq_def) lemma add_right_isotone: "x \ y \ z + x \ z + y" by (metis add_commutative add_left_isotone) lemma add_isotone: "w \ y \ x \ z \ w + x \ y + z" by (smt add_associative add_commutative less_eq_def) lemma add_left_upper_bound: "x \ x + y" by (metis add_associative add_idempotent less_eq_def) lemma add_right_upper_bound: "y \ x + y" by (metis add_commutative add_left_upper_bound) lemma add_least_upper_bound: "x \ z \ y \ z \ x + y \ z" by (smt add_associative add_commutative add_left_upper_bound less_eq_def) lemma add_left_divisibility: "x \ y \ (\z . x + z = y)" by (metis add_left_upper_bound less_eq_def) lemma add_right_divisibility: "x \ y \ (\z . z + x = y)" by (metis add_commutative add_left_divisibility) lemma add_right_zero: "x + 0 = x" by (metis add_commutative add_left_zero) lemma zero_least: "0 \ x" by (metis add_left_upper_bound add_left_zero) lemma mult_left_isotone: "x \ y \ x ; z \ y ; z" by (metis less_eq_def mult_right_dist_add) lemma mult_right_isotone: "x \ y \ z ; x \ z ; y" by (metis less_eq_def mult_left_dist_add) lemma mult_isotone: "w \ y \ x \ z \ w ; x \ y ; z" by (smt mult_left_isotone mult_right_isotone order_trans) lemma mult_left_subdist_add_left: "x ; y \ x ; (y + z)" by (metis add_left_upper_bound mult_left_dist_add) lemma mult_left_subdist_add_right: "x ; z \ x ; (y + z)" by (metis add_right_upper_bound mult_left_dist_add) lemma mult_right_subdist_add_left: "x ; z \ (x + y) ; z" by (metis add_left_upper_bound mult_right_dist_add) lemma mult_right_subdist_add_right: "y ; z \ (x + y) ; z" by (metis add_right_upper_bound mult_right_dist_add) lemma case_split_left: "1 \ w + z \ w ; x \ y \ z ; x \ y \ x \ y" by (smt add_least_upper_bound mult_left_isotone mult_left_one mult_right_dist_add order_trans) lemma case_split_left_equal: "w + z = 1 \ w ; x = w ; y \ z ; x = z ; y \ x = y" by (metis mult_left_one mult_right_dist_add) lemma case_split_right: "1 \ w + z \ x ; w \ y \ x ; z \ y \ x \ y" by (smt add_least_upper_bound mult_right_isotone mult_right_one mult_left_dist_add order_trans) lemma case_split_right_equal: "w + z = 1 \ x ; w = y ; w \ x ; z = y ; z \ x = y" by (metis mult_left_dist_add mult_right_one) lemma zero_right_mult_decreasing: "x ; 0 \ x" by (metis add_right_zero mult_left_subdist_add_right mult_right_one) lemma add_same_context:"x \ y + z \ y \ x + z \ x + z = y + z" by (smt add_associative add_commutative less_eq_def) end class semiring_T = semiring + fixes T :: "'a" ("\") assumes add_left_top: "T + x = T" begin lemma add_right_top: "x + T = T" by (metis add_commutative add_left_top) lemma top_greatest: "x \ T" by (metis add_left_top add_right_upper_bound) lemma top_left_mult_increasing: "x \ T ; x" by (metis mult_left_isotone mult_left_one top_greatest) lemma top_right_mult_increasing: "x \ x ; T" by (metis mult_right_isotone mult_right_one top_greatest) lemma top_mult_top: "T ; T = T" by (metis add_right_divisibility add_right_top top_right_mult_increasing) definition vector :: "'a \ bool" where "vector x \ x = x ; T" lemma vector_zero: "vector 0" by (metis mult_left_zero vector_def) lemma vector_top: "vector T" by (metis top_mult_top vector_def) lemma vector_add_closed: "vector x \ vector y \ vector (x + y)" by (metis mult_right_dist_add vector_def) lemma vector_left_mult_closed: "vector y \ vector (x ; y)" by (metis mult_associative vector_def) end (* end theory 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 RelativeDomain imports Semiring Tests begin *) declare [[ smt_timeout = 60 ]] class dom = fixes d :: "'a \ 'a" fixes Z :: "'a" class relative_domain_semiring = semiring + dom + assumes d_restrict : "x \ d(x) ; x + Z" assumes d_mult_d : "d(x ; y) = d(x ; d(y))" assumes d_below_one: "d(x) \ 1" assumes d_Z : "d(Z) = 0" assumes d_dist_add : "d(x + y) = d(x) + d(y)" assumes d_export : "d(d(x) ; y) = d(x) ; d(y)" begin lemma d_plus_one: "d(x) + 1 = 1" by (metis d_below_one less_eq_def) lemma d_zero: "d(0) = 0" by (metis d_Z d_export mult_left_zero) 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_dist_add mult_right_one) lemma d_sub_one: "x \ 1 \ x \ d(x) + Z" by (metis add_left_isotone d_restrict mult_right_isotone mult_right_one order_trans) lemma d_one: "d(1) + Z = 1 + Z" by (smt add_associative add_commutative d_plus_one d_restrict less_eq_def mult_right_one) lemma d_strict: "d(x) = 0 \ x \ Z" by (metis add_commutative add_right_zero d_Z d_dist_add d_restrict less_eq_def mult_left_zero) 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_idempotent: "d(x) ; d(x) = d(x)" by (metis add_commutative add_right_zero d_Z d_dist_add d_export d_involutive d_mult_sub d_restrict less_eq_def) lemma d_least_left_preserver: "x \ d(y) ; x + Z \ d(x) \ d(y)" by (rule iffI, metis add_associative add_left_divisibility add_right_zero d_Z d_dist_add d_involutive d_mult_sub less_eq_def, smt add_associative add_commutative d_restrict less_eq_def mult_right_dist_add) lemma d_weak_locality: "x ; y \ Z \ x ; d(y) \ Z" 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_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_commutative: "d(x) ; d(y) = d(y) ; d(x)" by (metis add_commutative antisym d_add_left_absorb_mult d_below_one d_export d_mult_left_absorb_add mult_associative mult_left_isotone mult_left_one) 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_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 Z_mult_decreasing: "Z ; x \ Z" by (metis add_left_zero d_Z d_least_left_preserver d_mult_sub mult_left_zero) lemma d_below_d_one: "d(x) \ d(1)" by (metis d_mult_sub mult_left_one) lemma d_relative_Z: "d(x) ; x + Z = x + Z" by (metis add_left_upper_bound add_same_context d_below_one d_restrict mult_isotone mult_left_one) lemma Z_left_zero_above_one: "1 \ x \ Z ; x = Z" by (metis Z_mult_decreasing eq_iff mult_right_isotone mult_right_one) end class relative_domain_semiring_T = relative_domain_semiring + semiring_T begin lemma Z_top: "Z ; T = Z" by (metis Z_mult_decreasing eq_iff top_right_mult_increasing) end class relative_antidomain_semiring = semiring + dom + neg + assumes a_restrict : "-x ; x \ Z" assumes a_mult_d : "-(x ; y) = -(x ; --y)" assumes a_complement: "-x ; --x = 0" assumes a_Z : "-Z = 1" assumes a_export : "-(--x ; y) = -x + -y" assumes a_dist_add : "-(x + y) = -x ; -y" assumes d_def : "d(x) = --x" begin notation uminus ("a") lemma a_complement_one: "--x + -x = 1" by (metis a_Z a_complement a_export a_mult_d mult_left_one) lemma a_greatest_left_absorber: "a(x) ; y \ Z \ a(x) \ a(y)" by (rule iffI, metis a_Z a_complement_one a_dist_add a_mult_d add_right_divisibility less_eq_def mult_left_dist_add mult_left_one mult_right_one mult_right_subdist_add_left, metis a_restrict le_less_trans le_neq_trans less_eq_def less_imp_le mult_right_subdist_add_left) 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 a_restrict add_commutative mult_left_subdist_add_right order_trans) lemma a_below_one: "a(x) \ 1" by (metis a_complement_one add_right_divisibility) lemma a_export_a: "a(a(x) ; y) = d(x) + a(y)" by (metis a_d_closed a_export d_def) subclass relative_domain_semiring apply unfold_locales apply (smt a_Z a_complement_one a_restrict add_commutative add_left_upper_bound case_split_left d_def order_trans) apply (metis a_mult_d d_def) apply (metis a_below_one d_def) apply (metis a_Z a_complement d_def mult_left_one) apply (metis a_dist_add a_export_a 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_one 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_complement) apply (metis a_complement) apply (metis a_Z a_d_closed d_Z d_def) 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_plus_mult_d: "-(x ; y) + -(x ; --y) = -(x ; --y)" by (metis a_mult_d add_idempotent) lemma a_mult_d_2: "a(x ; y) = a(x ; d(y))" by (metis a_mult_d d_def) lemma a_idempotent: "a(x) ; a(x) = a(x)" by (metis a_dist_add add_idempotent) lemma a_3: "a(x) ; a(y) ; d(x + y) = 0" by (metis a_complement a_dist_add d_def) lemma a_fixpoint: "\x . (a(x) = x \ (\y . y = 0))" by (metis a_idempotent mult_left_one mult_left_zero one_def zero_def) lemma a_strict: "a(x) = 1 \ x \ Z" by (metis d_def d_strict double_negation one_compl one_def) lemma d_complement_zero: "d(x) ; a(x) = 0" by (metis d_def sub_comm zero_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 d_def leq_mult_zero) 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_antitone d_def d_mult_sub double_negation) 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_export d_def) 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 d_def double_negation leq_mult_zero) 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 (metis d_complement_zero eq_iff mult_associative mult_left_zero mult_right_isotone zero_least) 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_Z a_below_one a_complement_one case_split_left d_def mult_associative mult_right_isotone mult_right_one zero_least) 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 (metis a_complement_one add_left_zero d_def mult_associative mult_left_one mult_left_zero mult_right_dist_add unique_zero zero_double_compl) 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 kat_equiv_5: "d(x) ; y \ y ; d(z) \ d(x) ; y ; a(z) = d(x) ; y ; 0" by (rule, metis d_complement_zero kat_4_equiv mult_associative, smt a_complement_one case_split_right d_def mult_isotone mult_left_one mult_right_subdist_add_left order_refl zero_least) lemma kat_equiv_6: "d(x) ; y ; a(z) = d(x) ; y ; 0 \ d(x) ; y ; a(z) \ y ; 0" by (metis a_d_closed antisym d_idempotent kat_4 mult_associative mult_right_isotone mult_right_one one_def zero_least_test) lemma d_restrict_iff: "(x \ y + Z) \ (x \ d(x) ; y + Z)" proof - have "x \ y + Z \ x \ d(x) ; (y + Z) + Z" by (smt add_left_isotone d_restrict less_eq_def mult_left_subdist_add_left order_trans) hence "x \ y + Z \ x \ d(x) ; y + Z" by (metis add_associative d_plus_one mult_left_dist_add mult_left_one mult_right_dist_add) thus ?thesis by (metis a_complement_one add_commutative add_right_isotone d_def mult_left_one mult_right_subdist_add_left order_trans) qed lemma d_restrict_iff_1: "(d(x) ; y \ z) \ (d(x) ; y \ d(x) ; z)" by (smt a_complement_one add_left_divisibility d_def d_idempotent mult_associative mult_left_dist_add mult_left_one mult_right_dist_add order_trans) lemma a_one: "a(1) = 0" by (metis one_compl) lemma d_one: "d(1) = 1" by (metis d_def one_double_compl) lemma case_split_right_add: "x ; -p \ y \ x ; --p \ z \ x \ y + z" by (smt a_complement a_dist_add add_isotone mult_left_dist_add mult_right_one one_def plus_closed) lemma case_split_left_add: "-p ; x \ y \ --p ; x \ z \ x \ y + z" by (smt a_complement a_dist_add add_isotone mult_left_one mult_right_dist_add one_def plus_closed) end class relative_antidomain_semiring_T = relative_antidomain_semiring + relative_domain_semiring_T begin lemma a_T: "a(T) = 0" by (metis a_dist_add a_one add_right_top mult_left_zero) lemma d_T: "d(T) = 1" by (metis a_dist_add add_left_top d_def one_def zero_def) lemma shunting_T: "-p ; x \ y \ x \ --p ; T + y" by (rule, metis add_commutative case_split_left_add mult_right_isotone top_greatest, metis a_complement add_left_zero add_right_divisibility mult_associative mult_left_dist_add mult_left_one mult_left_zero mult_right_dist_add mult_right_isotone order_trans plus_left_one) end (* end theory RelativeModal imports RelativeDomain begin *) class relative_diamond_semiring = relative_domain_semiring + fixes diamond :: "'a \ 'a \ 'a" ("| _ > _" [50,90] 95) assumes diamond_def: "|x>y = d(x ; y)" begin lemma diamond_x_1: "|x>1 = d(x)" by (metis diamond_def mult_right_one) lemma diamond_x_d: "|x>d(y) = d(x ; y)" by (metis d_mult_d diamond_def) lemma diamond_x_und: "|x>d(y) = |x>y" by (metis diamond_def diamond_x_d) lemma diamond_d_closed: "|x>y = d( |x>y)" by (metis d_fixpoint diamond_def) lemma diamond_0_y: "|0>y = 0" by (metis d_zero diamond_def mult_left_zero) lemma diamond_1_y: "|1>y = d(y)" by (metis diamond_def mult_left_one) lemma diamond_1_d: "|1>d(y) = d(y)" by (metis diamond_1_y diamond_x_und) lemma diamond_d_y: "|d(x)>y = d(x) ; d(y)" by (metis d_export diamond_def) lemma diamond_d_0: "|d(x)>0 = 0" by (metis d_commutative diamond_0_y diamond_d_y diamond_x_1) lemma diamond_d_1: "|d(x)>1 = d(x)" by (metis diamond_d_closed diamond_x_1) lemma diamond_d_d: "|d(x)>d(y) = d(x) ; d(y)" by (metis d_mult_closed diamond_def) lemma diamond_d_d_same: "|d(x)>d(x) = d(x)" by (metis d_idempotent diamond_d_d) lemma diamond_left_dist_add: "|x + y>z = |x>z + |y>z" by (metis d_dist_add diamond_def mult_right_dist_add) lemma diamond_right_dist_add: "|x>(y + z) = |x>y + |x>z" by (metis d_dist_add diamond_def mult_left_dist_add) lemma diamond_associative: "|x ; y>z = |x>(y ; z)" by (metis diamond_def mult_associative) lemma diamond_left_mult: "|x ; y>z = |x>|y>z" by (metis diamond_def diamond_x_d mult_associative) lemma diamond_right_mult: "|x>(y ; z) = |x>|y>z" by (metis diamond_associative diamond_left_mult) lemma diamond_d_export: "|d(x) ; y>z = d(x) ; |y>z" by (metis diamond_associative diamond_d_closed diamond_d_y diamond_right_mult) lemma diamond_diamond_export: "||x>y>z = |x>y ; |z>1" by (metis diamond_d_d diamond_def diamond_x_1 diamond_x_und) lemma diamond_left_isotone: "x \ y \ |x>z \ |y>z" by (metis diamond_left_dist_add less_eq_def) lemma diamond_right_isotone: "y \ z \ |x>y \ |x>z" by (metis diamond_right_dist_add less_eq_def) lemma diamond_isotone: "w \ y \ x \ z \ |w>x \ |y>z" by (metis diamond_left_isotone diamond_right_isotone order_trans) lemma diamond_left_upper_bound: "|x>y \ |x+z>y" by (metis add_left_upper_bound diamond_left_dist_add) lemma diamond_right_upper_bound: "|x>y \ |x>(y+z)" by (metis add_left_upper_bound diamond_right_dist_add) lemma diamond_lower_bound_right: "|x>(d(y) ; d(z)) \ |x>d(y)" by (metis d_mult_left_lower_bound diamond_right_isotone) lemma diamond_lower_bound_left: "|x>(d(y) ; d(z)) \ |x>d(z)" by (metis d_commutative diamond_lower_bound_right) lemma diamond_right_sub_dist_mult: "|x>(d(y) ; d(z)) \ |x>d(y) ; |x>d(z)" by (metis d_mult_greatest_lower_bound diamond_def diamond_lower_bound_left diamond_lower_bound_right) lemma diamond_demodalisation_1: "d(x) ; |y>z \ Z \ d(x) ; y ; d(z) \ Z" by (metis d_strict diamond_associative diamond_right_mult diamond_x_1 diamond_x_und) lemma diamond_demodalisation_3: "|x>y \ d(z) \ x ; d(y) \ d(z) ; x + Z" by (rule iffI, metis add_commutative add_right_isotone d_below_one d_restrict diamond_def diamond_x_und mult_left_isotone mult_right_isotone mult_right_one order_trans, smt add_commutative add_left_zero d_Z d_dist_add d_isotone d_mult_greatest_lower_bound diamond_d_y diamond_def diamond_x_und) end class relative_box_semiring = relative_diamond_semiring + relative_antidomain_semiring + fixes box :: "'a \ 'a \ 'a" ("| _ ] _" [50,90] 95) assumes box_def: "|x]y = a(x ; a(y))" begin lemma box_diamond: "|x]y = a( |x>a(y))" by (metis box_def d_a_closed diamond_def) lemma diamond_box: "|x>y = a( |x]a(y))" by (metis box_diamond d_def diamond_d_closed diamond_def diamond_x_d) lemma box_x_0: "|x]0 = a(x)" by (metis box_def mult_right_one one_def) lemma box_x_1: "|x]1 = a(x ; 0)" by (metis box_def one_compl) lemma box_x_d: "|x]d(y) = a(x ; a(y))" by (metis box_def d_a_closed) lemma box_x_und: "|x]d(y) = |x]y" by (metis box_def box_x_d) lemma box_x_a: "|x]a(y) = a(x ; y)" by (metis a_mult_d box_def) lemma box_0_y: "|0]y = 1" by (metis box_def mult_left_zero one_def) lemma box_1_y: "|1]y = d(y)" by (metis box_def d_def mult_left_one) lemma box_1_d: "|1]d(y) = d(y)" by (metis box_1_y d_involutive) lemma box_1_a: "|1]a(y) = a(y)" by (metis a_d_closed box_1_y) lemma box_d_y: "|d(x)]y = a(x) + d(y)" by (metis a_dist_add box_def box_x_a diamond_box diamond_x_1 mult_right_one plus_closed) lemma box_a_y: "|a(x)]y = d(x) + d(y)" by (metis a_mult_deMorgan_1 box_def) lemma box_d_0: "|d(x)]0 = a(x)" by (metis box_x_0 d_a_closed) lemma box_a_0: "|a(x)]0 = d(x)" by (metis box_x_0 d_def) lemma box_d_1: "|d(x)]1 = 1" by (metis box_diamond diamond_d_0 one_compl one_def) lemma box_a_1: "|a(x)]1 = 1" by (metis box_x_1 bs_mult_right_zero one_def) lemma box_d_d: "|d(x)]d(y) = a(x) + d(y)" by (metis box_d_y box_x_und) lemma box_a_d: "|a(x)]d(y) = d(x) + d(y)" by (metis a_mult_deMorgan_1 box_x_d) lemma box_d_a: "|d(x)]a(y) = a(x) + a(y)" by (metis a_export_d box_x_a) lemma box_a_a: "|a(x)]a(y) = d(x) + a(y)" by (metis a_export_a box_x_a) lemma box_d_d_same: "|d(x)]d(x) = 1" by (metis box_d_y d_a_closed d_def plus_compl) lemma box_a_a_same: "|a(x)]a(x) = 1" by (metis box_def mult_compl one_def) lemma box_d_closed: "|x]y = d( |x]y)" by (metis box_1_a box_1_y box_def) lemma box_deMorgan_1: "a( |x]y) = |x>a(y)" by (metis box_def d_def diamond_def) lemma box_deMorgan_2: "a( |x>y) = |x]a(y)" by (metis box_def diamond_box double_negation) lemma box_left_dist_add: "|x + y]z = |x]z ; |y]z" by (metis a_dist_add box_def mult_right_dist_add) lemma box_right_dist_add: "|x](y + z) = a(x ; a(y) ; a(z))" by (metis a_dist_add box_def mult_associative) lemma box_associative: "|x ; y]z = a(x ; y ; a(z))" by (metis box_def) lemma box_left_mult: "|x ; y]z = |x]|y]z" by (metis box_def box_x_a mult_associative) lemma box_right_mult: "|x](y ; z) = a(x ; a(y ; z))" by (metis box_def) lemma box_right_mult_d_d: "|x](d(y) ; d(z)) = |x]d(y) ; |x]d(z)" by (smt a_dist_add box_x_a diamond_box diamond_x_1 mult_left_dist_add) lemma box_right_mult_a_d: "|x](a(y) ; d(z)) = |x]a(y) ; |x]d(z)" by (metis box_d_closed box_right_mult_d_d box_x_0) lemma box_right_mult_d_a: "|x](d(y) ; a(z)) = |x]d(y) ; |x]a(z)" by (metis box_a_0 box_left_mult box_right_mult_d_d box_x_0 box_x_und diamond_d_y) lemma box_right_mult_a_a: "|x](a(y) ; a(z)) = |x]a(y) ; |x]a(z)" by (metis a_dist_add box_x_a mult_left_dist_add) lemma box_d_export: "|d(x) ; y]z = a(x) + |y]z" by (metis a_d_closed box_d_y box_def box_left_mult) lemma box_a_export: "|a(x) ; y]z = d(x) + |y]z" by (metis a_d_closed box_d_a box_def box_left_mult d_def) lemma box_left_antitone: "y \ x \ |x]z \ |y]z" by (metis a_antitone box_def mult_left_isotone) lemma box_right_isotone: "y \ z \ |x]y \ |x]z" by (metis a_antitone box_def mult_right_isotone) lemma box_antitone_isotone: "y \ w \ x \ z \ |w]x \ |y]z" by (metis box_left_antitone box_right_isotone order_trans) lemma diamond_1_a: "|1>a(y) = a(y)" by (metis a_d_closed diamond_1_y) lemma diamond_a_y: "|a(x)>y = a(x) ; d(y)" by (metis a_mult_closed d_def d_mult_d diamond_def) lemma diamond_a_0: "|a(x)>0 = 0" by (metis box_a_1 box_deMorgan_1 one_compl) lemma diamond_a_1: "|a(x)>1 = a(x)" by (metis a_d_closed diamond_x_1) lemma diamond_a_d: "|a(x)>d(y) = a(x) ; d(y)" by (metis diamond_a_y diamond_x_und) lemma diamond_d_a: "|d(x)>a(y) = d(x) ; a(y)" by (metis a_d_closed diamond_d_y) lemma diamond_a_a: "|a(x)>a(y) = a(x) ; a(y)" by (metis a_mult_closed diamond_def) lemma diamond_a_a_same: "|a(x)>a(x) = a(x)" by (metis a_idempotent diamond_a_a) lemma diamond_a_export: "|a(x) ; y>z = a(x) ; |y>z" by (metis diamond_a_a diamond_box diamond_left_mult) lemma a_box_a_a: "a(p) ; |a(p)]a(q) = a(p) ; a(q)" by (metis box_x_a double_negation mult_compl_intro plus_def) lemma box_left_lower_bound: "|x+y]z \ |x]z" by (metis add_left_upper_bound box_left_antitone) lemma box_right_upper_bound: "|x]y \ |x](y+z)" by (metis add_left_upper_bound box_right_isotone) lemma box_lower_bound_right: "|x](d(y) ; d(z)) \ |x]d(y)" by (metis box_right_isotone d_mult_left_lower_bound) lemma box_lower_bound_left: "|x](d(y) ; d(z)) \ |x]d(z)" by (metis box_lower_bound_right d_commutative) lemma box_demodalisation_2: "-p \ |y](-q) \ -p ; y ; --q \ Z" by (metis a_greatest_left_absorber box_def mult_associative) lemma box_demodalisation_3: "d(x) \ |y]d(z) \ d(x) ; y \ y ; d(z) + Z" proof - have "d(x) \ |y]d(z) \ d(x) ; y ; a(z) \ Z" by (metis mult_left_isotone a_mult_d a_restrict box_def d_def mult_associative order_trans) thus ?thesis by (metis add_commutative case_split_right_add d_def d_restrict_iff_1 eq_refl mult_associative) qed lemma box_right_sub_dist_add: "|x]d(y) + |x]d(z) \ |x](d(y) + d(z))" by (metis add_commutative add_least_upper_bound box_right_upper_bound) lemma box_diff_var: "|x](d(y) + a(z)) ; |x]d(z) \ |x]d(z)" by (metis box_lower_bound_right box_right_mult_d_d box_x_und d_commutative) lemma fbox_diff: "|x](d(y) + a(z)) \ |x]y + a( |x]z)" by (smt a_compl_intro a_dist_add a_mult_d a_plus_left_lower_bound add_commutative box_def d_def mult_left_dist_add shunting) lemma diamond_demodalisation_2: "|x>y \ d(z) \ a(z) ; x ; d(y) \ Z" by (metis a_mult_d box_def d_a_shunting_zero d_strict diamond_a_y diamond_box diamond_x_1 mult_associative mult_right_one sub_comm) lemma diamond_diff_var: "|x>d(y) \ |x>(d(y) ; a(z)) + |x>d(z)" by (smt a_dist_add add_commutative box_def box_right_mult_a_a diamond_box diamond_right_upper_bound diamond_x_1 double_negation mult_compl_intro mult_right_one one_def plus_closed sub_comm) lemma diamond_diff: "|x>y ; a( |x>z) \ |x>(d(y) ; a(z))" by (metis d_a_shunting d_involutive diamond_def diamond_diff_var diamond_x_und) lemma diamond_split: "|x>y = d(z) ; |x>y + a(z) ; |x>y" by (metis a_export_d a_restrict add_commutative d_def d_strict mult_left_one mult_right_dist_add one_def) lemma box_import_shunting: "-p;-q \ |x](-r) \ -q \ |-p;x](-r)" by (smt box_demodalisation_2 mult_associative sub_comm sub_mult_closed) end (* end theory Precondition imports RelativeModal begin *) context tests begin definition test_set :: "'a set \ bool" where "test_set A \ (\x\A . x = --x)" lemma mult_left_dist_test_set: "test_set A \ test_set { -p ; x | x . x \ A }" by (smt mem_Collect_eq sub_mult_closed test_set_def) lemma mult_right_dist_test_set: "test_set A \ test_set { x ; -p | x . x \ A }" by (smt mem_Collect_eq sub_mult_closed test_set_def) lemma plus_left_dist_test_set: "test_set A \ test_set { -p + x | x . x \ A }" by (smt mem_Collect_eq plus_closed test_set_def) lemma plus_right_dist_test_set: "test_set A \ test_set { x + -p | x . x \ A }" by (smt mem_Collect_eq plus_closed test_set_def) lemma test_set_closed: "A \ B \ test_set B \ test_set A" by (smt set_rev_mp test_set_def) definition test_seq :: "(nat \ 'a) \ bool" where "test_seq t \ (\n . t n = --t n)" lemma test_seq_test_set: "test_seq t \ test_set { t n | n::nat . True }" by (smt mem_Collect_eq test_seq_def test_set_def) definition nat_test :: "(nat \ 'a) \ 'a \ bool" where "nat_test t s \ (\n . t n = --t n) \ s = --s \ (\n . t n \ s) \ (\x y . (\n . t n ; -x \ -y) \ s ; -x \ -y)" lemma nat_test_seq: "nat_test t s \ test_seq t" by (metis nat_test_def test_seq_def) primrec pSum :: "(nat \ 'a) \ nat \ 'a" where "pSum f 0 = 0" | "pSum f (Suc n) = pSum f n + f n" lemma pSum_test: "test_seq t \ pSum t n = --(pSum t n)" by (induct n, metis pSum.simps(1) one_compl one_def, smt pSum.simps(2) plus_closed test_seq_def) lemma pSum_test_nat: "nat_test t s \ pSum t n = --(pSum t n)" by (metis nat_test_seq pSum_test) lemma pSum_upper: "test_seq t \ i t i \ pSum t n" by (induct n, smt less_zeroE, smt pSum.simps(2) pSum_test test_seq_def transitive upper_bound_left upper_bound_right) lemma pSum_below: "test_seq t \ (\m -q) \ pSum t n ; -p \ -q" by (induct n, metis bs_mult_left_zero pSum.simps(1) zero_least_test, smt least_upper_bound mult_distr_plus_right pSum.simps(2) pSum_test test_seq_def sub_mult_closed) lemma pSum_below_nat: "nat_test t s \ (\m -q) \ pSum t n ; -p \ -q" by (metis nat_test_seq pSum_below) lemma pSum_below_sum: "nat_test t s \ pSum t n \ s" by (smt bs_mult_right_one nat_test_def one_def pSum_below_nat pSum_test_nat) end class complete_tests = tests + Sup + assumes sup_test: "test_set A \ Sup A = --Sup A" assumes sup_upper: "test_set A \ x \ A \ x \ Sup A" assumes sup_least: "test_set A \ (\x\A . x \ -y) \ Sup A \ -y" begin lemma Sup_isotone: "test_set B \ A \ B \ Sup A \ Sup B" by (smt subsetD sup_least sup_test sup_upper test_set_closed) lemma mult_right_dist_sup: "test_set A \ Sup A ; -p = Sup { x;-p | x . x \ A }" proof assume 1: "test_set A" hence 2: "test_set { x;-p | x . x \ A }" by (simp add: mult_right_dist_test_set) have 3: "Sup { x;-p | x . x \ A } \ Sup A ; -p" using 1 by (smt mem_Collect_eq mult_iso_left sub_mult_closed sup_test sup_least sup_upper test_set_def) have "Sup A ; -p \ Sup { x;-p | x . x \ A }" proof - have "\x\A . x \ --(--Sup { x;-p | x . x \ A } + --p)" proof fix x assume 4: "x \ A" hence "x;-p + --p \ Sup { x;-p | x . x \ A } + --p" using 1 2 by (smt mem_Collect_eq plus_iso_left sub_mult_closed sup_upper test_set_def sup_test) thus "x \ --(--Sup { x;-p | x . x \ A } + --p)" using 1 2 4 by (smt plus_closed plus_compl_intro sub_comm test_set_def transitive upper_bound_left sup_test) qed hence "Sup A \ --(--Sup { x;-p | x . x \ A } + --p)" using 1 by (simp add: sup_least) thus "Sup A ; -p \ Sup { x;-p | x . x \ A }" using 1 2 by (smt plus_closed plus_comm shunting sub_comm sup_test) qed thus "Sup A ; -p = Sup { x;-p | x . x \ A }" using 1 2 3 by (smt antisymmetric sub_mult_closed sup_test) qed lemma mult_left_dist_sup: "test_set A \ -p ; Sup A = Sup { -p;x | x . x \ A }" proof assume 1: "test_set A" hence 2: "Sup A ; -p = Sup { x;-p | x . x \ A }" by (simp add: mult_right_dist_sup) have 3: "-p ; Sup A = Sup A ; -p" using 1 by (metis sub_comm sup_test) have "{ -p;x | x . x \ A } = { x;-p | x . x \ A }" by (rule set_eqI, simp, metis 1 sub_comm test_set_def) thus "-p ; Sup A = Sup { -p;x | x . x \ A }" using 2 3 by simp qed definition Sum :: "(nat \ 'a) \ 'a" where "Sum f = Sup { f n | n::nat . True }" lemma Sum_test: "test_seq t \ Sum t = --Sum t" by (metis Sum_def sup_test test_seq_test_set) lemma Sum_upper: "test_seq t \ t n \ Sum t" proof - have "t n \ { t n | n::nat . True }" by (smt mem_Collect_eq) thus ?thesis by (metis Sum_def sup_upper test_seq_test_set) qed lemma Sum_least: "test_seq t \ (\n . t n \ -p) \ Sum t \ -p" proof assume 1: "test_seq t \ (\n . t n \ -p)" hence "\x\{ t n | n::nat . True } . x \ -p" by (smt mem_Collect_eq) thus "Sum t \ -p" using 1 by (metis Sum_def test_seq_test_set sup_least) qed lemma mult_right_dist_Sum: "test_seq t \ (\n . t n;-p \ -q) \ Sum t;-p \ -q" proof assume 1: "test_seq t \ (\n . t n;-p \ -q)" hence "Sup { x;-p | x . x \ { t n | n::nat . True } } \ -q" by (smt mem_Collect_eq sub_mult_closed sup_least test_seq_def test_set_def) thus "Sum t;-p \ -q" using 1 test_seq_test_set Sum_def mult_right_dist_sup by simp qed lemma pSum_below_Sum: "test_seq t \ pSum t n \ Sum t" by (smt Sum_test Sum_upper bs_mult_right_one one_def pSum_below pSum_test test_seq_def) lemma pSum_sup: "test_seq t \ pSum t n = Sup { t i | i . i \ {.. {..x\{ t i | i . i \ {.. --pSum t n" by (simp, smt 1 pSum_test pSum_upper) hence 3: "Sup { t i | i . i \ {.. --pSum t n" using 2 by (simp add: sup_least) have "pSum t n \ Sup { t i | i . i \ {.. Sup {t i |i. i \ {.. {..x\{t i |i. i \ {.. --Sup {t i |i. i < Suc n}" using 6 apply simp apply rule+ apply (rule mp) apply (rule sup_upper) apply simp by smt hence 8: "Sup {t i |i. i \ {.. --Sup {t i |i. i < Suc n}" using 5 by (simp add: sup_least) have "t n \ {t i |i. i < Suc n}" by (simp, metis lessI) hence "t n \ Sup {t i |i. i < Suc n}" using 6 by (smt sup_upper) hence "pSum t n + t n \ Sup {t i |i. i Sup {t i |i. i \ {.. {.. 'a \ 'a" (infixr "\" 55) class precondition = tests + pre + assumes pre_closed: "x\-q = --(x\-q)" assumes pre_distrib: "x\-p;-q = (x\-p);(x\-q)" assumes pre_seq: "x;y\-q = x\y\-q" assumes pre_test: "-p\-q = --p + -q" begin lemma pre_below_one: "x\-p \ 1" by (metis one_greatest pre_closed) lemma pre_iso: "-p \ -q \ x\-p \ x\-q" by (metis leq_def pre_closed pre_distrib) lemma pre_lower_bound_left: "x\-p;-q \ x\-p" by (metis lower_bound_left pre_distrib pre_closed) lemma pre_lower_bound_right: "x\-p;-q \ x\-q" by (metis lower_bound_right pre_distrib pre_closed) lemma pre_below_pre_one: "x\-p \ x\1" by (metis one_def one_greatest pre_iso) lemma pre_seq_below_pre_one: "x;y\1 \ x\1" by (metis one_def pre_below_pre_one pre_closed pre_seq) lemma pre_compose: "-p \ x\-q \ -q \ y\-s \ -p \ x;y\-s" by (metis pre_closed pre_iso transitive pre_seq) lemma pre_test_test: "-p;(-p\-q) = -p;-q" by (metis mult_compl_intro pre_test) lemma pre_test_neg: "--p;(-p\-q) = --p" by (metis mult_absorb pre_test) lemma pre_zero: "0\-q = 1" by (metis one_compl one_def plus_left_one pre_test) lemma pre_one: "1\-p = -p" by (metis one_compl one_def plus_left_zero pre_test) lemma pre_export: "-p;x\-q = --p + (x\-q)" by (metis pre_closed pre_seq pre_test) lemma pre_neg_mult: "--p \ -p;x\-q" by (metis leq_def pre_closed pre_seq pre_test_neg) lemma pre_import: "-p;(x\-q) = -p;(-p;x\-q)" by (metis pre_closed pre_seq pre_test_test) lemma pre_import_composition: "-p;(-p;x;y\-q) = -p;(x\y\-q)" by (metis pre_closed pre_seq pre_import) lemma pre_import_equiv: "-p \ x\-q \ -p \ -p;x\-q" by (metis leq_def pre_closed pre_import) lemma pre_import_equiv_mult: "-p;-q \ x\-s \ -p;-q \ -q;x\-s" by (smt leq_def pre_closed sub_assoc sub_mult_closed pre_import) lemma pre_test_promote: "-p\-q = -p\-p;-q" by (metis bs_mult_right_one leq_plus_right_one one_def plus_right_one pre_distrib pre_test reflexive sub_comm) lemma pre_mult_test_promote: "x;-p\-q = x;-p\-p;-q" by (metis pre_seq pre_test_promote sub_mult_closed) lemma pre_test_test_same: "-p\-p = 1" by (metis plus_comm plus_compl pre_test) lemma test_below_pre_test_mult: "-q \ -p\-p;-q" by (metis pre_test pre_test_promote upper_bound_right) lemma test_below_pre_test: "-q \ -p\-q" by (metis pre_test upper_bound_right) end class complete_pre = complete_tests + precondition + power begin definition bnd :: "'a \ 'a" where "bnd x = Sup { x^n\0 | n::nat . True }" lemma bnd_test_set: "test_set { x^n\0 | n::nat . True }" by (smt mem_Collect_eq one_compl pre_closed test_set_def) lemma bnd_test: "bnd x = --bnd x" by (metis bnd_def bnd_test_set sup_test) lemma bnd_upper: "x^n\0 \ bnd x" proof - have "x^n\0 \ { x^n\0 | n::nat . True }" by (smt mem_Collect_eq) thus ?thesis by (metis bnd_def bnd_test_set sup_upper) qed lemma bnd_least: "(\n . x^n\0 \ -p) \ bnd x \ -p" proof assume "\n . x^n\0 \ -p" hence "\y\{ x^n\0 | n::nat . True } . y \ -p" by (smt mem_Collect_eq) thus "bnd x \ -p" by (metis bnd_def bnd_test_set sup_least) qed lemma mult_right_dist_bnd: "(\n . (x^n\0);-p \ -q) \ bnd x;-p \ -q" proof assume "\n . (x^n\0);-p \ -q" hence "Sup { y;-p | y . y \ { x^n\0 | n::nat . True } } \ -q" by (smt mem_Collect_eq one_compl pre_closed sub_mult_closed sup_least test_set_def) thus "bnd x;-p \ -q" using bnd_test_set bnd_def mult_right_dist_sup by simp qed lemma tests_complete: "nat_test (\n . (-p;x)^n\0) (bnd(-p;x))" by (smt bnd_test bnd_upper mult_right_dist_bnd nat_test_def one_compl pre_closed) end class modal_precondition = relative_box_semiring + pre + assumes pre_def: "x\p = |x]p" begin subclass precondition by (unfold_locales, metis box_def double_negation pre_def, metis box_right_mult_a_a pre_def, metis box_left_mult pre_def, metis box_a_a d_def pre_def) lemma pre_Z: "-p \ x\-q \ -p ; x ; --q \ Z" by (metis box_demodalisation_2 pre_def) lemma pre_left_dist_add: "x+y\-q = (x\-q) ; (y\-q)" by (metis box_left_dist_add pre_def) lemma pre_left_antitone: "x \ y \ y\-q \ x\-q" by (metis box_left_antitone pre_def) lemma pre_sub_promote: "(x\-q) ; x \ (x\-q) ; x ; -q + Z" by (metis case_split_right_add order_refl pre_Z pre_closed) lemma pre_promote: "(x\-q) ; x + Z = (x\-q) ; x ; -q + Z" by (smt a_below_one add_left_upper_bound add_same_context mult_right_isotone mult_right_one order_trans pre_sub_promote) lemma pre_mult_sub_promote: "(x;y\-q) ; x \ (x;y\-q) ; x ; (y\-q) + Z" by (metis pre_closed pre_seq pre_sub_promote) lemma pre_mult_promote: "(x;y\-q) ; x ; (y\-q) + Z = (x;y\-q) ; x + Z" by (smt pre_below_one add_left_upper_bound add_same_context mult_right_isotone mult_right_one order_trans pre_mult_sub_promote) lemma pre_promote_neg: "(x\-q) ; x ; --q \ Z" by (metis order_refl pre_Z pre_closed) lemma pre_pc_Z: "x\1 = 1 \ x ; 0 \ Z" by (metis a_strict box_x_1 pre_def) end (* end theory Hoare imports Precondition Omega begin *) class ite = fixes ite :: "'a \ 'a \ 'a \ 'a" ("_ \ _ \ _" [58,58,58] 57) class while = fixes while :: "'a \ 'a \ 'a" (infixr "\" 59) class hoare_triple = fixes hoare_triple :: "'a \ 'a \ 'a \ bool" ("_ \ _ \ _" [54,54,54] 53) class ifthenelse = precondition + ite + assumes ite_pre: "x\-p\y\-q = -p;(x\-q) + --p;(y\-q)" begin lemma ite_pre_then: "-p;(x\-p\y\-q) = -p;(x\-q)" by (smt ite_pre plus_absorb plus_distr_mult plus_right_zero pre_closed sub_assoc sub_mult_closed zero_def) lemma ite_pre_else: "--p;(x\-p\y\-q) = --p;(y\-q)" by (smt ite_pre mult_distr_plus mult_idempotent plus_left_zero pre_closed sub_assoc sub_mult_closed zero_def) lemma ite_import_mult_then: "-p;-q \ x\-r \ -p;-q \ x\-p\y\-r" by (smt ite_pre_then leq_def pre_closed sub_assoc sub_comm sub_mult_closed) lemma ite_import_mult_else: "--p;-q \ y\-r \ --p;-q \ x\-p\y\-r" by (smt ite_pre_else leq_def pre_closed sub_assoc sub_comm sub_mult_closed) lemma ite_import_mult: "-p;-q \ x\-r \ --p;-q \ y\-r \ -q \ x\-p\y\-r" by (smt ite_import_mult_then ite_import_mult_else leq_cases pre_closed) end class whiledo = ifthenelse + while + assumes while_pre: "-p\x\-q = x;(-p\x)\-p\1\-q" begin lemma while_pre_2: "-p\x\-q = -p;(x\-p\x\-q) + --p;-q" by (metis ite_pre pre_one pre_seq while_pre) lemma while_pre_then: "-p;(-p\x\-q) = -p;(x\-p\x\-q)" by (metis ite_pre_then pre_seq while_pre) lemma while_pre_else: "--p;(-p\x\-q) = --p;-q" by (metis ite_pre_else pre_one while_pre) lemma while_pre_compl: "--p \ -p\x\--p" by (metis lower_bound_right mult_idempotent pre_closed while_pre_else) lemma while_pre_compl_one: "--p \ -p\x\1" by (metis bs_mult_right_one lower_bound_right one_def pre_closed while_pre_else) lemma while_export_equiv: "-q \ -p\x\1 \ -p;-q \ -p\x\1" by (smt bs_mult_left_one leq_plus lower_bound_right one_def pre_closed shunting sub_comm while_pre_else) lemma nat_test_pre: "nat_test t s \ -p;-q \ x\-q \ -q \ s \ (\n . t n;-p;-q \ x\pSum t n) \ -q \ -p\x\--p;-q" proof assume 1: "nat_test t s \ -p;-q \ x\-q \ -q \ s \ (\n . t n;-p;-q \ x\pSum t n)" have 2: "-q;--p \ -p\x\--p;-q" by (smt leq_def mult_idempotent pre_closed sub_assoc sub_comm sub_mult_closed while_pre_else) have "\n . t n;-p;-q \ -p\x\--p;-q" proof fix n show "t n;-p;-q \ -p\x\--p;-q" proof (induct n rule: nat_less_induct) fix n have 3: "t n = --(t n)" using 1 by (smt nat_test_def) assume "\m -p\x\--p;-q" hence "\m -p\x\--p;-q" using 1 2 by (smt least_upper_bound leq_def nat_test_def pre_closed sub_assoc sub_comm sub_mult_closed) hence "\m -p\x\--p;-q" using 1 by (smt bs_mult_right_one mult_distr_plus mult_distr_plus_right nat_test_def plus_compl sub_mult_closed) hence "pSum t n;-q \ -p\x\--p;-q" using 1 by (smt pSum_below_nat pre_closed sub_mult_closed) hence "t n;-p;-q;(-p\x\--p;-q) = t n;-p;-q" using 1 3 by (smt leq_def pSum_test_nat pre_closed pre_distrib sub_assoc sub_comm sub_mult_closed while_pre_then) thus "t n;-p;-q \ -p\x\--p;-q" using 3 by (smt lower_bound_right pre_closed sub_mult_closed) qed qed hence "-q;-p \ -p\x\--p;-q" using 1 by (smt leq_def nat_test_def pre_closed sub_assoc sub_comm sub_mult_closed) thus "-q \ -p\x\--p;-q" using 2 by (smt bs_mult_right_one leq_def mult_distr_plus mult_distr_plus_right plus_compl pre_closed sub_mult_closed) qed lemma nat_test_pre_1: "nat_test t s \ -p;-q \ x\-q \ -r \ s \ -r \ -q \ (\n . t n;-p;-q \ x\pSum t n) \ -r \ -p\x\--p;-q" proof let ?qs = "-q;s" assume 1: "nat_test t s \ -p;-q \ x\-q \ -r \ s \ -r \ -q \ (\n . t n;-p;-q \ x\pSum t n)" hence 2: "-r \ ?qs" by (metis greatest_lower_bound nat_test_def) have "-p;?qs \ x\?qs" using 1 by (smt greatest_lower_bound lower_bound_left nat_test_def pSum_below_sum pSum_test_nat pre_closed pre_distrib pre_iso sub_assoc sub_comm sub_mult_closed transitive) hence "?qs \ -p\x\--p;?qs" using 1 by (smt lower_bound_left lower_bound_right nat_test_def nat_test_pre pSum_test_nat pre_closed sub_assoc sub_mult_closed transitive) thus "-r \ -p\x\--p;-q" using 1 2 by (smt lower_bound_left nat_test_def pre_closed pre_iso sub_assoc sub_mult_closed transitive) qed lemma nat_test_pre_2: "nat_test t s \ -r \ s \ (\n . t n;-p \ x\pSum t n) \ -r \ -p\x\1" proof assume 1: "nat_test t s \ -r \ s \ (\n . t n;-p \ x\pSum t n)" hence "-p;s \ x\s" by (smt nat_test_def pSum_below_sum pSum_test_nat pre_closed pre_iso sub_comm sub_mult_closed transitive) hence "-r \ -p\x\--p;s" using 1 by (smt leq_def nat_test_def nat_test_pre_1 sub_assoc sub_comm) thus "-r \ -p\x\1" using 1 by (smt nat_test_def one_def pre_below_pre_one pre_closed sub_mult_closed transitive) qed lemma nat_test_pre_3: "nat_test t s \ -p;-q \ x\-q \ -q \ s \ (\n . t n;-p;-q \ x\pSum t n) \ -q \ -p\x\1" by (smt nat_test_pre one_double_compl pre_below_pre_one pre_closed sub_mult_closed transitive) abbreviation aL :: "'a" where "aL \ 1\1\1" end class atoms = tests + fixes Atomic_program :: "'a set" fixes Atomic_test :: "'a set" assumes one_atomic_program: "1 \ Atomic_program" assumes zero_atomic_test: "0 \ Atomic_test" assumes atomic_test_test: "p \ Atomic_test \ p = --p" class while_program = whiledo + atoms + power begin inductive_set Test_expression :: "'a set" where atom_test: "p \ Atomic_test \ p \ Test_expression" | neg_test: "p \ Test_expression \ -p \ Test_expression" | conj_test: "p \ Test_expression \ q \ Test_expression \ p;q \ Test_expression" lemma test_expression_test: "p \ Test_expression \ p = --p" by (rule, induct rule: Test_expression.induct, metis atomic_test_test, simp, metis sub_mult_closed) lemma disj_test: "p \ Test_expression \ q \ Test_expression \ p+q \ Test_expression" by (smt conj_test neg_test plus_def test_expression_test) lemma zero_test_expression: "0 \ Test_expression" by (metis atom_test zero_atomic_test) lemma one_test_expression: "1 \ Test_expression" by (metis neg_test one_def zero_test_expression) lemma pSum_test_expression: "(\n . t n \ Test_expression) \ pSum t n \ Test_expression" by (rule, induct n, metis pSum.simps(1) zero_test_expression, metis disj_test pSum.simps(2)) inductive_set While_program :: "'a set" where atom_prog: "x \ Atomic_program \ x \ While_program" | seq_prog: "x \ While_program \ y \ While_program \ x;y \ While_program" | cond_prog: "p \ Test_expression \ x \ While_program \ y \ While_program \ x\p\y \ While_program" | while_prog: "p \ Test_expression \ x \ While_program \ p\x \ While_program" lemma one_while_program: "1 \ While_program" by (metis atom_prog one_atomic_program) lemma power_while_program: "x \ While_program \ x^n \ While_program" by (rule, induct n, metis one_while_program power_0, metis seq_prog power_Suc) inductive_set Pre_expression :: "'a set" where test_pre: "p \ Test_expression \ p \ Pre_expression" | neg_pre: "p \ Pre_expression \ -p \ Pre_expression" | conj_pre: "p \ Pre_expression \ q \ Pre_expression \ p;q \ Pre_expression" | pre_pre: "p \ Pre_expression \ x \ While_program \ x\p \ Pre_expression" lemma pre_expression_test: "p \ Pre_expression \ p = --p" by (rule, induct rule: Pre_expression.induct, metis test_expression_test, simp, metis sub_mult_closed, metis pre_closed) lemma disj_pre: "p \ Pre_expression \ q \ Pre_expression \ p+q \ Pre_expression" by (smt conj_pre neg_pre plus_def pre_expression_test) lemma zero_pre_expression: "0 \ Pre_expression" by (metis test_pre zero_test_expression) lemma one_pre_expression: "1 \ Pre_expression" by (metis test_pre one_test_expression) lemma pSum_pre_expression: "(\n . t n \ Pre_expression) \ pSum t n \ Pre_expression" by (rule, induct n, metis pSum.simps(1) zero_pre_expression, metis disj_pre pSum.simps(2)) lemma aL_pre_expression: "aL \ Pre_expression" by (metis pre_pre while_prog one_test_expression one_while_program one_pre_expression) lemma bnd_pre_expression: "p \ Test_expression \ x \ While_program \ (p;x)^n\0 \ Pre_expression" by (rule, induct n, metis pre_pre one_while_program power_0 zero_pre_expression, simp, smt disj_pre neg_pre one_compl pre_closed pre_export pre_pre pre_seq test_expression_test test_pre) end class hoare_calculus = while_program + complete_pre + assumes while_soundness: "-p;-q \ x\-q \ -q;aL \ -p\x\--p;-q" begin inductive derived_hoare_triple :: "'a \ 'a \ 'a \ bool" ("_ \ _ \ _" [54,54,54] 53) where atom_trip: "p \ Pre_expression \ x \ Atomic_program \ x\p\x\p" | seq_trip: "p\x\q \ q\y\r \ p\x;y\r" | cond_trip: "p \ Test_expression \ q \ Pre_expression \ p;q\x\r \ -p;q\y\r \ q\x\p\y\r" | while_trip: "p \ Test_expression \ test_seq t \ p;q\x\q \ q \ aL + Sum t \ (\n . t n;p;q\x\aL+pSum t n) \ q\p\x\-p;q" | cons_trip: "p \ Pre_expression \ s \ Pre_expression \ p \ q \ q\x\r \ r \ s \ p\x\s" lemma derived_type: "p\x\q \ p \ Pre_expression \ q \ Pre_expression \ x \ While_program" by (induct rule: derived_hoare_triple.induct, (smt atom_prog seq_prog cond_prog while_prog test_pre neg_pre conj_pre pre_pre)+) lemma cons_pre_trip: "p \ Pre_expression \ q\y\r \ p;q\y\r" by (smt conj_pre cons_trip derived_type lower_bound_right reflexive pre_expression_test) lemma cons_post_trip: "q \ Pre_expression \ r \ Pre_expression \ p\y\q;r \ p\y\r" by (smt cons_trip derived_type lower_bound_right reflexive pre_expression_test) definition valid_hoare_triple :: "'a \ 'a \ 'a \ bool" ("_ \ _ \ _" [54,54,54] 53) where "p\x\q \ (p \ Pre_expression \ q \ Pre_expression \ x \ While_program \ p \ x\q)" lemma while_soundness_1: "test_seq t \ -p;-q \ x\-q \ -q \ aL + Sum t \ (\n . t n;-p;-q \ x\aL+pSum t n) \ -q \ -p\x\--p;-q" proof assume 1: "test_seq t \ -p;-q \ x\-q \ -q \ aL + Sum t \ (\n . t n;-p;-q \ x\aL+pSum t n)" have "\n . t n;-q \ -p\x\--p;-q \ pSum t n;-q \ -p\x\--p;-q" proof fix n show "t n;-q \ -p\x\--p;-q \ pSum t n;-q \ -p\x\--p;-q" proof (induct n rule: nat_less_induct) fix n assume "\m -p\x\--p;-q \ pSum t m;-q \ -p\x\--p;-q" hence 2: "pSum t n;-q \ -p\x\--p;-q" using 1 by (cases n, smt bs_mult_left_zero pSum.simps(1) pre_closed sub_mult_closed zero_least_test, smt least_upper_bound mult_distr_plus_right pSum.simps(2) pSum_test pre_closed sub_mult_closed test_seq_def) hence 3: "x\(aL+pSum t n);-q \ x\-p\x\--p;-q" using 1 by (smt least_upper_bound mult_distr_plus_right one_def pSum_test plus_closed pre_closed pre_iso sub_comm sub_mult_closed while_soundness) have "t n;-p;-q \ x\(aL+pSum t n);-q" using 1 by (smt greatest_lower_bound lower_bound_right one_def pSum_test plus_closed pre_closed pre_distrib sub_assoc sub_mult_closed test_seq_def transitive) hence 4: "-p;(t n;-q) \ -p;(-p\x\--p;-q)" using 1 3 by (smt greatest_lower_bound lower_bound_left one_def pSum_test plus_closed pre_closed sub_assoc sub_comm sub_mult_closed test_seq_def transitive while_pre_then) have "--p;(t n;-q) \ --p;(-p\x\--p;-q)" using 1 by (smt leq_def lower_bound_right sub_assoc sub_comm sub_mult_closed test_seq_def while_pre_else) thus "t n;-q \ -p\x\--p;-q \ pSum t n;-q \ -p\x\--p;-q" using 1 2 4 by (smt leq_cases_2 pre_closed sub_mult_closed test_seq_def) qed qed thus "-q \ -p\x\--p;-q" using 1 by (smt Sum_test leq_def mult_distr_plus_right mult_right_dist_Sum one_def plus_closed pre_closed sub_comm sub_mult_closed while_soundness) qed lemma while_soundness_2: "test_seq t \ -r \ Sum t \ (\n . t n;-p \ x\pSum t n) \ -r \ -p\x\1" proof assume 1: "test_seq t \ -r \ Sum t \ (\n . t n;-p \ x\pSum t n)" hence 2: "\n . t n;-p;--Sum t \ x\aL+pSum t n" by (smt leq_def one_def pSum_test plus_closed pre_closed pre_iso sub_assoc sub_comm sub_mult_closed test_seq_def upper_bound_right) have "-p;--Sum t \ x\--Sum t" using 1 by (smt Sum_test mult_right_dist_Sum pSum_below_Sum pSum_test pre_closed pre_iso sub_comm sub_mult_closed test_seq_def transitive) hence "--Sum t \ -p\x\--p;--Sum t" using 1 2 by (smt Sum_test one_def pre_closed upper_bound_right while_soundness_1) thus "-r \ -p\x\1" using 1 by (smt Sum_test one_def pre_below_pre_one pre_closed sub_mult_closed transitive) qed theorem soundness: "p\x\q \ p\x\q" by (induct rule: derived_hoare_triple.induct, metis atom_prog pre_pre valid_hoare_triple_def pre_closed reflexive pre_expression_test, metis valid_hoare_triple_def pre_expression_test pre_compose seq_prog, metis valid_hoare_triple_def ite_import_mult pre_expression_test cond_prog test_pre, smt valid_hoare_triple_def pre_expression_test conj_pre neg_pre test_pre while_prog while_soundness_1, smt valid_hoare_triple_def pre_expression_test pre_pre pre_iso transitive) end class hoare_calculus_completeness = hoare_calculus + assumes while_bnd: "p \ Test_expression \ x \ While_program \ p\x\1 \ aL + bnd(p;x)" begin lemma while_complete: "p \ Test_expression \ q \ Pre_expression \ x \ While_program \ (\r\Pre_expression . x\r\x\r) \ p\x\q\p\x\q" proof assume 1: "p \ Test_expression \ q \ Pre_expression \ x \ While_program \ (\r\Pre_expression . x\r\x\r)" hence 2: "p;(p\x\q)\x\p\x\q" by (smt cons_pre_trip pre_pre pre_expression_test while_pre_then while_prog test_pre) let ?t = "\n . (p;x)^n\0" have 3: "test_seq ?t" by (smt one_compl pre_closed test_seq_def) have 4: "p\x\q \ aL + bnd(p;x)" using 1 by (smt bnd_test one_def plus_closed pre_below_pre_one pre_closed pre_expression_test transitive while_bnd) have "\n . ?t n;p;(p\x\q)\x\aL+pSum ?t n" proof fix n show "?t n;p;(p\x\q)\x\aL+pSum ?t n" proof (cases n) show "n = 0 \ ?t n;p;(p\x\q)\x\aL+pSum ?t n" using 1 by (smt aL_pre_expression bnd_pre_expression bs_mult_left_zero cons_trip disj_pre one_compl pSum_pre_expression power_0 pre_closed pre_expression_test pre_one test_pre zero_least_test) next fix m have "?t m \ aL + pSum ?t (Suc m)" using 3 by (smt one_compl one_def pSum.simps(2) pSum_test plus_closed pre_closed transitive upper_bound_right) thus "n = Suc m \ ?t n;p;(p\x\q)\x\aL+pSum ?t n" using 1 by (smt aL_pre_expression bnd_pre_expression conj_pre cons_trip disj_pre lower_bound_right one_compl pSum_pre_expression power_Suc pre_expression_test pre_import_composition pre_pre sub_comm test_pre transitive while_prog) qed qed hence "p \ Test_expression \ test_seq ?t \ p;(p\x\q)\x\p\x\q \ p\x\q \ aL + Sum ?t \ (\n . ?t n;p;(p\x\q)\x\aL+pSum ?t n)" using 1 2 3 4 by (metis Sum_def bnd_def) thus "p\x\q\p\x\q" using 1 by (smt cons_post_trip neg_pre pre_expression_test test_pre while_pre_else while_trip) qed lemma pre_completeness: "\ x \ While_program ; q \ Pre_expression \ \ x\q\x\q" by (induct arbitrary: q rule: While_program.induct, metis atom_trip, metis pre_pre pre_seq seq_trip pre_expression_test, smt cond_prog cond_trip cons_pre_trip ite_pre_else ite_pre_then neg_pre pre_pre pre_expression_test test_pre, metis while_complete) theorem completeness: "p\x\q \ p\x\q" by (metis valid_hoare_triple_def pre_completeness reflexive pre_expression_test cons_trip) theorem soundness_completeness: "p\x\q \ p\x\q" by (smt soundness completeness) end class hoare_rules = whiledo + complete_pre + hoare_triple + assumes rule_pre: "x\-q\x\-q" assumes rule_seq: "-p\x\-q \ -q\y\-r \ -p\x;y\-r" assumes rule_cond: "-p;-q\x\-r \ --p;-q\y\-r \ -q\x\-p\y\-r" assumes rule_while: "test_seq t \ -p;-q\x\-q \ -q \ aL + Sum t \ (\n . t n;-p;-q\x\aL+pSum t n) \ -q\-p\x\--p;-q" assumes rule_cons: "-p \ -q \ -q\x\-r \ -r \ -s \ -p\x\-s" assumes rule_disj: "-p\x\-r \ -q\x\-s \ -p+-q\x\-r+-s" assumes rule_conj: "-p\x\-r \ -q\x\-s \ -p;-q\x\-r;-s" begin lemma rule_cons_pre: "-p \ -q \ -q\x\-r \ -p\x\-r" by (metis rule_cons reflexive) lemma rule_cons_pre_mult: "-q\x\-r \ -p;-q\x\-r" by (metis rule_cons_pre lower_bound_left sub_comm sub_mult_closed) lemma rule_cons_pre_plus: "-p+-q\x\-r \ -p\x\-r" by (metis rule_cons_pre upper_bound_left plus_closed) lemma rule_cons_post: "-q\x\-r \ -r \ -s \ -q\x\-s" by (metis rule_cons reflexive) lemma rule_cons_post_mult: "-q\x\-r;-s \ -q\x\-s" by (metis rule_cons_post lower_bound_left sub_comm sub_mult_closed) lemma rule_cons_post_plus: "-q\x\-r \ -q\x\-r+-s" by (metis rule_cons_post upper_bound_left plus_closed) lemma rule_disj_pre: "-p\x\-r \ -q\x\-r \ -p+-q\x\-r" by (metis rule_disj plus_idempotent) lemma rule_conj_post: "-p\x\-r \ -p\x\-s \ -p\x\-r;-s" by (metis rule_conj mult_idempotent) end class hoare_calculus_valid = hoare_calculus_completeness + hoare_triple + assumes hoare_triple_valid: "-p\x\-q \ -p \ x\-q" begin lemma valid_hoare_triple_same: "p \ Pre_expression \ q \ Pre_expression \ x \ While_program \ p\x\q = p\x\q" by (metis valid_hoare_triple_def hoare_triple_valid pre_expression_test) lemma derived_hoare_triple_same: "p \ Pre_expression \ q \ Pre_expression \ x \ While_program \ p\x\q = p\x\q" by (metis valid_hoare_triple_same soundness_completeness) subclass hoare_rules apply unfold_locales apply (smt hoare_triple_valid pre_closed reflexive) apply (smt hoare_triple_valid pre_compose) apply (smt hoare_triple_valid ite_import_mult sub_mult_closed) apply (smt hoare_triple_valid one_def pSum_test plus_closed pre_closed sub_mult_closed test_seq_def while_soundness_1) apply (smt hoare_triple_valid pre_iso transitive pre_closed) apply (smt hoare_triple_valid pre_closed least_upper_bound plus_closed upper_bound_left upper_bound_right transitive pre_iso) apply (smt hoare_triple_valid pre_closed greatest_lower_bound sub_mult_closed lower_bound_left lower_bound_right transitive pre_distrib) done lemma nat_test_rule_while: "nat_test t s \ -q \ s \ (\n . t n;-p;-q\x\pSum t n) \ -p;-q\x\-q \ -q\-p\x\--p;-q" by (smt hoare_triple_valid nat_test_def nat_test_pre pSum_test_nat sub_mult_closed) lemma test_seq_rule_while: "test_seq t \ -p;-q\x\-q \ -q \ aL + Sum t \ (\n . t n;-p;-q\x\aL+pSum t n) \ -q\-p\x\--p;-q" by (smt hoare_triple_valid one_def pSum_test plus_closed pre_closed sub_mult_closed test_seq_def while_soundness_1) lemma rule_skip: "-p\1\-p" by (metis pre_one rule_pre) (* The above proof is a derivation in the Hoare calculus, except for the application of rule_pre. *) lemma rule_example_4: "test_seq t \ Sum t = 1 \ -p1\z1\-p1;-p2 \ -p1;-p2;-p3\z2\-p1;-p2 \ (\n . t n;-p1;-p3\z2\pSum t n) \ -p1\z1;(-p3\z2)\-p2;--p3" proof assume 1: "test_seq t \ Sum t = 1 \ -p1\z1\-p1;-p2 \ -p1;-p2;-p3\z2\-p1;-p2 \ (\n . t n;-p1;-p3\z2\pSum t n)" hence "\n . t n;-p3;(-p1;-p2)\z2\aL+pSum t n" by (smt lower_bound_left one_def pSum_test plus_closed pre_closed rule_cons sub_assoc sub_comm sub_mult_closed test_seq_def upper_bound_right) hence "-p1;-p2\-p3\z2\--p3;(-p1;-p2)" using 1 by (smt one_def one_greatest plus_right_one pre_closed rule_while sub_comm sub_mult_closed) thus "-p1\z1;(-p3\z2)\-p2;--p3" using 1 by (smt lower_bound_left rule_cons_post rule_seq sub_assoc sub_comm sub_mult_closed) qed end class hoare_calculus_pc = hoare_calculus_completeness + assumes pre_one_one: "x\1 = 1" begin lemma aL_one: "aL = 1" by (metis pre_one_one) lemma while_soundness_pc: "-p;-q \ x\-q \ -q \ -p\x\--p;-q" proof - have "test_seq (\x . 0)" by (metis test_seq_def zero_double_compl) thus ?thesis by (metis Sum_test bs_mult_left_zero one_def one_greatest pSum_test plus_left_one pre_one_one while_soundness_1 zero_least_test) qed inductive dp :: "'a \ 'a \ 'a \ bool" where atom_trip: "p \ Pre_expression \ x \ Atomic_program \ dp (x\p) x p" | seq_trip: "dp p x q \ dp q y r \ dp p (x;y) r" | cond_trip: "p \ Test_expression \ q \ Pre_expression \ dp (p;q) x r \ dp (-p;q) y r \ dp q (x\p\y) r" | while_trip: "p \ Test_expression \ dp (p;q) x q \ dp q (p\x) (-p;q)" | cons_trip: "p \ Pre_expression \ s \ Pre_expression \ p \ q \ dp q x r \ r \ s \ dp p x s" lemma derived_dp: "p\x\q \ dp p x q" by (rule iffI, induct rule: derived_hoare_triple.induct, metis dp.atom_trip, metis dp.seq_trip, metis dp.cond_trip, metis dp.while_trip, metis dp.cons_trip, induct rule: dp.induct, metis derived_hoare_triple.atom_trip, metis derived_hoare_triple.seq_trip, metis derived_hoare_triple.cond_trip, metis conj_pre neg_pre test_pre soundness_completeness pre_expression_test valid_hoare_triple_def while_prog while_soundness_pc, metis derived_hoare_triple.cons_trip) end class hoare_calculus_pc_valid = hoare_calculus_pc + hoare_calculus_valid begin lemma rule_while_pc: "-p;-q\x\-q \ -q\-p\x\--p;-q" by (metis hoare_triple_valid sub_mult_closed while_soundness_pc) lemma rule_alternation: "-p\x\-q \ -q\y\-p \ -p\-r\x;y\--r;-p" by (metis rule_seq rule_cons_pre_mult rule_while_pc) lemma rule_alternation_context: "-p\v\-p \ -p\w\-q \ -q\x\-q \ -q\y\-p \ -p\z\-p \ -p\-r\v;w;x;y;z\--r;-p" by (metis rule_seq rule_cons_pre_mult rule_while_pc) lemma rule_example_3: "-p\x\--p \ --p\x\-p \ -q\x\-q \ -r\x\-r \ -p\y\-p \ -r\y\-q \ --p\z\--p \ -q\z\-r \ -p;-q+--p;-r\-s\x;(y\-p\z)\--s;(-p;-q+--p;-r)" proof (rule, (erule conjE)+) assume "-p\x\--p" and "-q\x\-q" and "--p\x\-p" and "-r\x\-r" hence t1: "-p;-q+--p;-r\x\--p;-q+-p;-r" by (smt rule_conj rule_disj sub_mult_closed) assume "-p\y\-p" and "-r\y\-q" hence "-p;-r\y\-p;-q+--p;-r" by (smt rule_conj rule_cons_post_plus sub_mult_closed) hence t2: "-p;(--p;-q+-p;-r)\y\-p;-q+--p;-r" by (metis mult_compl mult_distr_plus mult_idempotent plus_left_zero sub_assoc sub_mult_closed) assume "--p\z\--p" and "-q\z\-r" hence "--p;-q\z\-p;-q+--p;-r" by (smt plus_comm rule_conj rule_cons_post_plus sub_mult_closed) hence "--p;(--p;-q+-p;-r)\z\-p;-q+--p;-r" by (metis mult_compl mult_distr_plus mult_idempotent plus_right_zero sub_assoc sub_mult_closed) hence "--p;-q+-p;-r\y\-p\z\-p;-q+--p;-r" using t2 by (smt plus_closed rule_cond sub_mult_closed) hence "-s;(-p;-q+--p;-r)\x;(y\-p\z)\-p;-q+--p;-r" using t1 by (smt plus_closed rule_cons_pre_mult rule_seq sub_mult_closed) thus "-p;-q+--p;-r\-s\x;(y\-p\z)\--s;(-p;-q+--p;-r)" by (smt plus_closed rule_while_pc sub_mult_closed) qed end class modal_itering_0 = modal_precondition + itering_T + atoms + ite + while + assumes ite_def: "x\p\y = p ; x + -p ; y" assumes while_def: "p\x = (p ; x)\<^sup>\ ; -p" begin subclass relative_antidomain_semiring_T .. lemma Z_circ_left_zero: "Z ; x\<^sup>\ = Z" by (metis Z_top circ_left_top mult_associative) subclass ifthenelse by (unfold_locales, smt a_d_closed box_a_export box_left_dist_add box_x_a case_duality d_def ite_def pre_def) subclass whiledo by (unfold_locales, metis circ_loop_fixpoint ite_def mult_associative mult_right_one while_def) subclass while_program .. lemma pre_while_1: "-p;(-p\x)\1 = -p\x\1" proof - have "--p;(-p;(-p\x)\1) = --p;(-p\x\1)" by (metis a_mult_left_upper_bound box_def bs_mult_right_one leq_def mult_associative one_def pre_def while_pre_else) thus ?thesis by (smt eq_cases one_def pre_closed pre_import) qed lemma a_while_soundness_1: "-p;-q \ |(-p ; x)\<^sup>\ ; --p]1 ; |x](-q) \ -q \ |(-p ; x)\<^sup>\ ; --p](--p;-q)" proof assume "-p;-q \ |(-p ; x)\<^sup>\ ; --p]1 ; |x](-q)" hence 1: "-p;-q \ |(-p ; x)\<^sup>\ ; --p]1 \ -p;-q \ |x](-q)" by (smt a_dist_add box_x_a greatest_lower_bound one_double_compl) hence 2: "-p;(-q;(-p ; x)\<^sup>\;0) \ Z" by (metis a_dist_add a_greatest_left_absorber box_x_1 bs_mult_right_zero mult_associative) have "--p;(-q;(-p ; x)\<^sup>\;0) = 0" by (smt a_dist_add add_commutative add_right_zero mult_associative mult_left_dist_add mult_left_zero mult_right_dist_add mult_right_one circ_left_unfold zero_def) hence 3: "-q;(-p ; x)\<^sup>\;0 \ Z" using 2 by (metis a_export_a a_greatest_left_absorber a_strict d_def less_eq_def zero_least) have "-q ; -p ; x ; Z \ Z" using 1 by (metis a_Z a_below_one a_dist_add a_greatest_left_absorber add_commutative box_left_mult box_right_isotone box_x_0 mult_associative order_trans) hence "-p ; x ; (--q ; T + Z) \ --q ; T + Z" using 1 by (smt Z_top a_dist_add a_greatest_left_absorber add_associative box_def circ_increasing circ_top less_eq_def mult_associative mult_isotone mult_left_dist_add shunting_T sub_comm) hence "(-p ; x)\<^sup>\ ; --q \ --q ; T + Z + (-p ; x)\<^sup>\ ; 0" by (metis add_commutative circ_simulate_absorb mult_associative mult_left_subdist_add_right order_trans top_right_mult_increasing) hence "-q ; (-p ; x)\<^sup>\ ; --q \ -q ; Z + -q ; (-p ; x)\<^sup>\ ; 0" by (smt a_complement add_left_zero add_right_divisibility mult_associative mult_left_dist_add mult_left_zero) also have "... \ Z" using 3 by (metis add_least_upper_bound add_right_upper_bound shunting_T) finally have "-q;(-p;x)\<^sup>\ \ -q;(-p;x)\<^sup>\;-q + Z" by (metis case_split_right_add mult_associative order_refl) hence "-q;(-p;x)\<^sup>\;--p;-(--p;-q) \ (-q;(-p;x)\<^sup>\;-q + Z);--p;--q" by (metis a_export_a d_def mult_associative mult_compl_intro mult_left_isotone) also have "... \ Z" using 3 by (smt Z_mult_decreasing a_dist_add add_commutative add_least_upper_bound mult_associative mult_left_zero mult_right_dist_add zero_def) finally show "-q \ |(-p ; x)\<^sup>\ ; --p](--p;-q)" by (metis a_greatest_left_absorber box_def mult_associative) qed lemma aL_one_circ: "aL = a(1\<^sup>\;0)" by (metis a_one box_0_y box_left_mult box_x_1 mult_left_one pre_def while_def) end class modal_itering_1 = modal_itering_0 + kleene_itering + complete_pre + hoare_triple + assumes split_Z: "x ; Z \ x ; 0 + Z" assumes aL_circ: "|x\<^sup>\]y \ |aL ; x\<^sup>\]y" assumes hoare_triple_def: "p\x\q \ p \ |x]q" begin lemma box_star_induct: "-p \ |x](-p) \ -p \ |x\<^sup>\](-p)" proof assume "-p \ |x](-p)" hence "x;--p;T \ Z + --p;T" by (metis Z_top add_commutative box_demodalisation_2 mult_associative mult_left_isotone shunting_T) hence "x;(Z + --p;T) + --p \ Z + --p;T" by (smt add_least_upper_bound add_left_upper_bound add_right_upper_bound mult_associative mult_left_dist_add mult_right_isotone order_trans split_Z top_right_mult_increasing zero_least) thus "-p \ |x\<^sup>\](-p)" by (metis add_commutative box_demodalisation_2 mult_associative shunting_T star_left_induct) qed lemma box_circ_induct: "-p \ |x](-p) \ -p;aL \ |x\<^sup>\](-p)" by (smt aL_circ box_left_mult box_star_induct one_def order_trans plus_comm pre_closed pre_def pre_test shunting_right) lemma a_while_soundness: "-p;-q \ |x](-q) \ -q;aL \ |(-p;x)\<^sup>\;--p](--p;-q)" by (metis add_right_upper_bound box_circ_induct box_def box_import_shunting box_right_dist_add box_right_isotone mult_associative mult_compl_intro mult_deMorgan order_trans) subclass hoare_calculus by (unfold_locales, metis a_while_soundness while_def pre_def) lemma rule_skip_valid: "-p\1\-p" by (metis box_1_a hoare_triple_def reflexive) (* The above proof is directly using validity. *) end class modal_itering_2 = modal_itering_1 + assumes bnd_circ: "p \ Test_expression \ x \ While_program \ |(p;x)\<^sup>\]1 \ aL + bnd(p;x)" begin lemma a_while_bnd: "p \ Test_expression \ x \ While_program \ |(p;x)\<^sup>\;-p]1 \ aL + bnd(p;x)" by (metis bnd_circ box_a_1 box_left_mult) subclass hoare_calculus_completeness by (unfold_locales, metis a_while_bnd while_def pre_def) subclass hoare_calculus_valid by (unfold_locales, metis hoare_triple_def pre_def) end class modal_itering_pc = modal_itering_2 + assumes mult_zero_below_Z: "x ; 0 \ Z" begin subclass hoare_calculus_pc by (unfold_locales, metis mult_zero_below_Z pre_pc_Z) subclass hoare_calculus_pc_valid .. end (* end theory PrePost imports Hoare begin *) class pre_post = fixes pre_post :: "'a \ 'a \ 'a" (infix "\" 55) class pre_post_spec = semiring_T + precondition + pre_post + assumes pre_post_galois: "-p \ x\-q \ x \ -p\-q" begin lemma pre_left_antitone: "x \ y \ y\-q \ x\-q" by (smt order_refl order_trans pre_closed pre_post_galois) lemma pre_left_subdist: "x+y\-q \ x\-q" by (metis add_left_upper_bound pre_left_antitone) lemma pre_post_left_antitone: "-p \ -q \ -q\-r \ -p\-r" by (metis order_refl order_trans pre_post_galois) lemma pre_post_left_subdist: "-p+-q\-r \ -p\-r" by (metis add_left_upper_bound plus_closed pre_post_left_antitone) lemma pre_post_left_supdist: "-p\-r \ -p;-q\-r" by (metis lower_bound_left pre_post_left_antitone sub_mult_closed) lemma pre_pre_post: "x \ (x\-p)\-p" by (metis order_refl pre_closed pre_post_galois) lemma pre_post_pre: "-p \ (-p\-q)\-q" by (metis eq_refl pre_post_galois) lemma pre_post_zero_top: "0\-q = T" by (metis eq_iff pre_post_galois top_greatest zero_double_compl zero_least) lemma pre_post_pre_one: "(1\-q)\-q = 1" by (metis add_left_zero leq_plus_right_one one_compl one_def pre_closed pre_post_pre) lemma pre_post_right_isotone: "-p \ -q \ -r\-p \ -r\-q" by (metis order_trans pre_iso pre_post_galois pre_post_pre) lemma pre_post_right_subdist: "-r\-p \ -r\-p+-q" by (metis add_left_upper_bound plus_closed pre_post_right_isotone) lemma pre_post_right_supdist: "-r\-p;-q \ -r\-p" by (metis lower_bound_left pre_post_right_isotone sub_mult_closed) lemma pre_post_seq_sub_associative: "(-p\-q);-r \ -p\-q;-r" by (smt leq_def pre_closed pre_distrib pre_post_galois pre_post_right_isotone pre_seq pre_test_test_same sub_mult_closed test_below_pre_test) lemma pre_post_right_import_mult: "(-p\-q) ; -r = (-p\-q;-r) ; -r" by (metis antisym mult_associative mult_idempotent mult_left_isotone pre_post_right_supdist pre_post_seq_sub_associative) lemma seq_pre_post_sub_associative: "-r;(-p\-q) \ --r+-p\-q" by (smt add_least_upper_bound leq_def mult_left_isotone mult_left_one mult_right_one one_def plus_closed pre_neg_mult pre_post_galois) lemma pre_post_left_import_add: "-r ; (-p\-q) = -r ; (--r+-p\-q)" by (smt add_commutative antisym mult_associative mult_idempotent mult_right_isotone pre_post_left_subdist seq_pre_post_sub_associative) lemma pre_post_import_same: "-p;(-p\-q) = -p;(1\-q)" by (metis double_negation plus_compl pre_post_left_import_add) lemma pre_post_import_complement: "--p;(-p\-q) = --p;T" by (metis mult_idempotent plus_cases plus_closed pre_post_left_import_add pre_post_zero_top zero_def zero_double_compl) lemma pre_post_export: "-p\-q = (1\-q) + --p;T" proof - have 1: "-p;(-p\-q) = -p;((1\-q) + --p;T)" by (metis add_right_zero mult_associative mult_left_dist_add mult_left_zero pre_post_import_same zero_def) have "--p;(-p\-q) = --p;((1\-q) + --p;T)" by (metis add_right_top mult_associative mult_idempotent mult_left_dist_add pre_post_import_complement) thus ?thesis using 1 by (metis case_split_left_equal plus_compl) qed lemma pre_post_left_dist_mult: "-p;-q\-r = (-p\-r) + (-q\-r)" proof - have "\p q . -p ; (-p;-q\-r) = -p ; (-q\-r)" by (metis add_commutative plus_compl_intro pre_post_left_import_add sub_mult_closed) hence 1: "(-p+-q) ; (-p;-q\-r) \ (-p\-r) + (-q\-r)" by (smt add_commutative add_least_upper_bound add_right_upper_bound mult_left_one mult_right_dist_add plus_left_one sub_comm) have "-(-p+-q) ; (-p;-q\-r) = -(-p+-q) ; T" by (smt add_associative add_commutative one_compl plus_absorb plus_closed plus_right_zero pre_post_left_import_add pre_post_zero_top sub_mult_closed) hence "-(-p+-q) ; (-p;-q\-r) \ (-p\-r) + (-q\-r)" by (smt add_left_upper_bound mult_left_one mult_right_subdist_add_right order_trans plus_left_one mult_associative plus_deMorgan pre_post_import_complement sub_comm) thus ?thesis using 1 by (smt add_least_upper_bound antisym case_split_left order_refl plus_closed plus_compl pre_post_left_supdist sub_comm) qed lemma pre_post_left_import_mult: "-r ; (-p\-q) = -r ; (-r;-p\-q)" by (metis add_commutative mult_left_dist_add mult_right_one one_def pre_post_import_same pre_post_left_dist_mult) lemma pre_post_right_dist_add: "-p\-q+-r = (-p\-q) + (-p\-r)" proof - have 1: "(-p\-q+-r);-q \ (-p\-q) + (-p\-r)" by (smt add_left_upper_bound mult_absorb mult_left_subdist_add_right mult_right_one order_trans plus_closed plus_left_one pre_post_right_import_mult sub_comm) have "(-p\-q+-r);--q = (-p\-r);--q" by (smt plus_def pre_post_right_import_mult mult_compl_intro mult_distr_plus_right mult_left_dist_add unique_zero) hence "(-p\-q+-r);--q \ (-p\-q) + (-p\-r)" by (metis add_right_upper_bound mult_left_subdist_add_right mult_right_one order_trans plus_left_one) thus ?thesis using 1 by (metis add_least_upper_bound antisym case_split_right one_greatest plus_comm plus_compl pre_post_right_subdist) qed lemma pre_post_right_import_add: "(-p\-q) ; -r = (-p\-q+--r) ; -r" by (smt bs_mult_right_one case_duality plus_closed plus_comm plus_compl pre_post_right_import_mult sub_comm wnf_lemma_1) lemma pre_left_dist_add: "x+y\-q = (x\-q) ; (y\-q)" by (smt add_commutative add_isotone antisym greatest_lower_bound pre_closed pre_left_subdist pre_post_galois pre_post_left_dist_mult pre_pre_post sub_mult_closed) lemma pre_post_reflexive: "1 \ -p\-p" by (metis pre_one pre_post_galois reflexive) lemma pre_post_compose: "-q \ -r \ (-p\-q);(-r\-s) \ -p\-s" by (smt order_trans pre_closed pre_iso pre_post_galois pre_post_pre pre_seq) lemma pre_post_compose_1: "(-p\-q);(-q\-r) \ -p\-r" by (metis pre_post_compose reflexive) lemma pre_post_compose_2: "(-p\-p);(-p\-q) = -p\-q" by (metis antisym mult_left_isotone mult_left_one pre_post_compose_1 pre_post_reflexive) lemma pre_post_compose_3: "(-p\-q);(-q\-q) = -p\-q" by (metis antisym mult_right_isotone mult_right_one pre_post_compose_1 pre_post_reflexive) lemma pre_post_compose_4: "(-p\-p);(-p\-p) = -p\-p" by (metis pre_post_compose_2) lemma pre_post_one_one: "x\1 = 1 \ x \ 1\1" by (metis eq_iff one_def pre_below_one pre_post_galois) lemma pre_post_shunting: "x \ -p;-q\-r \ -p;x \ -q\-r" proof - have "--p;x \ --p;(-p;-q\-r)" by (smt mult_compl mult_left_zero mult_right_isotone pre_post_left_import_mult pre_post_zero_top sub_assoc sub_comm sub_mult_closed top_greatest) hence "-p;x \ -q\-r \ x \ -p;-q\-r" by (smt add_least_upper_bound case_split_left less_eq_def mult_left_isotone mult_left_one order_refl plus_compl pre_post_left_supdist sub_comm) thus ?thesis by (smt mult_right_isotone pre_post_left_import_mult mult_left_isotone mult_left_one one_greatest order_trans) qed end class havoc = fixes H :: "'a" class semiring_H = semiring_T + havoc + assumes H_zero : "H ; 0 = 0" assumes H_split: "x \ x ; 0 + H" begin lemma H_galois: "x ; 0 \ y \ x \ y + H" by (smt H_split H_zero add_associative add_commutative add_left_zero add_right_isotone less_eq_def mult_right_dist_add mult_right_subdist_add_left zero_right_mult_decreasing) lemma H_greatest_finite: "x ; 0 = 0 \ x \ H" by (metis H_galois add_left_zero eq_iff zero_least) lemma H_reflexive: "1 \ H" by (metis H_greatest_finite mult_left_one) lemma H_transitive: "H = H ; H" by (metis H_greatest_finite H_reflexive H_zero antisym_conv mult_associative mult_right_isotone mult_right_one) lemma T_split_H: "T ; 0 + H = T" by (metis H_split add_left_top less_eq_def) end class pre_post_spec_H = pre_post_spec + modal_precondition + semiring_H begin lemma pre_post_def_iff: "-p ; x ; --q \ Z \ x \ Z + --p ; T + H ; -q" proof (rule iffI) assume 1: "-p ; x ; --q \ Z" have "-p ; x ; -q \ -p ; x ; 0 + H ; -q" by (smt H_split bs_mult_left_zero mult_associative mult_isotone mult_right_dist_add reflexive) hence "-p ; x ; -q \ -p ; x ; --q + H ; -q" by (smt add_commutative add_right_isotone mult_right_isotone order_trans zero_least) hence "-p ; x \ Z + H ; -q" using 1 by (smt add_associative add_commutative case_split_right_add less_eq_def) thus "x \ Z + --p ; T + H ; -q" by (smt add_associative add_commutative case_split_left_add mult_right_isotone top_greatest) next assume "x \ Z + --p ; T + H ; -q" hence "-p ; x ; --q \ (-p ; Z + -p ; H ; -q) ; --q" by (smt a_complement add_right_zero mult_associative mult_isotone mult_left_dist_add mult_left_zero reflexive) also have "... = -p ; Z ; --q" by (smt H_zero a_complement add_commutative add_left_zero bs_mult_right_zero mult_associative mult_right_dist_add) finally show "-p ; x ; --q \ Z" by (metis Z_mult_decreasing a_below_one a_greatest_left_absorber a_strict mult_associative order_trans) qed lemma pre_post_def: "-p\-q = Z + --p;T + H;-q" by (metis eq_iff pre_Z pre_post_def_iff pre_post_galois) end class pre_post_spec_whiledo = pre_post_spec + whiledo begin lemma nat_test_pre_post: "nat_test t s \ x \ -p;-q\-q \ -q \ s \ (\n . x \ t n;-p;-q\(pSum t n)) \ -p\x \ -q\--p;-q" by (smt nat_test_def nat_test_pre pSum_test_nat pre_post_galois sub_mult_closed) lemma nat_test_pre_post_2: "nat_test t s \ -r \ s \ (\n . x \ t n;-p\(pSum t n)) \ -p\x \ -r\1" by (smt nat_test_def nat_test_pre_2 one_def pSum_test_nat pre_post_galois sub_mult_closed) end class pre_post_spec_hoare = pre_post_spec_whiledo + hoare_calculus begin lemma pre_post_while: "x \ -p;-q\-q \ -p\x \ -q;aL\--p;-q" by (smt one_def pre_closed pre_post_galois sub_mult_closed while_soundness) lemma while_soundness_1: "test_seq t \ x \ -p;-q\-q \ -q \ aL + Sum t \ (\n . x \ t n;-p;-q\aL+pSum t n) \ -p\x \ -q\--p;-q" by (smt one_def pSum_test plus_closed pre_closed pre_post_galois sub_mult_closed test_seq_def while_soundness_1) lemma while_soundness_2: "test_seq t \ -r \ Sum t \ (\n . x \ t n;-p\pSum t n) \ -p\x \ -r\1" by (smt one_def pSum_test pre_post_galois sub_mult_closed test_seq_def while_soundness_2) end class pre_post_spec_hoare_pc = pre_post_spec_hoare + hoare_calculus_pc begin lemma pre_post_one_one_top: "1\1 = T" by (metis add_left_top less_eq_def pre_one_one pre_post_one_one) lemma pre_post_while_pc: "x \ -p;-q\-q \ -p\x \ -q\--p;-q" by (metis pre_post_galois sub_mult_closed while_soundness_pc) end class pre_post_L = pre_post_spec + modal_itering_1 + itering_L + assumes circ_below_L_add_star: "x\<^sup>\ \ L + x\<^sup>\" begin lemma body_abort_loop: "Z = L \ x \ -p\1 \ -p\x \ 1\1" proof assume 1: "Z = L \ x \ -p\1" hence "-p ; x ; 0 \ L" by (metis a_one one_def pre_Z pre_post_galois) hence "(-p ; x)\<^sup>\ ; 0 \ L" by (smt L_left_zero L_split add_commutative add_left_zero circ_below_L_add_star less_eq_def mult_right_dist_add star_left_induct) thus "-p\x \ 1\1" using 1 by (metis a_one a_strict box_def bs_mult_right_zero mult_associative pre_def pre_post_one_one while_def) qed (* a loop does not abort if its body does not abort *) (* this avoids abortion from all states; alternatively from states in -r if -r is an invariant *) end (* end *) end