--- a/src/HOL/IMP/AbsInt0.thy Mon Sep 26 21:13:26 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,67 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory AbsInt0
-imports Astate
-begin
-
-subsection "Computable Abstract Interpretation"
-
-text{* Abstract interpretation over type @{text astate} instead of
-functions. *}
-
-locale Abs_Int = Val_abs +
-fixes pfp :: "('a astate \<Rightarrow> 'a astate) \<Rightarrow> 'a astate \<Rightarrow> 'a astate"
-assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
-assumes above: "x0 \<sqsubseteq> pfp f x0"
-begin
-
-fun aval' :: "aexp \<Rightarrow> 'a astate \<Rightarrow> 'a" where
-"aval' (N n) _ = num' n" |
-"aval' (V x) S = lookup S x" |
-"aval' (Plus e1 e2) S = plus' (aval' e1 S) (aval' e2 S)"
-
-abbreviation astate_in_rep (infix "<:" 50) where
-"s <: S == ALL x. s x <: lookup S x"
-
-lemma astate_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
-by (metis in_mono le_astate_def le_rep lookup_def top)
-
-lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
-by (induct a) (auto simp: rep_num' rep_plus')
-
-
-fun AI :: "com \<Rightarrow> 'a astate \<Rightarrow> 'a astate" where
-"AI SKIP S = S" |
-"AI (x ::= a) S = update S x (aval' a S)" |
-"AI (c1;c2) S = AI c2 (AI c1 S)" |
-"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
-"AI (WHILE b DO c) S = pfp (AI c) S"
-
-lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
-proof(induction c arbitrary: s t S0)
- case SKIP thus ?case by fastforce
-next
- case Assign thus ?case
- by (auto simp: lookup_update aval'_sound)
-next
- case Semi thus ?case by auto
-next
- case If thus ?case
- by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2)
-next
- case (While b c)
- let ?P = "pfp (AI c) S0"
- { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
- proof(induction "WHILE b DO c" s t rule: big_step_induct)
- case WhileFalse thus ?case by simp
- next
- case WhileTrue thus ?case using While.IH pfp astate_in_rep_le by metis
- qed
- }
- with astate_in_rep_le[OF `s <: S0` above]
- show ?case by (metis While(2) AI.simps(5))
-qed
-
-end
-
-end
--- a/src/HOL/IMP/AbsInt0_const.thy Mon Sep 26 21:13:26 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory AbsInt0_const
-imports AbsInt0
-begin
-
-subsection "Constant Propagation"
-
-datatype cval = Const val | Any
-
-fun rep_cval where
-"rep_cval (Const n) = {n}" |
-"rep_cval (Any) = UNIV"
-
-fun plus_cval where
-"plus_cval (Const m) (Const n) = Const(m+n)" |
-"plus_cval _ _ = Any"
-
-instantiation cval :: SL_top
-begin
-
-fun le_cval where
-"_ \<sqsubseteq> Any = True" |
-"Const n \<sqsubseteq> Const m = (n=m)" |
-"Any \<sqsubseteq> Const _ = False"
-
-fun join_cval where
-"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
-"_ \<squnion> _ = Any"
-
-definition "Top = Any"
-
-instance
-proof
- case goal1 thus ?case by (cases x) simp_all
-next
- case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
-next
- case goal3 thus ?case by(cases x, cases y, simp_all)
-next
- case goal4 thus ?case by(cases y, cases x, simp_all)
-next
- case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
-next
- case goal6 thus ?case by(simp add: Top_cval_def)
-qed
-
-end
-
-interpretation Rep rep_cval
-proof
- case goal1 thus ?case
- by(cases a, cases b, simp, simp, cases b, simp, simp)
-qed
-
-interpretation Val_abs rep_cval Const plus_cval
-proof
- case goal1 show ?case by simp
-next
- case goal2 thus ?case
- by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
-qed
-
-interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
-defines AI_const is AI
-and aval'_const is aval'
-proof qed (auto simp: iter'_pfp_above)
-
-text{* Straight line code: *}
-definition "test1_const =
- ''y'' ::= N 7;
- ''z'' ::= Plus (V ''y'') (N 2);
- ''y'' ::= Plus (V ''x'') (N 0)"
-
-text{* Conditional: *}
-definition "test2_const =
- IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
-
-text{* Conditional, test is ignored: *}
-definition "test3_const =
- ''x'' ::= N 42;
- IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
-
-text{* While: *}
-definition "test4_const =
- ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
-
-text{* While, test is ignored: *}
-definition "test5_const =
- ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
-
-text{* Iteration is needed: *}
-definition "test6_const =
- ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
- WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
-
-text{* More iteration would be needed: *}
-definition "test7_const =
- ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
- WHILE Less (V ''x'') (N 1)
- DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
-
-value [code] "list (AI_const test1_const Top)"
-value [code] "list (AI_const test2_const Top)"
-value [code] "list (AI_const test3_const Top)"
-value [code] "list (AI_const test4_const Top)"
-value [code] "list (AI_const test5_const Top)"
-value [code] "list (AI_const test6_const Top)"
-value [code] "list (AI_const test7_const Top)"
-
-end
--- a/src/HOL/IMP/AbsInt0_fun.thy Mon Sep 26 21:13:26 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,187 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-header "Abstract Interpretation"
-
-theory AbsInt0_fun
-imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
-begin
-
-subsection "Orderings"
-
-class preord =
-fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
-assumes le_refl[simp]: "x \<sqsubseteq> x"
-and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
-
-text{* Note: no antisymmetry. Allows implementations where some abstract
-element is implemented by two different values @{prop "x \<noteq> y"}
-such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not
-needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}.
-*}
-
-class SL_top = preord +
-fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
-fixes Top :: "'a"
-assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
-and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
-and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
-and top[simp]: "x \<sqsubseteq> Top"
-begin
-
-lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
-by (metis join_ge1 join_ge2 join_least le_trans)
-
-fun iter :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter 0 f _ = Top" |
-"iter (Suc n) f x = (if f x \<sqsubseteq> x then x else iter n f (f x))"
-
-lemma iter_pfp: "f(iter n f x) \<sqsubseteq> iter n f x"
-apply (induction n arbitrary: x)
- apply (simp)
-apply (simp)
-done
-
-abbreviation iter' :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter' n f x0 == iter n (\<lambda>x. x0 \<squnion> f x) x0"
-
-lemma iter'_pfp_above:
- "f(iter' n f x0) \<sqsubseteq> iter' n f x0" "x0 \<sqsubseteq> iter' n f x0"
-using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"] by auto
-
-text{* So much for soundness. But how good an approximation of the post-fixed
-point does @{const iter} yield? *}
-
-lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
-apply(induction n arbitrary: x)
- apply simp
-apply (auto)
- apply(metis funpow.simps(1) id_def)
-by (metis funpow.simps(2) funpow_swap1 o_apply)
-
-text{* For monotone @{text f}, @{term "iter f n x0"} yields the least
-post-fixed point above @{text x0}, unless it yields @{text Top}. *}
-
-lemma iter_least_pfp:
-assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter n f x0 \<noteq> Top"
-and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter n f x0 \<sqsubseteq> p"
-proof-
- obtain k where "iter n f x0 = (f^^k) x0"
- using iter_funpow[OF `iter n f x0 \<noteq> Top`] by blast
- moreover
- { fix n have "(f^^n) x0 \<sqsubseteq> p"
- proof(induction n)
- case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
- next
- case (Suc n) thus ?case
- by (simp add: `x0 \<sqsubseteq> p`)(metis Suc assms(3) le_trans mono)
- qed
- } ultimately show ?thesis by simp
-qed
-
-end
-
-text{* The interface of abstract values: *}
-
-locale Rep =
-fixes rep :: "'a::SL_top \<Rightarrow> 'b set"
-assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
-begin
-
-abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a"
-
-lemma in_rep_join: "x <: a1 \<or> x <: a2 \<Longrightarrow> x <: a1 \<squnion> a2"
-by (metis SL_top_class.join_ge1 SL_top_class.join_ge2 le_rep subsetD)
-
-end
-
-locale Val_abs = Rep rep
- for rep :: "'a::SL_top \<Rightarrow> val set" +
-fixes num' :: "val \<Rightarrow> 'a"
-and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-assumes rep_num': "rep(num' n) = {n}"
-and rep_plus': "n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: plus' a1 a2"
-
-
-instantiation "fun" :: (type, SL_top) SL_top
-begin
-
-definition "f \<sqsubseteq> g = (ALL x. f x \<sqsubseteq> g x)"
-definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
-definition "Top = (\<lambda>x. Top)"
-
-lemma join_apply[simp]:
- "(f \<squnion> g) x = f x \<squnion> g x"
-by (simp add: join_fun_def)
-
-instance
-proof
- case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
-qed (simp_all add: le_fun_def Top_fun_def)
-
-end
-
-subsection "Abstract Interpretation Abstractly"
-
-text{* Abstract interpretation over abstract values. Abstract states are
-simply functions. The post-fixed point finder is parameterized over. *}
-
-type_synonym 'a st = "name \<Rightarrow> 'a"
-
-locale Abs_Int_Fun = Val_abs +
-fixes pfp :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
-assumes pfp: "f(pfp f x) \<sqsubseteq> pfp f x"
-assumes above: "x \<sqsubseteq> pfp f x"
-begin
-
-fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a" where
-"aval' (N n) _ = num' n" |
-"aval' (V x) S = S x" |
-"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
-
-abbreviation fun_in_rep (infix "<:" 50) where
-"f <: F == \<forall>x. f x <: F x"
-
-lemma fun_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
-by (metis le_fun_def le_rep subsetD)
-
-lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
-by (induct a) (auto simp: rep_num' rep_plus')
-
-fun AI :: "com \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> 'a)" where
-"AI SKIP S = S" |
-"AI (x ::= a) S = S(x := aval' a S)" |
-"AI (c1;c2) S = AI c2 (AI c1 S)" |
-"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
-"AI (WHILE b DO c) S = pfp (AI c) S"
-
-lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
-proof(induction c arbitrary: s t S0)
- case SKIP thus ?case by fastforce
-next
- case Assign thus ?case by (auto simp: aval'_sound)
-next
- case Semi thus ?case by auto
-next
- case If thus ?case by(auto simp: in_rep_join)
-next
- case (While b c)
- let ?P = "pfp (AI c) S0"
- { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
- proof(induction "WHILE b DO c" s t rule: big_step_induct)
- case WhileFalse thus ?case by simp
- next
- case WhileTrue thus ?case by(metis While.IH pfp fun_in_rep_le)
- qed
- }
- with fun_in_rep_le[OF `s <: S0` above]
- show ?case by (metis While(2) AI.simps(5))
-qed
-
-end
-
-
-text{* Problem: not executable because of the comparison of abstract states,
-i.e. functions, in the post-fixedpoint computation. Need to implement
-abstract states concretely. *}
-
-end
--- a/src/HOL/IMP/AbsInt1.thy Mon Sep 26 21:13:26 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,214 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory AbsInt1
-imports AbsInt0_const
-begin
-
-subsection "Backward Analysis of Expressions"
-
-class L_top_bot = SL_top +
-fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
-and Bot :: "'a"
-assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
-and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
-and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
-assumes bot[simp]: "Bot \<sqsubseteq> x"
-
-locale Rep1 = Rep rep for rep :: "'a::L_top_bot \<Rightarrow> 'b set" +
-assumes inter_rep_subset_rep_meet: "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
-and rep_Bot: "rep Bot = {}"
-begin
-
-lemma in_rep_meet: "x <: a1 \<Longrightarrow> x <: a2 \<Longrightarrow> x <: a1 \<sqinter> a2"
-by (metis IntI inter_rep_subset_rep_meet set_mp)
-
-lemma rep_meet[simp]: "rep(a1 \<sqinter> a2) = rep a1 \<inter> rep a2"
-by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2)
-
-end
-
-
-locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
- for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' +
-fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
-and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
-assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
- n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
-and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
- n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
-
-datatype 'a up = bot | Up 'a
-
-instantiation up :: (SL_top)SL_top
-begin
-
-fun le_up where
-"Up x \<sqsubseteq> Up y = (x \<sqsubseteq> y)" |
-"bot \<sqsubseteq> y = True" |
-"Up _ \<sqsubseteq> bot = False"
-
-lemma [simp]: "(x \<sqsubseteq> bot) = (x = bot)"
-by (cases x) simp_all
-
-lemma [simp]: "(Up x \<sqsubseteq> u) = (EX y. u = Up y & x \<sqsubseteq> y)"
-by (cases u) auto
-
-fun join_up where
-"Up x \<squnion> Up y = Up(x \<squnion> y)" |
-"bot \<squnion> y = y" |
-"x \<squnion> bot = x"
-
-lemma [simp]: "x \<squnion> bot = x"
-by (cases x) simp_all
-
-
-definition "Top = Up Top"
-
-instance proof
- case goal1 show ?case by(cases x, simp_all)
-next
- case goal2 thus ?case
- by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
-next
- case goal3 thus ?case by(cases x, simp, cases y, simp_all)
-next
- case goal4 thus ?case by(cases y, simp, cases x, simp_all)
-next
- case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
-next
- case goal6 thus ?case by(cases x, simp_all add: Top_up_def)
-qed
-
-end
-
-
-locale Abs_Int1 = Val_abs1 +
-fixes pfp :: "('a astate up \<Rightarrow> 'a astate up) \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up"
-assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
-assumes above: "x0 \<sqsubseteq> pfp f x0"
-begin
-
-(* FIXME avoid duplicating this defn *)
-abbreviation astate_in_rep (infix "<:" 50) where
-"s <: S == ALL x. s x <: lookup S x"
-
-abbreviation in_rep_up :: "state \<Rightarrow> 'a astate up \<Rightarrow> bool" (infix "<::" 50) where
-"s <:: S == EX S0. S = Up S0 \<and> s <: S0"
-
-lemma in_rep_up_trans: "(s::state) <:: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:: T"
-apply auto
-by (metis in_mono le_astate_def le_rep lookup_def top)
-
-lemma in_rep_join_UpI: "s <:: S1 | s <:: S2 \<Longrightarrow> s <:: S1 \<squnion> S2"
-by (metis in_rep_up_trans SL_top_class.join_ge1 SL_top_class.join_ge2)
-
-fun aval' :: "aexp \<Rightarrow> 'a astate up \<Rightarrow> 'a" ("aval\<^isup>#") where
-"aval' _ bot = Bot" |
-"aval' (N n) _ = num' n" |
-"aval' (V x) (Up S) = lookup S x" |
-"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
-
-lemma aval'_sound: "s <:: S \<Longrightarrow> aval a s <: aval' a S"
-by (induct a) (auto simp: rep_num' rep_plus')
-
-fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
-"afilter (N n) a S = (if n <: a then S else bot)" |
-"afilter (V x) a S = (case S of bot \<Rightarrow> bot | Up S \<Rightarrow>
- let a' = lookup S x \<sqinter> a in
- if a' \<sqsubseteq> Bot then bot else Up(update S x a'))" |
-"afilter (Plus e1 e2) a S =
- (let (a1,a2) = filter_plus' a (aval' e1 S) (aval' e2 S)
- in afilter e1 a1 (afilter e2 a2 S))"
-
-text{* The test for @{const Bot} in the @{const V}-case is important: @{const
-Bot} indicates that a variable has no possible values, i.e.\ that the current
-program point is unreachable. But then the abstract state should collapse to
-@{const bot}. Put differently, we maintain the invariant that in an abstract
-state all variables are mapped to non-@{const Bot} values. Otherwise the
-(pointwise) join of two abstract states, one of which contains @{const Bot}
-values, may produce too large a result, thus making the analysis less
-precise. *}
-
-
-fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
-"bfilter (B bv) res S = (if bv=res then S else bot)" |
-"bfilter (Not b) res S = bfilter b (\<not> res) S" |
-"bfilter (And b1 b2) res S =
- (if res then bfilter b1 True (bfilter b2 True S)
- else bfilter b1 False S \<squnion> bfilter b2 False S)" |
-"bfilter (Less e1 e2) res S =
- (let (res1,res2) = filter_less' res (aval' e1 S) (aval' e2 S)
- in afilter e1 res1 (afilter e2 res2 S))"
-
-lemma afilter_sound: "s <:: S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:: afilter e a S"
-proof(induction e arbitrary: a S)
- case N thus ?case by simp
-next
- case (V x)
- obtain S' where "S = Up S'" and "s <: S'" using `s <:: S` by auto
- moreover hence "s x <: lookup S' x" by(simp)
- moreover have "s x <: a" using V by simp
- ultimately show ?case using V(1)
- by(simp add: lookup_update Let_def)
- (metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
-next
- case (Plus e1 e2) thus ?case
- using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
- by (auto split: prod.split)
-qed
-
-lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S"
-proof(induction b arbitrary: S bv)
- case B thus ?case by simp
-next
- case (Not b) thus ?case by simp
-next
- case (And b1 b2) thus ?case by (auto simp: in_rep_join_UpI)
-next
- case (Less e1 e2) thus ?case
- by (auto split: prod.split)
- (metis afilter_sound filter_less' aval'_sound Less)
-qed
-
-fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
-"AI SKIP S = S" |
-"AI (x ::= a) S =
- (case S of bot \<Rightarrow> bot | Up S \<Rightarrow> Up(update S x (aval' a (Up S))))" |
-"AI (c1;c2) S = AI c2 (AI c1 S)" |
-"AI (IF b THEN c1 ELSE c2) S =
- AI c1 (bfilter b True S) \<squnion> AI c2 (bfilter b False S)" |
-"AI (WHILE b DO c) S =
- bfilter b False (pfp (\<lambda>S. AI c (bfilter b True S)) S)"
-
-lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
-proof(induction c arbitrary: s t S)
- case SKIP thus ?case by fastforce
-next
- case Assign thus ?case
- by (auto simp: lookup_update aval'_sound)
-next
- case Semi thus ?case by fastforce
-next
- case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
-next
- case (While b c)
- let ?P = "pfp (\<lambda>S. AI c (bfilter b True S)) S"
- { fix s t
- have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
- t <:: bfilter b False ?P"
- proof(induction "WHILE b DO c" s t rule: big_step_induct)
- case WhileFalse thus ?case by(metis bfilter_sound)
- next
- case WhileTrue show ?case
- by(rule WhileTrue, rule in_rep_up_trans[OF _ pfp],
- rule While.IH[OF WhileTrue(2)],
- rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1))
- qed
- }
- with in_rep_up_trans[OF `s <:: S` above] While(2,3) AI.simps(5)
- show ?case by simp
-qed
-
-end
-
-end
--- a/src/HOL/IMP/AbsInt1_ivl.thy Mon Sep 26 21:13:26 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,260 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory AbsInt1_ivl
-imports AbsInt1
-begin
-
-subsection "Interval Analysis"
-
-datatype ivl = I "int option" "int option"
-
-text{* We assume an important invariant: arithmetic operations are never
-applied to empty intervals @{term"I (Some i) (Some j)"} with @{term"j <
-i"}. This avoids special cases. Why can we assume this? Because an empty
-interval of values for a variable means that the current program point is
-unreachable. But this should actually translate into the bottom state, not a
-state where some variables have empty intervals. *}
-
-definition "rep_ivl i =
- (case i of I (Some l) (Some h) \<Rightarrow> {l..h} | I (Some l) None \<Rightarrow> {l..}
- | I None (Some h) \<Rightarrow> {..h} | I None None \<Rightarrow> UNIV)"
-
-definition "num_ivl n = I (Some n) (Some n)"
-
-instantiation option :: (plus)plus
-begin
-
-fun plus_option where
-"Some x + Some y = Some(x+y)" |
-"_ + _ = None"
-
-instance proof qed
-
-end
-
-definition empty where "empty = I (Some 1) (Some 0)"
-
-fun is_empty where
-"is_empty(I (Some l) (Some h)) = (h<l)" |
-"is_empty _ = False"
-
-lemma [simp]: "is_empty(I l h) =
- (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
-by(auto split:option.split)
-
-lemma [simp]: "is_empty i \<Longrightarrow> rep_ivl i = {}"
-by(auto simp add: rep_ivl_def split: ivl.split option.split)
-
-definition "plus_ivl i1 i2 = ((*if is_empty i1 | is_empty i2 then empty else*)
- case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
-
-instantiation ivl :: SL_top
-begin
-
-definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where
-"le_option pos x y =
- (case x of (Some i) \<Rightarrow> (case y of Some j \<Rightarrow> i\<le>j | None \<Rightarrow> pos)
- | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))"
-
-fun le_aux where
-"le_aux (I l1 h1) (I l2 h2) = (le_option False l2 l1 & le_option True h1 h2)"
-
-definition le_ivl where
-"i1 \<sqsubseteq> i2 =
- (if is_empty i1 then True else
- if is_empty i2 then False else le_aux i1 i2)"
-
-definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
-"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)"
-
-definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
-"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)"
-
-definition "i1 \<squnion> i2 =
- (if is_empty i1 then i2 else if is_empty i2 then i1
- else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
- I (min_option False l1 l2) (max_option True h1 h2))"
-
-definition "Top = I None None"
-
-instance
-proof
- case goal1 thus ?case
- by(cases x, simp add: le_ivl_def le_option_def split: option.split)
-next
- case goal2 thus ?case
- by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits)
-next
- case goal3 thus ?case
- by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
-next
- case goal4 thus ?case
- by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
-next
- case goal5 thus ?case
- by(cases x, cases y, cases z, auto simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits if_splits)
-next
- case goal6 thus ?case
- by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split)
-qed
-
-end
-
-
-instantiation ivl :: L_top_bot
-begin
-
-definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
- case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
- I (max_option False l1 l2) (min_option True h1 h2))"
-
-definition "Bot = empty"
-
-instance
-proof
- case goal1 thus ?case
- by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
-next
- case goal2 thus ?case
- by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
-next
- case goal3 thus ?case
- by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_option_def max_option_def min_option_def split: option.splits if_splits)
-next
- case goal4 show ?case by(cases x, simp add: Bot_ivl_def empty_def le_ivl_def)
-qed
-
-end
-
-instantiation option :: (minus)minus
-begin
-
-fun minus_option where
-"Some x - Some y = Some(x-y)" |
-"_ - _ = None"
-
-instance proof qed
-
-end
-
-definition "minus_ivl i1 i2 = ((*if is_empty i1 | is_empty i2 then empty else*)
- case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
-
-lemma rep_minus_ivl:
- "n1 : rep_ivl i1 \<Longrightarrow> n2 : rep_ivl i2 \<Longrightarrow> n1-n2 : rep_ivl(minus_ivl i1 i2)"
-by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)
-
-
-definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
- i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
-
-fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
-"filter_less_ivl res (I l1 h1) (I l2 h2) =
- ((*if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else*)
- if res
- then (I l1 (min_option True h1 (h2 - Some 1)),
- I (max_option False (l1 + Some 1) l2) h2)
- else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
-
-interpretation Rep rep_ivl
-proof
- case goal1 thus ?case
- by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
-qed
-
-interpretation Val_abs rep_ivl num_ivl plus_ivl
-proof
- case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)
-next
- case goal2 thus ?case
- by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
-qed
-
-interpretation Rep1 rep_ivl
-proof
- case goal1 thus ?case
- by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
-next
- case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
-qed
-
-interpretation
- Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
-proof
- case goal1 thus ?case
- by(auto simp add: filter_plus_ivl_def)
- (metis rep_minus_ivl add_diff_cancel add_commute)+
-next
- case goal2 thus ?case
- by(cases a1, cases a2,
- auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
-qed
-
-interpretation
- Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
-defines afilter_ivl is afilter
-and bfilter_ivl is bfilter
-and AI_ivl is AI
-and aval_ivl is aval'
-proof qed (auto simp: iter'_pfp_above)
-
-
-fun list_up where
-"list_up bot = bot" |
-"list_up (Up x) = Up(list x)"
-
-value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)"
-value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)"
-value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4))
- (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
-value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5))
- (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
-value [code] "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10))
- (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
-value [code] "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10))
- (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
-
-value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
- (Up(FunDom(Top(''x'':= I (Some 0) (Some 0)))[''x''])))"
-value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
- (Up(FunDom(Top(''x'':= I (Some 0) (Some 2)))[''x''])))"
-value [code] "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True
- (Up(FunDom(Top(''x'':= I (Some 15) (Some 20),''y'':= I (Some 5) (Some 7)))[''x'', ''y''])))"
-
-definition "test_ivl1 =
- ''y'' ::= N 7;
- IF Less (V ''x'') (V ''y'')
- THEN ''y'' ::= Plus (V ''y'') (V ''x'')
- ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
-value [code] "list_up(AI_ivl test_ivl1 Top)"
-
-value "list_up (AI_ivl test3_const Top)"
-
-value "list_up (AI_ivl test5_const Top)"
-
-value "list_up (AI_ivl test6_const Top)"
-
-definition "test2_ivl =
- ''y'' ::= N 7;
- WHILE Less (V ''x'') (N 100) DO ''y'' ::= Plus (V ''y'') (N 1)"
-value [code] "list_up(AI_ivl test2_ivl Top)"
-
-definition "test3_ivl =
- ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
- WHILE Less (V ''x'') (N 11)
- DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
-value [code] "list_up(AI_ivl test3_ivl Top)"
-
-definition "test4_ivl =
- ''x'' ::= N 0; ''y'' ::= N 0;
- WHILE Less (V ''x'') (N 1001)
- DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
-value [code] "list_up(AI_ivl test4_ivl Top)"
-
-text{* Nontermination not detected: *}
-definition "test5_ivl =
- ''x'' ::= N 0;
- WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
-value [code] "list_up(AI_ivl test5_ivl Top)"
-
-end
--- a/src/HOL/IMP/AbsInt2.thy Mon Sep 26 21:13:26 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,207 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory AbsInt2
-imports AbsInt1_ivl
-begin
-
-context preord
-begin
-
-definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
-
-lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def)
-
-lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)"
-by(simp add: mono_def)
-
-declare le_trans[trans]
-
-end
-
-
-subsection "Widening and Narrowing"
-
-text{* Jumping to the trivial post-fixed point @{const Top} in case @{text k}
-rounds of iteration did not reach a post-fixed point (as in @{const iter}) is
-a trivial widening step. We generalise this idea and complement it with
-narrowing, a process to regain precision.
-
-Class @{text WN} makes some assumptions about the widening and narrowing
-operators. The assumptions serve two purposes. Together with a further
-assumption that certain chains become stationary, they permit to prove
-termination of the fixed point iteration, which we do not --- we limit the
-number of iterations as before. The second purpose of the narrowing
-assumptions is to prove that the narrowing iteration keeps on producing
-post-fixed points and that it goes down. However, this requires the function
-being iterated to be monotone. Unfortunately, abstract interpretation with
-widening is not monotone. Hence the (recursive) abstract interpretation of a
-loop body that again contains a loop may result in a non-monotone
-function. Therefore our narrowing iteration needs to check at every step
-that a post-fixed point is maintained, and we cannot prove that the precision
-increases. *}
-
-class WN = SL_top +
-fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
-assumes widen: "y \<sqsubseteq> x \<nabla> y"
-fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
-assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
-assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
-begin
-
-fun iter_up :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter_up f 0 x = Top" |
-"iter_up f (Suc n) x =
- (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla> fx))"
-
-lemma iter_up_pfp: "f(iter_up f n x) \<sqsubseteq> iter_up f n x"
-apply (induction n arbitrary: x)
- apply (simp)
-apply (simp add: Let_def)
-done
-
-fun iter_down :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter_down f 0 x = x" |
-"iter_down f (Suc n) x =
- (let y = x \<triangle> f x in if f y \<sqsubseteq> y then iter_down f n y else x)"
-
-lemma iter_down_pfp: "f x \<sqsubseteq> x \<Longrightarrow> f(iter_down f n x) \<sqsubseteq> iter_down f n x"
-apply (induction n arbitrary: x)
- apply (simp)
-apply (simp add: Let_def)
-done
-
-definition iter' :: "nat \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter' m n f x =
- (let f' = (\<lambda>y. x \<squnion> f y) in iter_down f' n (iter_up f' m x))"
-
-lemma iter'_pfp_above:
-shows "f(iter' m n f x0) \<sqsubseteq> iter' m n f x0"
-and "x0 \<sqsubseteq> iter' m n f x0"
-using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> f x"]
-by(auto simp add: iter'_def Let_def)
-
-text{* This is how narrowing works on monotone functions: you just iterate. *}
-
-abbreviation iter_down_mono :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter_down_mono f n x == ((\<lambda>x. x \<triangle> f x)^^n) x"
-
-text{* Narrowing always yields a post-fixed point: *}
-
-lemma iter_down_mono_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0"
-defines "x n == iter_down_mono f n x0"
-shows "f(x n) \<sqsubseteq> x n"
-proof (induction n)
- case 0 show ?case by (simp add: x_def assms(2))
-next
- case (Suc n)
- have "f (x (Suc n)) = f(x n \<triangle> f(x n))" by(simp add: x_def)
- also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2[OF Suc]])
- also have "\<dots> \<sqsubseteq> x n \<triangle> f(x n)" by(rule narrow1[OF Suc])
- also have "\<dots> = x(Suc n)" by(simp add: x_def)
- finally show ?case .
-qed
-
-text{* Narrowing can only increase precision: *}
-
-lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0"
-defines "x n == iter_down_mono f n x0"
-shows "x n \<sqsubseteq> x0"
-proof (induction n)
- case 0 show ?case by(simp add: x_def)
-next
- case (Suc n)
- have "x(Suc n) = x n \<triangle> f(x n)" by(simp add: x_def)
- also have "\<dots> \<sqsubseteq> x n" unfolding x_def
- by(rule narrow2[OF iter_down_mono_pfp[OF assms(1), OF assms(2)]])
- also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
- finally show ?case .
-qed
-
-
-end
-
-
-instantiation ivl :: WN
-begin
-
-definition "widen_ivl ivl1 ivl2 =
- ((*if is_empty ivl1 then ivl2 else if is_empty ivl2 then ivl1 else*)
- case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
- I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l2)
- (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h2))"
-
-definition "narrow_ivl ivl1 ivl2 =
- ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
- case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
- I (if l1 = None then l2 else l1)
- (if h1 = None then h2 else h1))"
-
-instance
-proof qed
- (auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
-
-end
-
-instantiation astate :: (WN) WN
-begin
-
-definition "widen_astate F1 F2 =
- FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"
-
-definition "narrow_astate F1 F2 =
- FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))"
-
-instance
-proof
- case goal1 thus ?case
- by(simp add: widen_astate_def le_astate_def lookup_def widen)
-next
- case goal2 thus ?case
- by(auto simp: narrow_astate_def le_astate_def lookup_def narrow1)
-next
- case goal3 thus ?case
- by(auto simp: narrow_astate_def le_astate_def lookup_def narrow2)
-qed
-
-end
-
-instantiation up :: (WN) WN
-begin
-
-fun widen_up where
-"widen_up bot x = x" |
-"widen_up x bot = x" |
-"widen_up (Up x) (Up y) = Up(x \<nabla> y)"
-
-fun narrow_up where
-"narrow_up bot x = bot" |
-"narrow_up x bot = bot" |
-"narrow_up (Up x) (Up y) = Up(x \<triangle> y)"
-
-instance
-proof
- case goal1 show ?case
- by(induct x y rule: widen_up.induct) (simp_all add: widen)
-next
- case goal2 thus ?case
- by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
-next
- case goal3 thus ?case
- by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
-qed
-
-end
-
-interpretation
- Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
-defines afilter_ivl' is afilter
-and bfilter_ivl' is bfilter
-and AI_ivl' is AI
-and aval_ivl' is aval'
-proof qed (auto simp: iter'_pfp_above)
-
-value [code] "list_up(AI_ivl' test3_ivl Top)"
-value [code] "list_up(AI_ivl' test4_ivl Top)"
-value [code] "list_up(AI_ivl' test5_ivl Top)"
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int0.thy Wed Sep 28 08:51:55 2011 +0200
@@ -0,0 +1,67 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int0
+imports Abs_State
+begin
+
+subsection "Computable Abstract Interpretation"
+
+text{* Abstract interpretation over type @{text astate} instead of
+functions. *}
+
+locale Abs_Int = Val_abs +
+fixes pfp :: "('a astate \<Rightarrow> 'a astate) \<Rightarrow> 'a astate \<Rightarrow> 'a astate"
+assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
+assumes above: "x0 \<sqsubseteq> pfp f x0"
+begin
+
+fun aval' :: "aexp \<Rightarrow> 'a astate \<Rightarrow> 'a" where
+"aval' (N n) _ = num' n" |
+"aval' (V x) S = lookup S x" |
+"aval' (Plus e1 e2) S = plus' (aval' e1 S) (aval' e2 S)"
+
+abbreviation astate_in_rep (infix "<:" 50) where
+"s <: S == ALL x. s x <: lookup S x"
+
+lemma astate_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
+by (metis in_mono le_astate_def le_rep lookup_def top)
+
+lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
+by (induct a) (auto simp: rep_num' rep_plus')
+
+
+fun AI :: "com \<Rightarrow> 'a astate \<Rightarrow> 'a astate" where
+"AI SKIP S = S" |
+"AI (x ::= a) S = update S x (aval' a S)" |
+"AI (c1;c2) S = AI c2 (AI c1 S)" |
+"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
+"AI (WHILE b DO c) S = pfp (AI c) S"
+
+lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
+proof(induction c arbitrary: s t S0)
+ case SKIP thus ?case by fastforce
+next
+ case Assign thus ?case
+ by (auto simp: lookup_update aval'_sound)
+next
+ case Semi thus ?case by auto
+next
+ case If thus ?case
+ by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2)
+next
+ case (While b c)
+ let ?P = "pfp (AI c) S0"
+ { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
+ proof(induction "WHILE b DO c" s t rule: big_step_induct)
+ case WhileFalse thus ?case by simp
+ next
+ case WhileTrue thus ?case using While.IH pfp astate_in_rep_le by metis
+ qed
+ }
+ with astate_in_rep_le[OF `s <: S0` above]
+ show ?case by (metis While(2) AI.simps(5))
+qed
+
+end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int0_const.thy Wed Sep 28 08:51:55 2011 +0200
@@ -0,0 +1,111 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int0_const
+imports Abs_Int0
+begin
+
+subsection "Constant Propagation"
+
+datatype cval = Const val | Any
+
+fun rep_cval where
+"rep_cval (Const n) = {n}" |
+"rep_cval (Any) = UNIV"
+
+fun plus_cval where
+"plus_cval (Const m) (Const n) = Const(m+n)" |
+"plus_cval _ _ = Any"
+
+instantiation cval :: SL_top
+begin
+
+fun le_cval where
+"_ \<sqsubseteq> Any = True" |
+"Const n \<sqsubseteq> Const m = (n=m)" |
+"Any \<sqsubseteq> Const _ = False"
+
+fun join_cval where
+"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
+"_ \<squnion> _ = Any"
+
+definition "Top = Any"
+
+instance
+proof
+ case goal1 thus ?case by (cases x) simp_all
+next
+ case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
+next
+ case goal3 thus ?case by(cases x, cases y, simp_all)
+next
+ case goal4 thus ?case by(cases y, cases x, simp_all)
+next
+ case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
+next
+ case goal6 thus ?case by(simp add: Top_cval_def)
+qed
+
+end
+
+interpretation Rep rep_cval
+proof
+ case goal1 thus ?case
+ by(cases a, cases b, simp, simp, cases b, simp, simp)
+qed
+
+interpretation Val_abs rep_cval Const plus_cval
+proof
+ case goal1 show ?case by simp
+next
+ case goal2 thus ?case
+ by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
+qed
+
+interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
+defines AI_const is AI
+and aval'_const is aval'
+proof qed (auto simp: iter'_pfp_above)
+
+text{* Straight line code: *}
+definition "test1_const =
+ ''y'' ::= N 7;
+ ''z'' ::= Plus (V ''y'') (N 2);
+ ''y'' ::= Plus (V ''x'') (N 0)"
+
+text{* Conditional: *}
+definition "test2_const =
+ IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
+
+text{* Conditional, test is ignored: *}
+definition "test3_const =
+ ''x'' ::= N 42;
+ IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
+
+text{* While: *}
+definition "test4_const =
+ ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
+
+text{* While, test is ignored: *}
+definition "test5_const =
+ ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
+
+text{* Iteration is needed: *}
+definition "test6_const =
+ ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
+ WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
+
+text{* More iteration would be needed: *}
+definition "test7_const =
+ ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
+ WHILE Less (V ''x'') (N 1)
+ DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
+
+value [code] "list (AI_const test1_const Top)"
+value [code] "list (AI_const test2_const Top)"
+value [code] "list (AI_const test3_const Top)"
+value [code] "list (AI_const test4_const Top)"
+value [code] "list (AI_const test5_const Top)"
+value [code] "list (AI_const test6_const Top)"
+value [code] "list (AI_const test7_const Top)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int0_fun.thy Wed Sep 28 08:51:55 2011 +0200
@@ -0,0 +1,187 @@
+(* Author: Tobias Nipkow *)
+
+header "Denotational Abstract Interpretation"
+
+theory Abs_Int0_fun
+imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
+begin
+
+subsection "Orderings"
+
+class preord =
+fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
+assumes le_refl[simp]: "x \<sqsubseteq> x"
+and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
+
+text{* Note: no antisymmetry. Allows implementations where some abstract
+element is implemented by two different values @{prop "x \<noteq> y"}
+such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not
+needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}.
+*}
+
+class SL_top = preord +
+fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
+fixes Top :: "'a"
+assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
+and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
+and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
+and top[simp]: "x \<sqsubseteq> Top"
+begin
+
+lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
+by (metis join_ge1 join_ge2 join_least le_trans)
+
+fun iter :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter 0 f _ = Top" |
+"iter (Suc n) f x = (if f x \<sqsubseteq> x then x else iter n f (f x))"
+
+lemma iter_pfp: "f(iter n f x) \<sqsubseteq> iter n f x"
+apply (induction n arbitrary: x)
+ apply (simp)
+apply (simp)
+done
+
+abbreviation iter' :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter' n f x0 == iter n (\<lambda>x. x0 \<squnion> f x) x0"
+
+lemma iter'_pfp_above:
+ "f(iter' n f x0) \<sqsubseteq> iter' n f x0" "x0 \<sqsubseteq> iter' n f x0"
+using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"] by auto
+
+text{* So much for soundness. But how good an approximation of the post-fixed
+point does @{const iter} yield? *}
+
+lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
+apply(induction n arbitrary: x)
+ apply simp
+apply (auto)
+ apply(metis funpow.simps(1) id_def)
+by (metis funpow.simps(2) funpow_swap1 o_apply)
+
+text{* For monotone @{text f}, @{term "iter f n x0"} yields the least
+post-fixed point above @{text x0}, unless it yields @{text Top}. *}
+
+lemma iter_least_pfp:
+assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter n f x0 \<noteq> Top"
+and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter n f x0 \<sqsubseteq> p"
+proof-
+ obtain k where "iter n f x0 = (f^^k) x0"
+ using iter_funpow[OF `iter n f x0 \<noteq> Top`] by blast
+ moreover
+ { fix n have "(f^^n) x0 \<sqsubseteq> p"
+ proof(induction n)
+ case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
+ next
+ case (Suc n) thus ?case
+ by (simp add: `x0 \<sqsubseteq> p`)(metis Suc assms(3) le_trans mono)
+ qed
+ } ultimately show ?thesis by simp
+qed
+
+end
+
+text{* The interface of abstract values: *}
+
+locale Rep =
+fixes rep :: "'a::SL_top \<Rightarrow> 'b set"
+assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
+begin
+
+abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a"
+
+lemma in_rep_join: "x <: a1 \<or> x <: a2 \<Longrightarrow> x <: a1 \<squnion> a2"
+by (metis SL_top_class.join_ge1 SL_top_class.join_ge2 le_rep subsetD)
+
+end
+
+locale Val_abs = Rep rep
+ for rep :: "'a::SL_top \<Rightarrow> val set" +
+fixes num' :: "val \<Rightarrow> 'a"
+and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+assumes rep_num': "rep(num' n) = {n}"
+and rep_plus': "n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: plus' a1 a2"
+
+
+instantiation "fun" :: (type, SL_top) SL_top
+begin
+
+definition "f \<sqsubseteq> g = (ALL x. f x \<sqsubseteq> g x)"
+definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+definition "Top = (\<lambda>x. Top)"
+
+lemma join_apply[simp]:
+ "(f \<squnion> g) x = f x \<squnion> g x"
+by (simp add: join_fun_def)
+
+instance
+proof
+ case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
+qed (simp_all add: le_fun_def Top_fun_def)
+
+end
+
+subsection "Abstract Interpretation Abstractly"
+
+text{* Abstract interpretation over abstract values. Abstract states are
+simply functions. The post-fixed point finder is parameterized over. *}
+
+type_synonym 'a st = "name \<Rightarrow> 'a"
+
+locale Abs_Int_Fun = Val_abs +
+fixes pfp :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
+assumes pfp: "f(pfp f x) \<sqsubseteq> pfp f x"
+assumes above: "x \<sqsubseteq> pfp f x"
+begin
+
+fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a" where
+"aval' (N n) _ = num' n" |
+"aval' (V x) S = S x" |
+"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
+
+abbreviation fun_in_rep (infix "<:" 50) where
+"f <: F == \<forall>x. f x <: F x"
+
+lemma fun_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
+by (metis le_fun_def le_rep subsetD)
+
+lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
+by (induct a) (auto simp: rep_num' rep_plus')
+
+fun AI :: "com \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> 'a)" where
+"AI SKIP S = S" |
+"AI (x ::= a) S = S(x := aval' a S)" |
+"AI (c1;c2) S = AI c2 (AI c1 S)" |
+"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
+"AI (WHILE b DO c) S = pfp (AI c) S"
+
+lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
+proof(induction c arbitrary: s t S0)
+ case SKIP thus ?case by fastforce
+next
+ case Assign thus ?case by (auto simp: aval'_sound)
+next
+ case Semi thus ?case by auto
+next
+ case If thus ?case by(auto simp: in_rep_join)
+next
+ case (While b c)
+ let ?P = "pfp (AI c) S0"
+ { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
+ proof(induction "WHILE b DO c" s t rule: big_step_induct)
+ case WhileFalse thus ?case by simp
+ next
+ case WhileTrue thus ?case by(metis While.IH pfp fun_in_rep_le)
+ qed
+ }
+ with fun_in_rep_le[OF `s <: S0` above]
+ show ?case by (metis While(2) AI.simps(5))
+qed
+
+end
+
+
+text{* Problem: not executable because of the comparison of abstract states,
+i.e. functions, in the post-fixedpoint computation. Need to implement
+abstract states concretely. *}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int1.thy Wed Sep 28 08:51:55 2011 +0200
@@ -0,0 +1,214 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int1
+imports Abs_Int0_const
+begin
+
+subsection "Backward Analysis of Expressions"
+
+class L_top_bot = SL_top +
+fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
+and Bot :: "'a"
+assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
+and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
+and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
+assumes bot[simp]: "Bot \<sqsubseteq> x"
+
+locale Rep1 = Rep rep for rep :: "'a::L_top_bot \<Rightarrow> 'b set" +
+assumes inter_rep_subset_rep_meet: "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
+and rep_Bot: "rep Bot = {}"
+begin
+
+lemma in_rep_meet: "x <: a1 \<Longrightarrow> x <: a2 \<Longrightarrow> x <: a1 \<sqinter> a2"
+by (metis IntI inter_rep_subset_rep_meet set_mp)
+
+lemma rep_meet[simp]: "rep(a1 \<sqinter> a2) = rep a1 \<inter> rep a2"
+by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2)
+
+end
+
+
+locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
+ for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' +
+fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
+and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
+assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
+ n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
+and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
+ n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
+
+datatype 'a up = bot | Up 'a
+
+instantiation up :: (SL_top)SL_top
+begin
+
+fun le_up where
+"Up x \<sqsubseteq> Up y = (x \<sqsubseteq> y)" |
+"bot \<sqsubseteq> y = True" |
+"Up _ \<sqsubseteq> bot = False"
+
+lemma [simp]: "(x \<sqsubseteq> bot) = (x = bot)"
+by (cases x) simp_all
+
+lemma [simp]: "(Up x \<sqsubseteq> u) = (EX y. u = Up y & x \<sqsubseteq> y)"
+by (cases u) auto
+
+fun join_up where
+"Up x \<squnion> Up y = Up(x \<squnion> y)" |
+"bot \<squnion> y = y" |
+"x \<squnion> bot = x"
+
+lemma [simp]: "x \<squnion> bot = x"
+by (cases x) simp_all
+
+
+definition "Top = Up Top"
+
+instance proof
+ case goal1 show ?case by(cases x, simp_all)
+next
+ case goal2 thus ?case
+ by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
+next
+ case goal3 thus ?case by(cases x, simp, cases y, simp_all)
+next
+ case goal4 thus ?case by(cases y, simp, cases x, simp_all)
+next
+ case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
+next
+ case goal6 thus ?case by(cases x, simp_all add: Top_up_def)
+qed
+
+end
+
+
+locale Abs_Int1 = Val_abs1 +
+fixes pfp :: "('a astate up \<Rightarrow> 'a astate up) \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up"
+assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
+assumes above: "x0 \<sqsubseteq> pfp f x0"
+begin
+
+(* FIXME avoid duplicating this defn *)
+abbreviation astate_in_rep (infix "<:" 50) where
+"s <: S == ALL x. s x <: lookup S x"
+
+abbreviation in_rep_up :: "state \<Rightarrow> 'a astate up \<Rightarrow> bool" (infix "<::" 50) where
+"s <:: S == EX S0. S = Up S0 \<and> s <: S0"
+
+lemma in_rep_up_trans: "(s::state) <:: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:: T"
+apply auto
+by (metis in_mono le_astate_def le_rep lookup_def top)
+
+lemma in_rep_join_UpI: "s <:: S1 | s <:: S2 \<Longrightarrow> s <:: S1 \<squnion> S2"
+by (metis in_rep_up_trans SL_top_class.join_ge1 SL_top_class.join_ge2)
+
+fun aval' :: "aexp \<Rightarrow> 'a astate up \<Rightarrow> 'a" ("aval\<^isup>#") where
+"aval' _ bot = Bot" |
+"aval' (N n) _ = num' n" |
+"aval' (V x) (Up S) = lookup S x" |
+"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
+
+lemma aval'_sound: "s <:: S \<Longrightarrow> aval a s <: aval' a S"
+by (induct a) (auto simp: rep_num' rep_plus')
+
+fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
+"afilter (N n) a S = (if n <: a then S else bot)" |
+"afilter (V x) a S = (case S of bot \<Rightarrow> bot | Up S \<Rightarrow>
+ let a' = lookup S x \<sqinter> a in
+ if a' \<sqsubseteq> Bot then bot else Up(update S x a'))" |
+"afilter (Plus e1 e2) a S =
+ (let (a1,a2) = filter_plus' a (aval' e1 S) (aval' e2 S)
+ in afilter e1 a1 (afilter e2 a2 S))"
+
+text{* The test for @{const Bot} in the @{const V}-case is important: @{const
+Bot} indicates that a variable has no possible values, i.e.\ that the current
+program point is unreachable. But then the abstract state should collapse to
+@{const bot}. Put differently, we maintain the invariant that in an abstract
+state all variables are mapped to non-@{const Bot} values. Otherwise the
+(pointwise) join of two abstract states, one of which contains @{const Bot}
+values, may produce too large a result, thus making the analysis less
+precise. *}
+
+
+fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
+"bfilter (B bv) res S = (if bv=res then S else bot)" |
+"bfilter (Not b) res S = bfilter b (\<not> res) S" |
+"bfilter (And b1 b2) res S =
+ (if res then bfilter b1 True (bfilter b2 True S)
+ else bfilter b1 False S \<squnion> bfilter b2 False S)" |
+"bfilter (Less e1 e2) res S =
+ (let (res1,res2) = filter_less' res (aval' e1 S) (aval' e2 S)
+ in afilter e1 res1 (afilter e2 res2 S))"
+
+lemma afilter_sound: "s <:: S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:: afilter e a S"
+proof(induction e arbitrary: a S)
+ case N thus ?case by simp
+next
+ case (V x)
+ obtain S' where "S = Up S'" and "s <: S'" using `s <:: S` by auto
+ moreover hence "s x <: lookup S' x" by(simp)
+ moreover have "s x <: a" using V by simp
+ ultimately show ?case using V(1)
+ by(simp add: lookup_update Let_def)
+ (metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
+next
+ case (Plus e1 e2) thus ?case
+ using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
+ by (auto split: prod.split)
+qed
+
+lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S"
+proof(induction b arbitrary: S bv)
+ case B thus ?case by simp
+next
+ case (Not b) thus ?case by simp
+next
+ case (And b1 b2) thus ?case by (auto simp: in_rep_join_UpI)
+next
+ case (Less e1 e2) thus ?case
+ by (auto split: prod.split)
+ (metis afilter_sound filter_less' aval'_sound Less)
+qed
+
+fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
+"AI SKIP S = S" |
+"AI (x ::= a) S =
+ (case S of bot \<Rightarrow> bot | Up S \<Rightarrow> Up(update S x (aval' a (Up S))))" |
+"AI (c1;c2) S = AI c2 (AI c1 S)" |
+"AI (IF b THEN c1 ELSE c2) S =
+ AI c1 (bfilter b True S) \<squnion> AI c2 (bfilter b False S)" |
+"AI (WHILE b DO c) S =
+ bfilter b False (pfp (\<lambda>S. AI c (bfilter b True S)) S)"
+
+lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
+proof(induction c arbitrary: s t S)
+ case SKIP thus ?case by fastforce
+next
+ case Assign thus ?case
+ by (auto simp: lookup_update aval'_sound)
+next
+ case Semi thus ?case by fastforce
+next
+ case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
+next
+ case (While b c)
+ let ?P = "pfp (\<lambda>S. AI c (bfilter b True S)) S"
+ { fix s t
+ have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
+ t <:: bfilter b False ?P"
+ proof(induction "WHILE b DO c" s t rule: big_step_induct)
+ case WhileFalse thus ?case by(metis bfilter_sound)
+ next
+ case WhileTrue show ?case
+ by(rule WhileTrue, rule in_rep_up_trans[OF _ pfp],
+ rule While.IH[OF WhileTrue(2)],
+ rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1))
+ qed
+ }
+ with in_rep_up_trans[OF `s <:: S` above] While(2,3) AI.simps(5)
+ show ?case by simp
+qed
+
+end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int1_ivl.thy Wed Sep 28 08:51:55 2011 +0200
@@ -0,0 +1,260 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int1_ivl
+imports Abs_Int1
+begin
+
+subsection "Interval Analysis"
+
+datatype ivl = I "int option" "int option"
+
+text{* We assume an important invariant: arithmetic operations are never
+applied to empty intervals @{term"I (Some i) (Some j)"} with @{term"j <
+i"}. This avoids special cases. Why can we assume this? Because an empty
+interval of values for a variable means that the current program point is
+unreachable. But this should actually translate into the bottom state, not a
+state where some variables have empty intervals. *}
+
+definition "rep_ivl i =
+ (case i of I (Some l) (Some h) \<Rightarrow> {l..h} | I (Some l) None \<Rightarrow> {l..}
+ | I None (Some h) \<Rightarrow> {..h} | I None None \<Rightarrow> UNIV)"
+
+definition "num_ivl n = I (Some n) (Some n)"
+
+instantiation option :: (plus)plus
+begin
+
+fun plus_option where
+"Some x + Some y = Some(x+y)" |
+"_ + _ = None"
+
+instance proof qed
+
+end
+
+definition empty where "empty = I (Some 1) (Some 0)"
+
+fun is_empty where
+"is_empty(I (Some l) (Some h)) = (h<l)" |
+"is_empty _ = False"
+
+lemma [simp]: "is_empty(I l h) =
+ (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
+by(auto split:option.split)
+
+lemma [simp]: "is_empty i \<Longrightarrow> rep_ivl i = {}"
+by(auto simp add: rep_ivl_def split: ivl.split option.split)
+
+definition "plus_ivl i1 i2 = ((*if is_empty i1 | is_empty i2 then empty else*)
+ case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
+
+instantiation ivl :: SL_top
+begin
+
+definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where
+"le_option pos x y =
+ (case x of (Some i) \<Rightarrow> (case y of Some j \<Rightarrow> i\<le>j | None \<Rightarrow> pos)
+ | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))"
+
+fun le_aux where
+"le_aux (I l1 h1) (I l2 h2) = (le_option False l2 l1 & le_option True h1 h2)"
+
+definition le_ivl where
+"i1 \<sqsubseteq> i2 =
+ (if is_empty i1 then True else
+ if is_empty i2 then False else le_aux i1 i2)"
+
+definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
+"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)"
+
+definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
+"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)"
+
+definition "i1 \<squnion> i2 =
+ (if is_empty i1 then i2 else if is_empty i2 then i1
+ else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
+ I (min_option False l1 l2) (max_option True h1 h2))"
+
+definition "Top = I None None"
+
+instance
+proof
+ case goal1 thus ?case
+ by(cases x, simp add: le_ivl_def le_option_def split: option.split)
+next
+ case goal2 thus ?case
+ by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits)
+next
+ case goal3 thus ?case
+ by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
+next
+ case goal4 thus ?case
+ by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
+next
+ case goal5 thus ?case
+ by(cases x, cases y, cases z, auto simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits if_splits)
+next
+ case goal6 thus ?case
+ by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split)
+qed
+
+end
+
+
+instantiation ivl :: L_top_bot
+begin
+
+definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
+ case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
+ I (max_option False l1 l2) (min_option True h1 h2))"
+
+definition "Bot = empty"
+
+instance
+proof
+ case goal1 thus ?case
+ by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
+next
+ case goal2 thus ?case
+ by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
+next
+ case goal3 thus ?case
+ by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_option_def max_option_def min_option_def split: option.splits if_splits)
+next
+ case goal4 show ?case by(cases x, simp add: Bot_ivl_def empty_def le_ivl_def)
+qed
+
+end
+
+instantiation option :: (minus)minus
+begin
+
+fun minus_option where
+"Some x - Some y = Some(x-y)" |
+"_ - _ = None"
+
+instance proof qed
+
+end
+
+definition "minus_ivl i1 i2 = ((*if is_empty i1 | is_empty i2 then empty else*)
+ case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
+
+lemma rep_minus_ivl:
+ "n1 : rep_ivl i1 \<Longrightarrow> n2 : rep_ivl i2 \<Longrightarrow> n1-n2 : rep_ivl(minus_ivl i1 i2)"
+by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)
+
+
+definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
+ i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
+
+fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
+"filter_less_ivl res (I l1 h1) (I l2 h2) =
+ ((*if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else*)
+ if res
+ then (I l1 (min_option True h1 (h2 - Some 1)),
+ I (max_option False (l1 + Some 1) l2) h2)
+ else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
+
+interpretation Rep rep_ivl
+proof
+ case goal1 thus ?case
+ by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
+qed
+
+interpretation Val_abs rep_ivl num_ivl plus_ivl
+proof
+ case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)
+next
+ case goal2 thus ?case
+ by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
+qed
+
+interpretation Rep1 rep_ivl
+proof
+ case goal1 thus ?case
+ by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
+next
+ case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
+qed
+
+interpretation
+ Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+proof
+ case goal1 thus ?case
+ by(auto simp add: filter_plus_ivl_def)
+ (metis rep_minus_ivl add_diff_cancel add_commute)+
+next
+ case goal2 thus ?case
+ by(cases a1, cases a2,
+ auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
+qed
+
+interpretation
+ Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
+defines afilter_ivl is afilter
+and bfilter_ivl is bfilter
+and AI_ivl is AI
+and aval_ivl is aval'
+proof qed (auto simp: iter'_pfp_above)
+
+
+fun list_up where
+"list_up bot = bot" |
+"list_up (Up x) = Up(list x)"
+
+value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)"
+value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)"
+value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4))
+ (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
+value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5))
+ (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
+value [code] "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10))
+ (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
+value [code] "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10))
+ (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
+
+value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
+ (Up(FunDom(Top(''x'':= I (Some 0) (Some 0)))[''x''])))"
+value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
+ (Up(FunDom(Top(''x'':= I (Some 0) (Some 2)))[''x''])))"
+value [code] "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True
+ (Up(FunDom(Top(''x'':= I (Some 15) (Some 20),''y'':= I (Some 5) (Some 7)))[''x'', ''y''])))"
+
+definition "test_ivl1 =
+ ''y'' ::= N 7;
+ IF Less (V ''x'') (V ''y'')
+ THEN ''y'' ::= Plus (V ''y'') (V ''x'')
+ ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
+value [code] "list_up(AI_ivl test_ivl1 Top)"
+
+value "list_up (AI_ivl test3_const Top)"
+
+value "list_up (AI_ivl test5_const Top)"
+
+value "list_up (AI_ivl test6_const Top)"
+
+definition "test2_ivl =
+ ''y'' ::= N 7;
+ WHILE Less (V ''x'') (N 100) DO ''y'' ::= Plus (V ''y'') (N 1)"
+value [code] "list_up(AI_ivl test2_ivl Top)"
+
+definition "test3_ivl =
+ ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
+ WHILE Less (V ''x'') (N 11)
+ DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
+value [code] "list_up(AI_ivl test3_ivl Top)"
+
+definition "test4_ivl =
+ ''x'' ::= N 0; ''y'' ::= N 0;
+ WHILE Less (V ''x'') (N 1001)
+ DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
+value [code] "list_up(AI_ivl test4_ivl Top)"
+
+text{* Nontermination not detected: *}
+definition "test5_ivl =
+ ''x'' ::= N 0;
+ WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
+value [code] "list_up(AI_ivl test5_ivl Top)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int2.thy Wed Sep 28 08:51:55 2011 +0200
@@ -0,0 +1,207 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int2
+imports Abs_Int1_ivl
+begin
+
+context preord
+begin
+
+definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
+
+lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def)
+
+lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)"
+by(simp add: mono_def)
+
+declare le_trans[trans]
+
+end
+
+
+subsection "Widening and Narrowing"
+
+text{* Jumping to the trivial post-fixed point @{const Top} in case @{text k}
+rounds of iteration did not reach a post-fixed point (as in @{const iter}) is
+a trivial widening step. We generalise this idea and complement it with
+narrowing, a process to regain precision.
+
+Class @{text WN} makes some assumptions about the widening and narrowing
+operators. The assumptions serve two purposes. Together with a further
+assumption that certain chains become stationary, they permit to prove
+termination of the fixed point iteration, which we do not --- we limit the
+number of iterations as before. The second purpose of the narrowing
+assumptions is to prove that the narrowing iteration keeps on producing
+post-fixed points and that it goes down. However, this requires the function
+being iterated to be monotone. Unfortunately, abstract interpretation with
+widening is not monotone. Hence the (recursive) abstract interpretation of a
+loop body that again contains a loop may result in a non-monotone
+function. Therefore our narrowing iteration needs to check at every step
+that a post-fixed point is maintained, and we cannot prove that the precision
+increases. *}
+
+class WN = SL_top +
+fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
+assumes widen: "y \<sqsubseteq> x \<nabla> y"
+fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
+assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
+assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
+begin
+
+fun iter_up :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter_up f 0 x = Top" |
+"iter_up f (Suc n) x =
+ (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla> fx))"
+
+lemma iter_up_pfp: "f(iter_up f n x) \<sqsubseteq> iter_up f n x"
+apply (induction n arbitrary: x)
+ apply (simp)
+apply (simp add: Let_def)
+done
+
+fun iter_down :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter_down f 0 x = x" |
+"iter_down f (Suc n) x =
+ (let y = x \<triangle> f x in if f y \<sqsubseteq> y then iter_down f n y else x)"
+
+lemma iter_down_pfp: "f x \<sqsubseteq> x \<Longrightarrow> f(iter_down f n x) \<sqsubseteq> iter_down f n x"
+apply (induction n arbitrary: x)
+ apply (simp)
+apply (simp add: Let_def)
+done
+
+definition iter' :: "nat \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter' m n f x =
+ (let f' = (\<lambda>y. x \<squnion> f y) in iter_down f' n (iter_up f' m x))"
+
+lemma iter'_pfp_above:
+shows "f(iter' m n f x0) \<sqsubseteq> iter' m n f x0"
+and "x0 \<sqsubseteq> iter' m n f x0"
+using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> f x"]
+by(auto simp add: iter'_def Let_def)
+
+text{* This is how narrowing works on monotone functions: you just iterate. *}
+
+abbreviation iter_down_mono :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter_down_mono f n x == ((\<lambda>x. x \<triangle> f x)^^n) x"
+
+text{* Narrowing always yields a post-fixed point: *}
+
+lemma iter_down_mono_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0"
+defines "x n == iter_down_mono f n x0"
+shows "f(x n) \<sqsubseteq> x n"
+proof (induction n)
+ case 0 show ?case by (simp add: x_def assms(2))
+next
+ case (Suc n)
+ have "f (x (Suc n)) = f(x n \<triangle> f(x n))" by(simp add: x_def)
+ also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2[OF Suc]])
+ also have "\<dots> \<sqsubseteq> x n \<triangle> f(x n)" by(rule narrow1[OF Suc])
+ also have "\<dots> = x(Suc n)" by(simp add: x_def)
+ finally show ?case .
+qed
+
+text{* Narrowing can only increase precision: *}
+
+lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0"
+defines "x n == iter_down_mono f n x0"
+shows "x n \<sqsubseteq> x0"
+proof (induction n)
+ case 0 show ?case by(simp add: x_def)
+next
+ case (Suc n)
+ have "x(Suc n) = x n \<triangle> f(x n)" by(simp add: x_def)
+ also have "\<dots> \<sqsubseteq> x n" unfolding x_def
+ by(rule narrow2[OF iter_down_mono_pfp[OF assms(1), OF assms(2)]])
+ also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
+ finally show ?case .
+qed
+
+
+end
+
+
+instantiation ivl :: WN
+begin
+
+definition "widen_ivl ivl1 ivl2 =
+ ((*if is_empty ivl1 then ivl2 else if is_empty ivl2 then ivl1 else*)
+ case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
+ I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l2)
+ (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h2))"
+
+definition "narrow_ivl ivl1 ivl2 =
+ ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
+ case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
+ I (if l1 = None then l2 else l1)
+ (if h1 = None then h2 else h1))"
+
+instance
+proof qed
+ (auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
+
+end
+
+instantiation astate :: (WN) WN
+begin
+
+definition "widen_astate F1 F2 =
+ FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"
+
+definition "narrow_astate F1 F2 =
+ FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))"
+
+instance
+proof
+ case goal1 thus ?case
+ by(simp add: widen_astate_def le_astate_def lookup_def widen)
+next
+ case goal2 thus ?case
+ by(auto simp: narrow_astate_def le_astate_def lookup_def narrow1)
+next
+ case goal3 thus ?case
+ by(auto simp: narrow_astate_def le_astate_def lookup_def narrow2)
+qed
+
+end
+
+instantiation up :: (WN) WN
+begin
+
+fun widen_up where
+"widen_up bot x = x" |
+"widen_up x bot = x" |
+"widen_up (Up x) (Up y) = Up(x \<nabla> y)"
+
+fun narrow_up where
+"narrow_up bot x = bot" |
+"narrow_up x bot = bot" |
+"narrow_up (Up x) (Up y) = Up(x \<triangle> y)"
+
+instance
+proof
+ case goal1 show ?case
+ by(induct x y rule: widen_up.induct) (simp_all add: widen)
+next
+ case goal2 thus ?case
+ by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
+next
+ case goal3 thus ?case
+ by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
+qed
+
+end
+
+interpretation
+ Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
+defines afilter_ivl' is afilter
+and bfilter_ivl' is bfilter
+and AI_ivl' is AI
+and aval_ivl' is aval'
+proof qed (auto simp: iter'_pfp_above)
+
+value [code] "list_up(AI_ivl' test3_ivl Top)"
+value [code] "list_up(AI_ivl' test4_ivl Top)"
+value [code] "list_up(AI_ivl' test5_ivl Top)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_State.thy Wed Sep 28 08:51:55 2011 +0200
@@ -0,0 +1,50 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_State
+imports Abs_Int0_fun
+ "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord"
+ (* Library import merely to allow string lists to be sorted for output *)
+begin
+
+subsection "Abstract State with Computable Ordering"
+
+text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
+
+datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
+
+fun "fun" where "fun (FunDom f _) = f"
+fun dom where "dom (FunDom _ A) = A"
+
+definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"
+
+definition "list S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
+
+definition "lookup F x = (if x : set(dom F) then fun F x else Top)"
+
+definition "update F x y =
+ FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)"
+
+lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
+by(rule ext)(auto simp: lookup_def update_def)
+
+instantiation astate :: (SL_top) SL_top
+begin
+
+definition "le_astate F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"
+
+definition
+"join_astate F G =
+ FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
+
+definition "Top = FunDom (\<lambda>x. Top) []"
+
+instance
+proof
+ case goal2 thus ?case
+ apply(auto simp: le_astate_def)
+ by (metis lookup_def preord_class.le_trans top)
+qed (auto simp: le_astate_def lookup_def join_astate_def Top_astate_def)
+
+end
+
+end
--- a/src/HOL/IMP/Astate.thy Mon Sep 26 21:13:26 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Astate
-imports AbsInt0_fun
- "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord"
- (* Library import merely to allow string lists to be sorted for output *)
-begin
-
-subsection "Abstract State with Computable Ordering"
-
-text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
-
-datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
-
-fun "fun" where "fun (FunDom f _) = f"
-fun dom where "dom (FunDom _ A) = A"
-
-definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"
-
-definition "list S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
-
-definition "lookup F x = (if x : set(dom F) then fun F x else Top)"
-
-definition "update F x y =
- FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)"
-
-lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
-by(rule ext)(auto simp: lookup_def update_def)
-
-instantiation astate :: (SL_top) SL_top
-begin
-
-definition "le_astate F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"
-
-definition
-"join_astate F G =
- FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
-
-definition "Top = FunDom (\<lambda>x. Top) []"
-
-instance
-proof
- case goal2 thus ?case
- apply(auto simp: le_astate_def)
- by (metis lookup_def preord_class.le_trans top)
-qed (auto simp: le_astate_def lookup_def join_astate_def Top_astate_def)
-
-end
-
-end
--- a/src/HOL/IMP/ROOT.ML Mon Sep 26 21:13:26 2011 +0200
+++ b/src/HOL/IMP/ROOT.ML Wed Sep 28 08:51:55 2011 +0200
@@ -15,10 +15,10 @@
"Def_Ass_Sound_Big",
"Def_Ass_Sound_Small",
"Live",
- "AbsInt2",
"Hoare_Examples",
"VC",
"HoareT",
+ "Abs_Int_Den/Abs_Int2",
"Procs_Dyn_Vars_Dyn",
"Procs_Stat_Vars_Dyn",
"Procs_Stat_Vars_Stat",
--- a/src/HOL/IsaMakefile Mon Sep 26 21:13:26 2011 +0200
+++ b/src/HOL/IsaMakefile Wed Sep 28 08:51:55 2011 +0200
@@ -515,9 +515,11 @@
HOL-IMP: HOL $(OUT)/HOL-IMP
-$(OUT)/HOL-IMP: $(OUT)/HOL IMP/AbsInt0_fun.thy IMP/Astate.thy \
- IMP/AbsInt0.thy IMP/AbsInt0_const.thy IMP/AbsInt1.thy IMP/AbsInt1_ivl.thy \
- IMP/AbsInt2.thy IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy \
+$(OUT)/HOL-IMP: $(OUT)/HOL IMP/Abs_Int_Den/Abs_Int0_fun.thy \
+ IMP/Abs_Int_Den/Abs_State.thy IMP/Abs_Int_Den/Abs_Int0.thy \
+ IMP/Abs_Int_Den/Abs_Int0_const.thy IMP/Abs_Int_Den/Abs_Int1.thy \
+ IMP/Abs_Int_Den/Abs_Int1_ivl.thy IMP/Abs_Int_Den/Abs_Int2.thy \
+ IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy \
IMP/Big_Step.thy IMP/C_like.thy IMP/Com.thy IMP/Compiler.thy \
IMP/Comp_Rev.thy IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \
IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \