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 add: mrec.psimps) |
|
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 fastforce |
|
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 fastforce |
|
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 simp: mrec.psimps) |
|
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 fastforce |
|
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 simp: mrec.psimps) |
|
126 next |
|
127 case None |
|
128 from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by (auto simp: mrec.psimps) |
|
129 qed |
|
130 qed |
|
131 next |
|
132 case None |
|
133 from this 1(1) mrec 1(3) show ?thesis by (simp add: mrec.psimps) |
|
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 "effect (MREC f g x) h h' r" |
|
149 assumes "\<And> x h h' r. effect (f x) h h' (Inl r) \<Longrightarrow> P x h h' r" |
|
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 |
|
151 \<Longrightarrow> effect (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 effect_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 effect_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 effect_def]) |
|
163 |
|
164 end |
|