separated monotonicity reasoning and defined narrowing with while_option
authornipkow
Wed Oct 12 09:16:30 2011 +0200 (2011-10-12 ago)
changeset 45127d2eb07a1e01b
parent 45126 fc3bb3a42369
child 45128 5af3a3203a76
separated monotonicity reasoning and defined narrowing with while_option
src/HOL/IMP/Abs_Int0.thy
src/HOL/IMP/Abs_Int0_const.thy
src/HOL/IMP/Abs_Int0_fun.thy
src/HOL/IMP/Abs_Int1.thy
src/HOL/IMP/Abs_Int1_ivl.thy
src/HOL/IMP/Abs_Int2.thy
src/HOL/IMP/Abs_State.thy
     1.1 --- a/src/HOL/IMP/Abs_Int0.thy	Mon Oct 10 20:14:25 2011 +0200
     1.2 +++ b/src/HOL/IMP/Abs_Int0.thy	Wed Oct 12 09:16:30 2011 +0200
     1.3 @@ -9,10 +9,7 @@
     1.4  text{* Abstract interpretation over type @{text astate} instead of
     1.5  functions. *}
     1.6  
     1.7 -locale Abs_Int = Val_abs +
     1.8 -fixes pfp :: "('a st up acom \<Rightarrow> 'a st up acom) \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
     1.9 -assumes pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> f(pfp f c) \<sqsubseteq> pfp f c"
    1.10 -and strip_pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> strip(pfp f c) = strip c"
    1.11 +locale Abs_Int = Val_abs
    1.12  begin
    1.13  
    1.14  fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
    1.15 @@ -31,27 +28,15 @@
    1.16  "step S ({Inv} WHILE b DO c {P}) =
    1.17     {S \<squnion> post c} WHILE b DO step Inv c {Inv}"
    1.18  
    1.19 +definition AI :: "com \<Rightarrow> 'a st up acom option" where
    1.20 +"AI = lpfp\<^isub>c (step \<top>)"
    1.21 +
    1.22 +
    1.23  lemma strip_step[simp]: "strip(step S c) = strip c"
    1.24  by(induct c arbitrary: S) (simp_all add: Let_def)
    1.25  
    1.26 -definition AI :: "com \<Rightarrow> 'a st up acom" where
    1.27 -"AI c = pfp (step Top) (bot_acom c)"
    1.28  
    1.29 -
    1.30 -subsubsection "Monotonicity"
    1.31 -
    1.32 -lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
    1.33 -by(induction e) (auto simp: le_st_def lookup_def mono_plus')
    1.34 -
    1.35 -lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
    1.36 -by(auto simp add: le_st_def lookup_def update_def)
    1.37 -
    1.38 -lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
    1.39 -apply(induction c arbitrary: S S')
    1.40 -apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split)
    1.41 -done
    1.42 -
    1.43 -subsubsection "Soundness"
    1.44 +text{* Soundness: *}
    1.45  
    1.46  lemma aval'_sound: "s <:f S \<Longrightarrow> aval a s <: aval' a S"
    1.47  by (induct a) (auto simp: rep_num' rep_plus' rep_st_def lookup_def)
    1.48 @@ -92,10 +77,29 @@
    1.49      by simp (metis `s <:up S` `S \<sqsubseteq> Inv` `Inv \<sqsubseteq> P` up_fun_in_rep_le)
    1.50  qed
    1.51  
    1.52 -lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> t <:up post(AI c)"
    1.53 -by(fastforce simp: AI_def strip_pfp in_rep_Top_up intro: step_sound pfp)
    1.54 +lemma AI_sound: "\<lbrakk> AI c = Some c';  (c,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> t <:up post c'"
    1.55 +by (metis AI_def in_rep_Top_up lpfpc_pfp step_sound strip_lpfpc strip_step)
    1.56  
    1.57  end
    1.58  
    1.59  
    1.60 +subsubsection "Monotonicity"
    1.61 +
    1.62 +locale Abs_Int_mono = Abs_Int +
    1.63 +assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
    1.64 +begin
    1.65 +
    1.66 +lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
    1.67 +by(induction e) (auto simp: le_st_def lookup_def mono_plus')
    1.68 +
    1.69 +lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
    1.70 +by(auto simp add: le_st_def lookup_def update_def)
    1.71 +
    1.72 +lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
    1.73 +apply(induction c arbitrary: S S')
    1.74 +apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split)
    1.75 +done
    1.76 +
    1.77  end
    1.78 +
    1.79 +end
     2.1 --- a/src/HOL/IMP/Abs_Int0_const.thy	Mon Oct 10 20:14:25 2011 +0200
     2.2 +++ b/src/HOL/IMP/Abs_Int0_const.thy	Wed Oct 12 09:16:30 2011 +0200
     2.3 @@ -51,33 +51,25 @@
     2.4  
     2.5  end
     2.6  
     2.7 -interpretation Rep rep_cval
     2.8 +
     2.9 +interpretation Val_abs rep_cval Const plus_cval
    2.10  proof
    2.11    case goal1 thus ?case
    2.12      by(cases a, cases b, simp, simp, cases b, simp, simp)
    2.13  next
    2.14    case goal2 show ?case by(simp add: Top_cval_def)
    2.15 -qed
    2.16 -
    2.17 -interpretation Val_abs rep_cval Const plus_cval
    2.18 -proof
    2.19 -  case goal1 show ?case by simp
    2.20  next
    2.21 -  case goal2 thus ?case
    2.22 -    by(auto simp: plus_cval_cases split: cval.split)
    2.23 +  case goal3 show ?case by simp
    2.24  next
    2.25 -  case goal3 thus ?case
    2.26 +  case goal4 thus ?case
    2.27      by(auto simp: plus_cval_cases split: cval.split)
    2.28  qed
    2.29  
    2.30 -text{* Could set the limit of the number of iterations to an arbitrarily
    2.31 -large number because all ascending chains in this semilattice are finite. *}
    2.32 -
    2.33 -interpretation Abs_Int rep_cval Const plus_cval "(iter 15)"
    2.34 +interpretation Abs_Int rep_cval Const plus_cval
    2.35  defines AI_const is AI
    2.36  and aval'_const is aval'
    2.37  and step_const is step
    2.38 -proof qed (auto simp: iter_pfp strip_iter)
    2.39 +proof qed
    2.40  
    2.41  text{* Straight line code: *}
    2.42  definition "test1_const =
    2.43 @@ -113,28 +105,20 @@
    2.44    WHILE Less (V ''x'') (N 1)
    2.45    DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
    2.46  
    2.47 -text{* For readability: *}
    2.48 -translations "x" <= "CONST V x"
    2.49 -translations "x" <= "CONST N x"
    2.50 -translations "x" <= "CONST Const x"
    2.51 -translations "x < y" <= "CONST Less x y"
    2.52 -translations "x" <= "CONST B x"
    2.53 -translations "x" <= "CONST Up x"
    2.54 -
    2.55  value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test1_const))"
    2.56  value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test1_const))"
    2.57  value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test1_const))"
    2.58  value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test1_const))"
    2.59 -value [code] "show_acom (AI_const test1_const)"
    2.60 +value [code] "show_acom_opt (AI_const test1_const)"
    2.61  
    2.62 -value [code] "show_acom (AI_const test2_const)"
    2.63 -value [code] "show_acom (AI_const test3_const)"
    2.64 +value [code] "show_acom_opt (AI_const test2_const)"
    2.65 +value [code] "show_acom_opt (AI_const test3_const)"
    2.66  
    2.67  value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test4_const))"
    2.68  value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test4_const))"
    2.69  value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test4_const))"
    2.70  value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test4_const))"
    2.71 -value [code] "show_acom (AI_const test4_const)"
    2.72 +value [code] "show_acom_opt (AI_const test4_const)"
    2.73  
    2.74  value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test5_const))"
    2.75  value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test5_const))"
    2.76 @@ -142,9 +126,17 @@
    2.77  value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test5_const))"
    2.78  value [code] "show_acom (((step_const \<top>)^^4) (\<bottom>\<^sub>c test5_const))"
    2.79  value [code] "show_acom (((step_const \<top>)^^5) (\<bottom>\<^sub>c test5_const))"
    2.80 -value [code] "show_acom (AI_const test5_const)"
    2.81 +value [code] "show_acom_opt (AI_const test5_const)"
    2.82 +
    2.83 +value [code] "show_acom_opt (AI_const test6_const)"
    2.84 +value [code] "show_acom_opt (AI_const test7_const)"
    2.85  
    2.86 -value [code] "show_acom (AI_const test6_const)"
    2.87 -value [code] "show_acom (AI_const test7_const)"
    2.88 +text{* Monotonicity: *}
    2.89 +
    2.90 +interpretation Abs_Int_mono rep_cval Const plus_cval
    2.91 +proof
    2.92 +  case goal1 thus ?case
    2.93 +    by(auto simp: plus_cval_cases split: cval.split)
    2.94 +qed
    2.95  
    2.96  end
     3.1 --- a/src/HOL/IMP/Abs_Int0_fun.thy	Mon Oct 10 20:14:25 2011 +0200
     3.2 +++ b/src/HOL/IMP/Abs_Int0_fun.thy	Wed Oct 12 09:16:30 2011 +0200
     3.3 @@ -4,6 +4,7 @@
     3.4  
     3.5  theory Abs_Int0_fun
     3.6  imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
     3.7 +        "~~/src/HOL/Library/While_Combinator"
     3.8  begin
     3.9  
    3.10  subsection "Annotated Commands"
    3.11 @@ -155,15 +156,6 @@
    3.12  
    3.13  end
    3.14  
    3.15 -definition Top_acom :: "com \<Rightarrow> ('a::SL_top) acom" ("\<top>\<^sub>c") where
    3.16 -"\<top>\<^sub>c = anno \<top>"
    3.17 -
    3.18 -lemma strip_Top_acom[simp]: "strip (\<top>\<^sub>c c) = c"
    3.19 -by(simp add: Top_acom_def)
    3.20 -
    3.21 -lemma le_Top_acomp[simp]: "strip c' = c \<Longrightarrow> c' \<sqsubseteq> \<top>\<^sub>c c"
    3.22 -by(induct c' arbitrary: c) (auto simp: Top_acom_def)
    3.23 -
    3.24  
    3.25  subsubsection "Lifting"
    3.26  
    3.27 @@ -216,23 +208,69 @@
    3.28  lemma strip_bot_acom[simp]: "strip(\<bottom>\<^sub>c c) = c"
    3.29  by(simp add: bot_acom_def)
    3.30  
    3.31 +lemma bot_acom[rule_format]: "strip c' = c \<longrightarrow> \<bottom>\<^sub>c c \<sqsubseteq> c'"
    3.32 +apply(induct c arbitrary: c')
    3.33 +apply (simp_all add: bot_acom_def)
    3.34 + apply(induct_tac c')
    3.35 +  apply simp_all
    3.36 + apply(induct_tac c')
    3.37 +  apply simp_all
    3.38 + apply(induct_tac c')
    3.39 +  apply simp_all
    3.40 + apply(induct_tac c')
    3.41 +  apply simp_all
    3.42 + apply(induct_tac c')
    3.43 +  apply simp_all
    3.44 +done
    3.45  
    3.46 -subsection "Absract Interpretation"
    3.47 +
    3.48 +subsubsection "Post-fixed point iteration"
    3.49  
    3.50 -text{* The representation of abstract by a set of concrete values: *}
    3.51 +definition
    3.52 +  pfp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
    3.53 +"pfp f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) f"
    3.54 +
    3.55 +lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<sqsubseteq> x"
    3.56 +using while_option_stop[OF assms[simplified pfp_def]] by simp
    3.57  
    3.58 -locale Rep =
    3.59 -fixes rep :: "'a::SL_top \<Rightarrow> 'b set"
    3.60 -assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
    3.61 -and rep_Top: "rep \<top> = UNIV"
    3.62 -begin
    3.63 +lemma pfp_least:
    3.64 +assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
    3.65 +and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" and "pfp f x0 = Some x" shows "x \<sqsubseteq> p"
    3.66 +proof-
    3.67 +  { fix x assume "x \<sqsubseteq> p"
    3.68 +    hence  "f x \<sqsubseteq> f p" by(rule mono)
    3.69 +    from this `f p \<sqsubseteq> p` have "f x \<sqsubseteq> p" by(rule le_trans)
    3.70 +  }
    3.71 +  thus "x \<sqsubseteq> p" using assms(2-) while_option_rule[where P = "%x. x \<sqsubseteq> p"]
    3.72 +    unfolding pfp_def by blast
    3.73 +qed
    3.74 +
    3.75 +definition
    3.76 + lpfp\<^isub>c :: "(('a::SL_top)up acom \<Rightarrow> 'a up acom) \<Rightarrow> com \<Rightarrow> 'a up acom option" where
    3.77 +"lpfp\<^isub>c f c = pfp f (\<bottom>\<^sub>c c)"
    3.78 +
    3.79 +lemma lpfpc_pfp: "lpfp\<^isub>c f c0 = Some c \<Longrightarrow> f c \<sqsubseteq> c"
    3.80 +by(simp add: pfp_pfp lpfp\<^isub>c_def)
    3.81  
    3.82 -abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a"
    3.83 +lemma strip_pfp:
    3.84 +assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0"
    3.85 +using assms while_option_rule[where P = "%x. g x = g x0" and c = f]
    3.86 +unfolding pfp_def by metis
    3.87 +
    3.88 +lemma strip_lpfpc: assumes "\<And>c. strip(f c) = strip c" and "lpfp\<^isub>c f c = Some c'"
    3.89 +shows "strip c' = c"
    3.90 +using assms(1) strip_pfp[OF _ assms(2)[simplified lpfp\<^isub>c_def]]
    3.91 +by(metis strip_bot_acom)
    3.92  
    3.93 -lemma in_rep_Top[simp]: "x <: \<top>"
    3.94 -by(simp add: rep_Top)
    3.95 +lemma lpfpc_least:
    3.96 +assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
    3.97 +and "strip p = c0" and "f p \<sqsubseteq> p" and lp: "lpfp\<^isub>c f c0 = Some c" shows "c \<sqsubseteq> p"
    3.98 +using pfp_least[OF _ _ bot_acom[OF `strip p = c0`] lp[simplified lpfp\<^isub>c_def]]
    3.99 +  mono `f p \<sqsubseteq> p`
   3.100 +by blast
   3.101  
   3.102 -end
   3.103 +
   3.104 +subsection "Abstract Interpretation"
   3.105  
   3.106  definition rep_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
   3.107  "rep_fun rep F = {f. \<forall>x. f x \<in> rep(F x)}"
   3.108 @@ -243,72 +281,28 @@
   3.109  
   3.110  text{* The interface for abstract values: *}
   3.111  
   3.112 -(* FIXME: separate Rep interface needed? *)
   3.113 -locale Val_abs = Rep rep for rep :: "'a::SL_top \<Rightarrow> val set" +
   3.114 +locale Val_abs =
   3.115 +fixes rep :: "'a::SL_top \<Rightarrow> val set"
   3.116 +  assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
   3.117 +  and rep_Top: "rep \<top> = UNIV"
   3.118  fixes num' :: "val \<Rightarrow> 'a"
   3.119  and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   3.120 -assumes rep_num': "n <: num' n"
   3.121 -and rep_plus': "n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: plus' a1 a2"
   3.122 -and mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
   3.123 -
   3.124 -
   3.125 -subsubsection "Post-fixed point iteration"
   3.126 -
   3.127 -fun iter :: "nat \<Rightarrow> (('a::SL_top) acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
   3.128 -"iter 0 f c = \<top>\<^sub>c (strip c)" |
   3.129 -"iter (Suc n) f c = (let fc = f c in if fc \<sqsubseteq> c then c else iter n f fc)"
   3.130 -(* code lemma?? *)
   3.131 -
   3.132 -lemma strip_iter: assumes "\<forall>c. strip(f c) = strip c"
   3.133 -shows "strip(iter n f c) = strip c"
   3.134 -apply (induction n arbitrary: c)
   3.135 - apply (metis iter.simps(1) strip_Top_acom)
   3.136 -apply (simp add:Let_def)
   3.137 -by (metis assms)
   3.138 -
   3.139 -lemma iter_pfp: assumes "\<forall>c. strip(f c) = strip c"
   3.140 -shows "f(iter n f c) \<sqsubseteq> iter n f c"
   3.141 -apply (induction n arbitrary: c)
   3.142 - apply(simp add: assms)
   3.143 -apply (simp add:Let_def)
   3.144 -done
   3.145 +  assumes rep_num': "n : rep(num' n)"
   3.146 +  and rep_plus':
   3.147 + "n1 : rep a1 \<Longrightarrow> n2 : rep a2 \<Longrightarrow> n1+n2 : rep(plus' a1 a2)"
   3.148 +begin
   3.149  
   3.150 -lemma iter_funpow: assumes "\<forall>c. strip(f c) = strip c"
   3.151 -shows "iter n f x \<noteq> \<top>\<^sub>c (strip x) \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
   3.152 -apply(induction n arbitrary: x)
   3.153 - apply simp
   3.154 -apply (auto simp: Let_def assms)
   3.155 - apply(metis funpow.simps(1) id_def)
   3.156 -by (metis assms funpow.simps(2) funpow_swap1 o_apply)
   3.157 -
   3.158 -text{* For monotone @{text f}, @{term "iter f n x0"} yields the least
   3.159 -post-fixed point above @{text x0}, unless it yields @{text Top}. *}
   3.160 +abbreviation in_rep (infix "<:" 50)
   3.161 + where "x <: a == x : rep a"
   3.162  
   3.163 -lemma iter_least_pfp:
   3.164 -assumes strip: "\<forall>c. strip(f c) = strip c"
   3.165 -and mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   3.166 -and not_top: "iter n f x0 \<noteq> \<top>\<^sub>c (strip x0)"
   3.167 -and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter n f x0 \<sqsubseteq> p"
   3.168 -proof-
   3.169 -  obtain k where "iter n f x0 = (f^^k) x0"
   3.170 -    using iter_funpow[OF strip not_top] by blast
   3.171 -  moreover
   3.172 -  { fix n have "(f^^n) x0 \<sqsubseteq> p"
   3.173 -    proof(induction n)
   3.174 -      case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
   3.175 -    next
   3.176 -      case (Suc n) thus ?case
   3.177 -        by (simp add: `x0 \<sqsubseteq> p`)(metis Suc `f p \<sqsubseteq> p` le_trans mono)
   3.178 -    qed
   3.179 -  } ultimately show ?thesis by simp
   3.180 -qed
   3.181 +lemma in_rep_Top[simp]: "x <: \<top>"
   3.182 +by(simp add: rep_Top)
   3.183 +
   3.184 +end
   3.185  
   3.186  type_synonym 'a st = "(name \<Rightarrow> 'a)"
   3.187  
   3.188 -locale Abs_Int_Fun = Val_abs +
   3.189 -fixes pfp :: "('a st up acom \<Rightarrow> 'a st up acom) \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
   3.190 -assumes pfp: "f(pfp f c) \<sqsubseteq> pfp f c"
   3.191 -and strip_pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> strip(pfp f c) = strip c"
   3.192 +locale Abs_Int_Fun = Val_abs
   3.193  begin
   3.194  
   3.195  fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
   3.196 @@ -316,24 +310,26 @@
   3.197  "aval' (V x) S = S x" |
   3.198  "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
   3.199  
   3.200 -fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" where
   3.201 +fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
   3.202 + where
   3.203  "step S (SKIP {P}) = (SKIP {S})" |
   3.204  "step S (x ::= e {P}) =
   3.205    x ::= e {case S of Bot \<Rightarrow> Bot | Up S \<Rightarrow> Up(S(x := aval' e S))}" |
   3.206  "step S (c1; c2) = step S c1; step (post c1) c2" |
   3.207  "step S (IF b THEN c1 ELSE c2 {P}) =
   3.208 -  (let c1' = step S c1; c2' = step S c2
   3.209 -   in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
   3.210 +   IF b THEN step S c1 ELSE step S c2 {post c1 \<squnion> post c2}" |
   3.211  "step S ({Inv} WHILE b DO c {P}) =
   3.212    {S \<squnion> post c} WHILE b DO (step Inv c) {Inv}"
   3.213  
   3.214 +definition AI :: "com \<Rightarrow> 'a st up acom option" where
   3.215 +"AI = lpfp\<^isub>c (step \<top>)"
   3.216 +
   3.217 +
   3.218  lemma strip_step[simp]: "strip(step S c) = strip c"
   3.219  by(induct c arbitrary: S) (simp_all add: Let_def)
   3.220  
   3.221  
   3.222 -definition AI :: "com \<Rightarrow> 'a st up acom" where
   3.223 -"AI c = pfp (step \<top>) (\<bottom>\<^sub>c c)"
   3.224 -
   3.225 +text{*Lifting @{text "<:"} to other types: *}
   3.226  
   3.227  abbreviation fun_in_rep :: "state \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
   3.228  "s <:f S == s \<in> rep_fun rep S"
   3.229 @@ -358,20 +354,7 @@
   3.230  by(simp add: Top_up_def in_rep_Top_fun)
   3.231  
   3.232  
   3.233 -subsubsection "Monotonicity"
   3.234 -
   3.235 -lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
   3.236 -by(induction e)(auto simp: le_fun_def mono_plus')
   3.237 -
   3.238 -lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')"
   3.239 -by(simp add: le_fun_def)
   3.240 -
   3.241 -lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
   3.242 -apply(induction c arbitrary: S S')
   3.243 -apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split)
   3.244 -done
   3.245 -
   3.246 -subsubsection "Soundness"
   3.247 +text{* Soundness: *}
   3.248  
   3.249  lemma aval'_sound: "s <:f S \<Longrightarrow> aval a s <: aval' a S"
   3.250  by (induct a) (auto simp: rep_num' rep_plus' rep_fun_def)
   3.251 @@ -380,7 +363,8 @@
   3.252  by(simp add: rep_fun_def)
   3.253  
   3.254  lemma step_sound:
   3.255 -  "step S c \<sqsubseteq> c \<Longrightarrow> (strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up S \<Longrightarrow> t <:up post c"
   3.256 +  "\<lbrakk> step S c \<sqsubseteq> c; (strip c,s) \<Rightarrow> t; s <:up S \<rbrakk>
   3.257 +   \<Longrightarrow> t <:up post c"
   3.258  proof(induction c arbitrary: S s t)
   3.259    case SKIP thus ?case
   3.260      by simp (metis skipE up_fun_in_rep_le)
   3.261 @@ -412,8 +396,29 @@
   3.262      by simp (metis `s <:up S` `S \<sqsubseteq> Inv` `Inv \<sqsubseteq> P` up_fun_in_rep_le)
   3.263  qed
   3.264  
   3.265 -lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> t <:up post(AI c)"
   3.266 -by(auto simp: AI_def strip_pfp in_rep_Top_up intro: step_sound pfp)
   3.267 +lemma AI_sound:
   3.268 + "\<lbrakk> AI c = Some c';  (c,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> t <:up post c'"
   3.269 +by (metis AI_def in_rep_Top_up lpfpc_pfp step_sound strip_lpfpc strip_step)
   3.270 +
   3.271 +end
   3.272 +
   3.273 +
   3.274 +subsubsection "Monotonicity"
   3.275 +
   3.276 +locale Abs_Int_Fun_mono = Abs_Int_Fun +
   3.277 +assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
   3.278 +begin
   3.279 +
   3.280 +lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
   3.281 +by(induction e)(auto simp: le_fun_def mono_plus')
   3.282 +
   3.283 +lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')"
   3.284 +by(simp add: le_fun_def)
   3.285 +
   3.286 +lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
   3.287 +apply(induction c arbitrary: S S')
   3.288 +apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split)
   3.289 +done
   3.290  
   3.291  end
   3.292  
     4.1 --- a/src/HOL/IMP/Abs_Int1.thy	Mon Oct 10 20:14:25 2011 +0200
     4.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Wed Oct 12 09:16:30 2011 +0200
     4.3 @@ -30,10 +30,19 @@
     4.4  and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
     4.5  and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
     4.6  assumes bot[simp]: "\<bottom> \<sqsubseteq> x"
     4.7 +begin
     4.8  
     4.9 -locale Rep1 = Rep rep for rep :: "'a::L_top_bot \<Rightarrow> 'b set" +
    4.10 -assumes inter_rep_subset_rep_meet: "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
    4.11 -  -- "this means the meet is precise"
    4.12 +lemma mono_meet: "x \<sqsubseteq> x' \<Longrightarrow> y \<sqsubseteq> y' \<Longrightarrow> x \<sqinter> y \<sqsubseteq> x' \<sqinter> y'"
    4.13 +by (metis meet_greatest meet_le1 meet_le2 le_trans)
    4.14 +
    4.15 +end
    4.16 +
    4.17 +
    4.18 +locale Val_abs1_rep =
    4.19 +  Val_abs rep num' plus'
    4.20 +  for rep :: "'a::L_top_bot \<Rightarrow> val set" and num' plus' +
    4.21 +assumes inter_rep_subset_rep_meet:
    4.22 +  "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
    4.23  and rep_Bot: "rep \<bottom> = {}"
    4.24  begin
    4.25  
    4.26 @@ -43,29 +52,19 @@
    4.27  lemma rep_meet[simp]: "rep(a1 \<sqinter> a2) = rep a1 \<inter> rep a2"
    4.28  by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2)
    4.29  
    4.30 -lemma mono_meet: "x \<sqsubseteq> x' \<Longrightarrow> y \<sqsubseteq> y' \<Longrightarrow> x \<sqinter> y \<sqsubseteq> x' \<sqinter> y'"
    4.31 -by (metis meet_greatest meet_le1 meet_le2 le_trans)
    4.32 -
    4.33  end
    4.34  
    4.35  
    4.36 -locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
    4.37 -  for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' +
    4.38 +locale Val_abs1 = Val_abs1_rep +
    4.39  fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
    4.40  and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
    4.41  assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
    4.42    n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
    4.43  and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
    4.44    n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
    4.45 -and mono_filter_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> r \<sqsubseteq> r' \<Longrightarrow>
    4.46 -  filter_plus' r a1 a2 \<sqsubseteq> filter_plus' r' b1 b2"
    4.47 -and mono_filter_less': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow>
    4.48 -  filter_less' bv a1 a2 \<sqsubseteq> filter_less' bv b1 b2"
    4.49 +
    4.50  
    4.51 -locale Abs_Int1 = Val_abs1 +
    4.52 -fixes pfp :: "('a st up acom \<Rightarrow> 'a st up acom) \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
    4.53 -assumes pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> mono f \<Longrightarrow> f(pfp f c) \<sqsubseteq> pfp f c"
    4.54 -and strip_pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> strip(pfp f c) = strip c"
    4.55 +locale Abs_Int1 = Val_abs1
    4.56  begin
    4.57  
    4.58  lemma in_rep_join_UpI: "s <:up S1 | s <:up S2 \<Longrightarrow> s <:up S1 \<squnion> S2"
    4.59 @@ -78,7 +77,9 @@
    4.60  "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
    4.61  
    4.62  lemma aval'_sound: "s <:up S \<Longrightarrow> aval a s <: aval' a S"
    4.63 -by (induct a)(auto simp: rep_num' rep_plus' in_rep_up_iff lookup_def rep_st_def)
    4.64 +by(induct a)(auto simp: rep_num' rep_plus' in_rep_up_iff lookup_def rep_st_def)
    4.65 +
    4.66 +subsubsection "Backward analysis"
    4.67  
    4.68  fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a st up \<Rightarrow> 'a st up" where
    4.69  "afilter (N n) a S = (if n <: a then S else Bot)" |
    4.70 @@ -141,7 +142,8 @@
    4.71  qed
    4.72  
    4.73  
    4.74 -fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" where
    4.75 +fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
    4.76 + where
    4.77  "step S (SKIP {P}) = (SKIP {S})" |
    4.78  "step S (x ::= e {P}) =
    4.79    x ::= e {case S of Bot \<Rightarrow> Bot
    4.80 @@ -155,51 +157,13 @@
    4.81     WHILE b DO step (bfilter b True Inv) c
    4.82     {bfilter b False Inv}"
    4.83  
    4.84 +definition AI :: "com \<Rightarrow> 'a st up acom option" where
    4.85 +"AI = lpfp\<^isub>c (step \<top>)"
    4.86 +
    4.87  lemma strip_step[simp]: "strip(step S c) = strip c"
    4.88  by(induct c arbitrary: S) (simp_all add: Let_def)
    4.89  
    4.90  
    4.91 -definition AI :: "com \<Rightarrow> 'a st up acom" where
    4.92 -"AI c = pfp (step \<top>) (\<bottom>\<^sub>c c)"
    4.93 -
    4.94 -
    4.95 -subsubsection "Monotonicity"
    4.96 -
    4.97 -lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
    4.98 -apply(cases S)
    4.99 - apply simp
   4.100 -apply(cases S')
   4.101 - apply simp
   4.102 -apply simp
   4.103 -by(induction e) (auto simp: le_st_def lookup_def mono_plus')
   4.104 -
   4.105 -lemma mono_afilter: "r \<sqsubseteq> r' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> afilter e r S \<sqsubseteq> afilter e r' S'"
   4.106 -apply(induction e arbitrary: r r' S S')
   4.107 -apply(auto simp: Let_def split: up.splits prod.splits)
   4.108 -apply (metis le_rep subsetD)
   4.109 -apply(drule_tac x = "list" in mono_lookup)
   4.110 -apply (metis mono_meet le_trans)
   4.111 -apply (metis mono_meet mono_lookup mono_update le_trans)
   4.112 -apply(metis mono_aval' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv)
   4.113 -done
   4.114 -
   4.115 -lemma mono_bfilter: "S \<sqsubseteq> S' \<Longrightarrow> bfilter b r S \<sqsubseteq> bfilter b r S'"
   4.116 -apply(induction b arbitrary: r S S')
   4.117 -apply(auto simp: le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] split: prod.splits)
   4.118 -apply(metis mono_aval' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv)
   4.119 -done
   4.120 -
   4.121 -
   4.122 -lemma post_le_post: "c \<sqsubseteq> c' \<Longrightarrow> post c \<sqsubseteq> post c'"
   4.123 -by (induction c c' rule: le_acom.induct) simp_all
   4.124 -
   4.125 -lemma mono_step: "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step S c \<sqsubseteq> step S' c'"
   4.126 -apply(induction c c' arbitrary: S S' rule: le_acom.induct)
   4.127 -apply (auto simp: post_le_post Let_def mono_bfilter mono_update mono_aval' le_join_disj
   4.128 -  split: up.split)
   4.129 -done
   4.130 -
   4.131 -
   4.132  subsubsection "Soundness"
   4.133  
   4.134  lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f update S x a"
   4.135 @@ -257,9 +221,59 @@
   4.136    show ?case using `\<not> bval b t` by simp
   4.137  qed
   4.138  
   4.139 -lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> t <:up post(AI c)"
   4.140 -by(fastforce simp: AI_def strip_pfp mono_def in_rep_Top_up
   4.141 -  intro: step_sound pfp  mono_step[OF le_refl])
   4.142 +lemma AI_sound: "\<lbrakk> AI c = Some c';  (c,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> t <:up post c'"
   4.143 +unfolding AI_def
   4.144 +by (metis in_rep_Top_up lpfpc_pfp step_sound strip_lpfpc strip_step)
   4.145 +(*
   4.146 +by(metis step_sound[of "\<top>" c' s t] strip_lpfp strip_step
   4.147 +  lpfp_pfp mono_def mono_step[OF le_refl] in_rep_Top_up)
   4.148 +*)
   4.149 +end
   4.150 +
   4.151 +
   4.152 +subsubsection "Monotonicity"
   4.153 +
   4.154 +locale Abs_Int1_mono = Abs_Int1 +
   4.155 +assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
   4.156 +and mono_filter_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> r \<sqsubseteq> r' \<Longrightarrow>
   4.157 +  filter_plus' r a1 a2 \<sqsubseteq> filter_plus' r' b1 b2"
   4.158 +and mono_filter_less': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow>
   4.159 +  filter_less' bv a1 a2 \<sqsubseteq> filter_less' bv b1 b2"
   4.160 +begin
   4.161 +
   4.162 +lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
   4.163 +apply(cases S)
   4.164 + apply simp
   4.165 +apply(cases S')
   4.166 + apply simp
   4.167 +apply simp
   4.168 +by(induction e) (auto simp: le_st_def lookup_def mono_plus')
   4.169 +
   4.170 +lemma mono_afilter: "r \<sqsubseteq> r' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> afilter e r S \<sqsubseteq> afilter e r' S'"
   4.171 +apply(induction e arbitrary: r r' S S')
   4.172 +apply(auto simp: Let_def split: up.splits prod.splits)
   4.173 +apply (metis le_rep subsetD)
   4.174 +apply(drule_tac x = "list" in mono_lookup)
   4.175 +apply (metis mono_meet le_trans)
   4.176 +apply (metis mono_meet mono_lookup mono_update le_trans)
   4.177 +apply(metis mono_aval' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv)
   4.178 +done
   4.179 +
   4.180 +lemma mono_bfilter: "S \<sqsubseteq> S' \<Longrightarrow> bfilter b r S \<sqsubseteq> bfilter b r S'"
   4.181 +apply(induction b arbitrary: r S S')
   4.182 +apply(auto simp: le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] split: prod.splits)
   4.183 +apply(metis mono_aval' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv)
   4.184 +done
   4.185 +
   4.186 +
   4.187 +lemma post_le_post: "c \<sqsubseteq> c' \<Longrightarrow> post c \<sqsubseteq> post c'"
   4.188 +by (induction c c' rule: le_acom.induct) simp_all
   4.189 +
   4.190 +lemma mono_step: "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step S c \<sqsubseteq> step S' c'"
   4.191 +apply(induction c c' arbitrary: S S' rule: le_acom.induct)
   4.192 +apply (auto simp: post_le_post Let_def mono_bfilter mono_update mono_aval' le_join_disj
   4.193 +  split: up.split)
   4.194 +done
   4.195  
   4.196  end
   4.197  
     5.1 --- a/src/HOL/IMP/Abs_Int1_ivl.thy	Mon Oct 10 20:14:25 2011 +0200
     5.2 +++ b/src/HOL/IMP/Abs_Int1_ivl.thy	Wed Oct 12 09:16:30 2011 +0200
     5.3 @@ -160,26 +160,20 @@
     5.4           I (max_option False (l1 + Some 1) l2) h2)
     5.5     else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
     5.6  
     5.7 -interpretation Rep rep_ivl
     5.8 +interpretation Val_abs rep_ivl num_ivl plus_ivl
     5.9  proof
    5.10    case goal1 thus ?case
    5.11      by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
    5.12  next
    5.13    case goal2 show ?case by(simp add: rep_ivl_def Top_ivl_def)
    5.14 +next
    5.15 +  case goal3 thus ?case by(simp add: rep_ivl_def num_ivl_def)
    5.16 +next
    5.17 +  case goal4 thus ?case
    5.18 +    by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
    5.19  qed
    5.20  
    5.21 -interpretation Val_abs rep_ivl num_ivl plus_ivl
    5.22 -proof
    5.23 -  case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)
    5.24 -next
    5.25 -  case goal2 thus ?case
    5.26 -    by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
    5.27 -next
    5.28 -  case goal3 thus ?case
    5.29 -    by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)
    5.30 -qed
    5.31 -
    5.32 -interpretation Rep1 rep_ivl
    5.33 +interpretation Val_abs1_rep rep_ivl num_ivl plus_ivl
    5.34  proof
    5.35    case goal1 thus ?case
    5.36      by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
    5.37 @@ -206,23 +200,16 @@
    5.38    case goal2 thus ?case
    5.39      by(cases a1, cases a2,
    5.40        auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
    5.41 -next
    5.42 -  case goal3 thus ?case
    5.43 -    by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)
    5.44 -next
    5.45 -  case goal4 thus ?case
    5.46 -    apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def)
    5.47 -    by(auto simp add: empty_def le_ivl_def le_option_def min_option_def max_option_def split: option.splits)
    5.48  qed
    5.49  
    5.50  interpretation
    5.51 -  Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter 20)"
    5.52 +  Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
    5.53  defines afilter_ivl is afilter
    5.54  and bfilter_ivl is bfilter
    5.55  and step_ivl is step
    5.56  and AI_ivl is AI
    5.57  and aval_ivl is aval'
    5.58 -proof qed (auto simp: iter_pfp strip_iter)
    5.59 +proof qed
    5.60  
    5.61  definition "test1_ivl =
    5.62   ''y'' ::= N 7;
    5.63 @@ -230,50 +217,78 @@
    5.64   THEN ''y'' ::= Plus (V ''y'') (V ''x'')
    5.65   ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
    5.66  
    5.67 -value [code] "show_acom (AI_ivl test1_ivl)"
    5.68 +value [code] "show_acom_opt (AI_ivl test1_ivl)"
    5.69  
    5.70 -value [code] "show_acom (AI_const test3_const)"
    5.71 -value [code] "show_acom (AI_ivl test3_const)"
    5.72 +value [code] "show_acom_opt (AI_const test3_const)"
    5.73 +value [code] "show_acom_opt (AI_ivl test3_const)"
    5.74  
    5.75 -value [code] "show_acom (AI_const test4_const)"
    5.76 -value [code] "show_acom (AI_ivl test4_const)"
    5.77 +value [code] "show_acom_opt (AI_const test4_const)"
    5.78 +value [code] "show_acom_opt (AI_ivl test4_const)"
    5.79  
    5.80 -value [code] "show_acom (AI_ivl test6_const)"
    5.81 +value [code] "show_acom_opt (AI_ivl test6_const)"
    5.82  
    5.83  definition "test2_ivl =
    5.84   WHILE Less (V ''x'') (N 100)
    5.85   DO ''x'' ::= Plus (V ''x'') (N 1)"
    5.86  
    5.87 -value [code] "show_acom (AI_ivl test2_ivl)"
    5.88 +value [code] "show_acom_opt (AI_ivl test2_ivl)"
    5.89 +value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test2_ivl))"
    5.90 +value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test2_ivl))"
    5.91 +value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test2_ivl))"
    5.92 +
    5.93 +text{* Fixed point reached in 2 steps. Not so if the start value of x is known: *}
    5.94  
    5.95  definition "test3_ivl =
    5.96   ''x'' ::= N 7;
    5.97   WHILE Less (V ''x'') (N 100)
    5.98   DO ''x'' ::= Plus (V ''x'') (N 1)"
    5.99  
   5.100 -value [code] "show_acom (AI_ivl test3_ivl)"
   5.101 +value [code] "show_acom_opt (AI_ivl test3_ivl)"
   5.102  value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test3_ivl))"
   5.103  value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test3_ivl))"
   5.104  value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test3_ivl))"
   5.105  value [code] "show_acom (((step_ivl \<top>)^^3) (\<bottom>\<^sub>c test3_ivl))"
   5.106  value [code] "show_acom (((step_ivl \<top>)^^4) (\<bottom>\<^sub>c test3_ivl))"
   5.107  
   5.108 +text{* Takes as many iterations as the actual execution. Would diverge if
   5.109 +loop did not terminate. Worse still, as the following example shows: even if
   5.110 +the actual execution terminates, the analysis may not: *}
   5.111 +
   5.112  definition "test4_ivl =
   5.113   ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
   5.114   WHILE Less (V ''x'') (N 11)
   5.115   DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
   5.116 -value [code] "show_acom(AI_ivl test4_ivl)"
   5.117 +
   5.118 +text{* The value of y keeps decreasing as the analysis is iterated, no matter
   5.119 +how long: *}
   5.120 +
   5.121 +value [code] "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test4_ivl))"
   5.122  
   5.123  definition "test5_ivl =
   5.124   ''x'' ::= N 0; ''y'' ::= N 0;
   5.125 - WHILE Less (V ''x'') (N 1001)
   5.126 + WHILE Less (V ''x'') (N 1000)
   5.127   DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
   5.128 -value [code] "show_acom(AI_ivl test5_ivl)"
   5.129 +value [code] "show_acom_opt (AI_ivl test5_ivl)"
   5.130  
   5.131 -text{* Nontermination not detected: *}
   5.132 +text{* Again, the analysis would not terminate: *}
   5.133  definition "test6_ivl =
   5.134   ''x'' ::= N 0;
   5.135   WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
   5.136 -value [code] "show_acom(AI_ivl test6_ivl)"
   5.137 +
   5.138 +text{* Monotonicity: *}
   5.139 +
   5.140 +interpretation
   5.141 +  Abs_Int1_mono rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
   5.142 +proof
   5.143 +  case goal1 thus ?case
   5.144 +    by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)
   5.145 +next
   5.146 +  case goal2 thus ?case
   5.147 +    by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)
   5.148 +next
   5.149 +  case goal3 thus ?case
   5.150 +    apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def)
   5.151 +    by(auto simp add: empty_def le_ivl_def le_option_def min_option_def max_option_def split: option.splits)
   5.152 +qed
   5.153  
   5.154  end
     6.1 --- a/src/HOL/IMP/Abs_Int2.thy	Mon Oct 10 20:14:25 2011 +0200
     6.2 +++ b/src/HOL/IMP/Abs_Int2.thy	Wed Oct 12 09:16:30 2011 +0200
     6.3 @@ -9,7 +9,8 @@
     6.4  
     6.5  class WN = SL_top +
     6.6  fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
     6.7 -assumes widen: "y \<sqsubseteq> x \<nabla> y"
     6.8 +assumes widen1: "x \<sqsubseteq> x \<nabla> y"
     6.9 +assumes widen2: "y \<sqsubseteq> x \<nabla> y"
    6.10  fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
    6.11  assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
    6.12  assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
    6.13 @@ -49,12 +50,15 @@
    6.14  instance
    6.15  proof
    6.16    case goal1 thus ?case
    6.17 -    by(simp add: widen_st_def le_st_def lookup_def widen)
    6.18 +    by(simp add: widen_st_def le_st_def lookup_def widen1)
    6.19  next
    6.20    case goal2 thus ?case
    6.21 +    by(simp add: widen_st_def le_st_def lookup_def widen2)
    6.22 +next
    6.23 +  case goal3 thus ?case
    6.24      by(auto simp: narrow_st_def le_st_def lookup_def narrow1)
    6.25  next
    6.26 -  case goal3 thus ?case
    6.27 +  case goal4 thus ?case
    6.28      by(auto simp: narrow_st_def le_st_def lookup_def narrow2)
    6.29  qed
    6.30  
    6.31 @@ -76,12 +80,15 @@
    6.32  instance
    6.33  proof
    6.34    case goal1 show ?case
    6.35 -    by(induct x y rule: widen_up.induct) (simp_all add: widen)
    6.36 +    by(induct x y rule: widen_up.induct) (simp_all add: widen1)
    6.37  next
    6.38 -  case goal2 thus ?case
    6.39 +  case goal2 show ?case
    6.40 +    by(induct x y rule: widen_up.induct) (simp_all add: widen2)
    6.41 +next
    6.42 +  case goal3 thus ?case
    6.43      by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
    6.44  next
    6.45 -  case goal3 thus ?case
    6.46 +  case goal4 thus ?case
    6.47      by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
    6.48  qed
    6.49  
    6.50 @@ -102,115 +109,112 @@
    6.51  abbreviation narrow_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<triangle>\<^sub>c" 65)
    6.52  where "narrow_acom == map2_acom (op \<triangle>)"
    6.53  
    6.54 +lemma widen1_acom: "strip c = strip c' \<Longrightarrow> c \<sqsubseteq> c \<nabla>\<^sub>c c'"
    6.55 +by(induct c c' rule: le_acom.induct)(simp_all add: widen1)
    6.56 +
    6.57 +lemma widen2_acom: "strip c = strip c' \<Longrightarrow> c' \<sqsubseteq> c \<nabla>\<^sub>c c'"
    6.58 +by(induct c c' rule: le_acom.induct)(simp_all add: widen2)
    6.59 +
    6.60  lemma narrow1_acom: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle>\<^sub>c y"
    6.61  by(induct y x rule: le_acom.induct) (simp_all add: narrow1)
    6.62  
    6.63  lemma narrow2_acom: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle>\<^sub>c y \<sqsubseteq> x"
    6.64  by(induct y x rule: le_acom.induct) (simp_all add: narrow2)
    6.65  
    6.66 -fun iter_up :: "(('a::WN)acom \<Rightarrow> 'a acom) \<Rightarrow> nat \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
    6.67 -"iter_up f 0 x = \<top>\<^sub>c (strip x)" |
    6.68 -"iter_up f (Suc n) x =
    6.69 -  (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla>\<^sub>c fx))"
    6.70  
    6.71 -abbreviation
    6.72 -  iter_down :: "(('a::WN)acom \<Rightarrow> 'a acom) \<Rightarrow> nat \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
    6.73 -"iter_down f n x == ((\<lambda>x. x \<triangle>\<^sub>c f x)^^n) x"
    6.74 +subsubsection "Post-fixed point computation"
    6.75  
    6.76  definition
    6.77 -  iter' :: "nat \<Rightarrow> nat \<Rightarrow> (('a::WN)acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
    6.78 -"iter' m n f x = iter_down f n (iter_up f m x)"
    6.79 +  prefp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
    6.80 +"prefp f = while_option (\<lambda>x. \<not> x \<sqsubseteq> f x) f"
    6.81 +
    6.82 +definition
    6.83 +  pfp_WN :: "(('a::WN)up acom \<Rightarrow> 'a up acom) \<Rightarrow> com \<Rightarrow> 'a up acom option"
    6.84 +where "pfp_WN f c = (case lpfp\<^isub>c (\<lambda>c. c \<nabla>\<^sub>c f c) c of None \<Rightarrow> None
    6.85 +                     | Some c' \<Rightarrow> prefp (\<lambda>c. c \<triangle>\<^sub>c f c) c')"
    6.86  
    6.87  lemma strip_map2_acom:
    6.88   "strip c1 = strip c2 \<Longrightarrow> strip(map2_acom f c1 c2) = strip c1"
    6.89  by(induct f c1 c2 rule: map2_acom.induct) simp_all
    6.90  
    6.91 -lemma strip_iter_up: assumes "\<forall>c. strip(f c) = strip c"
    6.92 -shows "strip(iter_up f n c) = strip c"
    6.93 -apply (induction n arbitrary: c)
    6.94 - apply (metis iter_up.simps(1) strip_Top_acom snd_conv)
    6.95 -apply (simp add:Let_def)
    6.96 -by (metis assms strip_map2_acom)
    6.97 -
    6.98 -lemma iter_up_pfp: assumes "\<forall>c. strip(f c) = strip c"
    6.99 -shows "f(iter_up f n c) \<sqsubseteq> iter_up f n c"
   6.100 -apply (induction n arbitrary: c)
   6.101 - apply(simp add: assms)
   6.102 -apply (simp add:Let_def)
   6.103 -done
   6.104 -
   6.105 -lemma strip_iter_down: assumes "\<forall>c. strip(f c) = strip c"
   6.106 -shows "strip(iter_down f n c) = strip c"
   6.107 -apply (induction n arbitrary: c)
   6.108 - apply(simp)
   6.109 -apply (simp add: strip_map2_acom assms)
   6.110 -done
   6.111 +lemma lpfp_step_up_pfp:
   6.112 + "\<lbrakk> \<forall>c. strip(f c) = strip c;  lpfp\<^isub>c (\<lambda>c. c \<nabla>\<^sub>c f c) c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'"
   6.113 +by (metis (no_types) assms lpfpc_pfp le_trans widen2_acom)
   6.114  
   6.115  lemma iter_down_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0" 
   6.116 -defines "x n == iter_down f n x0"
   6.117 -shows "f(x n) \<sqsubseteq> x n"
   6.118 -proof (induction n)
   6.119 -  case 0 show ?case by (simp add: x_def assms(2))
   6.120 -next
   6.121 -  case (Suc n)
   6.122 -  have "f (x (Suc n)) = f(x n \<triangle>\<^sub>c f(x n))" by(simp add: x_def)
   6.123 -  also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2_acom[OF Suc]])
   6.124 -  also have "\<dots> \<sqsubseteq> x n \<triangle>\<^sub>c f(x n)" by(rule narrow1_acom[OF Suc])
   6.125 -  also have "\<dots> = x(Suc n)" by(simp add: x_def)
   6.126 -  finally show ?case .
   6.127 -qed
   6.128 -
   6.129 -lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0" 
   6.130 -defines "x n == iter_down f n x0"
   6.131 -shows "x n \<sqsubseteq> x0"
   6.132 -proof (induction n)
   6.133 -  case 0 show ?case by(simp add: x_def)
   6.134 -next
   6.135 -  case (Suc n)
   6.136 -  have "x(Suc n) = x n \<triangle>\<^sub>c f(x n)" by(simp add: x_def)
   6.137 -  also have "\<dots> \<sqsubseteq> x n" unfolding x_def
   6.138 -    by(rule narrow2_acom[OF iter_down_pfp[OF assms(1), OF assms(2)]])
   6.139 -  also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
   6.140 -  finally show ?case .
   6.141 +and "prefp (\<lambda>c. c \<triangle>\<^sub>c f c) x0 = Some x"
   6.142 +shows "f x \<sqsubseteq> x \<and> x \<sqsubseteq> x0" (is "?P x")
   6.143 +proof-
   6.144 +  { fix x assume "?P x"
   6.145 +    note 1 = conjunct1[OF this] and 2 = conjunct2[OF this]
   6.146 +    let ?x' = "x \<triangle>\<^sub>c f x"
   6.147 +    have "?P ?x'"
   6.148 +    proof
   6.149 +      have "f ?x' \<sqsubseteq> f x"  by(rule monoD[OF `mono f` narrow2_acom[OF 1]])
   6.150 +      also have "\<dots> \<sqsubseteq> ?x'" by(rule narrow1_acom[OF 1])
   6.151 +      finally show "f ?x' \<sqsubseteq> ?x'" .
   6.152 +      have "?x' \<sqsubseteq> x" by (rule narrow2_acom[OF 1])
   6.153 +      also have "x \<sqsubseteq> x0" by(rule 2)
   6.154 +      finally show "?x' \<sqsubseteq> x0" .
   6.155 +    qed
   6.156 +  }
   6.157 +  with while_option_rule[where P = ?P, OF _ assms(3)[simplified prefp_def]]
   6.158 +    assms(2) le_refl
   6.159 +  show ?thesis by blast
   6.160  qed
   6.161  
   6.162  
   6.163 -lemma iter'_pfp: assumes "\<forall>c. strip (f c) = strip c" and "mono f"
   6.164 -shows "f (iter' m n f c) \<sqsubseteq> iter' m n f c"
   6.165 -using iter_up_pfp[of f] iter_down_pfp[of f]
   6.166 -by(auto simp add: iter'_def Let_def assms)
   6.167 +lemma pfp_WN_pfp:
   6.168 +  "\<lbrakk> \<forall>c. strip (f c) = strip c;  mono f;  pfp_WN f c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'"
   6.169 +unfolding pfp_WN_def
   6.170 +by (auto dest: iter_down_pfp lpfp_step_up_pfp split: option.splits)
   6.171 +
   6.172 +lemma strip_while: fixes f :: "'a acom \<Rightarrow> 'a acom"
   6.173 +assumes "\<forall>c. strip (f c) = strip c" and "while_option P f c = Some c'"
   6.174 +shows "strip c' = strip c"
   6.175 +using while_option_rule[where P = "\<lambda>c'. strip c' = strip c", OF _ assms(2)]
   6.176 +by (metis assms(1))
   6.177  
   6.178 -lemma strip_iter': assumes "\<forall>c. strip(f c) = strip c"
   6.179 -shows "strip(iter' m n f c) = strip c"
   6.180 -by(simp add: iter'_def strip_iter_down strip_iter_up assms)
   6.181 +lemma strip_pfp_WN:
   6.182 +  "\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_WN f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c"
   6.183 +apply(auto simp add: pfp_WN_def prefp_def split: option.splits)
   6.184 +by (metis (no_types) strip_lpfpc strip_map2_acom strip_while)
   6.185 +
   6.186 +locale Abs_Int2 = Abs_Int1_mono rep for rep :: "'a::{WN,L_top_bot} \<Rightarrow> val set"
   6.187 +begin
   6.188  
   6.189 +definition AI_WN :: "com \<Rightarrow> 'a st up acom option" where
   6.190 +"AI_WN = pfp_WN (step \<top>)"
   6.191 +
   6.192 +lemma AI_sound: "\<lbrakk> AI_WN c = Some c';  (c,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> t <:up post c'"
   6.193 +unfolding AI_WN_def
   6.194 +by(metis step_sound[of "\<top>" c' s t] strip_pfp_WN strip_step
   6.195 +  pfp_WN_pfp mono_def mono_step[OF le_refl] in_rep_Top_up)
   6.196 +
   6.197 +end
   6.198  
   6.199  interpretation
   6.200 -  Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 20 5)"
   6.201 -defines afilter_ivl' is afilter
   6.202 -and bfilter_ivl' is bfilter
   6.203 -and step_ivl' is step
   6.204 -and AI_ivl' is AI
   6.205 -and aval_ivl' is aval'
   6.206 -proof qed (auto simp: iter'_pfp strip_iter')
   6.207 +  Abs_Int2 num_ivl plus_ivl filter_plus_ivl filter_less_ivl rep_ivl
   6.208 +defines AI_ivl' is AI_WN
   6.209 +proof qed
   6.210  
   6.211 -value [code] "show_acom (AI_ivl test3_ivl)"
   6.212 -value [code] "show_acom (AI_ivl' test3_ivl)"
   6.213 +value [code] "show_acom_opt (AI_ivl test3_ivl)"
   6.214 +value [code] "show_acom_opt (AI_ivl' test3_ivl)"
   6.215 +
   6.216 +definition "step_up_ivl n = ((\<lambda>c. c \<nabla>\<^sub>c step_ivl \<top> c)^^n)"
   6.217 +definition "step_down_ivl n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> c)^^n)"
   6.218  
   6.219 -definition "step_up n = ((\<lambda>c. c \<nabla>\<^sub>c step_ivl \<top> c)^^n)"
   6.220 -definition "step_down n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> c)^^n)"
   6.221 +value [code] "show_acom (step_up_ivl 1 (\<bottom>\<^sub>c test3_ivl))"
   6.222 +value [code] "show_acom (step_up_ivl 2 (\<bottom>\<^sub>c test3_ivl))"
   6.223 +value [code] "show_acom (step_up_ivl 3 (\<bottom>\<^sub>c test3_ivl))"
   6.224 +value [code] "show_acom (step_up_ivl 4 (\<bottom>\<^sub>c test3_ivl))"
   6.225 +value [code] "show_acom (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl))"
   6.226 +value [code] "show_acom (step_down_ivl 1 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
   6.227 +value [code] "show_acom (step_down_ivl 2 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
   6.228 +value [code] "show_acom (step_down_ivl 3 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
   6.229  
   6.230 -value [code] "show_acom (step_up 1 (\<bottom>\<^sub>c test3_ivl))"
   6.231 -value [code] "show_acom (step_up 2 (\<bottom>\<^sub>c test3_ivl))"
   6.232 -value [code] "show_acom (step_up 3 (\<bottom>\<^sub>c test3_ivl))"
   6.233 -value [code] "show_acom (step_up 4 (\<bottom>\<^sub>c test3_ivl))"
   6.234 -value [code] "show_acom (step_up 5 (\<bottom>\<^sub>c test3_ivl))"
   6.235 -value [code] "show_acom (step_down 1 (step_up 5 (\<bottom>\<^sub>c test3_ivl)))"
   6.236 -value [code] "show_acom (step_down 2 (step_up 5 (\<bottom>\<^sub>c test3_ivl)))"
   6.237 -value [code] "show_acom (step_down 3 (step_up 5 (\<bottom>\<^sub>c test3_ivl)))"
   6.238 -
   6.239 -value [code] "show_acom (AI_ivl' test4_ivl)"
   6.240 -value [code] "show_acom (AI_ivl' test5_ivl)"
   6.241 -value [code] "show_acom (AI_ivl' test6_ivl)"
   6.242 +value [code] "show_acom_opt (AI_ivl' test4_ivl)"
   6.243 +value [code] "show_acom_opt (AI_ivl' test5_ivl)"
   6.244 +value [code] "show_acom_opt (AI_ivl' test6_ivl)"
   6.245  
   6.246  end
     7.1 --- a/src/HOL/IMP/Abs_State.thy	Mon Oct 10 20:14:25 2011 +0200
     7.2 +++ b/src/HOL/IMP/Abs_State.thy	Wed Oct 12 09:16:30 2011 +0200
     7.3 @@ -24,6 +24,7 @@
     7.4  "show_st_up (Up S) = Up(show_st S)"
     7.5  
     7.6  definition "show_acom = map_acom show_st_up"
     7.7 +definition "show_acom_opt = Option.map show_acom"
     7.8  
     7.9  definition "lookup F x = (if x : set(dom F) then fun F x else \<top>)"
    7.10  
    7.11 @@ -61,10 +62,10 @@
    7.12  lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
    7.13  by(auto simp add: le_st_def lookup_def update_def)
    7.14  
    7.15 -context Rep
    7.16 +context Val_abs
    7.17  begin
    7.18  
    7.19 -abbreviation fun_in_rep :: "(name \<Rightarrow> 'b) \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
    7.20 +abbreviation fun_in_rep :: "state \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
    7.21  "s <:f S == s \<in> rep_st rep S"
    7.22  
    7.23  notation fun_in_rep (infix "<:\<^sub>f" 50)
    7.24 @@ -73,7 +74,7 @@
    7.25  apply(auto simp add: rep_st_def le_st_def dest: le_rep)
    7.26  by (metis in_rep_Top le_rep lookup_def subsetD)
    7.27  
    7.28 -abbreviation in_rep_up :: "(name \<Rightarrow> 'b) \<Rightarrow> 'a st up \<Rightarrow> bool"  (infix "<:up" 50)
    7.29 +abbreviation in_rep_up :: "state \<Rightarrow> 'a st up \<Rightarrow> bool"  (infix "<:up" 50)
    7.30  where "s <:up S == s : rep_up (rep_st rep) S"
    7.31  
    7.32  notation (output) in_rep_up (infix "<:\<^sub>u\<^sub>p" 50)