author  haftmann 
Tue, 13 Jul 2010 11:38:03 +0200  
changeset 37787  30dc3abf4a58 
parent 37772  026ed2fc15d4 
child 37792  ba0bc31b90d7 
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 
)" 

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]) 

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

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