45 case goal6 thus ?case by(simp add: Top_cval_def) |
45 case goal6 thus ?case by(simp add: Top_cval_def) |
46 qed |
46 qed |
47 |
47 |
48 end |
48 end |
49 |
49 |
50 interpretation Rep rep_cval |
50 permanent_interpretation Rep rep_cval |
51 proof |
51 proof |
52 case goal1 thus ?case |
52 case goal1 thus ?case |
53 by(cases a, cases b, simp, simp, cases b, simp, simp) |
53 by(cases a, cases b, simp, simp, cases b, simp, simp) |
54 qed |
54 qed |
55 |
55 |
56 interpretation Val_abs rep_cval Const plus_cval |
56 permanent_interpretation Val_abs rep_cval Const plus_cval |
57 proof |
57 proof |
58 case goal1 show ?case by simp |
58 case goal1 show ?case by simp |
59 next |
59 next |
60 case goal2 thus ?case |
60 case goal2 thus ?case |
61 by(cases a1, cases a2, simp, simp, cases a2, simp, simp) |
61 by(cases a1, cases a2, simp, simp, cases a2, simp, simp) |
62 qed |
62 qed |
63 |
63 |
64 interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)" |
64 permanent_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)" |
65 defines AI_const is AI |
65 defines AI_const is AI |
66 and aval'_const is aval' |
66 and aval'_const is aval' |
67 proof qed (auto simp: iter'_pfp_above) |
67 proof qed (auto simp: iter'_pfp_above) |
68 |
68 |
69 text{* Straight line code: *} |
69 text{* Straight line code: *} |