51 qed |
51 qed |
52 |
52 |
53 end |
53 end |
54 |
54 |
55 |
55 |
56 permanent_interpretation Val_semilattice |
56 global_interpretation Val_semilattice |
57 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
57 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
58 proof (standard, goal_cases) |
58 proof (standard, goal_cases) |
59 case (1 a b) thus ?case |
59 case (1 a b) thus ?case |
60 by(cases a, cases b, simp, simp, cases b, simp, simp) |
60 by(cases a, cases b, simp, simp, cases b, simp, simp) |
61 next |
61 next |
64 case 3 show ?case by simp |
64 case 3 show ?case by simp |
65 next |
65 next |
66 case 4 thus ?case by(auto simp: plus_const_cases split: const.split) |
66 case 4 thus ?case by(auto simp: plus_const_cases split: const.split) |
67 qed |
67 qed |
68 |
68 |
69 permanent_interpretation Abs_Int |
69 global_interpretation Abs_Int |
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 = AI and step_const = step' and aval'_const = aval' |
71 defines AI_const = AI and step_const = step' and aval'_const = aval' |
72 .. |
72 .. |
73 |
73 |
74 |
74 |
118 value "show_acom (the(AI_const test6_const))" |
118 value "show_acom (the(AI_const test6_const))" |
119 |
119 |
120 |
120 |
121 text{* Monotonicity: *} |
121 text{* Monotonicity: *} |
122 |
122 |
123 permanent_interpretation Abs_Int_mono |
123 global_interpretation Abs_Int_mono |
124 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
124 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
125 proof (standard, goal_cases) |
125 proof (standard, goal_cases) |
126 case 1 thus ?case by(auto simp: plus_const_cases split: const.split) |
126 case 1 thus ?case by(auto simp: plus_const_cases split: const.split) |
127 qed |
127 qed |
128 |
128 |
129 text{* Termination: *} |
129 text{* Termination: *} |
130 |
130 |
131 definition m_const :: "const \<Rightarrow> nat" where |
131 definition m_const :: "const \<Rightarrow> nat" where |
132 "m_const x = (if x = Any then 0 else 1)" |
132 "m_const x = (if x = Any then 0 else 1)" |
133 |
133 |
134 permanent_interpretation Abs_Int_measure |
134 global_interpretation Abs_Int_measure |
135 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
135 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
136 and m = m_const and h = "1" |
136 and m = m_const and h = "1" |
137 proof (standard, goal_cases) |
137 proof (standard, goal_cases) |
138 case 1 thus ?case by(auto simp: m_const_def split: const.splits) |
138 case 1 thus ?case by(auto simp: m_const_def split: const.splits) |
139 next |
139 next |