author  krauss 
Tue, 28 Sep 2010 09:54:07 +0200  
changeset 39754  150f831ce4a3 
parent 37792  ba0bc31b90d7 
child 40671  5e46057ba8e0 
permissions  rwrr 
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 
)" 

39754  57 
apply (cases "mrec_dom (x,h)", simp add: mrec.psimps) 
37772  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 = 

37792  67 
do { y \<leftarrow> f x; 
37772  68 
(case y of 
69 
Inl r \<Rightarrow> return r 

70 
 Inr s \<Rightarrow> 

37792  71 
do { z \<leftarrow> MREC s ; 
72 
g x s z })}" 

37772  73 
unfolding MREC_def 
74 
unfolding bind_def return_def 

75 
apply simp 

76 
apply (rule ext) 

77 
apply (unfold mrec_rule[of x]) 

37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37772
diff
changeset

78 
by (auto simp add: execute_simps split: option.splits prod.splits sum.splits) 
37772  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 

39754  108 
by (auto simp: mrec.psimps) 
37772  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 

39754  125 
unfolding MREC_def by (auto simp: mrec.psimps) 
37772  126 
next 
127 
case None 

39754  128 
from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by (auto simp: mrec.psimps) 
37772  129 
qed 
130 
qed 

131 
next 

132 
case None 

39754  133 
from this 1(1) mrec 1(3) show ?thesis by (simp add: mrec.psimps) 
37772  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 