src/HOL/Imperative_HOL/Mrec.thy
author wenzelm
Thu May 24 17:25:53 2012 +0200 (2012-05-24)
changeset 47988 e4b69e10b990
parent 44890 22f665a2e91c
permissions -rw-r--r--
tuned proofs;
haftmann@37772
     1
theory Mrec
haftmann@37772
     2
imports Heap_Monad
haftmann@37772
     3
begin
haftmann@37772
     4
haftmann@37772
     5
subsubsection {* A monadic combinator for simple recursive functions *}
haftmann@37772
     6
haftmann@37772
     7
text {* Using a locale to fix arguments f and g of MREC *}
haftmann@37772
     8
haftmann@37772
     9
locale mrec =
haftmann@37772
    10
  fixes f :: "'a \<Rightarrow> ('b + 'a) Heap"
haftmann@37772
    11
  and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b Heap"
haftmann@37772
    12
begin
haftmann@37772
    13
haftmann@37772
    14
function (default "\<lambda>(x, h). None") mrec :: "'a \<Rightarrow> heap \<Rightarrow> ('b \<times> heap) option" where
haftmann@37772
    15
  "mrec x h = (case execute (f x) h of
haftmann@37772
    16
     Some (Inl r, h') \<Rightarrow> Some (r, h')
haftmann@37772
    17
   | Some (Inr s, h') \<Rightarrow> (case mrec s h' of
haftmann@37772
    18
             Some (z, h'') \<Rightarrow> execute (g x s z) h''
haftmann@37772
    19
           | None \<Rightarrow> None)
haftmann@37772
    20
   | None \<Rightarrow> None)"
haftmann@37772
    21
by auto
haftmann@37772
    22
haftmann@37772
    23
lemma graph_implies_dom:
haftmann@37772
    24
  "mrec_graph x y \<Longrightarrow> mrec_dom x"
haftmann@37772
    25
apply (induct rule:mrec_graph.induct) 
haftmann@37772
    26
apply (rule accpI)
haftmann@37772
    27
apply (erule mrec_rel.cases)
haftmann@37772
    28
by simp
haftmann@37772
    29
haftmann@37772
    30
lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = None"
haftmann@37772
    31
  unfolding mrec_def 
haftmann@37772
    32
  by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified])
haftmann@37772
    33
haftmann@37772
    34
lemma mrec_di_reverse: 
haftmann@37772
    35
  assumes "\<not> mrec_dom (x, h)"
haftmann@37772
    36
  shows "
haftmann@37772
    37
   (case execute (f x) h of
haftmann@37772
    38
     Some (Inl r, h') \<Rightarrow> False
haftmann@37772
    39
   | Some (Inr s, h') \<Rightarrow> \<not> mrec_dom (s, h')
haftmann@37772
    40
   | None \<Rightarrow> False
haftmann@37772
    41
   )" 
haftmann@37772
    42
using assms apply (auto split: option.split sum.split)
haftmann@37772
    43
apply (rule ccontr)
haftmann@37772
    44
apply (erule notE, rule accpI, elim mrec_rel.cases, auto)+
haftmann@37772
    45
done
haftmann@37772
    46
haftmann@37772
    47
lemma mrec_rule:
haftmann@37772
    48
  "mrec x h = 
haftmann@37772
    49
   (case execute (f x) h of
haftmann@37772
    50
     Some (Inl r, h') \<Rightarrow> Some (r, h')
haftmann@37772
    51
   | Some (Inr s, h') \<Rightarrow> 
haftmann@37772
    52
          (case mrec s h' of
haftmann@37772
    53
             Some (z, h'') \<Rightarrow> execute (g x s z) h''
haftmann@37772
    54
           | None \<Rightarrow> None)
haftmann@37772
    55
   | None \<Rightarrow> None
haftmann@37772
    56
   )"
krauss@39754
    57
apply (cases "mrec_dom (x,h)", simp add: mrec.psimps)
haftmann@37772
    58
apply (frule mrec_default)
haftmann@37772
    59
apply (frule mrec_di_reverse, simp)
haftmann@37772
    60
by (auto split: sum.split option.split simp: mrec_default)
haftmann@37772
    61
haftmann@37772
    62
definition
haftmann@37772
    63
  "MREC x = Heap_Monad.Heap (mrec x)"
haftmann@37772
    64
haftmann@37772
    65
lemma MREC_rule:
haftmann@37772
    66
  "MREC x = 
krauss@37792
    67
  do { y \<leftarrow> f x;
haftmann@37772
    68
                (case y of 
haftmann@37772
    69
                Inl r \<Rightarrow> return r
haftmann@37772
    70
              | Inr s \<Rightarrow> 
krauss@37792
    71
                do { z \<leftarrow> MREC s ;
krauss@37792
    72
                     g x s z })}"
haftmann@37772
    73
  unfolding MREC_def
haftmann@37772
    74
  unfolding bind_def return_def
haftmann@37772
    75
  apply simp
haftmann@37772
    76
  apply (rule ext)
haftmann@37772
    77
  apply (unfold mrec_rule[of x])
haftmann@37787
    78
  by (auto simp add: execute_simps split: option.splits prod.splits sum.splits)
haftmann@37772
    79
haftmann@37772
    80
lemma MREC_pinduct:
haftmann@37772
    81
  assumes "execute (MREC x) h = Some (r, h')"
haftmann@37772
    82
  assumes non_rec_case: "\<And> x h h' r. execute (f x) h = Some (Inl r, h') \<Longrightarrow> P x h h' r"
haftmann@37772
    83
  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
haftmann@37772
    84
    \<Longrightarrow> execute (g x s z) h2 = Some (r, h') \<Longrightarrow> P x h h' r"
haftmann@37772
    85
  shows "P x h h' r"
haftmann@37772
    86
proof -
haftmann@37772
    87
  from assms(1) have mrec: "mrec x h = Some (r, h')"
haftmann@37772
    88
    unfolding MREC_def execute.simps .
haftmann@37772
    89
  from mrec have dom: "mrec_dom (x, h)"
haftmann@37772
    90
    apply -
haftmann@37772
    91
    apply (rule ccontr)
haftmann@37772
    92
    apply (drule mrec_default) by auto
haftmann@37772
    93
  from mrec have h'_r: "h' = snd (the (mrec x h))" "r = fst (the (mrec x h))"
haftmann@37772
    94
    by auto
haftmann@37772
    95
  from mrec have "P x h (snd (the (mrec x h))) (fst (the (mrec x h)))"
haftmann@37772
    96
  proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom])
haftmann@37772
    97
    case (1 x h)
nipkow@44890
    98
    obtain rr h' where "the (mrec x h) = (rr, h')" by fastforce
haftmann@37772
    99
    show ?case
haftmann@37772
   100
    proof (cases "execute (f x) h")
haftmann@37772
   101
      case (Some result)
nipkow@44890
   102
      then obtain a h1 where exec_f: "execute (f x) h = Some (a, h1)" by fastforce
haftmann@37772
   103
      note Inl' = this
haftmann@37772
   104
      show ?thesis
haftmann@37772
   105
      proof (cases a)
haftmann@37772
   106
        case (Inl aa)
haftmann@37772
   107
        from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis
krauss@39754
   108
          by (auto simp: mrec.psimps)
haftmann@37772
   109
      next
haftmann@37772
   110
        case (Inr b)
haftmann@37772
   111
        note Inr' = this
haftmann@37772
   112
        show ?thesis
haftmann@37772
   113
        proof (cases "mrec b h1")
haftmann@37772
   114
          case (Some result)
nipkow@44890
   115
          then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastforce
haftmann@37772
   116
          moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
haftmann@37772
   117
            apply (intro 1(2))
haftmann@37772
   118
            apply (auto simp add: Inr Inl')
haftmann@37772
   119
            done
haftmann@37772
   120
          moreover note mrec mrec_rec exec_f Inl' Inr' 1(1) 1(3)
haftmann@37772
   121
          ultimately show ?thesis
haftmann@37772
   122
            apply auto
haftmann@37772
   123
            apply (rule rec_case)
haftmann@37772
   124
            apply auto
krauss@39754
   125
            unfolding MREC_def by (auto simp: mrec.psimps)
haftmann@37772
   126
        next
haftmann@37772
   127
          case None
krauss@39754
   128
          from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by (auto simp: mrec.psimps)
haftmann@37772
   129
        qed
haftmann@37772
   130
      qed
haftmann@37772
   131
    next
haftmann@37772
   132
      case None
krauss@39754
   133
      from this 1(1) mrec 1(3) show ?thesis by (simp add: mrec.psimps)
haftmann@37772
   134
    qed
haftmann@37772
   135
  qed
haftmann@37772
   136
  from this h'_r show ?thesis by simp
haftmann@37772
   137
qed
haftmann@37772
   138
haftmann@37772
   139
end
haftmann@37772
   140
haftmann@37772
   141
text {* Providing global versions of the constant and the theorems *}
haftmann@37772
   142
haftmann@37772
   143
abbreviation "MREC == mrec.MREC"
haftmann@37772
   144
lemmas MREC_rule = mrec.MREC_rule
haftmann@37772
   145
lemmas MREC_pinduct = mrec.MREC_pinduct
haftmann@37772
   146
haftmann@37772
   147
lemma MREC_induct:
haftmann@40671
   148
  assumes "effect (MREC f g x) h h' r"
haftmann@40671
   149
  assumes "\<And> x h h' r. effect (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
haftmann@40671
   150
  assumes "\<And> x h h1 h2 h' s z r. effect (f x) h h1 (Inr s) \<Longrightarrow> effect (MREC f g s) h1 h2 z \<Longrightarrow> P s h1 h2 z
haftmann@40671
   151
    \<Longrightarrow> effect (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
haftmann@37772
   152
  shows "P x h h' r"
haftmann@40671
   153
proof (rule MREC_pinduct[OF assms(1) [unfolded effect_def]])
haftmann@37772
   154
  fix x h h1 h2 h' s z r
haftmann@37772
   155
  assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)"
haftmann@37772
   156
    "Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)"
haftmann@37772
   157
    "P s h1 h2 z"
haftmann@37772
   158
    "Heap_Monad.execute (g x s z) h2 = Some (r, h')"
haftmann@40671
   159
  from assms(3) [unfolded effect_def, OF this(1) this(2) this(3) this(4)]
haftmann@37772
   160
  show "P x h h' r" .
haftmann@37772
   161
next
haftmann@40671
   162
qed (auto simp add: assms(2)[unfolded effect_def])
haftmann@37772
   163
haftmann@37772
   164
end