author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46355  42a01315d998 
permissions  rwrr 
46345  1 
theory Abs_Int0_parity 
2 
imports Abs_Int0 

3 
begin 

4 

5 
subsection "Parity Analysis" 

6 

7 
datatype parity = Even  Odd  Either 

8 

9 
text{* Instantiation of class @{class preord} with type @{typ parity}: *} 

10 

11 
instantiation parity :: preord 

12 
begin 

13 

14 
text{* First the definition of the interface function @{text"\<sqsubseteq>"}. Note that 

15 
the header of the definition must refer to the ascii name @{const le} of the 

16 
constants as @{text le_parity} and the definition is named @{text 

17 
le_parity_def}. Inside the definition the symbolic names can be used. *} 

18 

19 
definition le_parity where 

20 
"x \<sqsubseteq> y = (y = Either \<or> x=y)" 

21 

22 
text{* Now the instance proof, i.e.\ the proof that the definition fulfills 

23 
the axioms (assumptions) of the class. The initial proofstep generates the 

24 
necessary proof obligations. *} 

25 

26 
instance 

27 
proof 

28 
fix x::parity show "x \<sqsubseteq> x" by(auto simp: le_parity_def) 

29 
next 

30 
fix x y z :: parity assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z" 

31 
by(auto simp: le_parity_def) 

32 
qed 

33 

34 
end 

35 

36 
text{* Instantiation of class @{class SL_top} with type @{typ parity}: *} 

37 

38 
instantiation parity :: SL_top 

39 
begin 

40 

41 

42 
definition join_parity where 

43 
"x \<squnion> y = (if x \<sqsubseteq> y then y else if y \<sqsubseteq> x then x else Either)" 

44 

45 
definition Top_parity where 

46 
"\<top> = Either" 

47 

48 
text{* Now the instance proof. This time we take a lazy shortcut: we do not 

49 
write out the proof obligations but use the @{text goali} primitive to refer 

50 
to the assumptions of subgoal i and @{text "case?"} to refer to the 

51 
conclusion of subgoal i. The class axioms are presented in the same order as 

52 
in the class definition. *} 

53 

54 
instance 

55 
proof 

56 
case goal1 (*join1*) show ?case by(auto simp: le_parity_def join_parity_def) 

57 
next 

58 
case goal2 (*join2*) show ?case by(auto simp: le_parity_def join_parity_def) 

59 
next 

60 
case goal3 (*join least*) thus ?case by(auto simp: le_parity_def join_parity_def) 

61 
next 

62 
case goal4 (*Top*) show ?case by(auto simp: le_parity_def Top_parity_def) 

63 
qed 

64 

65 
end 

66 

67 

68 
text{* Now we define the functions used for instantiating the abstract 

69 
interpretation locales. Note that the Isabelle terminology is 

70 
\emph{interpretation}, not \emph{instantiation} of locales, but we use 

71 
instantiation to avoid confusion with abstract interpretation. *} 

72 

73 
fun \<gamma>_parity :: "parity \<Rightarrow> val set" where 

74 
"\<gamma>_parity Even = {i. i mod 2 = 0}"  

75 
"\<gamma>_parity Odd = {i. i mod 2 = 1}"  

76 
"\<gamma>_parity Either = UNIV" 

77 

78 
fun num_parity :: "val \<Rightarrow> parity" where 

79 
"num_parity i = (if i mod 2 = 0 then Even else Odd)" 

80 

81 
fun plus_parity :: "parity \<Rightarrow> parity \<Rightarrow> parity" where 

82 
"plus_parity Even Even = Even"  

83 
"plus_parity Odd Odd = Even"  

84 
"plus_parity Even Odd = Odd"  

85 
"plus_parity Odd Even = Odd"  

86 
"plus_parity Either y = Either"  

87 
"plus_parity x Either = Either" 

88 

89 
text{* First we instantiate the abstract value interface and prove that the 

90 
functions on type @{typ parity} have all the necessary properties: *} 

91 

92 
interpretation Val_abs 

93 
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity 

94 
proof txt{* of the locale axioms *} 

95 
fix a b :: parity 

96 
assume "a \<sqsubseteq> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b" 

97 
by(auto simp: le_parity_def) 

98 
next txt{* The rest in the lazy, implicit way *} 

99 
case goal2 show ?case by(auto simp: Top_parity_def) 

100 
next 

101 
case goal3 show ?case by auto 

102 
next 

103 
txt{* Warning: this subproof refers to the names @{text a1} and @{text a2} 

104 
from the statement of the axiom. *} 

105 
case goal4 thus ?case 

106 
proof(cases a1 a2 rule: parity.exhaust[case_product parity.exhaust]) 

107 
qed (auto simp add:mod_add_eq) 

108 
qed 

109 

110 
text{* Instantiating the abstract interpretation locale requires no more 

111 
proofs (they happened in the instatiation above) but delivers the 

112 
instantiated abstract interpreter which we call AI: *} 

113 

114 
interpretation Abs_Int 

115 
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity 

46346
10c18630612a
removed duplicate definitions that made locale inconsistent
nipkow
parents:
46345
diff
changeset

116 
defines aval_parity is aval' and step_parity is step' and AI_parity is AI 
46355
42a01315d998
removed accidental dependance of abstract interpreter on gamma
nipkow
parents:
46346
diff
changeset

117 
.. 
46345  118 

119 

120 
subsubsection "Tests" 

121 

122 
definition "test1_parity = 

123 
''x'' ::= N 1; 

124 
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)" 

125 

126 
value "show_acom_opt (AI_parity test1_parity)" 

127 

128 
definition "test2_parity = 

129 
''x'' ::= N 1; 

130 
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)" 

131 

132 
value "show_acom ((step_parity \<top> ^^1) (anno None test2_parity))" 

133 
value "show_acom ((step_parity \<top> ^^2) (anno None test2_parity))" 

134 
value "show_acom ((step_parity \<top> ^^3) (anno None test2_parity))" 

135 
value "show_acom ((step_parity \<top> ^^4) (anno None test2_parity))" 

136 
value "show_acom ((step_parity \<top> ^^5) (anno None test2_parity))" 

137 
value "show_acom_opt (AI_parity test2_parity)" 

138 

139 

140 
subsubsection "Termination" 

141 

142 
interpretation Abs_Int_mono 

143 
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity 

144 
proof 

145 
case goal1 thus ?case 

146 
proof(cases a1 a2 b1 b2 

147 
rule: parity.exhaust[case_product parity.exhaust[case_product parity.exhaust[case_product parity.exhaust]]]) (* FIXME  UGLY! *) 

148 
qed (auto simp add:le_parity_def) 

149 
qed 

150 

151 

152 
definition m_parity :: "parity \<Rightarrow> nat" where 

153 
"m_parity x = (if x=Either then 0 else 1)" 

154 

155 
lemma measure_parity: 

156 
"(strict{(x::parity,y). x \<sqsubseteq> y})^1 \<subseteq> measure m_parity" 

157 
by(auto simp add: m_parity_def le_parity_def) 

158 

159 
lemma measure_parity_eq: 

160 
"\<forall>x y::parity. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> m_parity x = m_parity y" 

161 
by(auto simp add: m_parity_def le_parity_def) 

162 

163 
lemma AI_parity_Some: "\<exists>c'. AI_parity c = Some c'" 

164 
by(rule AI_Some_measure[OF measure_parity measure_parity_eq]) 

165 

166 
end 