theory Escalate

imports Main

begin

text {* This is the function escalate. It's not particularly useful,
but a lot of other graph functions can be similar. *}

function
  escalate :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
  "escalate m lim n = (if n \<ge> lim then n else escalate m lim (m n))"
by pat_completeness auto

print_theorems
find_theorems name: escalate
text {* There are not many useful theorems produced yet.
Partial simp and induct rules, which might be useful, if
there was any way to prove anything was in the domain. But
how? *}

text {* OK, it happens I remember how to get around the
theorem hiding and see what's really out there. *}
ML {*
Global_Theory.facts_of @{theory}
  |> Facts.dest_static true []
  |> filter (fn (s, _) => can (unprefix "Escalate.esc") s)
  |> map fst |> commas
*}

text {* Here's an important (hidden) rule. We can use it to prove that
escalate terminates everywhere. A pity it doesn't. *}
thm escalate.termination

text {* This is an example domain, easy to reason about, on which
I expect escalate to terminate. *}
definition
  escalate_known_dom :: "(nat \<Rightarrow> nat) \<times> nat \<times> nat \<Rightarrow> bool"
where
  "escalate_known_dom \<equiv> \<lambda>(m, l, n). \<exists>S. n \<in> S \<and> (\<forall>i \<in> S. m i \<in> S \<and> m i > i)"

text {* Here's what we need to prove. But we don't have any theorems
about escalate_dom. *}
lemma escalate_known_dom:
  "escalate_known_dom v \<Longrightarrow> escalate_dom v"
  apply (simp add: accp_eq_acc)
  oops

text {* OK, using the ML level lets us "see through" the abbreviation,
and realise that escalate_dom is just syntax for "accp escalate_rel". *}
ML {* @{term escalate_dom} *}

text {* Here's the key low-level rule which tells us what elements are
in escalate_rel. Now we can get to work. *}
thm escalate_rel.cases

text {* Unfortunately, we need to prove something about accp
(the accessible part of the relation) but all the useful rules are
about wf (well-foundedness of a relation). Various theorems tell us
that a relation is well-founded if it is accessible everywhere. But
we don't want to prove it is accessible everywhere, just within
some well-behaved region.

Fast-forward a little, we need a new rule about Wellfounded.acc and
wf, one which allows us to also use an invariant. The idea is to show
that an element is in the accessible part if it satisfies the
invariant, if the invariant is always preserved by (leftward) steps
in the relation, and if the subset of the relation within the
invariant is well-founded. Once phrased correctly, the proof is easy.
*}

lemma acc_invariant_wf_pointwise:
  assumes inv: "\<And>x y. (x, y) \<in> r \<Longrightarrow> y \<in> I \<Longrightarrow> x \<in> I"
  assumes wf: "wf (r \<inter> (I \<times> I))"
  assumes x: "x \<in> I"
  shows "x \<in> Wellfounded.acc r"
  using wf x
  apply (induct rule: wf_induct[consumes 1])
  apply simp
  apply (rule accI)
  apply (metis inv)
  done

text {* Let's rephrase this in predicate form, with an unknown
well-founded relation to be supplied (as in escalate.termination). *}
lemma accp_invariant_wf_R:
  "\<lbrakk> I x; wf R; \<And>x y. r x y \<Longrightarrow> I y \<Longrightarrow> I x \<and> (x, y) \<in> R \<rbrakk>
    \<Longrightarrow> Wellfounded.accp r x"
  apply (simp add: accp_eq_acc)
  apply (rule acc_invariant_wf_pointwise[where I="{x. I x}"], simp_all)
  apply (erule wf_subset)
  apply clarsimp
  done

text {* Now we can apply this to escalate. *}
lemma escalate_known_dom:
  "escalate_known_dom v \<Longrightarrow> escalate_dom v"
  apply (erule_tac I=escalate_known_dom and R="measure (\<lambda>(m, l, n). l - n)"
    in accp_invariant_wf_R)
   apply (rule wf_measure)
  apply (erule escalate_rel.cases)
  apply (auto simp: escalate_known_dom_def)[1]
  done

text {* Now we can prove a silly property about escalate. *}
lemma escalate_even:
  assumes even: "\<forall>i. even i \<longrightarrow> even (m i)"
  assumes inc: "\<forall>i. even i \<longrightarrow> m i > i"
  assumes n: "even n"
  shows "even (escalate m l n)"
  using even n
proof (induct m l n rule: escalate.pinduct[OF escalate_known_dom])
  case 1
  show ?case
    apply (simp add: escalate_known_dom_def)
    apply (rule exI[where x="{i. even i}"])
    apply (simp add: n even inc)
    done
next
  case (2 m l n)
  then show ?case
    by (clarsimp simp: escalate.psimps)
qed

text {* It would be nice to have a partial termination rule,
similar to the termination rule, available generally for this
use case. This nonsense generates a rule that's a lot like a
partial termination rule. *}
ML {*
val pterm = @{thm accp_invariant_wf_R[where r=escalate_rel]}
  |> eresolve_tac @{context} @{thms escalate_rel.cases} 3
  |> Seq.hd
val pterm_simp = pterm
  |> bound_hyp_subst_tac @{context} 3
  |> Seq.hd
  |> rewrite_rule @{context} [@{thm triv_forall_equality}]
val term = @{thm escalate.termination}
*}

end