37772
|
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 |
done) done)"
|
|
74 |
unfolding MREC_def
|
|
75 |
unfolding bind_def return_def
|
|
76 |
apply simp
|
|
77 |
apply (rule ext)
|
|
78 |
apply (unfold mrec_rule[of x])
|
|
79 |
by (auto split: option.splits prod.splits sum.splits)
|
|
80 |
|
|
81 |
lemma MREC_pinduct:
|
|
82 |
assumes "execute (MREC x) h = Some (r, h')"
|
|
83 |
assumes non_rec_case: "\<And> x h h' r. execute (f x) h = Some (Inl r, h') \<Longrightarrow> P x h h' r"
|
|
84 |
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
|
|
85 |
\<Longrightarrow> execute (g x s z) h2 = Some (r, h') \<Longrightarrow> P x h h' r"
|
|
86 |
shows "P x h h' r"
|
|
87 |
proof -
|
|
88 |
from assms(1) have mrec: "mrec x h = Some (r, h')"
|
|
89 |
unfolding MREC_def execute.simps .
|
|
90 |
from mrec have dom: "mrec_dom (x, h)"
|
|
91 |
apply -
|
|
92 |
apply (rule ccontr)
|
|
93 |
apply (drule mrec_default) by auto
|
|
94 |
from mrec have h'_r: "h' = snd (the (mrec x h))" "r = fst (the (mrec x h))"
|
|
95 |
by auto
|
|
96 |
from mrec have "P x h (snd (the (mrec x h))) (fst (the (mrec x h)))"
|
|
97 |
proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom])
|
|
98 |
case (1 x h)
|
|
99 |
obtain rr h' where "the (mrec x h) = (rr, h')" by fastsimp
|
|
100 |
show ?case
|
|
101 |
proof (cases "execute (f x) h")
|
|
102 |
case (Some result)
|
|
103 |
then obtain a h1 where exec_f: "execute (f x) h = Some (a, h1)" by fastsimp
|
|
104 |
note Inl' = this
|
|
105 |
show ?thesis
|
|
106 |
proof (cases a)
|
|
107 |
case (Inl aa)
|
|
108 |
from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis
|
|
109 |
by auto
|
|
110 |
next
|
|
111 |
case (Inr b)
|
|
112 |
note Inr' = this
|
|
113 |
show ?thesis
|
|
114 |
proof (cases "mrec b h1")
|
|
115 |
case (Some result)
|
|
116 |
then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastsimp
|
|
117 |
moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
|
|
118 |
apply (intro 1(2))
|
|
119 |
apply (auto simp add: Inr Inl')
|
|
120 |
done
|
|
121 |
moreover note mrec mrec_rec exec_f Inl' Inr' 1(1) 1(3)
|
|
122 |
ultimately show ?thesis
|
|
123 |
apply auto
|
|
124 |
apply (rule rec_case)
|
|
125 |
apply auto
|
|
126 |
unfolding MREC_def by auto
|
|
127 |
next
|
|
128 |
case None
|
|
129 |
from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by auto
|
|
130 |
qed
|
|
131 |
qed
|
|
132 |
next
|
|
133 |
case None
|
|
134 |
from this 1(1) mrec 1(3) show ?thesis by simp
|
|
135 |
qed
|
|
136 |
qed
|
|
137 |
from this h'_r show ?thesis by simp
|
|
138 |
qed
|
|
139 |
|
|
140 |
end
|
|
141 |
|
|
142 |
text {* Providing global versions of the constant and the theorems *}
|
|
143 |
|
|
144 |
abbreviation "MREC == mrec.MREC"
|
|
145 |
lemmas MREC_rule = mrec.MREC_rule
|
|
146 |
lemmas MREC_pinduct = mrec.MREC_pinduct
|
|
147 |
|
|
148 |
lemma MREC_induct:
|
|
149 |
assumes "crel (MREC f g x) h h' r"
|
|
150 |
assumes "\<And> x h h' r. crel (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
|
|
151 |
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
|
|
152 |
\<Longrightarrow> crel (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
|
|
153 |
shows "P x h h' r"
|
|
154 |
proof (rule MREC_pinduct[OF assms(1) [unfolded crel_def]])
|
|
155 |
fix x h h1 h2 h' s z r
|
|
156 |
assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)"
|
|
157 |
"Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)"
|
|
158 |
"P s h1 h2 z"
|
|
159 |
"Heap_Monad.execute (g x s z) h2 = Some (r, h')"
|
|
160 |
from assms(3) [unfolded crel_def, OF this(1) this(2) this(3) this(4)]
|
|
161 |
show "P x h h' r" .
|
|
162 |
next
|
|
163 |
qed (auto simp add: assms(2)[unfolded crel_def])
|
|
164 |
|
|
165 |
end
|