# Theory Mono_Bool_Tran

Up to index of Isabelle/HOL/LatticeProperties/MonoBoolTranAlgebra

theory Mono_Bool_Tran
imports Complete_Lattice_Prop Conj_Disj
`header {* Monotonic Boolean Transformers *}theory  Mono_Bool_Tranimports "../LatticeProperties/Complete_Lattice_Prop"   "../LatticeProperties/Conj_Disj"begintext{*The type of monotonic transformers is the type associated to the set of monotonicfunctions from a partially ordered set (poset) to itself. The type of monotonictransformers with the pointwise extended order is also a poset. The monotonic transformers with composition and identity form a monoid, and the monoid operation is compatible with the order.Gradually we extend the algebraic structure of monotonic transformers tolattices, and complete lattices. We also introduce a dual operator (\$(\mathsf{dual}\;f) p = - f (-p)\$) on monotonic transformers overa boolean algebra. However the monotonic transformers over a booleanalgebra are not closed to the pointwise extended negation operator.Finally we introduce an iteration operator on monotonic transformersover a complete lattice.*}notation  bot ("⊥") and  top ("\<top>") and  inf (infixl "\<sqinter>" 70)  and sup (infixl "\<squnion>" 65)definition "MonoTran = {f::'a::order => 'a . mono f}"typedef 'a MonoTran = "MonoTran :: ('a::order => 'a) set"proof  show "id ∈ MonoTran" by (simp add: MonoTran_def mono_def)qedlemma [simp]: "Rep_MonoTran x ∈ MonoTran"  by (rule Rep_MonoTran)instantiation MonoTran :: (order) orderbegindefinition  less_eq_MonoTran_def: "(x ≤ y) = (Rep_MonoTran x ≤ Rep_MonoTran y)"definition  less_MonoTran_def: "((x::'a MonoTran) < y) = (x ≤ y ∧ ¬ y ≤ x)"instance proof  fix x y :: "'a MonoTran" show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"    by (simp add: less_MonoTran_def)next  fix x :: "'a MonoTran" show "x ≤ x"    by (simp add: less_eq_MonoTran_def)next  fix x y z :: "'a MonoTran" assume A: "x ≤ y" assume B: "y ≤ z" from A B show "x ≤ z"    by (simp add: less_eq_MonoTran_def)next  fix x y :: "'a MonoTran" assume A: "x ≤ y" assume B: "y ≤ x" from A B show "x = y"    apply (simp add: less_eq_MonoTran_def)    apply (subgoal_tac "Abs_MonoTran (Rep_MonoTran y) = Abs_MonoTran (Rep_MonoTran x)")    apply (subst (asm) Rep_MonoTran_inverse, subst (asm) Rep_MonoTran_inverse, simp)    by simpqedendlemma [simp]: "(λ u . v) ∈ MonoTran"  by (simp add: MonoTran_def mono_def)lemma comp_MonoTran [simp]: "f ∈ MonoTran ==> g ∈ MonoTran ==> f o g ∈ MonoTran"  by (simp add: MonoTran_def mono_def)lemma [simp]: "id ∈ MonoTran"  by (simp add: MonoTran_def mono_def)instantiation MonoTran :: (order) monoid_multbegindefinition  one_MonoTran_def: "1 = Abs_MonoTran id"definition  times_MonoTran_def: "x * y = Abs_MonoTran (Rep_MonoTran x  o Rep_MonoTran y)"instance proof  fix a b c :: "'a MonoTran" show "a * b * c = a * (b * c)"    by (simp add: times_MonoTran_def Abs_MonoTran_inverse o_assoc)  next  fix a :: "'a MonoTran" show "1 * a = a"    by (simp add: one_MonoTran_def times_MonoTran_def Abs_MonoTran_inverse Rep_MonoTran_inverse)  next  fix a :: "'a MonoTran" show "a * 1 = a"    by (simp add: one_MonoTran_def times_MonoTran_def Abs_MonoTran_inverse Rep_MonoTran_inverse)qedendlemma [simp]: "⊥ ∈ MonoTran"  by (simp add: MonoTran_def mono_def bot_fun_def)class order_bot = order + botinstantiation MonoTran :: (order_bot) botbegindefinition  bot_MonoTran_def: "⊥ = Abs_MonoTran ⊥"instance proof  fix x :: "'a MonoTran" show "⊥ ≤ x"    by (simp add: bot_MonoTran_def Abs_MonoTran_inverse less_eq_MonoTran_def)qedendlemma [simp]: "\<top> ∈ MonoTran"  by (simp add: MonoTran_def mono_def top_fun_def)class order_top = order + topinstantiation MonoTran :: (order_top) topbegindefinition  top_MonoTran_def: "\<top> = Abs_MonoTran \<top>"instance proof  fix x :: "'a MonoTran" show "x ≤ \<top>"    by (simp add: top_MonoTran_def Abs_MonoTran_inverse less_eq_MonoTran_def)qedendlemma inf_MonoTran [simp]: "f ∈ MonoTran ==> g ∈ MonoTran ==> f \<sqinter> g ∈ MonoTran"  apply (simp add: MonoTran_def mono_def inf_fun_def)  apply safe  apply (rule_tac y = "f x" in order_trans)  apply simp_all  apply (rule_tac y = "g x" in order_trans)  by simp_alllemma sup_MonoTran [simp]: "f ∈ MonoTran ==> g ∈ MonoTran ==> f \<squnion> g ∈ MonoTran"  apply (simp add: MonoTran_def mono_def sup_fun_def)  apply safe  apply (rule_tac y = "f y" in order_trans)  apply simp_all  apply (rule_tac y = "g y" in order_trans)  by simp_alltext{*The type of monotonic transformers on a lattice is also a lattice*}instantiation MonoTran :: (lattice) latticebegindefinition  inf_MonoTran_def: "x \<sqinter> y = Abs_MonoTran (Rep_MonoTran x \<sqinter> Rep_MonoTran y)"definition  sup_MonoTran_def: "x \<squnion> y = Abs_MonoTran (Rep_MonoTran x \<squnion> Rep_MonoTran y)"instance proof  fix x y :: "'a MonoTran" show "x \<sqinter> y ≤ x"    by (simp add: inf_MonoTran_def less_eq_MonoTran_def Abs_MonoTran_inverse)   fix x y :: "'a MonoTran" show "x \<sqinter> y ≤ y"    by (simp add: inf_MonoTran_def less_eq_MonoTran_def Abs_MonoTran_inverse)  fix x y z :: "'a MonoTran" assume A: "x ≤ y" assume B: "x ≤ z" from A B show "x ≤ y \<sqinter> z"    by (simp add: inf_MonoTran_def less_eq_MonoTran_def Abs_MonoTran_inverse)next  fix x y :: "'a MonoTran" show "x ≤ x \<squnion> y"    by (simp add: sup_MonoTran_def less_eq_MonoTran_def Abs_MonoTran_inverse)   fix x y :: "'a MonoTran" show "y ≤ x \<squnion> y"    by (simp add: sup_MonoTran_def less_eq_MonoTran_def Abs_MonoTran_inverse)  fix x y z :: "'a MonoTran" assume A: "y ≤ x" assume B: "z ≤ x" from A B show "y \<squnion> z ≤ x"    by (simp add: sup_MonoTran_def less_eq_MonoTran_def Abs_MonoTran_inverse)qedendinstantiation MonoTran :: (distrib_lattice) distrib_latticebegininstance proof  fix x y z :: "'a MonoTran" show "x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)"    by (simp add: sup_MonoTran_def inf_MonoTran_def sup_inf_distrib Abs_MonoTran_inverse)qedendcontext complete_lattice beginsubclass order_top proof qedendcontext complete_lattice beginsubclass order_bot proof qedendlemma Sup_MonoTran [simp]: "X ⊆ MonoTran ==> Sup X ∈ MonoTran"  apply (simp add: MonoTran_def mono_def Sup_fun_def)  apply safe  apply (rule SUP_least)  apply (rule_tac y = "f y" in order_trans)   apply blast  by (rule SUP_upper, blast)lemma Inf_MonoTran [simp]: "X ⊆ MonoTran ==> Inf X ∈ MonoTran"  apply (simp add: MonoTran_def mono_def Inf_fun_def)  apply safe  apply (rule INF_greatest)  apply (rule_tac y = "f x" in order_trans)   apply (rule INF_lower, blast)  by blastlemma [simp]: "Rep_MonoTran ` A ⊆ MonoTran"  apply (rule subsetI)  apply (simp add: image_def, safe)  by (rule Rep_MonoTran) instantiation MonoTran :: (complete_lattice) complete_latticebegindefinition  Sup_MonoTran_def: "Sup X = Abs_MonoTran (Sup (Rep_MonoTran`X))"definition  Inf_MonoTran_def: "Inf X = Abs_MonoTran (Inf (Rep_MonoTran`X))"instance proof  fix x :: "'a MonoTran" fix A assume A: "x ∈ A" from A show "Inf A ≤ x"    apply (simp add: Inf_MonoTran_def less_eq_MonoTran_def Abs_MonoTran_inverse)    by (rule Inf_lower, blast)next  fix z :: "'a MonoTran" fix A assume A: "!! x . x ∈ A ==> z ≤ x" from A show "z ≤ Inf A"    apply (simp add: Inf_MonoTran_def less_eq_MonoTran_def Abs_MonoTran_inverse)    by (rule Inf_greatest, blast)next  fix x :: "'a MonoTran" fix A assume A: "x ∈ A" from A show "x ≤ Sup A"    apply (simp add: Sup_MonoTran_def less_eq_MonoTran_def Abs_MonoTran_inverse)    by (rule Sup_upper, blast)next  fix z :: "'a MonoTran" fix A assume A: "!! x . x ∈ A ==> x ≤ z" from A show "Sup A ≤ z"    apply (simp add: Sup_MonoTran_def less_eq_MonoTran_def Abs_MonoTran_inverse)    by (rule Sup_least, blast)nextqedendinstantiation MonoTran :: (complete_distrib_lattice) complete_distrib_latticebegininstance proof  fix x :: "'a MonoTran" fix Y :: "'a MonoTran set" show "x \<sqinter> Sup Y = (SUP y:Y. x \<sqinter> y)"    apply (simp add: SUP_def Sup_MonoTran_def inf_MonoTran_def less_eq_MonoTran_def Abs_MonoTran_inverse inf_Sup)    apply (simp add: image_def)    apply (subgoal_tac "{y . ∃xa . (∃x ∈ Y . xa = Rep_MonoTran x) ∧ y = Rep_MonoTran x \<sqinter> xa}        = {y . ∃xa . (∃xb::'a MonoTran∈Y. xa = Abs_MonoTran (Rep_MonoTran x \<sqinter> Rep_MonoTran xb)) ∧ y = Rep_MonoTran xa}")    apply (simp, safe)    apply (rule_tac x = "Abs_MonoTran (Rep_MonoTran x \<sqinter> Rep_MonoTran xb)" in exI)    by (simp_all add: Abs_MonoTran_inverse, auto)next  fix x :: "'a MonoTran" fix Y show "x \<squnion> Inf Y = (INF y:Y. x \<squnion> y)"    apply (simp add: INF_def Inf_MonoTran_def sup_MonoTran_def less_eq_MonoTran_def Abs_MonoTran_inverse sup_Inf)    apply (simp add: image_def)    apply (subgoal_tac "{y . ∃xa . (∃x ∈ Y . xa = Rep_MonoTran x) ∧ y = Rep_MonoTran x \<squnion> xa}       = {y . ∃xa . (∃xb ∈Y. xa = Abs_MonoTran (Rep_MonoTran x \<squnion> Rep_MonoTran xb)) ∧ y = Rep_MonoTran xa}")    apply (simp, safe)    apply (rule_tac x = "Abs_MonoTran (Rep_MonoTran x \<squnion> Rep_MonoTran xb)" in exI)    by (simp_all add: Abs_MonoTran_inverse, auto)qedenddefinition  "dual_fun (f::'a::boolean_algebra => 'a) = (λ p . - (f (- p)))"lemma [simp]: "f ∈ MonoTran ==> dual_fun f ∈ MonoTran"  by (simp add: MonoTran_def dual_fun_def mono_def)definition  "Omega_fun f g = (λ h . (f o h) \<sqinter> g)"definition   "omega_fun f = lfp (Omega_fun f id)"definition  "star_fun f = gfp (Omega_fun f id)"lemma [simp]: "f ∈ MonoTran ==> mono f"  by (unfold MonoTran_def, simp)lemma [simp]: "f ∈ MonoTran ==> Omega_fun f g ∈ MonoTran"  apply (simp add: Omega_fun_def mono_def MonoTran_def)  apply safe  apply (simp add: le_fun_def inf_fun_def id_def o_def)  apply safe  apply (rule_tac y = "f (x xa)" in order_trans)  by simp_alllemma [simp]: "f ∈ MonoTran ==> omega_fun f ∈ MonoTran"   apply (unfold omega_fun_def MonoTran_def Omega_fun_def, simp)  apply (rule lfp_mono)  apply (simp add: mono_mono_def mono_def)  apply safe  apply (rule_tac y = "f o x" in order_trans)  apply simp  apply (simp add: le_fun_def inf_fun_def id_def o_def)  apply (rule_tac y = "f (fa x)" in order_trans)  apply simp_all  apply (rule_tac y = "x" in order_trans)  by simp_alllemma [simp]: "f ∈ MonoTran ==> star_fun f ∈ MonoTran"   apply (unfold star_fun_def MonoTran_def Omega_fun_def, simp)  apply (rule gfp_mono)  apply (simp add: mono_mono_def mono_def)  apply safe  apply (rule_tac y = "f o x" in order_trans)  apply simp  apply (simp add: le_fun_def inf_fun_def id_def o_def)  apply (rule_tac y = "f (fa x)" in order_trans)  apply simp_all  apply (rule_tac y = "x" in order_trans)  by simp_alllemma Sup_comp_fun: "(Sup M) o f = Sup {g . ∃ m ∈ M . g = m o f}"  apply (simp add: fun_eq_iff Sup_fun_def o_def)  apply safe  apply (simp add: SUP_def image_def)  apply (subgoal_tac "{y . ∃fa ∈ M . y = fa (f x)} = {y . ∃fa . (∃m ∈ M . ∀x . fa x = m (f x)) ∧ y = fa x}")  by autolemma Inf_comp_fun: "(Inf M) o f = Inf {g . ∃ m ∈ M . g = m o f}"  apply (simp add: fun_eq_iff Inf_fun_def o_def)  apply safe  apply (simp add: INF_def image_def)  apply (subgoal_tac "{y . ∃fa ∈ M . y = fa (f x)} = {y . ∃fa . (∃m ∈ M . ∀x::'a. fa x = m (f x)) ∧ y = fa x}")  by autolemma lfp_omega_lowerbound: "f ∈ MonoTran ==> Omega_fun f g A ≤ A ==> (omega_fun f) o g ≤ A"  apply (simp add: omega_fun_def)  apply (rule_tac P = "λ x . x o g ≤ A" and f = "Omega_fun f id" in lfp_ordinal_induct)  apply simp_all  apply (simp add: le_fun_def o_def inf_fun_def id_def Omega_fun_def)  apply auto  apply (rule_tac y = "f (A x) \<sqinter> g x" in order_trans)  apply simp_all  apply (rule_tac y = "f (S (g x))" in order_trans)  apply simp_all  apply (simp add: mono_def MonoTran_def)  apply (unfold Sup_comp_fun)  apply (rule Sup_least)  by autolemma gfp_omega_upperbound: "f ∈ MonoTran ==> A ≤ Omega_fun f g A ==> A ≤ (star_fun f) o g"  apply (simp add: star_fun_def)  apply (rule_tac P = "λ x . A ≤ x o g" and f = "Omega_fun f id" in gfp_ordinal_induct)  apply simp_all  apply (simp add: le_fun_def o_def inf_fun_def id_def Omega_fun_def)  apply auto  apply (rule_tac y = "f (A x) \<sqinter> g x" in order_trans)  apply simp_all  apply (rule_tac y = "f (A x)" in order_trans)  apply simp_all  apply (simp add: mono_def MonoTran_def)  apply (unfold Inf_comp_fun)  apply (rule Inf_greatest)  by autolemma lfp_omega_greatest: "(∀ u . Omega_fun f g u ≤ u --> A ≤ u) ==> A ≤ (omega_fun f) o g"  apply (unfold omega_fun_def)  apply (simp add: lfp_def)  apply (unfold Inf_comp_fun)  apply (rule Inf_greatest)  apply simp  apply safe  apply (drule_tac x = "m o g" in spec)  by (simp add: le_fun_def o_def inf_fun_def Omega_fun_def)lemma gfp_star_least: "(∀ u . u ≤ Omega_fun f g u --> u ≤ A) ==> (star_fun f) o g ≤ A"  apply (unfold star_fun_def)  apply (simp add: gfp_def)  apply (unfold Sup_comp_fun)  apply (rule Sup_least)  apply simp  apply safe  apply (drule_tac x = "m o g" in spec)  by (simp add: le_fun_def o_def inf_fun_def Omega_fun_def)lemma lfp_omega: "f ∈ MonoTran ==> ((omega_fun f) o g) = lfp (Omega_fun f g)"  apply (rule antisym)  apply (rule lfp_omega_lowerbound)  apply simp_all  apply (simp add: lfp_def)  apply (rule Inf_greatest)  apply safe  apply (rule_tac y = "Omega_fun f g x" in order_trans)  apply simp_all  apply (rule_tac f = " Omega_fun f g" in monoD)  apply simp_all  apply (rule Inf_lower)  apply simp  apply (rule lfp_omega_greatest)  apply safe  apply (simp add: lfp_def)  apply (rule Inf_lower)  by simplemma gfp_star: "f ∈ MonoTran ==> ((star_fun f) o g) = gfp (Omega_fun f g)"  apply (rule antisym)  apply (rule gfp_star_least)  apply safe  apply (simp add: gfp_def)  apply (rule Sup_upper, simp)  apply (rule gfp_omega_upperbound)  apply simp_all  apply (simp add: gfp_def)  apply (rule Sup_least)  apply safe  apply (rule_tac y = "Omega_fun f g x" in order_trans)  apply simp_all  apply (rule_tac f = " Omega_fun f g" in monoD)  apply simp_all  apply (rule Sup_upper)  by simpdefinition "assert_fun p q = (p \<sqinter> q :: 'a::semilattice_inf)"lemma assert_fun_MonoTran [simp]: "(assert_fun p) ∈ MonoTran"  apply (simp add: assert_fun_def MonoTran_def mono_def, safe)  by (rule_tac y = x in order_trans, simp_all)lemma assert_fun_le_id [simp]: "assert_fun p ≤ id"  by (simp add: assert_fun_def id_def le_fun_def)lemma assert_fun_disjunctive [simp]: "assert_fun (p::'a::distrib_lattice) ∈ Apply.disjunctive"  by (simp add: assert_fun_def Apply.disjunctive_def inf_sup_distrib)  definition  "assertion_fun = {x . ∃ p . x = assert_fun p}"lemma assert_cont:  "(x :: 'a::boolean_algebra => 'a)  ≤ id ==> x ∈ Apply.disjunctive ==> x = assert_fun (x \<top>)"  apply (rule antisym)  apply (simp_all add: le_fun_def assert_fun_def, safe)  apply (rule_tac f = x in  monoD, simp_all)  apply (subgoal_tac "x top = sup (x xa) (x (-xa))")  apply simp  apply (subst inf_sup_distrib)  apply simp  apply (rule_tac y = "inf (- xa) xa" in order_trans)  apply (simp del: compl_inf_bot)  apply (rule_tac y = "x (- xa)" in order_trans)  apply simp  apply simp  apply simp  apply (cut_tac x = x and y = xa and z = "-xa" in Apply.disjunctiveD, simp)  apply (subst (asm) sup_commute)  apply (subst (asm) compl_sup_top)  by simplemma assertion_fun_disj_less_one: "assertion_fun = Apply.disjunctive ∩ {x::'a::boolean_algebra => 'a . x ≤ id}"  apply safe  apply (simp_all add: assertion_fun_def, auto)  apply (rule_tac x = "x \<top>" in exI)  by (rule assert_cont, simp_all)lemma assert_fun_dual: "((assert_fun p) o \<top>) \<sqinter> (dual_fun (assert_fun p)) = assert_fun p"  by (simp add: fun_eq_iff inf_fun_def dual_fun_def o_def assert_fun_def top_fun_def inf_sup_distrib inf_compl_bot)lemma assertion_fun_dual: "x ∈ assertion_fun ==> (x o \<top>) \<sqinter> (dual_fun x) = x"  by (simp add: assertion_fun_def, safe, simp add: assert_fun_dual)lemma assertion_fun_MonoTran [simp]: "x ∈ assertion_fun ==> x ∈ MonoTran"  by (unfold assertion_fun_def MonoTran_def, auto)lemma assertion_fun_le_one [simp]: "x ∈ assertion_fun ==> x ≤ id"  by (unfold assertion_fun_def, auto)end`