src/HOL/IMP/Collecting.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 61890 f6ded81f5690
child 67399 eab6ce8368fa
permissions -rw-r--r--
Lots of new material for multivariate analysis
     1 theory Collecting
     2 imports Complete_Lattice Big_Step ACom
     3 begin
     4 
     5 subsection "The generic Step function"
     6 
     7 notation
     8   sup (infixl "\<squnion>" 65) and
     9   inf (infixl "\<sqinter>" 70) and
    10   bot ("\<bottom>") and
    11   top ("\<top>")
    12 
    13 context
    14   fixes f :: "vname \<Rightarrow> aexp \<Rightarrow> 'a \<Rightarrow> 'a::sup"
    15   fixes g :: "bexp \<Rightarrow> 'a \<Rightarrow> 'a"
    16 begin
    17 fun Step :: "'a \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
    18 "Step S (SKIP {Q}) = (SKIP {S})" |
    19 "Step S (x ::= e {Q}) =
    20   x ::= e {f x e S}" |
    21 "Step S (C1;; C2) = Step S C1;; Step (post C1) C2" |
    22 "Step S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
    23   IF b THEN {g b S} Step P1 C1 ELSE {g (Not b) S} Step P2 C2
    24   {post C1 \<squnion> post C2}" |
    25 "Step S ({I} WHILE b DO {P} C {Q}) =
    26   {S \<squnion> post C} WHILE b DO {g b I} Step P C {g (Not b) I}"
    27 end
    28 
    29 lemma strip_Step[simp]: "strip(Step f g S C) = strip C"
    30 by(induct C arbitrary: S) auto
    31 
    32 
    33 subsection "Collecting Semantics of Commands"
    34 
    35 subsubsection "Annotated commands as a complete lattice"
    36 
    37 instantiation acom :: (order) order
    38 begin
    39 
    40 definition less_eq_acom :: "('a::order)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
    41 "C1 \<le> C2 \<longleftrightarrow> strip C1 = strip C2 \<and> (\<forall>p<size(annos C1). anno C1 p \<le> anno C2 p)"
    42 
    43 definition less_acom :: "'a acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
    44 "less_acom x y = (x \<le> y \<and> \<not> y \<le> x)"
    45 
    46 instance
    47 proof (standard, goal_cases)
    48   case 1 show ?case by(simp add: less_acom_def)
    49 next
    50   case 2 thus ?case by(auto simp: less_eq_acom_def)
    51 next
    52   case 3 thus ?case by(fastforce simp: less_eq_acom_def size_annos)
    53 next
    54   case 4 thus ?case
    55     by(fastforce simp: le_antisym less_eq_acom_def size_annos
    56          eq_acom_iff_strip_anno)
    57 qed
    58 
    59 end
    60 
    61 lemma less_eq_acom_annos:
    62   "C1 \<le> C2 \<longleftrightarrow> strip C1 = strip C2 \<and> list_all2 (op \<le>) (annos C1) (annos C2)"
    63 by(auto simp add: less_eq_acom_def anno_def list_all2_conv_all_nth size_annos_same2)
    64 
    65 lemma SKIP_le[simp]: "SKIP {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<le> S')"
    66 by (cases c) (auto simp:less_eq_acom_def anno_def)
    67 
    68 lemma Assign_le[simp]: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')"
    69 by (cases c) (auto simp:less_eq_acom_def anno_def)
    70 
    71 lemma Seq_le[simp]: "C1;;C2 \<le> C \<longleftrightarrow> (\<exists>C1' C2'. C = C1';;C2' \<and> C1 \<le> C1' \<and> C2 \<le> C2')"
    72 apply (cases C)
    73 apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
    74 done
    75 
    76 lemma If_le[simp]: "IF b THEN {p1} C1 ELSE {p2} C2 {S} \<le> C \<longleftrightarrow>
    77   (\<exists>p1' p2' C1' C2' S'. C = IF b THEN {p1'} C1' ELSE {p2'} C2' {S'} \<and>
    78      p1 \<le> p1' \<and> p2 \<le> p2' \<and> C1 \<le> C1' \<and> C2 \<le> C2' \<and> S \<le> S')"
    79 apply (cases C)
    80 apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
    81 done
    82 
    83 lemma While_le[simp]: "{I} WHILE b DO {p} C {P} \<le> W \<longleftrightarrow>
    84   (\<exists>I' p' C' P'. W = {I'} WHILE b DO {p'} C' {P'} \<and> C \<le> C' \<and> p \<le> p' \<and> I \<le> I' \<and> P \<le> P')"
    85 apply (cases W)
    86 apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
    87 done
    88 
    89 lemma mono_post: "C \<le> C' \<Longrightarrow> post C \<le> post C'"
    90 using annos_ne[of C']
    91 by(auto simp: post_def less_eq_acom_def last_conv_nth[OF annos_ne] anno_def
    92      dest: size_annos_same)
    93 
    94 definition Inf_acom :: "com \<Rightarrow> 'a::complete_lattice acom set \<Rightarrow> 'a acom" where
    95 "Inf_acom c M = annotate (\<lambda>p. INF C:M. anno C p) c"
    96 
    97 global_interpretation
    98   Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c
    99 proof (standard, goal_cases)
   100   case 1 thus ?case
   101     by(auto simp: Inf_acom_def less_eq_acom_def size_annos intro:INF_lower)
   102 next
   103   case 2 thus ?case
   104     by(auto simp: Inf_acom_def less_eq_acom_def size_annos intro:INF_greatest)
   105 next
   106   case 3 thus ?case by(auto simp: Inf_acom_def)
   107 qed
   108 
   109 
   110 subsubsection "Collecting semantics"
   111 
   112 definition "step = Step (\<lambda>x e S. {s(x := aval e s) |s. s : S}) (\<lambda>b S. {s:S. bval b s})"
   113 
   114 definition CS :: "com \<Rightarrow> state set acom" where
   115 "CS c = lfp c (step UNIV)"
   116 
   117 lemma mono2_Step: fixes C1 C2 :: "'a::semilattice_sup acom"
   118   assumes "!!x e S1 S2. S1 \<le> S2 \<Longrightarrow> f x e S1 \<le> f x e S2"
   119           "!!b S1 S2. S1 \<le> S2 \<Longrightarrow> g b S1 \<le> g b S2"
   120   shows "C1 \<le> C2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> Step f g S1 C1 \<le> Step f g S2 C2"
   121 proof(induction S1 C1 arbitrary: C2 S2 rule: Step.induct)
   122   case 1 thus ?case by(auto)
   123 next
   124   case 2 thus ?case by (auto simp: assms(1))
   125 next
   126   case 3 thus ?case by(auto simp: mono_post)
   127 next
   128   case 4 thus ?case
   129     by(auto simp: subset_iff assms(2))
   130       (metis mono_post le_supI1 le_supI2)+
   131 next
   132   case 5 thus ?case
   133     by(auto simp: subset_iff assms(2))
   134       (metis mono_post le_supI1 le_supI2)+
   135 qed
   136 
   137 lemma mono2_step: "C1 \<le> C2 \<Longrightarrow> S1 \<subseteq> S2 \<Longrightarrow> step S1 C1 \<le> step S2 C2"
   138 unfolding step_def by(rule mono2_Step) auto
   139 
   140 lemma mono_step: "mono (step S)"
   141 by(blast intro: monoI mono2_step)
   142 
   143 lemma strip_step: "strip(step S C) = strip C"
   144 by (induction C arbitrary: S) (auto simp: step_def)
   145 
   146 lemma lfp_cs_unfold: "lfp c (step S) = step S (lfp c (step S))"
   147 apply(rule lfp_unfold[OF _  mono_step])
   148 apply(simp add: strip_step)
   149 done
   150 
   151 lemma CS_unfold: "CS c = step UNIV (CS c)"
   152 by (metis CS_def lfp_cs_unfold)
   153 
   154 lemma strip_CS[simp]: "strip(CS c) = c"
   155 by(simp add: CS_def index_lfp[simplified])
   156 
   157 
   158 subsubsection "Relation to big-step semantics"
   159 
   160 lemma asize_nz: "asize(c::com) \<noteq> 0"
   161 by (metis length_0_conv length_annos_annotate annos_ne)
   162 
   163 lemma post_Inf_acom:
   164   "\<forall>C\<in>M. strip C = c \<Longrightarrow> post (Inf_acom c M) = \<Inter>(post ` M)"
   165 apply(subgoal_tac "\<forall>C\<in>M. size(annos C) = asize c")
   166  apply(simp add: post_anno_asize Inf_acom_def asize_nz neq0_conv[symmetric])
   167 apply(simp add: size_annos)
   168 done
   169 
   170 lemma post_lfp: "post(lfp c f) = (\<Inter>{post C|C. strip C = c \<and> f C \<le> C})"
   171 by(auto simp add: lfp_def post_Inf_acom)
   172 
   173 lemma big_step_post_step:
   174   "\<lbrakk> (c, s) \<Rightarrow> t;  strip C = c;  s \<in> S;  step S C \<le> C \<rbrakk> \<Longrightarrow> t \<in> post C"
   175 proof(induction arbitrary: C S rule: big_step_induct)
   176   case Skip thus ?case by(auto simp: strip_eq_SKIP step_def post_def)
   177 next
   178   case Assign thus ?case
   179     by(fastforce simp: strip_eq_Assign step_def post_def)
   180 next
   181   case Seq thus ?case
   182     by(fastforce simp: strip_eq_Seq step_def post_def last_append annos_ne)
   183 next
   184   case IfTrue thus ?case apply(auto simp: strip_eq_If step_def post_def)
   185     by (metis (lifting,full_types) mem_Collect_eq set_mp)
   186 next
   187   case IfFalse thus ?case apply(auto simp: strip_eq_If step_def post_def)
   188     by (metis (lifting,full_types) mem_Collect_eq set_mp)
   189 next
   190   case (WhileTrue b s1 c' s2 s3)
   191   from WhileTrue.prems(1) obtain I P C' Q where "C = {I} WHILE b DO {P} C' {Q}" "strip C' = c'"
   192     by(auto simp: strip_eq_While)
   193   from WhileTrue.prems(3) `C = _`
   194   have "step P C' \<le> C'"  "{s \<in> I. bval b s} \<le> P"  "S \<le> I"  "step (post C') C \<le> C"
   195     by (auto simp: step_def post_def)
   196   have "step {s \<in> I. bval b s} C' \<le> C'"
   197     by (rule order_trans[OF mono2_step[OF order_refl `{s \<in> I. bval b s} \<le> P`] `step P C' \<le> C'`])
   198   have "s1: {s:I. bval b s}" using `s1 \<in> S` `S \<subseteq> I` `bval b s1` by auto
   199   note s2_in_post_C' = WhileTrue.IH(1)[OF `strip C' = c'` this `step {s \<in> I. bval b s} C' \<le> C'`]
   200   from WhileTrue.IH(2)[OF WhileTrue.prems(1) s2_in_post_C' `step (post C') C \<le> C`]
   201   show ?case .
   202 next
   203   case (WhileFalse b s1 c') thus ?case
   204     by (force simp: strip_eq_While step_def post_def)
   205 qed
   206 
   207 lemma big_step_lfp: "\<lbrakk> (c,s) \<Rightarrow> t;  s \<in> S \<rbrakk> \<Longrightarrow> t \<in> post(lfp c (step S))"
   208 by(auto simp add: post_lfp intro: big_step_post_step)
   209 
   210 lemma big_step_CS: "(c,s) \<Rightarrow> t \<Longrightarrow> t : post(CS c)"
   211 by(simp add: CS_def big_step_lfp)
   212 
   213 end