Theory Constructive

theory Constructive
imports Main
(**-----------------------------------------------------------------------------
 * © [I Dragomir, V Preoteasa, S Tripakis]
 *
 * Contributors:
 *  Viorel Preoteasa
 *
 * This software is governed by the MIT licence and abiding by the rules of
 * distribution of free software. You can use, modify and/or redistribute the
 * software under the terms of the MIT licence included in this distribution.
 *)

subsection‹Constructive Functions›

theory Constructive imports Main
begin

  notation
    bot ("⊥") and
    top ("⊤") and
    inf (infixl "⊓" 70)
    and sup (infixl "⊔" 65)

  class order_bot_max = order_bot +
    fixes maximal :: "'a ⇒ bool"
    assumes maximal_def: "maximal x = (∀ y . ¬ x < y)"
    assumes [simp]: "¬ maximal ⊥"
    begin
      lemma ex_not_le_bot[simp]: "∃ a. ¬ a ≤ ⊥"
        apply (subgoal_tac "¬ maximal ⊥")
        apply (subst (asm) maximal_def, simp_all add: less_le, auto)
        apply (rule_tac x = x in exI, auto)
        apply (subgoal_tac "x = ⊥", simp)
        by (rule antisym, simp_all)
    end

  instantiation "option" :: (type) order_bot_max
    begin
      definition bot_option_def: "(⊥::'a option) = None"
      definition le_option_def: "((x::'a option) ≤ y) = (x = None ∨ x = y)"
      definition less_option_def: "((x::'a option) < y) = (x ≤ y ∧ ¬ (y ≤ x))"
      definition maximal_option_def: "maximal (x::'a option) = (∀ y . ¬ x < y)"

      instance 
      proof
        qed (auto simp add: le_option_def less_option_def maximal_option_def bot_option_def)

     lemma [simp]: "None ≤ x"
      by (subst bot_option_def [THEN sym], simp)
    end

  context order_bot
    begin
      definition "is_lfp f x = ((f x = x) ∧ (∀ y . f y = y ⟶ x ≤ y))"
      definition "emono f = (∀ x y. x ≤ y ⟶ f x ≤ f y)"

      definition "Lfp f = Eps (is_lfp f)"

      lemma lfp_unique: "is_lfp f x ⟹ is_lfp f y ⟹ x = y"
        apply (simp add: is_lfp_def)
        by (simp add: local.antisym)

      lemma lfp_exists: "is_lfp f x ⟹ Lfp f = x"
        apply (rule lfp_unique, simp_all)
        by (simp add: Lfp_def someI)
  
      lemma emono_a: "emono f ⟹ x ≤ y ⟹ f x ≤ f y"
        by (simp add: emono_def)

      lemma emono_fix: "emono f ⟹ f y = y ⟹ (f ^^ n) ⊥ ≤ y"
        apply (induction n)
        apply (simp_all)
        apply (drule emono_a, simp_all)
        by simp

      lemma emono_is_lfp: "emono (f::'a ⇒ 'a) ⟹ (f ^^ (n + 1)) ⊥ = (f ^^ n) ⊥ ⟹ is_lfp f ((f ^^ n) ⊥)"
        apply (simp add: is_lfp_def, safe)
        by (rule emono_fix, simp_all)

      lemma emono_lfp_bot: "emono (f::'a ⇒ 'a) ⟹ (f ^^ (n + 1)) ⊥ = (f ^^ n) ⊥ ⟹ Lfp f = ((f ^^ n) ⊥)"
        apply (drule emono_is_lfp, simp_all)
        by (simp add: lfp_exists)


      lemma emono_up: "emono f ⟹ (f ^^ n) ⊥ ≤ (f ^^ (Suc n)) ⊥"
        apply (induction n)
        apply (simp_all)
        by (drule emono_a, simp_all)
    end

   context order
    begin
       definition "min_set A = (SOME n . n ∈ A ∧ (∀ x ∈ A . n ≤ x))"
    end

   lemma min_nonempty_nat_set_aux: "∀ A . (n::nat) ∈ A ⟶ (∃ k ∈ A . (∀ x ∈ A . k ≤ x))"
     apply (induction n, safe)
     apply (rule_tac x = 0 in bexI, simp_all)
     apply (case_tac "0 ∈ A")
     apply (rule_tac x = 0 in bexI, simp_all)
     apply (drule_tac x = "{n . Suc n ∈ A}" in spec)
     apply safe
     apply (rule_tac x = "Suc k" in bexI, simp_all, safe)
     apply (drule_tac x = "x - 1" in spec)
     by (case_tac x, simp_all)

   lemma min_nonempty_nat_set: "(n::nat) ∈ A ⟹ (∃ k . k ∈ A ∧ (∀ x ∈ A . k ≤ x))"
     by (cut_tac min_nonempty_nat_set_aux, auto)

  thm someI_ex

  lemma min_set_nat_aux: "(n::nat) ∈ A ⟹ min_set A ∈ A ∧ (∀ x ∈ A . min_set A ≤ x)"
    apply (simp add: min_set_def)
    apply (drule min_nonempty_nat_set)
    by (rule someI_ex, simp_all)

  lemma "(n::nat) ∈ A ⟹ min_set A ∈ A ∧ min_set A ≤ n"
    by (simp add: min_set_nat_aux)
    
  lemma min_set_in: "(n::nat) ∈ A ⟹ min_set A ∈ A"
    by (simp add: min_set_nat_aux)

  lemma min_set_less: "(n::nat) ∈ A ⟹ min_set A ≤ n"
    by (simp add: min_set_nat_aux)


  definition "mono_a f = (∀ a b a' b'. (a::'a::order) ≤ a' ∧ (b::'b::order) ≤ b' ⟶ f a b ≤ f a' b')"

  class fin_cpo = order_bot_max +
    
    assumes fin_up_chain: "(∀ i:: nat . a i ≤ a (Suc i)) ⟹ ∃ n . ∀ i ≥ n . a i = a n"
    begin
      lemma emono_ex_lfp: "emono f ⟹ ∃ n . is_lfp f ((f ^^ n) ⊥)"
        apply (cut_tac a = "λ i . (f ^^ i) ⊥" in fin_up_chain)
        apply (safe, rule emono_up, simp)
        apply (rule_tac x= n in exI)
        apply (rule emono_is_lfp, simp)
        by (drule_tac x = "n + 1" in spec, simp)

      lemma emono_lfp: "emono f ⟹ ∃ n . Lfp f = (f ^^ n) ⊥"
        apply (drule emono_ex_lfp, safe)
        apply (rule_tac x = n in exI)
        by (rule lfp_exists, simp)

      lemma emono_is_lfp: "emono f ⟹ is_lfp f (Lfp f)"
        apply (drule emono_ex_lfp, safe)
        by (frule lfp_exists, simp)

      definition "lfp_index (f::'a ⇒ 'a) = min_set {n . (f ^^ n) ⊥ = (f ^^ (n + 1)) ⊥}"

      lemma lfp_index_aux: "emono f ⟹ (∀ i < (lfp_index f) . (f ^^ i) ⊥ < (f ^^ (i + 1)) ⊥) ∧ (f ^^ (lfp_index f)) ⊥ = (f ^^ ((lfp_index f) + 1)) ⊥"
        apply (simp add: lfp_index_def)
        apply safe
        apply (simp add: less_le_not_le, safe)
        apply (cut_tac n = i in emono_up, simp_all)
        apply (cut_tac n = i and A = "{n . (f ^^ n) ⊥ = (f ^^ (n + 1)) ⊥}" in min_set_less, simp)
        apply (rule antisym, simp_all)
        apply (cut_tac n = i in emono_up, simp_all)
        apply (cut_tac a = "λ i . (f ^^ i) ⊥" in fin_up_chain, simp, safe)
        apply (drule emono_up, simp)
        apply (cut_tac n = "n" and A = "{n . (f ^^ n) ⊥ = (f ^^ (n + 1)) ⊥}" in min_set_in)
        apply (drule_tac x = "Suc n" in spec, simp)
        by simp

      lemma [simp]: "emono f ⟹ i < lfp_index f ⟹ (f ^^ i) ⊥ < f ((f ^^ i) ⊥)"
        by (drule lfp_index_aux, simp)

      lemma [simp]: "emono f ⟹ f ((f ^^ (lfp_index f)) ⊥) = (f ^^ (lfp_index f)) ⊥"
        by (drule lfp_index_aux, simp)

      lemma "emono f ⟹ Lfp f = (f ^^ lfp_index f) ⊥"
        by (rule emono_lfp_bot, simp_all)



      lemma AA_aux: "emono f ⟹ (⋀ b . b ≤ a ⟹ f b ≤ a) ⟹ (f ^^ n) ⊥ ≤ a"
        by (induction n, simp_all)

      lemma AA: "emono f ⟹ (⋀ b . b ≤ a ⟹ f b ≤ a) ⟹ Lfp f ≤ a"
        apply (cut_tac f = f in  emono_lfp, simp_all, safe, simp)
        by (simp add: AA_aux)

      lemma BB: "emono f ⟹ f (Lfp f) = Lfp f"
        using local.emono_is_lfp local.is_lfp_def by blast
 
      lemma Lfp_mono: "emono f ⟹ emono g ⟹ (⋀ a . f a ≤ g a) ⟹ Lfp f ≤ Lfp g"
        by (metis AA BB local.emono_def local.order_trans)


    end
    declare [[show_types]]

      lemma [simp]: "mono_a f ⟹ emono (f a)"
        by (simp add: emono_def mono_a_def)

      lemma [simp]: "mono_a f ⟹ emono (λ a . f a b)"
        by (simp add: emono_def mono_a_def)

      lemma mono_aD: "mono_a f ⟹ a ≤ a' ⟹ b ≤ b' ⟹ f a b ≤ f a' b'"
        by (simp add: mono_a_def)

      lemma [simp]: "mono_a (f::'a::fin_cpo ⇒ 'b::fin_cpo ⇒ 'b) ⟹ mono_a g ⟹ emono (λb. f (Lfp (g b)) b)"
        apply (simp add: emono_def, safe)
        apply (rule_tac f = f in mono_aD, simp_all)
        by (rule Lfp_mono, simp_all add: mono_a_def)

      lemma CCC: "mono_a  (f::'a::fin_cpo ⇒ 'b::fin_cpo ⇒ 'b) ⟹ mono_a g ⟹ Lfp (λa. g (Lfp (f a)) a) ≤ Lfp (g (Lfp (λb. f (Lfp (g b)) b)))"
        apply (rule AA, simp_all)
        apply (subst (2) BB [THEN sym], simp_all)
        apply (rule_tac f = g in mono_aD, simp_all)
        apply (rule AA, simp_all)
        apply (subst BB [THEN sym], simp_all)
        by (rule_tac f = f in mono_aD, simp_all)


    lemma Lfp_commute: "mono_a (f::'a::fin_cpo ⇒ 'b::fin_cpo ⇒ 'b::fin_cpo) ⟹ mono_a g ⟹ Lfp (λ b . f  (Lfp (λ a . (g (Lfp (f a))) a)) b) = Lfp (λ b . f (Lfp (g b)) b)"
      apply (rule antisym)
      apply (rule AA, simp_all)
      apply (subst (3) BB [THEN sym], simp_all)
      apply (rule_tac f = f in mono_aD)
      apply simp_all
      by (simp_all add: CCC)

  instantiation "option" :: (type) fin_cpo
    begin
      lemma fin_up_non_bot: "(∀ i . (a::nat ⇒ 'a option) i ≤ a (Suc i)) ⟹ a n ≠ ⊥ ⟹ n ≤ i ⟹ a i = a n"
        apply (induction i, simp_all)
        apply (case_tac "n ≤ i", simp_all)
        apply (drule_tac x = i in spec)
        apply (simp add: le_option_def bot_option_def, safe, simp_all)
        using le_Suc_eq by blast

     lemma fin_up_chain_option: "(∀ i:: nat . (a::nat ⇒ 'a option) i ≤ a (Suc i)) ⟹ ∃ n . ∀ i ≥ n . a i = a n"
      apply (case_tac "∃ n .  a n ≠ ⊥", safe, simp_all)
      apply (rule_tac x = n in exI, safe)
      by (rule fin_up_non_bot, simp_all)
      
    instance
      proof
        qed (simp add: fin_up_chain_option)
    end

  instantiation "prod" :: (order_bot_max, order_bot_max) order_bot_max
    begin
      definition bot_prod_def: "(⊥ :: 'a × 'b) = (⊥, ⊥)"
      definition le_prod_def: "(x ≤ y) = (fst x ≤ fst y ∧ snd x ≤ snd y)"
      definition less_prod_def: "((x::'a×'b) < y) = (x ≤ y ∧ ¬ (y ≤ x))"
      definition maximal_prod_def: "maximal (x::'a × 'b) = (∀ y . ¬ x < y)"

      instance proof
        qed (auto simp add: le_prod_def less_prod_def bot_prod_def maximal_prod_def)
    end

  instantiation "prod" :: (fin_cpo, fin_cpo) fin_cpo
    begin
      
      lemma fin_up_chain_prod: "(∀ i:: nat . (a::nat ⇒ 'a × 'b) i ≤ a (Suc i)) ⟹ ∃ n . ∀ i ≥ n . a i = a n"
        apply (cut_tac a = "fst o a" in fin_up_chain)
        apply (simp add: le_prod_def)
        apply (cut_tac a = "snd o a" in fin_up_chain)
        apply (simp add: le_prod_def)
        apply safe
        apply (rule_tac x = "max n na" in exI)
        by (metis (no_types, hide_lams) comp_apply max.bounded_iff max.cobounded1 max.cobounded2 prod.collapse)
      instance proof
        qed (auto simp add: fin_up_chain_prod)
    end

end