author | nipkow |
Wed, 28 Sep 2011 09:55:11 +0200 | |
changeset 45963 | 054a9ac0d7ef |
parent 45962 | src/HOL/IMP/Abs_Int_Den/Abs_Int0.thy@305f83b6da54 |
child 48689 | 151d137f1095 |
permissions | -rw-r--r-- |
nipkow@45527 | 1 |
(* Author: Tobias Nipkow *) |
nipkow@45527 | 2 |
|
nipkow@45963 | 3 |
theory Abs_Int_den0 |
nipkow@45963 | 4 |
imports Abs_State_den |
nipkow@45527 | 5 |
begin |
nipkow@45527 | 6 |
|
nipkow@45527 | 7 |
subsection "Computable Abstract Interpretation" |
nipkow@45527 | 8 |
|
nipkow@45527 | 9 |
text{* Abstract interpretation over type @{text astate} instead of |
nipkow@45527 | 10 |
functions. *} |
nipkow@45527 | 11 |
|
nipkow@45803 | 12 |
locale Abs_Int = Val_abs + |
nipkow@45815 | 13 |
fixes pfp :: "('a astate \<Rightarrow> 'a astate) \<Rightarrow> 'a astate \<Rightarrow> 'a astate" |
nipkow@45815 | 14 |
assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0" |
nipkow@45815 | 15 |
assumes above: "x0 \<sqsubseteq> pfp f x0" |
nipkow@45527 | 16 |
begin |
nipkow@45527 | 17 |
|
nipkow@45803 | 18 |
fun aval' :: "aexp \<Rightarrow> 'a astate \<Rightarrow> 'a" where |
nipkow@45527 | 19 |
"aval' (N n) _ = num' n" | |
nipkow@45527 | 20 |
"aval' (V x) S = lookup S x" | |
nipkow@45527 | 21 |
"aval' (Plus e1 e2) S = plus' (aval' e1 S) (aval' e2 S)" |
nipkow@45527 | 22 |
|
nipkow@45527 | 23 |
abbreviation astate_in_rep (infix "<:" 50) where |
nipkow@45527 | 24 |
"s <: S == ALL x. s x <: lookup S x" |
nipkow@45527 | 25 |
|
nipkow@45527 | 26 |
lemma astate_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T" |
nipkow@45527 | 27 |
by (metis in_mono le_astate_def le_rep lookup_def top) |
nipkow@45527 | 28 |
|
nipkow@45527 | 29 |
lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S" |
nipkow@45527 | 30 |
by (induct a) (auto simp: rep_num' rep_plus') |
nipkow@45527 | 31 |
|
nipkow@45527 | 32 |
|
nipkow@45527 | 33 |
fun AI :: "com \<Rightarrow> 'a astate \<Rightarrow> 'a astate" where |
nipkow@45527 | 34 |
"AI SKIP S = S" | |
nipkow@45527 | 35 |
"AI (x ::= a) S = update S x (aval' a S)" | |
nipkow@45527 | 36 |
"AI (c1;c2) S = AI c2 (AI c1 S)" | |
nipkow@45527 | 37 |
"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" | |
nipkow@45815 | 38 |
"AI (WHILE b DO c) S = pfp (AI c) S" |
nipkow@45527 | 39 |
|
nipkow@45527 | 40 |
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0" |
nipkow@45886 | 41 |
proof(induction c arbitrary: s t S0) |
nipkow@45761 | 42 |
case SKIP thus ?case by fastforce |
nipkow@45527 | 43 |
next |
nipkow@45527 | 44 |
case Assign thus ?case |
nipkow@45527 | 45 |
by (auto simp: lookup_update aval'_sound) |
nipkow@45527 | 46 |
next |
nipkow@45527 | 47 |
case Semi thus ?case by auto |
nipkow@45527 | 48 |
next |
nipkow@45527 | 49 |
case If thus ?case |
nipkow@45527 | 50 |
by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2) |
nipkow@45527 | 51 |
next |
nipkow@45527 | 52 |
case (While b c) |
nipkow@45815 | 53 |
let ?P = "pfp (AI c) S0" |
nipkow@45527 | 54 |
{ fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P" |
nipkow@45886 | 55 |
proof(induction "WHILE b DO c" s t rule: big_step_induct) |
nipkow@45527 | 56 |
case WhileFalse thus ?case by simp |
nipkow@45527 | 57 |
next |
nipkow@45886 | 58 |
case WhileTrue thus ?case using While.IH pfp astate_in_rep_le by metis |
nipkow@45527 | 59 |
qed |
nipkow@45527 | 60 |
} |
nipkow@45803 | 61 |
with astate_in_rep_le[OF `s <: S0` above] |
nipkow@45527 | 62 |
show ?case by (metis While(2) AI.simps(5)) |
nipkow@45527 | 63 |
qed |
nipkow@45527 | 64 |
|
nipkow@45527 | 65 |
end |
nipkow@45527 | 66 |
|
nipkow@45527 | 67 |
end |