21 by(auto split: prod.split const.split) |
21 by(auto split: prod.split const.split) |
22 |
22 |
23 instantiation const :: semilattice |
23 instantiation const :: semilattice |
24 begin |
24 begin |
25 |
25 |
26 fun le_const where |
26 fun less_eq_const where |
27 "_ \<sqsubseteq> Any = True" | |
27 "_ \<le> Any = True" | |
28 "Const n \<sqsubseteq> Const m = (n=m)" | |
28 "Const n \<le> Const m = (n=m)" | |
29 "Any \<sqsubseteq> Const _ = False" |
29 "Any \<le> Const _ = False" |
|
30 |
|
31 definition "a < (b::const) = (a \<le> b & ~ b \<le> a)" |
30 |
32 |
31 fun join_const where |
33 fun join_const where |
32 "Const m \<squnion> Const n = (if n=m then Const m else Any)" | |
34 "Const m \<squnion> Const n = (if n=m then Const m else Any)" | |
33 "_ \<squnion> _ = Any" |
35 "_ \<squnion> _ = Any" |
34 |
36 |
35 definition "\<top> = Any" |
37 definition "\<top> = Any" |
36 |
38 |
37 instance |
39 instance |
38 proof |
40 proof |
39 case goal1 thus ?case by (cases x) simp_all |
41 case goal1 thus ?case by (rule less_const_def) |
40 next |
42 next |
41 case goal2 thus ?case by(cases z, cases y, cases x, simp_all) |
43 case goal2 show ?case by (cases x) simp_all |
42 next |
44 next |
43 case goal3 thus ?case by(cases x, cases y, simp_all) |
45 case goal3 thus ?case by(cases z, cases y, cases x, simp_all) |
44 next |
46 next |
45 case goal4 thus ?case by(cases y, cases x, simp_all) |
47 case goal4 thus ?case by(cases x, cases y, simp_all, cases y, simp_all) |
46 next |
48 next |
47 case goal5 thus ?case by(cases z, cases y, cases x, simp_all) |
49 case goal6 thus ?case by(cases x, cases y, simp_all) |
48 next |
50 next |
49 case goal6 thus ?case by(simp add: Top_const_def) |
51 case goal7 thus ?case by(cases y, cases x, simp_all) |
|
52 next |
|
53 case goal8 thus ?case by(cases z, cases y, cases x, simp_all) |
|
54 next |
|
55 case goal5 thus ?case by(simp add: top_const_def) |
50 qed |
56 qed |
51 |
57 |
52 end |
58 end |
53 |
59 |
54 |
60 |
56 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
62 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
57 proof |
63 proof |
58 case goal1 thus ?case |
64 case goal1 thus ?case |
59 by(cases a, cases b, simp, simp, cases b, simp, simp) |
65 by(cases a, cases b, simp, simp, cases b, simp, simp) |
60 next |
66 next |
61 case goal2 show ?case by(simp add: Top_const_def) |
67 case goal2 show ?case by(simp add: top_const_def) |
62 next |
68 next |
63 case goal3 show ?case by simp |
69 case goal3 show ?case by simp |
64 next |
70 next |
65 case goal4 thus ?case |
71 case goal4 thus ?case |
66 by(auto simp: plus_const_cases split: const.split) |
72 by(auto simp: plus_const_cases split: const.split) |
72 .. |
78 .. |
73 |
79 |
74 |
80 |
75 subsubsection "Tests" |
81 subsubsection "Tests" |
76 |
82 |
77 definition "steps c i = (step_const(top(vars c)) ^^ i) (bot c)" |
83 definition "steps c i = (step_const(Top(vars c)) ^^ i) (bot c)" |
78 |
84 |
79 value "show_acom (steps test1_const 0)" |
85 value "show_acom (steps test1_const 0)" |
80 value "show_acom (steps test1_const 1)" |
86 value "show_acom (steps test1_const 1)" |
81 value "show_acom (steps test1_const 2)" |
87 value "show_acom (steps test1_const 2)" |
82 value "show_acom (steps test1_const 3)" |
88 value "show_acom (steps test1_const 3)" |