Theory Flat_CCPO

section ‹Flat Chain Complete Partial Orders›
theory Flat_CCPO
imports Main
begin

  text ‹We establish some theory for recursion, based on flat orderings. ›

  subsection ‹Auxiliary lemmas›
  
  text ‹Technical shortcut: Derive less-than from less-or-equal:›  
  definition "mk_lt l a b ≡ l a b ∧ a≠b"
  
  lemma preorder_mk_ltI:
    assumes 
      "⋀x. le x x"
      "⋀x y z. ⟦le x y; le y z⟧ ⟹ le x z"
      "⋀x y. ⟦le x y; le y x⟧ ⟹ x = y"
    shows "class.preorder le (mk_lt le)"
    apply unfold_locales
    by (auto intro: assms simp: mk_lt_def)
  
  
  
  text ‹Fixed points are monotone›
  lemma (in ccpo) fixp_mono:  
    assumes MF: "monotone (≤) (≤) f"
    assumes MF': "monotone (≤) (≤) f'"
    assumes LF: "⋀x. f x ≤ f' x"
    shows "ccpo.fixp Sup (≤) f ≤ ccpo.fixp Sup (≤) f'"
    by (metis LF MF MF' local.fixp_lowerbound local.fixp_unfold)
  
  text ‹CCPOs extend to pointwise ordering on functions›     
  lemma (in ccpo) ccpo_ext_fun: 
    "class.ccpo (fun_lub Sup) (fun_ord (≤)) (mk_lt (fun_ord (≤)))"  
    apply unfold_locales
    apply (auto simp: mk_lt_def fun_ord_def fun_eq_iff)
    subgoal using order.antisym by blast
    subgoal by metis
    subgoal using order.trans by blast
    subgoal by (simp add: order.antisym)
    subgoal by (metis (mono_tags, lifting) chain_fun fun_lub_def local.ccpo_Sup_upper mem_Collect_eq)
    subgoal by (smt (verit, best) chain_fun fun_lub_def local.ccpo_Sup_least mem_Collect_eq)
    done

  subsection ‹Flat Ordering›
    
  
  thm partial_function_mono
  (* Such that we can use ∀x. monotone … in assumptions. Handy as abbreviation!*)
  lemmas [partial_function_mono] = allI


  lemma mono_fun_fun: "monotone (fun_ord le) (fun_ord le) F = (∀x. monotone (fun_ord le) le (λD. F D x))"  
    unfolding monotone_def fun_ord_def by blast

  (* Do not move this inside locale, as it will
    monomorphise the types of the two le's, which
  
  *)  
  abbreviation (input) gen_is_mono' where "gen_is_mono' orda ordb ≡ monotone (fun_ord orda) ordb"
    
  text ‹We establish a theory of flat orderings, parameterized with the bottom element›
  locale flat_rec =
    fixes bot :: "'a" 
  begin
    subsubsection ‹Definitions›
    definition "le a b ≡ a=bot ∨ a=b"
    definition "lt ≡ mk_lt le"
    text ‹A chain is a set of mutually comparable elements›  
    abbreviation "chain ≡ Complete_Partial_Order.chain le"

    text ‹Least upper bound in flat ordering›
    definition "lub M ≡ if M - {bot} = {} then bot else THE m. M-{bot}={m}"

    subsubsection ‹Auxiliary Lemmas›
    lemma lub_simps[simp]:
      "lub {} = bot"  
      "lub {x} = x"  
      "lub {bot,x} = x"
      unfolding lub_def by auto

    lemma fun_lub_empty: "fun_lub lub {} = (λ_. bot)"
      by (auto simp: fun_lub_def)
    
    lemma fun_lub_apply: "fun_lub L A x = L {f x | f. f∈A}"  
      unfolding fun_lub_def
      by meson
      
    lemma chain_apply:
      assumes "Complete_Partial_Order.chain (fun_ord le) A"
      shows "chain {f x |f. f ∈ A}"
      using assms
      unfolding Complete_Partial_Order.chain_def fun_ord_def
      by blast
      
              
    subsubsection ‹CCPO property›    
    text ‹Our structure is a partial order› 
    interpretation ord: order le lt
      apply unfold_locales 
      unfolding le_def lt_def mk_lt_def
      apply auto
      done
    
    text ‹For a flat ordering, chains are either empty, singleton, 
      or doubleton sets that contain \<^term>‹bot›.›
    lemma chain_cases:
      assumes "chain M"
      obtains "M={}" | "M={bot}" | x where "x≠bot" "M={x}" | x where "x≠bot" "M={bot,x}"
      using assms
      unfolding chain_def le_def
      by fast

      
    text ‹Our structure is a chain complete partial order, 
      i.e., every chain has a least upper bound›        
    interpretation ord: ccpo lub le lt
      apply unfold_locales
      apply (auto simp: le_def lub_def elim: chain_cases)
      done
      
    subsubsection ‹Pointwise extension to functions›
    interpretation f_ord: ccpo "fun_lub lub" "fun_ord le" "mk_lt (fun_ord le)"
      by (rule ord.ccpo_ext_fun)

    subsubsection ‹Recursion combinator›  
    thm partial_function_mono

    abbreviation (input) is_mono_body where "is_mono_body F ≡ (∀x. gen_is_mono' le le (λD. F D x))"
  
        
    definition "REC F ≡ if is_mono_body F then f_ord.fixp F else (λ_. bot)"

    text ‹Unfold rule›    
    lemma REC_unfold: "is_mono_body F ⟹ REC F = F (REC F)"
      unfolding REC_def
      apply simp
      by (auto intro: f_ord.fixp_unfold simp: mono_fun_fun)
    
    text ‹Well-founded induction rule›    
    lemma REC_wf_induct: 
      assumes WF: "wf V"
      assumes MONO: "is_mono_body F"
      assumes STEP: "⋀x D. ⟦⋀y. ⟦(y,x)∈V⟧ ⟹ P y (D y) ⟧ ⟹ P x (F D x)"
      shows "P x (REC F x)"
      using WF
      apply (induction x)
      apply (subst REC_unfold[OF MONO])
      by (rule STEP)

    text ‹Pointwise induction rule›    
    lemma REC_pointwise_induct:
      assumes BOT: "⋀x. P x bot"
      assumes STEP: "⋀D x. (⋀y. P y (D y)) ⟹ P x (F D x)"
      shows "P x (REC F x)"
      unfolding REC_def
    proof (clarsimp simp: BOT)
    
      note fixp_induct = f_ord.fixp_induct[unfolded mono_fun_fun]
    
      assume "is_mono_body F"
      then have "∀x. P x (f_ord.fixp F x)"
        apply (induction F rule: fixp_induct; simp add: BOT fun_lub_empty STEP)
        apply (rule ccpo.admissibleI)
        apply clarify
        subgoal for A x
          apply (auto simp: fun_lub_apply dest!: chain_apply[where x=x])
          apply (erule chain_cases; force)
          done
      done
      thus "P x (f_ord.fixp F x)" ..
    qed

    text ‹Monotonicity Rule› 
    lemma REC_mono:
      assumes M: "⋀D. is_mono_body (F D)"
      assumes "⋀x. fun_ord le (F D x) (F D' x)"
      shows "fun_ord le (REC (F D)) (REC (F D'))"
      unfolding REC_def 
      apply (simp add: M)
      apply (rule f_ord.fixp_mono[unfolded mono_fun_fun])
      apply (simp add: M)
      apply (simp add: M)
      by fact
           
  end

  subsection ‹General Setup›
  
  lemma (in ccpo) partial_function_definitions: "partial_function_definitions (≤) Sup"
    using local.ccpo_Sup_least local.ccpo_Sup_upper local.dual_order.antisym local.order_trans partial_function_definitions_def by blast
    
  
  locale rec_setup =
    fixes lub le lt
    assumes A: "class.ccpo lub le lt"
  begin
  
    interpretation ccpo lub le lt by (rule A)

    abbreviation "bt ≡ lub {}"
        
    interpretation f_ord: ccpo "fun_lub lub" "fun_ord le" "mk_lt (fun_ord le)"
      by (rule ccpo_ext_fun)

    lemma fun_lub_empty: "fun_lub lub {} = (λ_. bt)"
      by (auto simp: fun_lub_def)

    lemma fun_lub_apply: "fun_lub L A x = L {f x | f. f∈A}"  
      unfolding fun_lub_def
      by meson
      
    lemma chain_apply:
      assumes "Complete_Partial_Order.chain (fun_ord le) A"
      shows "Complete_Partial_Order.chain le {f x |f. f ∈ A}"
      using assms
      unfolding Complete_Partial_Order.chain_def fun_ord_def
      by blast
            

    abbreviation (input) is_mono_body where "is_mono_body F ≡ (∀x. monotone (fun_ord le) le (λD. F D x))"
      
    (*          
    abbreviation fmono :: "(('b ⇒ 'a) ⇒ 'b ⇒ 'a) ⇒ bool" 
      where "fmono ≡ monotone (fun_ord le) (fun_ord le)"
      
    lemma fmono_alt: "fmono F = (∀x y. fun_ord le x y ⟶ fun_ord le (F x) (F y))"
      unfolding monotone_def ..
    *)  
      
      
    definition "REC F ≡ if is_mono_body F then f_ord.fixp F else (λ_. bt)"
    
    lemma REC_unfold: "is_mono_body F ⟹ REC F = F (REC F)"
      unfolding REC_def
      by (auto intro: f_ord.fixp_unfold[unfolded mono_fun_fun])
  
    find_theorems "ccpo.admissible" fun_ord
      
    text ‹Pointwise induction rule›    
    lemma REC_pointwise_induct:
      assumes BOT: "⋀x. P x bt"
      assumes ADM: "⋀x. ccpo.admissible lub le (P x)"
      assumes STEP: "⋀D x. (⋀y. P y (D y)) ⟹ P x (F D x)"
      shows "P x (REC F x)"
      unfolding REC_def
    proof (clarsimp simp: BOT)
    
      note fixp_induct = f_ord.fixp_induct[unfolded mono_fun_fun]
    
      assume "is_mono_body F"
      then have "∀x. P x (f_ord.fixp F x)"
        apply (induction F rule: fixp_induct; simp add: BOT fun_lub_empty STEP)
        apply (rule admissible_fun[OF partial_function_definitions])
        apply (rule ADM)
      done
      thus "P x (f_ord.fixp F x)" ..
    qed
  
    lemma REC_wf_induct: 
      assumes WF: "wf V"
      assumes MONO: "is_mono_body F"
      assumes STEP: "⋀x D. ⟦⋀y. ⟦(y,x)∈V⟧ ⟹ P y (D y) ⟧ ⟹ P x (F D x)"
      shows "P x (REC F x)"
      using WF
      apply (induction x)
      apply (subst REC_unfold[OF MONO])
      by (rule STEP)
    
    
    lemma REC_mono:
      assumes M: "⋀D. is_mono_body (F D)"
      assumes "⋀x. fun_ord le (F D x) (F D' x)"
      shows "fun_ord le (REC (F D)) (REC (F D'))"
      unfolding REC_def 
      apply (simp add: M)
      apply (rule f_ord.fixp_mono[unfolded mono_fun_fun])
      apply (simp add: M)
      apply (simp add: M)
      by fact
  
  
  end
  
end