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