Theory Induction

(*
 * Copyright (C) 2014 NICTA
 * All rights reserved.
 *)

(* Author: David Cock - David.Cock@nicta.com.au *)

section "Induction"

theory Induction
  imports Expectations Transformers
begin

text_raw ‹\label{s:induction}›

subsection ‹The Lattice of Expectations›

text_raw ‹\label{s:exp_induct}›

text ‹Defining recursive (or iterative) programs requires us to reason about
fixed points on the semantic objects, in this case expectations.  The
complication here, compared to the standard Knaster-Tarski theorem (for example,
as shown in @{theory HOL.Inductive}), is that we do not have a complete lattice.

Finding a lower bound is easy (it's @{term "λ_. 0"}), but as we do not insist
on any global bound on expectations (and work directly in HOL's real type, rather
than extending it with a point at infinity), there is no top element.  We solve
the problem by defining the least (greatest) fixed point, restricted to an
internally-bounded set, allowing us to substitute this bound for the top element.
This works as long as the set contains at least one fixed point, which appears
as an extra assumption in all the theorems.

This also works semantically, thanks to the definition of healthiness.  Given a
healthy transformer parameterised by some sound expectation:
@{term "t::('s ⇒ real) ⇒ ('s ⇒ real) ⇒ 's ⇒ real"}.  Imagine that we wish to find
the least fixed point of @{term "t P"}.  In practice, @{term t} is generally
doubly healthy, that is @{term "∀P. sound P ⟶ healthy (t P)"} and
@{term "∀Q. sound Q ⟶ healthy (λP. t P Q)"}.  Thus by feasibility, @{term "t P Q"}
must be bounded by @{term "bound_of P"}.  Thus, as by definition @{term "x ≤ t P x"}
for any fixed point, all must lie in the
set of sound expectations bounded above by @{term "λ_. bound_of P"}.›

definition Inf_exp :: "'s expect set ⇒ 's expect"
where "Inf_exp S = (λs. Inf {f s |f. f ∈ S})"

lemma Inf_exp_lower:
  "⟦ P ∈ S; ∀P∈S. nneg P ⟧ ⟹ Inf_exp S ≤ P"
  unfolding Inf_exp_def
  by(intro le_funI cInf_lower bdd_belowI[where m=0], auto)

lemma Inf_exp_greatest:
  "⟦ S ≠ {}; ∀P∈S. Q ≤ P ⟧ ⟹ Q ≤ Inf_exp S"
  unfolding Inf_exp_def by(auto intro!:le_funI[OF cInf_greatest])

definition Sup_exp :: "'s expect set ⇒ 's expect"
where "Sup_exp S = (if S = {} then λs. 0 else (λs. Sup {f s |f. f ∈ S}))"

lemma Sup_exp_upper:
  "⟦ P ∈ S; ∀P∈S. bounded_by b P ⟧ ⟹ P ≤ Sup_exp S"
  unfolding Sup_exp_def
  by(cases "S={}", simp_all, intro le_funI cSup_upper bdd_aboveI[where M=b], auto)

lemma Sup_exp_least:
  "⟦ ∀P∈S. P ≤ Q; nneg Q ⟧ ⟹ Sup_exp S ≤ Q"
  unfolding Sup_exp_def
  by(cases "S={}", auto intro!:le_funI[OF cSup_least])

lemma Sup_exp_sound:
  assumes sS: "⋀P. P∈S ⟹ sound P"
      and bS: "⋀P. P∈S ⟹ bounded_by b P"
  shows "sound (Sup_exp S)"
proof(cases "S={}", simp add:Sup_exp_def, blast,
      intro soundI2 bounded_byI2 nnegI2)
  assume neS: "S ≠ {}"
  then obtain P where Pin: "P ∈ S" by(auto)
  with sS bS have nP: "nneg P" "bounded_by b P" by(auto)
  hence nb: "0 ≤ b" by(auto)

  from bS nb show "Sup_exp S ⊩ λs. b"
    by(auto intro:Sup_exp_least)

  from nP have "λs. 0 ⊩ P" by(auto)
  also from Pin bS have "P ⊩ Sup_exp S"
    by(auto intro:Sup_exp_upper)
  finally show "λs. 0 ⊩ Sup_exp S" .
qed

definition lfp_exp :: "'s trans ⇒ 's expect"
where "lfp_exp t = Inf_exp {P. sound P ∧ t P ≤ P}"

lemma lfp_exp_lowerbound:
  "⟦ t P ≤ P; sound P ⟧ ⟹ lfp_exp t ≤ P"
  unfolding lfp_exp_def by(auto intro:Inf_exp_lower)

lemma lfp_exp_greatest:
  "⟦ ⋀P. ⟦ t P ≤ P; sound P ⟧ ⟹ Q ≤ P; sound Q; t R ⊩ R; sound R ⟧ ⟹ Q ≤ lfp_exp t"
  unfolding lfp_exp_def by(auto intro:Inf_exp_greatest)

lemma feasible_lfp_exp_sound:
  "feasible t ⟹ sound (lfp_exp t)"
  by(intro soundI2 bounded_byI2 nnegI2, auto intro!:lfp_exp_lowerbound lfp_exp_greatest)

lemma lfp_exp_sound:
  assumes fR: "t R ⊩ R" and sR: "sound R"
  shows "sound (lfp_exp t)"
proof(intro soundI2)
  from fR sR have "lfp_exp t ⊩ R"
    by(auto intro:lfp_exp_lowerbound)
  also from sR have "R ⊩ λs. bound_of R" by(auto)
  finally show "bounded_by (bound_of R) (lfp_exp t)" by(auto)
  from fR sR show "nneg (lfp_exp t)" by(auto intro:lfp_exp_greatest)
qed

lemma lfp_exp_bound:
  "(⋀P. unitary P ⟹ unitary (t P)) ⟹ bounded_by 1 (lfp_exp t)"
  by(auto intro!:lfp_exp_lowerbound)

lemma lfp_exp_unitary:
  "(⋀P. unitary P ⟹ unitary (t P)) ⟹ unitary (lfp_exp t)"
proof(intro unitaryI[OF lfp_exp_sound lfp_exp_bound], simp_all)
  assume IH: "⋀P. unitary P ⟹ unitary (t P)"
  have "unitary (λs. 1)" by(auto)
  with IH have "unitary (t (λs. 1))" by(auto)
  thus "t (λs. 1) ⊩ λs. 1" by(auto)
  show "sound (λs. 1)" by(auto)
qed

lemma lfp_exp_lemma2:
  fixes t::"'s trans"
  assumes st: "⋀P. sound P ⟹ sound (t P)"
      and mt: "mono_trans t"
      and fR: "t R ⊩ R" and sR: "sound R"
  shows "t (lfp_exp t) ≤ lfp_exp t"
proof(rule lfp_exp_greatest[of t, OF _ _ fR sR])
  from fR sR show "sound (t (lfp_exp t))" by(auto intro:lfp_exp_sound st)

  fix P::"'s expect"
  assume fP: "t P ⊩ P" and sP: "sound P"
  hence "lfp_exp t ⊩ P" by(rule lfp_exp_lowerbound)
  with fP sP have "t (lfp_exp t) ⊩ t P" by(auto intro:mono_transD[OF mt] lfp_exp_sound)
  also note fP
  finally show "t (lfp_exp t) ⊩ P" .
qed

lemma lfp_exp_lemma3:
  assumes st: "⋀P. sound P ⟹ sound (t P)"
      and mt: "mono_trans t"
      and fR: "t R ⊩ R" and sR: "sound R"
  shows "lfp_exp t ≤ t (lfp_exp t)"
  by(iprover intro:lfp_exp_lowerbound lfp_exp_sound lfp_exp_lemma2 assms
                   mono_transD[OF mt])

lemma lfp_exp_unfold:
  assumes nt: "⋀P. sound P ⟹ sound (t P)"
      and mt: "mono_trans t"
      and fR: "t R ⊩ R" and sR: "sound R"
  shows "lfp_exp t = t (lfp_exp t)"
  by(iprover intro:antisym lfp_exp_lemma2 lfp_exp_lemma3 assms)

definition gfp_exp :: "'s trans ⇒ 's expect"
where "gfp_exp t = Sup_exp {P. unitary P ∧ P ≤ t P}"

lemma gfp_exp_upperbound:
  "⟦ P ≤ t P; unitary P ⟧ ⟹ P ≤ gfp_exp t"
  by(auto simp:gfp_exp_def intro:Sup_exp_upper)

lemma gfp_exp_least:
  "⟦ ⋀P. ⟦ P ≤ t P; unitary P ⟧ ⟹ P ≤ Q; unitary Q ⟧ ⟹ gfp_exp t ≤ Q"
  unfolding gfp_exp_def by(auto intro:Sup_exp_least)

lemma gfp_exp_bound:
  "(⋀P. unitary P ⟹ unitary (t P)) ⟹ bounded_by 1 (gfp_exp t)"
  unfolding gfp_exp_def
  by(rule bounded_byI2[OF Sup_exp_least], auto)

lemma gfp_exp_nneg[iff]:
  "nneg (gfp_exp t)"
proof(intro nnegI2, simp add:gfp_exp_def, cases)
  assume empty: "{P. unitary P ∧ P ⊩ t P} = {}"
  show "λs. 0 ⊩ Sup_exp {P. unitary P ∧ P ⊩ t P}"
    by(simp only:empty Sup_exp_def, auto)
next
  assume "{P. unitary P ∧ P ⊩ t P} ≠ {}"
  then obtain Q where Qin: "Q ∈ {P. unitary P ∧ P ⊩ t P}" by(auto)
  hence "λs. 0 ⊩ Q" by(auto)
  also from Qin have "Q ⊩ Sup_exp {P. unitary P ∧ P ⊩ t P}"
    by(auto intro:Sup_exp_upper)
  finally show "λs. 0 ⊩ Sup_exp {P. unitary P ∧ P ⊩ t P}" .
qed

lemma gfp_exp_unitary:
  "(⋀P. unitary P ⟹ unitary (t P)) ⟹ unitary (gfp_exp t)"
  by(iprover intro:gfp_exp_nneg gfp_exp_bound unitaryI2)

lemma gfp_exp_lemma2:
  assumes ft: "⋀P. unitary P ⟹ unitary (t P)"
      and mt: "⋀P Q. ⟦ unitary P; unitary Q; P ⊩ Q ⟧ ⟹ t P ⊩ t Q"
  shows "gfp_exp t ≤ t (gfp_exp t)"
proof(rule gfp_exp_least)
  show "unitary (t (gfp_exp t))" by(auto intro:gfp_exp_unitary ft)
  fix P
  assume fp: "P ≤ t P" and uP: "unitary P"
  with ft have "P ≤ gfp_exp t" by(auto intro:gfp_exp_upperbound)
  with uP gfp_exp_unitary ft
  have "t P ≤ t (gfp_exp t)" by(blast intro: mt)
  with fp show "P ≤ t (gfp_exp t)" by(auto)
qed

lemma gfp_exp_lemma3:
  assumes ft: "⋀P. unitary P ⟹ unitary (t P)"
      and mt: "⋀P Q. ⟦ unitary P; unitary Q; P ⊩ Q ⟧ ⟹ t P ⊩ t Q"
  shows "t (gfp_exp t) ≤ gfp_exp t"
  by(iprover intro:gfp_exp_upperbound unitary_sound
                   gfp_exp_unitary gfp_exp_lemma2 assms)

lemma gfp_exp_unfold:
  "(⋀P. unitary P ⟹ unitary (t P)) ⟹ (⋀P Q. ⟦ unitary P; unitary Q; P ⊩ Q ⟧ ⟹ t P ⊩ t Q) ⟹
   gfp_exp t = t (gfp_exp t)"
  by(iprover intro:antisym gfp_exp_lemma2 gfp_exp_lemma3)

subsection ‹The Lattice of Transformers›

text_raw ‹\label{s:trans_induct}›

text ‹In addition to fixed points on expectations, we also need
to reason about fixed points on expectation transformers.  The
interpretation of a recursive program in pGCL is as a fixed
point of a function from transformers to transformers.  In contrast
to the case of expectations, \emph{healthy} transformers do form
a complete lattice, where the bottom element is @{term "λ_. (λ_. 0)"},
and the top element is the greatest allowed by feasibility:
@{term "λP. (λ_. bound_of P)"}.›

definition Inf_trans :: "'s trans set ⇒ 's trans"
where "Inf_trans S = (λP. Inf_exp {t P |t. t ∈ S})"

lemma Inf_trans_lower:
  "⟦ t ∈ S; ∀u∈S. ∀P. sound P ⟶ sound (u P) ⟧ ⟹ le_trans (Inf_trans S) t"
  unfolding Inf_trans_def
  by(rule le_transI[OF Inf_exp_lower], blast+)

lemma Inf_trans_greatest:
  "⟦ S ≠ {}; ∀t∈S. ∀P. le_trans u t ⟧ ⟹ le_trans u (Inf_trans S)"
  unfolding Inf_trans_def by(auto intro!:le_transI[OF Inf_exp_greatest])

definition Sup_trans :: "'s trans set ⇒ 's trans"
where "Sup_trans S = (λP. Sup_exp {t P |t. t ∈ S})"

lemma Sup_trans_upper:
  "⟦ t ∈ S; ∀u∈S. ∀P. unitary P ⟶ unitary (u P) ⟧ ⟹ le_utrans t (Sup_trans S)"
  unfolding Sup_trans_def
  by(intro le_utransI[OF Sup_exp_upper], auto intro:unitary_bound)

lemma Sup_trans_upper2:
  "⟦ t ∈ S; ∀u∈S. ∀P. (nneg P ∧ bounded_by b P) ⟶ (nneg (u P) ∧ bounded_by b (u P));
     nneg P; bounded_by b P ⟧ ⟹ t P ⊩ Sup_trans S P"
  unfolding Sup_trans_def by(blast intro:Sup_exp_upper)

lemma Sup_trans_least:
  "⟦ ∀t∈S. le_utrans t u; ⋀P. unitary P ⟹ unitary (u P) ⟧ ⟹ le_utrans (Sup_trans S) u"
  unfolding Sup_trans_def
  by(auto intro!:sound_nneg[OF unitary_sound] le_utransI[OF Sup_exp_least])

lemma Sup_trans_least2:
  "⟦ ∀t∈S. ∀P. nneg P ⟶ bounded_by b P ⟶ t P ⊩ u P;
     ∀u∈S. ∀P. (nneg P ∧ bounded_by b P) ⟶ (nneg (u P) ∧ bounded_by b (u P));
     nneg P; bounded_by b P; ⋀P. ⟦ nneg P; bounded_by b P ⟧ ⟹ nneg (u P) ⟧ ⟹ Sup_trans S P ⊩ u P"
   unfolding Sup_trans_def by(blast intro!:Sup_exp_least)

lemma feasible_Sup_trans:
  fixes S::"'s trans set"
  assumes fS: "∀t∈S. feasible t"
  shows "feasible (Sup_trans S)"
proof(cases "S={}", simp add:Sup_trans_def Sup_exp_def, blast, intro feasibleI)
  fix b::real and P::"'s expect"
  assume bP: "bounded_by b P" and nP: "nneg P"
     and neS: "S ≠ {}"

  from neS obtain t where tin: "t ∈ S" by(auto)
  with fS have ft: "feasible t" by(auto)
  with bP nP have "λs. 0 ⊩ t P" by(auto)
  also {
    from bP nP have "sound P" by(auto)
    with tin fS have "t P ⊩ Sup_trans S P"
      by(auto intro!:Sup_trans_upper2)
  }
  finally show "nneg (Sup_trans S P)" by(auto)

  from fS bP nP
  show "bounded_by b (Sup_trans S P)"
    by(auto intro!:bounded_byI2[OF Sup_trans_least2])
qed

definition lfp_trans :: "('s trans ⇒ 's trans) ⇒ 's trans"
where "lfp_trans T = Inf_trans {t. (∀P. sound P ⟶ sound (t P)) ∧ le_trans (T t) t}"

lemma lfp_trans_lowerbound:
  "⟦ le_trans (T t) t; ⋀P. sound P ⟹ sound (t P) ⟧ ⟹ le_trans (lfp_trans T) t"
  unfolding lfp_trans_def
  by(auto intro:Inf_trans_lower)

lemma lfp_trans_greatest:
  "⟦ ⋀t P. ⟦ le_trans (T t) t; ⋀P. sound P ⟹ sound (t P) ⟧ ⟹ le_trans u t;
     ⋀P. sound P ⟹ sound (v P); le_trans (T v) v ⟧ ⟹
   le_trans u (lfp_trans T)"
  unfolding lfp_trans_def by(rule Inf_trans_greatest, auto)

lemma lfp_trans_sound:
  fixes P Q::"'s expect"
  assumes sP: "sound P"
      and fv: "le_trans (T v) v"
      and sv: "⋀P. sound P ⟹ sound (v P)"
  shows  "sound (lfp_trans T P)"
proof(intro soundI2 bounded_byI2 nnegI2)
  from fv sv have "le_trans (lfp_trans T) v"
    by(iprover intro:lfp_trans_lowerbound)
  with sP have "lfp_trans T P ⊩ v P" by(auto)
  also {
    from sv sP have "sound (v P)" by(iprover)
    hence "v P ⊩ λs. bound_of (v P)" by(auto)
  }
  finally show "lfp_trans T P ⊩ λs. bound_of (v P)" .

  have "le_trans (λP s. 0) (lfp_trans T)"
  proof(intro lfp_trans_greatest)
    fix t::"'s trans"
    assume "⋀P. sound P ⟹ sound (t P)"
    hence "⋀P. sound P ⟹ λs. 0 ⊩ t P" by(auto)
    thus "le_trans (λP s. 0) t" by(auto)
  next
    fix P::"'s expect"
    assume "sound P" thus "sound (v P)" by(rule sv)
  next
    show "le_trans (T v) v" by(rule fv)
  qed
  with sP show "λs. 0 ⊩ lfp_trans T P" by(auto)
qed

lemma lfp_trans_unitary:
  fixes P Q::"'s expect"
  assumes uP: "unitary P"
      and fv: "le_trans (T v) v"
      and sv: "⋀P. sound P ⟹ sound (v P)"
      and fT: "le_trans (T (λP s. bound_of P)) (λP s. bound_of P)"
  shows  "unitary (lfp_trans T P)"
proof(rule unitaryI)
  from unitary_sound[OF uP] fv sv show "sound (lfp_trans T P)"
    by(rule lfp_trans_sound)

  show "bounded_by 1 (lfp_trans T P)"
  proof(rule bounded_byI2)
    from fT have "le_trans (lfp_trans T) (λP s. bound_of P)"
      by(auto intro: lfp_trans_lowerbound)
    with uP have "lfp_trans T P ⊩ λs. bound_of P" by(auto)
    also from uP have "... ⊩ λs. 1" by(auto)
    finally show "lfp_trans T P ⊩ λs. 1" .
  qed
qed

lemma lfp_trans_lemma2:
  fixes v::"'s trans"
  assumes mono: "⋀t u. ⟦ le_trans t u; ⋀P. sound P ⟹ sound (t P);
                         ⋀P. sound P ⟹ sound (u P) ⟧ ⟹ le_trans (T t) (T u)"
      and nT:   "⋀t P. ⟦ ⋀Q. sound Q ⟹ sound (t Q); sound P ⟧ ⟹ sound (T t P)"
      and fv:   "le_trans (T v) v"
      and sv:   "⋀P. sound P ⟹ sound (v P)"
  shows "le_trans (T (lfp_trans T)) (lfp_trans T)"
proof(rule lfp_trans_greatest[where T=T and v=v], simp_all add:assms)
  fix t::"'s trans" and P::"'s expect"
  assume ft: "le_trans (T t) t" and st: "⋀P. sound P ⟹ sound (t P)"
  hence "le_trans (lfp_trans T) t" by(auto intro!:lfp_trans_lowerbound)
  with ft st have "le_trans (T (lfp_trans T)) (T t)"
    by(iprover intro:mono lfp_trans_sound fv sv)
  also note ft
  finally show "le_trans (T (lfp_trans T)) t" .
qed

lemma lfp_trans_lemma3:
  fixes v::"'s trans"
  assumes mono: "⋀t u. ⟦ le_trans t u; ⋀P. sound P ⟹ sound (t P);
                         ⋀P. sound P ⟹ sound (u P) ⟧ ⟹ le_trans (T t) (T u)"
      and sT:   "⋀t P. ⟦ ⋀Q. sound Q ⟹ sound (t Q); sound P ⟧ ⟹ sound (T t P)"
      and fv:   "le_trans (T v) v"
      and sv:   "⋀P. sound P ⟹ sound (v P)"
  shows "le_trans (lfp_trans T) (T (lfp_trans T))"
proof(rule lfp_trans_lowerbound)
  fix P::"'s expect"
  assume sP: "sound P"
  have n1: "⋀P. sound P ⟹ sound (lfp_trans T P)"
    by(iprover intro:lfp_trans_sound fv sv)
  with sP have n2: "sound (lfp_trans T P)"
    by(iprover intro:lfp_trans_sound fv sv sT)
  with n1 sP show n3: "sound (T (lfp_trans T) P)"
    by(iprover intro: sT)
  next
  show "le_trans (T (T (lfp_trans T))) (T (lfp_trans T))"
    by(rule mono[OF lfp_trans_lemma2, OF mono],
            (iprover intro:assms lfp_trans_sound)+)
qed

lemma lfp_trans_unfold:
  fixes P::"'s expect"
  assumes mono: "⋀t u. ⟦ le_trans t u; ⋀P. sound P ⟹ sound (t P);
                         ⋀P. sound P ⟹ sound (u P) ⟧ ⟹ le_trans (T t) (T u)"
      and sT:   "⋀t P. ⟦ ⋀Q. sound Q ⟹ sound (t Q); sound P ⟧ ⟹ sound (T t P)"
      and fv:   "le_trans (T v) v"
      and sv:   "⋀P. sound P ⟹ sound (v P)"
  shows "equiv_trans (lfp_trans T) (T (lfp_trans T))"
  by(rule le_trans_antisym,
     rule lfp_trans_lemma3[OF mono], (iprover intro:assms)+,
     rule lfp_trans_lemma2[OF mono], (iprover intro:assms)+)

definition gfp_trans :: "('s trans ⇒ 's trans) ⇒ 's trans"
where "gfp_trans T = Sup_trans {t. (∀P. unitary P ⟶ unitary (t P)) ∧ le_utrans t (T t)}"

lemma gfp_trans_upperbound:
  "⟦ le_utrans t (T t); ⋀P. unitary P ⟹ unitary (t P) ⟧ ⟹ le_utrans t (gfp_trans T)"
  unfolding gfp_trans_def by(auto intro:Sup_trans_upper)

lemma gfp_trans_least:
  "⟦ ⋀t. ⟦ le_utrans t (T t); ⋀P. unitary P ⟹ unitary (t P) ⟧ ⟹ le_utrans t u;
     ⋀P. unitary P ⟹ unitary (u P) ⟧ ⟹
   le_utrans (gfp_trans T) u"
  unfolding gfp_trans_def by(auto intro:Sup_trans_least)

lemma gfp_trans_unitary:
  fixes P::"'s expect"
  assumes uP: "unitary P"
  shows "unitary (gfp_trans T P)"
proof(intro unitaryI2 nnegI2 bounded_byI2)
  show "gfp_trans T P ⊩ λs. 1"
  unfolding gfp_trans_def Sup_trans_def
  proof(rule Sup_exp_least, clarify)
    fix t::"'s trans"
    assume "∀P. unitary P ⟶ unitary (t P)"
    with uP have "unitary (t P)" by(auto)
    thus "t P ⊩ λs. 1" by(auto)
  next
    show "nneg (λs. 1::real)" by(auto)
  qed
  let ?S = "{t P |t. t ∈ {t. (∀P. unitary P ⟶ unitary (t P)) ∧ le_utrans t (T t)}}"
  show "λs. 0 ⊩ gfp_trans T P"
  unfolding gfp_trans_def Sup_trans_def
  proof(cases)
    assume empty: "?S = {}"
    show "λs. 0 ⊩ Sup_exp ?S"
      by(simp only:empty Sup_exp_def, auto)
  next
    assume "?S ≠ {}"
    then obtain Q where Qin: "Q ∈ ?S" by(auto)
    with uP have "unitary Q" by(auto)
    hence "λs. 0 ⊩ Q" by(auto)
    also with uP Qin have "Q ⊩ Sup_exp ?S"
    proof(intro Sup_exp_upper, blast, clarify)
      fix t::"'s trans"
      assume "∀Q. unitary Q ⟶ unitary (t Q)"
      with uP show "bounded_by 1 (t P)" by(auto)
    qed
    finally show "λs. 0 ⊩ Sup_exp ?S" .
  qed
qed

lemma gfp_trans_lemma2:
  assumes mono: "⋀t u. ⟦ le_utrans t u; ⋀P. unitary P ⟹ unitary (t P);
                         ⋀P. unitary P ⟹ unitary (u P) ⟧ ⟹ le_utrans (T t) (T u)"
      and hT:   "⋀t P. ⟦ ⋀Q. unitary Q ⟹ unitary (t Q); unitary P ⟧ ⟹ unitary (T t P)"
  shows "le_utrans (gfp_trans T) (T (gfp_trans T))"
proof(rule gfp_trans_least, simp_all add:hT gfp_trans_unitary)
  fix t
  assume fp: "le_utrans t (T t)" and ht: "⋀P. unitary P ⟹ unitary (t P)"

  note fp
  also {
    from fp ht have "le_utrans t (gfp_trans T)"by(rule gfp_trans_upperbound)
    moreover note ht gfp_trans_unitary
    ultimately have "le_utrans (T t) (T (gfp_trans T))" by(rule mono)
  }
  finally show "le_utrans t (T (gfp_trans T))" .
qed

lemma gfp_trans_lemma3:
  assumes mono: "⋀t u. ⟦ le_utrans t u; ⋀P. unitary P ⟹ unitary (t P);
                         ⋀P. unitary P ⟹ unitary (u P) ⟧ ⟹ le_utrans (T t) (T u)"
      and hT:   "⋀t P. ⟦ ⋀Q. unitary Q ⟹ unitary (t Q); unitary P ⟧ ⟹ unitary (T t P)"
  shows "le_utrans (T (gfp_trans T)) (gfp_trans T)"
  by(blast intro!:mono gfp_trans_unitary gfp_trans_upperbound gfp_trans_lemma2 mono hT)

lemma gfp_trans_unfold:
  assumes mono: "⋀t u. ⟦ le_utrans t u; ⋀P. unitary P ⟹ unitary (t P);
                         ⋀P. unitary P ⟹ unitary (u P) ⟧ ⟹ le_utrans (T t) (T u)"
      and hT:   "⋀t P. ⟦ ⋀Q. unitary Q ⟹ unitary (t Q); unitary P ⟧ ⟹ unitary (T t P)"
  shows "equiv_utrans (gfp_trans T) (T (gfp_trans T))"
  using assms by(auto intro!: le_utrans_antisym gfp_trans_lemma2 gfp_trans_lemma3)

subsection ‹Tail Recursion›

text_raw ‹\label{s:tail}›

text ‹The least (greatest) fixed point of a tail-recursive expression on transformers is
equivalent (given appropriate side conditions) to the least (greatest) fixed point on
expectations.›

lemma gfp_pulldown:
  fixes P::"'s expect"
  assumes tailcall:  "⋀u P. unitary P ⟹ T u P = t P (u P)"
      and fT:        "⋀t P. ⟦ ⋀Q. unitary Q ⟹ unitary (t Q); unitary P ⟧ ⟹ unitary (T t P)"
      and ft:        "⋀P Q. unitary P ⟹ unitary Q ⟹ unitary (t P Q)"
      and mt:        "⋀P Q R. ⟦ unitary P; unitary Q; unitary R; Q ⊩ R ⟧ ⟹ t P Q ⊩ t P R"
      and uP:        "unitary P"
      and monoT:     "⋀t u. ⟦ le_utrans t u; ⋀P. unitary P ⟹ unitary (t P);
                              ⋀P. unitary P ⟹ unitary (u P) ⟧ ⟹ le_utrans (T t) (T u)"
  shows "gfp_trans T P = gfp_exp (t P)" (is "?X P = ?Y P")
proof(rule antisym)
  show "?X P ≤ ?Y P"
  proof(rule gfp_exp_upperbound)
    from monoT fT uP have "(gfp_trans T) P ≤ (T (gfp_trans T)) P"
      by(auto intro!: le_utransD[OF gfp_trans_lemma2])
    also from uP have "(T (gfp_trans T)) P = t P (gfp_trans T P)" by(rule tailcall)
    finally show "gfp_trans T P ⊩ t P (gfp_trans T P)" .
    from uP gfp_trans_unitary show "unitary (gfp_trans T P)" by(auto)
  qed
  show "?Y P ≤ ?X P"
  proof(rule le_utransD[OF gfp_trans_upperbound], simp_all add:assms)
    show "le_utrans (λa. gfp_exp (t a)) (T (λa. gfp_exp (t a)))"
    proof(rule le_utransI)
      fix Q::"'s expect" assume uQ: "unitary Q"
      with ft have "⋀R. unitary R ⟹ unitary (t Q R)" by(auto)
      with mt[OF uQ] have "gfp_exp (t Q) = t Q (gfp_exp (t Q))" by(blast intro:gfp_exp_unfold)
      also from uQ have "... = T (λa. gfp_exp (t a)) Q" by(rule tailcall[symmetric])
      finally show "gfp_exp (t Q) ≤ T (λa. gfp_exp (t a)) Q" by(simp)
    qed
    fix Q::"'s expect" assume "unitary Q"
    with ft have "⋀R. unitary R ⟹ unitary (t Q R)" by(auto)
    thus "unitary (gfp_exp (t Q))" by(rule gfp_exp_unitary)
  qed
qed

lemma lfp_pulldown:
  fixes P::"'s expect" and t::"'s expect ⇒ 's trans"
    and T::"'s trans ⇒ 's trans"
  assumes tailcall:  "⋀u P. sound P ⟹ T u P = t P (u P)"
      and st:        "⋀P Q. sound P ⟹ sound Q ⟹ sound (t P Q)"
      and mt:        "⋀P. sound P ⟹ mono_trans (t P)"
      and monoT: "⋀t u. ⟦ le_trans t u; ⋀P. sound P ⟹ sound (t P);
                          ⋀P. sound P ⟹ sound (u P) ⟧ ⟹ le_trans (T t) (T u)"
      and nT:   "⋀t P. ⟦ ⋀Q. sound Q ⟹ sound (t Q); sound P ⟧ ⟹ sound (T t P)"
      and fv:   "le_trans (T v) v"
      and sv:   "⋀P. sound P ⟹ sound (v P)"
      and sP:   "sound P"
  shows "lfp_trans T P = lfp_exp (t P)" (is "?X P = ?Y P")
proof(rule antisym)
  show "?Y P ≤ ?X P"
  proof(rule lfp_exp_lowerbound)
    from sP have "t P (lfp_trans T P) = (T (lfp_trans T)) P" by(rule tailcall[symmetric])
    also have "(T (lfp_trans T)) P ≤ (lfp_trans T) P"
      by(rule le_transD[OF lfp_trans_lemma2[OF monoT]], (iprover intro:assms)+)
    finally show "t P (lfp_trans T P) ≤ lfp_trans T P" .
    from sP show "sound (lfp_trans T P)"
      by(iprover intro:lfp_trans_sound assms)
  qed

  have "⋀P. sound P ⟹ t P (v P) = T v P" by(simp add:tailcall)
  also have "⋀P. sound P ⟹ ... P ⊩ v P" by(auto intro:le_transD[OF fv])
  finally have fvP: "⋀P. sound P ⟹ t P (v P) ⊩ v P" .
  have svP: "⋀P. sound P ⟹ sound (v P)" by(rule sv)

  show "?X P ≤ ?Y P"
  proof(rule le_transD[OF lfp_trans_lowerbound, OF _ _ sP])
    show "le_trans (T (λa. lfp_exp (t a))) (λa. lfp_exp (t a))"
    proof(rule le_transI)
      fix P::"'s expect"
      assume sP: "sound P"

      from sP have "T (λa. lfp_exp (t a)) P = t P (lfp_exp (t P))" by(rule tailcall)
      also have "t P (lfp_exp (t P)) = lfp_exp (t P)"
        by(iprover intro: lfp_exp_unfold[symmetric] sP st mt fvP svP)
      finally show "T (λa. lfp_exp (t a)) P ⊩ lfp_exp (t P)" by(simp)
    qed
    fix P::"'s expect"
    assume "sound P"
    with fvP svP show "sound (lfp_exp (t P))"
      by(blast intro:lfp_exp_sound)
  qed
qed

definition Inf_utrans :: "'s trans set ⇒ 's trans"
where "Inf_utrans S = (if S = {} then λP s. 1 else Inf_trans S)"

lemma Inf_utrans_lower:
  "⟦ t ∈ S; ∀t∈S. ∀P. unitary P ⟶ unitary (t P) ⟧ ⟹ le_utrans (Inf_utrans S) t"
  unfolding Inf_utrans_def
  by(cases "S={}",
     auto intro!:le_utransI Inf_exp_lower sound_nneg unitary_sound
          simp:Inf_trans_def)

lemma Inf_utrans_greatest:
  "⟦ ⋀P. unitary P ⟹ unitary (t P); ∀u∈S. le_utrans t u ⟧ ⟹ le_utrans t (Inf_utrans S)"
  unfolding Inf_utrans_def Inf_trans_def
  by(cases "S={}", simp_all, (blast intro!:le_utransI Inf_exp_greatest)+)

end