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