src/HOL/Imperative_HOL/Mrec.thy

no longer declare .psimps rules as [simp].

This regularly caused confusion (e.g., they show up in simp traces
when the regular simp rules are disabled). In the few places where the
rules are used, explicitly mentioning them actually clarifies the
proof text.

theory Mrec
imports Heap_Monad
begin

subsubsection {* A monadic combinator for simple recursive functions *}

text {* Using a locale to fix arguments f and g of MREC *}

locale mrec =
  fixes f :: "'a \<Rightarrow> ('b + 'a) Heap"
  and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b Heap"
begin

function (default "\<lambda>(x, h). None") mrec :: "'a \<Rightarrow> heap \<Rightarrow> ('b \<times> heap) option" where
  "mrec x h = (case execute (f x) h of
     Some (Inl r, h') \<Rightarrow> Some (r, h')
   | Some (Inr s, h') \<Rightarrow> (case mrec s h' of
             Some (z, h'') \<Rightarrow> execute (g x s z) h''
           | None \<Rightarrow> None)
   | None \<Rightarrow> None)"
by auto

lemma graph_implies_dom:
  "mrec_graph x y \<Longrightarrow> mrec_dom x"
apply (induct rule:mrec_graph.induct) 
apply (rule accpI)
apply (erule mrec_rel.cases)
by simp

lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = None"
  unfolding mrec_def 
  by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified])

lemma mrec_di_reverse: 
  assumes "\<not> mrec_dom (x, h)"
  shows "
   (case execute (f x) h of
     Some (Inl r, h') \<Rightarrow> False
   | Some (Inr s, h') \<Rightarrow> \<not> mrec_dom (s, h')
   | None \<Rightarrow> False
   )" 
using assms apply (auto split: option.split sum.split)
apply (rule ccontr)
apply (erule notE, rule accpI, elim mrec_rel.cases, auto)+
done

lemma mrec_rule:
  "mrec x h = 
   (case execute (f x) h of
     Some (Inl r, h') \<Rightarrow> Some (r, h')
   | Some (Inr s, h') \<Rightarrow> 
          (case mrec s h' of
             Some (z, h'') \<Rightarrow> execute (g x s z) h''
           | None \<Rightarrow> None)
   | None \<Rightarrow> None
   )"
apply (cases "mrec_dom (x,h)", simp add: mrec.psimps)
apply (frule mrec_default)
apply (frule mrec_di_reverse, simp)
by (auto split: sum.split option.split simp: mrec_default)

definition
  "MREC x = Heap_Monad.Heap (mrec x)"

lemma MREC_rule:
  "MREC x = 
  do { y \<leftarrow> f x;
                (case y of 
                Inl r \<Rightarrow> return r
              | Inr s \<Rightarrow> 
                do { z \<leftarrow> MREC s ;
                     g x s z })}"
  unfolding MREC_def
  unfolding bind_def return_def
  apply simp
  apply (rule ext)
  apply (unfold mrec_rule[of x])
  by (auto simp add: execute_simps split: option.splits prod.splits sum.splits)

lemma MREC_pinduct:
  assumes "execute (MREC x) h = Some (r, h')"
  assumes non_rec_case: "\<And> x h h' r. execute (f x) h = Some (Inl r, h') \<Longrightarrow> P x h h' r"
  assumes rec_case: "\<And> x h h1 h2 h' s z r. execute (f x) h = Some (Inr s, h1) \<Longrightarrow> execute (MREC s) h1 = Some (z, h2) \<Longrightarrow> P s h1 h2 z
    \<Longrightarrow> execute (g x s z) h2 = Some (r, h') \<Longrightarrow> P x h h' r"
  shows "P x h h' r"
proof -
  from assms(1) have mrec: "mrec x h = Some (r, h')"
    unfolding MREC_def execute.simps .
  from mrec have dom: "mrec_dom (x, h)"
    apply -
    apply (rule ccontr)
    apply (drule mrec_default) by auto
  from mrec have h'_r: "h' = snd (the (mrec x h))" "r = fst (the (mrec x h))"
    by auto
  from mrec have "P x h (snd (the (mrec x h))) (fst (the (mrec x h)))"
  proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom])
    case (1 x h)
    obtain rr h' where "the (mrec x h) = (rr, h')" by fastsimp
    show ?case
    proof (cases "execute (f x) h")
      case (Some result)
      then obtain a h1 where exec_f: "execute (f x) h = Some (a, h1)" by fastsimp
      note Inl' = this
      show ?thesis
      proof (cases a)
        case (Inl aa)
        from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis
          by (auto simp: mrec.psimps)
      next
        case (Inr b)
        note Inr' = this
        show ?thesis
        proof (cases "mrec b h1")
          case (Some result)
          then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastsimp
          moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
            apply (intro 1(2))
            apply (auto simp add: Inr Inl')
            done
          moreover note mrec mrec_rec exec_f Inl' Inr' 1(1) 1(3)
          ultimately show ?thesis
            apply auto
            apply (rule rec_case)
            apply auto
            unfolding MREC_def by (auto simp: mrec.psimps)
        next
          case None
          from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by (auto simp: mrec.psimps)
        qed
      qed
    next
      case None
      from this 1(1) mrec 1(3) show ?thesis by (simp add: mrec.psimps)
    qed
  qed
  from this h'_r show ?thesis by simp
qed

end

text {* Providing global versions of the constant and the theorems *}

abbreviation "MREC == mrec.MREC"
lemmas MREC_rule = mrec.MREC_rule
lemmas MREC_pinduct = mrec.MREC_pinduct

lemma MREC_induct:
  assumes "crel (MREC f g x) h h' r"
  assumes "\<And> x h h' r. crel (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
  assumes "\<And> x h h1 h2 h' s z r. crel (f x) h h1 (Inr s) \<Longrightarrow> crel (MREC f g s) h1 h2 z \<Longrightarrow> P s h1 h2 z
    \<Longrightarrow> crel (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
  shows "P x h h' r"
proof (rule MREC_pinduct[OF assms(1) [unfolded crel_def]])
  fix x h h1 h2 h' s z r
  assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)"
    "Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)"
    "P s h1 h2 z"
    "Heap_Monad.execute (g x s z) h2 = Some (r, h')"
  from assms(3) [unfolded crel_def, OF this(1) this(2) this(3) this(4)]
  show "P x h h' r" .
next
qed (auto simp add: assms(2)[unfolded crel_def])

end