equal
deleted
inserted
replaced
50 qed |
50 qed |
51 |
51 |
52 end |
52 end |
53 |
53 |
54 |
54 |
55 interpretation Val_abs |
55 permanent_interpretation Val_abs |
56 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
56 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
57 proof |
57 proof |
58 case goal1 thus ?case |
58 case goal1 thus ?case |
59 by(cases a, cases b, simp, simp, cases b, simp, simp) |
59 by(cases a, cases b, simp, simp, cases b, simp, simp) |
60 next |
60 next |
64 next |
64 next |
65 case goal4 thus ?case |
65 case goal4 thus ?case |
66 by(auto simp: plus_const_cases split: const.split) |
66 by(auto simp: plus_const_cases split: const.split) |
67 qed |
67 qed |
68 |
68 |
69 interpretation Abs_Int |
69 permanent_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 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 .. |
72 .. |
73 |
73 |
74 |
74 |
112 value "show_acom_opt (AI_const test6_const)" |
112 value "show_acom_opt (AI_const test6_const)" |
113 |
113 |
114 |
114 |
115 text{* Monotonicity: *} |
115 text{* Monotonicity: *} |
116 |
116 |
117 interpretation Abs_Int_mono |
117 permanent_interpretation Abs_Int_mono |
118 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
118 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
119 proof |
119 proof |
120 case goal1 thus ?case |
120 case goal1 thus ?case |
121 by(auto simp: plus_const_cases split: const.split) |
121 by(auto simp: plus_const_cases split: const.split) |
122 qed |
122 qed |