1(* Author: Tobias Nipkow *) 2 3theory Abs_Int1_const 4imports Abs_Int1 5begin 6 7subsection "Constant Propagation" 8 9datatype const = Const val | Any 10 11fun \<gamma>_const where 12"\<gamma>_const (Const i) = {i}" | 13"\<gamma>_const (Any) = UNIV" 14 15fun plus_const where 16"plus_const (Const i) (Const j) = Const(i+j)" | 17"plus_const _ _ = Any" 18 19lemma plus_const_cases: "plus_const a1 a2 = 20 (case (a1,a2) of (Const i, Const j) \<Rightarrow> Const(i+j) | _ \<Rightarrow> Any)" 21by(auto split: prod.split const.split) 22 23instantiation const :: semilattice_sup_top 24begin 25 26fun less_eq_const where "x \<le> y = (y = Any | x=y)" 27 28definition "x < (y::const) = (x \<le> y & \<not> y \<le> x)" 29 30fun sup_const where "x \<squnion> y = (if x=y then x else Any)" 31 32definition "\<top> = Any" 33 34instance 35proof (standard, goal_cases) 36 case 1 thus ?case by (rule less_const_def) 37next 38 case (2 x) show ?case by (cases x) simp_all 39next 40 case (3 x y z) thus ?case by(cases z, cases y, cases x, simp_all) 41next 42 case (4 x y) thus ?case by(cases x, cases y, simp_all, cases y, simp_all) 43next 44 case (6 x y) thus ?case by(cases x, cases y, simp_all) 45next 46 case (5 x y) thus ?case by(cases y, cases x, simp_all) 47next 48 case (7 x y z) thus ?case by(cases z, cases y, cases x, simp_all) 49next 50 case 8 thus ?case by(simp add: top_const_def) 51qed 52 53end 54 55 56global_interpretation Val_semilattice 57where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const 58proof (standard, goal_cases) 59 case (1 a b) thus ?case 60 by(cases a, cases b, simp, simp, cases b, simp, simp) 61next 62 case 2 show ?case by(simp add: top_const_def) 63next 64 case 3 show ?case by simp 65next 66 case 4 thus ?case by(auto simp: plus_const_cases split: const.split) 67qed 68 69global_interpretation Abs_Int 70where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const 71defines AI_const = AI and step_const = step' and aval'_const = aval' 72.. 73 74 75subsubsection "Tests" 76 77definition "steps c i = (step_const \<top> ^^ i) (bot c)" 78 79value "show_acom (steps test1_const 0)" 80value "show_acom (steps test1_const 1)" 81value "show_acom (steps test1_const 2)" 82value "show_acom (steps test1_const 3)" 83value "show_acom (the(AI_const test1_const))" 84 85value "show_acom (the(AI_const test2_const))" 86value "show_acom (the(AI_const test3_const))" 87 88value "show_acom (steps test4_const 0)" 89value "show_acom (steps test4_const 1)" 90value "show_acom (steps test4_const 2)" 91value "show_acom (steps test4_const 3)" 92value "show_acom (steps test4_const 4)" 93value "show_acom (the(AI_const test4_const))" 94 95value "show_acom (steps test5_const 0)" 96value "show_acom (steps test5_const 1)" 97value "show_acom (steps test5_const 2)" 98value "show_acom (steps test5_const 3)" 99value "show_acom (steps test5_const 4)" 100value "show_acom (steps test5_const 5)" 101value "show_acom (steps test5_const 6)" 102value "show_acom (the(AI_const test5_const))" 103 104value "show_acom (steps test6_const 0)" 105value "show_acom (steps test6_const 1)" 106value "show_acom (steps test6_const 2)" 107value "show_acom (steps test6_const 3)" 108value "show_acom (steps test6_const 4)" 109value "show_acom (steps test6_const 5)" 110value "show_acom (steps test6_const 6)" 111value "show_acom (steps test6_const 7)" 112value "show_acom (steps test6_const 8)" 113value "show_acom (steps test6_const 9)" 114value "show_acom (steps test6_const 10)" 115value "show_acom (steps test6_const 11)" 116value "show_acom (steps test6_const 12)" 117value "show_acom (steps test6_const 13)" 118value "show_acom (the(AI_const test6_const))" 119 120 121text\<open>Monotonicity:\<close> 122 123global_interpretation Abs_Int_mono 124where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const 125proof (standard, goal_cases) 126 case 1 thus ?case by(auto simp: plus_const_cases split: const.split) 127qed 128 129text\<open>Termination:\<close> 130 131definition m_const :: "const \<Rightarrow> nat" where 132"m_const x = (if x = Any then 0 else 1)" 133 134global_interpretation Abs_Int_measure 135where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const 136and m = m_const and h = "1" 137proof (standard, goal_cases) 138 case 1 thus ?case by(auto simp: m_const_def split: const.splits) 139next 140 case 2 thus ?case by(auto simp: m_const_def less_const_def split: const.splits) 141qed 142 143thm AI_Some_measure 144 145end 146