70 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
70 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
71 defines AI_const is AI and step_const is step' and aval'_const is aval' |
71 defines AI_const is AI and step_const is step' and aval'_const is aval' |
72 proof qed |
72 proof qed |
73 |
73 |
74 |
74 |
|
75 subsubsection "Tests" |
|
76 |
|
77 value "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test1_const))" |
|
78 value "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test1_const))" |
|
79 value "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test1_const))" |
|
80 value "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test1_const))" |
|
81 value "show_acom_opt (AI_const test1_const)" |
|
82 |
|
83 value "show_acom_opt (AI_const test2_const)" |
|
84 value "show_acom_opt (AI_const test3_const)" |
|
85 |
|
86 value "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test4_const))" |
|
87 value "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test4_const))" |
|
88 value "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test4_const))" |
|
89 value "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test4_const))" |
|
90 value "show_acom_opt (AI_const test4_const)" |
|
91 |
|
92 value "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test5_const))" |
|
93 value "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test5_const))" |
|
94 value "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test5_const))" |
|
95 value "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test5_const))" |
|
96 value "show_acom (((step_const \<top>)^^4) (\<bottom>\<^sub>c test5_const))" |
|
97 value "show_acom (((step_const \<top>)^^5) (\<bottom>\<^sub>c test5_const))" |
|
98 value "show_acom_opt (AI_const test5_const)" |
|
99 |
|
100 value "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test6_const))" |
|
101 value "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test6_const))" |
|
102 value "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test6_const))" |
|
103 value "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test6_const))" |
|
104 value "show_acom (((step_const \<top>)^^4) (\<bottom>\<^sub>c test6_const))" |
|
105 value "show_acom (((step_const \<top>)^^5) (\<bottom>\<^sub>c test6_const))" |
|
106 value "show_acom (((step_const \<top>)^^6) (\<bottom>\<^sub>c test6_const))" |
|
107 value "show_acom (((step_const \<top>)^^7) (\<bottom>\<^sub>c test6_const))" |
|
108 value "show_acom (((step_const \<top>)^^8) (\<bottom>\<^sub>c test6_const))" |
|
109 value "show_acom (((step_const \<top>)^^9) (\<bottom>\<^sub>c test6_const))" |
|
110 value "show_acom (((step_const \<top>)^^10) (\<bottom>\<^sub>c test6_const))" |
|
111 value "show_acom (((step_const \<top>)^^11) (\<bottom>\<^sub>c test6_const))" |
|
112 value "show_acom_opt (AI_const test6_const)" |
|
113 |
|
114 |
75 text{* Monotonicity: *} |
115 text{* Monotonicity: *} |
76 |
116 |
77 interpretation Abs_Int_mono |
117 interpretation Abs_Int_mono |
78 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
118 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
79 proof |
119 proof |
94 by(auto simp: m_const_def split: const.splits) |
134 by(auto simp: m_const_def split: const.splits) |
95 |
135 |
96 lemma "EX c'. AI_const c = Some c'" |
136 lemma "EX c'. AI_const c = Some c'" |
97 by(rule AI_Some_measure[OF measure_const measure_const_eq]) |
137 by(rule AI_Some_measure[OF measure_const measure_const_eq]) |
98 |
138 |
99 |
|
100 subsubsection "Tests" |
|
101 |
|
102 value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test1_const))" |
|
103 value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test1_const))" |
|
104 value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test1_const))" |
|
105 value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test1_const))" |
|
106 value [code] "show_acom_opt (AI_const test1_const)" |
|
107 |
|
108 value [code] "show_acom_opt (AI_const test2_const)" |
|
109 value [code] "show_acom_opt (AI_const test3_const)" |
|
110 |
|
111 value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test4_const))" |
|
112 value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test4_const))" |
|
113 value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test4_const))" |
|
114 value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test4_const))" |
|
115 value [code] "show_acom_opt (AI_const test4_const)" |
|
116 |
|
117 value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test5_const))" |
|
118 value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test5_const))" |
|
119 value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test5_const))" |
|
120 value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test5_const))" |
|
121 value [code] "show_acom (((step_const \<top>)^^4) (\<bottom>\<^sub>c test5_const))" |
|
122 value [code] "show_acom (((step_const \<top>)^^5) (\<bottom>\<^sub>c test5_const))" |
|
123 value [code] "show_acom_opt (AI_const test5_const)" |
|
124 |
|
125 value [code] "show_acom_opt (AI_const test6_const)" |
|
126 |
|
127 end |
139 end |