1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/IMP/Abs_Int1_const.thy Thu Apr 19 20:19:13 2012 +0200
1.3 @@ -0,0 +1,143 @@
1.4 +(* Author: Tobias Nipkow *)
1.5 +
1.6 +theory Abs_Int1_const
1.7 +imports Abs_Int1
1.8 +begin
1.9 +
1.10 +subsection "Constant Propagation"
1.11 +
1.12 +datatype const = Const val | Any
1.13 +
1.14 +fun \<gamma>_const where
1.15 +"\<gamma>_const (Const n) = {n}" |
1.16 +"\<gamma>_const (Any) = UNIV"
1.17 +
1.18 +fun plus_const where
1.19 +"plus_const (Const m) (Const n) = Const(m+n)" |
1.20 +"plus_const _ _ = Any"
1.21 +
1.22 +lemma plus_const_cases: "plus_const a1 a2 =
1.23 + (case (a1,a2) of (Const m, Const n) \<Rightarrow> Const(m+n) | _ \<Rightarrow> Any)"
1.24 +by(auto split: prod.split const.split)
1.25 +
1.26 +instantiation const :: SL_top
1.27 +begin
1.28 +
1.29 +fun le_const where
1.30 +"_ \<sqsubseteq> Any = True" |
1.31 +"Const n \<sqsubseteq> Const m = (n=m)" |
1.32 +"Any \<sqsubseteq> Const _ = False"
1.33 +
1.34 +fun join_const where
1.35 +"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
1.36 +"_ \<squnion> _ = Any"
1.37 +
1.38 +definition "\<top> = Any"
1.39 +
1.40 +instance
1.41 +proof
1.42 + case goal1 thus ?case by (cases x) simp_all
1.43 +next
1.44 + case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
1.45 +next
1.46 + case goal3 thus ?case by(cases x, cases y, simp_all)
1.47 +next
1.48 + case goal4 thus ?case by(cases y, cases x, simp_all)
1.49 +next
1.50 + case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
1.51 +next
1.52 + case goal6 thus ?case by(simp add: Top_const_def)
1.53 +qed
1.54 +
1.55 +end
1.56 +
1.57 +
1.58 +interpretation Val_abs
1.59 +where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
1.60 +proof
1.61 + case goal1 thus ?case
1.62 + by(cases a, cases b, simp, simp, cases b, simp, simp)
1.63 +next
1.64 + case goal2 show ?case by(simp add: Top_const_def)
1.65 +next
1.66 + case goal3 show ?case by simp
1.67 +next
1.68 + case goal4 thus ?case
1.69 + by(auto simp: plus_const_cases split: const.split)
1.70 +qed
1.71 +
1.72 +interpretation Abs_Int
1.73 +where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
1.74 +defines AI_const is AI and step_const is step' and aval'_const is aval'
1.75 +..
1.76 +
1.77 +
1.78 +subsubsection "Tests"
1.79 +
1.80 +definition "steps c i = (step_const(top c) ^^ i) (bot c)"
1.81 +
1.82 +value "show_acom (steps test1_const 0)"
1.83 +value "show_acom (steps test1_const 1)"
1.84 +value "show_acom (steps test1_const 2)"
1.85 +value "show_acom (steps test1_const 3)"
1.86 +value "show_acom_opt (AI_const test1_const)"
1.87 +
1.88 +value "show_acom_opt (AI_const test2_const)"
1.89 +value "show_acom_opt (AI_const test3_const)"
1.90 +
1.91 +value "show_acom (steps test4_const 0)"
1.92 +value "show_acom (steps test4_const 1)"
1.93 +value "show_acom (steps test4_const 2)"
1.94 +value "show_acom (steps test4_const 3)"
1.95 +value "show_acom_opt (AI_const test4_const)"
1.96 +
1.97 +value "show_acom (steps test5_const 0)"
1.98 +value "show_acom (steps test5_const 1)"
1.99 +value "show_acom (steps test5_const 2)"
1.100 +value "show_acom (steps test5_const 3)"
1.101 +value "show_acom (steps test5_const 4)"
1.102 +value "show_acom (steps test5_const 5)"
1.103 +value "show_acom_opt (AI_const test5_const)"
1.104 +
1.105 +value "show_acom (steps test6_const 0)"
1.106 +value "show_acom (steps test6_const 1)"
1.107 +value "show_acom (steps test6_const 2)"
1.108 +value "show_acom (steps test6_const 3)"
1.109 +value "show_acom (steps test6_const 4)"
1.110 +value "show_acom (steps test6_const 5)"
1.111 +value "show_acom (steps test6_const 6)"
1.112 +value "show_acom (steps test6_const 7)"
1.113 +value "show_acom (steps test6_const 8)"
1.114 +value "show_acom (steps test6_const 9)"
1.115 +value "show_acom (steps test6_const 10)"
1.116 +value "show_acom (steps test6_const 11)"
1.117 +value "show_acom_opt (AI_const test6_const)"
1.118 +
1.119 +
1.120 +text{* Monotonicity: *}
1.121 +
1.122 +interpretation Abs_Int_mono
1.123 +where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
1.124 +proof
1.125 + case goal1 thus ?case
1.126 + by(auto simp: plus_const_cases split: const.split)
1.127 +qed
1.128 +
1.129 +text{* Termination: *}
1.130 +
1.131 +definition "m_const x = (case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0)"
1.132 +
1.133 +interpretation Abs_Int_measure
1.134 +where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
1.135 +and m = m_const and h = "2"
1.136 +proof
1.137 + case goal1 thus ?case by(auto simp: m_const_def split: const.splits)
1.138 +next
1.139 + case goal2 thus ?case by(auto simp: m_const_def split: const.splits)
1.140 +next
1.141 + case goal3 thus ?case by(auto simp: m_const_def split: const.splits)
1.142 +qed
1.143 +
1.144 +thm AI_Some_measure
1.145 +
1.146 +end