src/HOL/IMP/Finite_Reachable.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 62390 842917225d56
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
nipkow@50050
     1
theory Finite_Reachable
nipkow@50050
     2
imports Small_Step
nipkow@50050
     3
begin
nipkow@50050
     4
nipkow@50050
     5
subsection "Finite number of reachable commands"
nipkow@50050
     6
nipkow@50050
     7
text{* This theory shows that in the small-step semantics one can only reach
nipkow@50050
     8
a finite number of commands from any given command. Hence one can see the
nipkow@50050
     9
command component of a small-step configuration as a combination of the
nipkow@50050
    10
program to be executed and a pc. *}
nipkow@50050
    11
nipkow@50050
    12
definition reachable :: "com \<Rightarrow> com set" where
nipkow@50050
    13
"reachable c = {c'. \<exists>s t. (c,s) \<rightarrow>* (c',t)}"
nipkow@50050
    14
nipkow@50050
    15
text{* Proofs need induction on the length of a small-step reduction sequence. *}
nipkow@50050
    16
nipkow@50050
    17
fun small_stepsn :: "com * state \<Rightarrow> nat \<Rightarrow> com * state \<Rightarrow> bool"
nipkow@50050
    18
    ("_ \<rightarrow>'(_') _" [55,0,55] 55) where
nipkow@50050
    19
"(cs \<rightarrow>(0) cs') = (cs' = cs)" |
nipkow@50050
    20
"cs \<rightarrow>(Suc n) cs'' = (\<exists>cs'. cs \<rightarrow> cs' \<and> cs' \<rightarrow>(n) cs'')"
nipkow@50050
    21
nipkow@50050
    22
lemma stepsn_if_star: "cs \<rightarrow>* cs' \<Longrightarrow> \<exists>n. cs \<rightarrow>(n) cs'"
nipkow@50050
    23
proof(induction rule: star.induct)
nipkow@50050
    24
  case refl show ?case by (metis small_stepsn.simps(1))
nipkow@50050
    25
next
nipkow@50050
    26
  case step thus ?case by (metis small_stepsn.simps(2))
nipkow@50050
    27
qed
nipkow@50050
    28
nipkow@50050
    29
lemma star_if_stepsn: "cs \<rightarrow>(n) cs' \<Longrightarrow> cs \<rightarrow>* cs'"
nipkow@50050
    30
by(induction n arbitrary: cs) (auto elim: star.step)
nipkow@50050
    31
nipkow@50050
    32
lemma SKIP_starD: "(SKIP, s) \<rightarrow>* (c,t) \<Longrightarrow> c = SKIP"
nipkow@50050
    33
by(induction SKIP s c t rule: star_induct) auto
nipkow@50050
    34
nipkow@50050
    35
lemma reachable_SKIP: "reachable SKIP = {SKIP}"
nipkow@50050
    36
by(auto simp: reachable_def dest: SKIP_starD)
nipkow@50050
    37
nipkow@50050
    38
nipkow@50050
    39
lemma Assign_starD: "(x::=a, s) \<rightarrow>* (c,t) \<Longrightarrow> c \<in> {x::=a, SKIP}"
nipkow@50050
    40
by (induction "x::=a" s c t rule: star_induct) (auto dest: SKIP_starD)
nipkow@50050
    41
nipkow@50050
    42
lemma reachable_Assign: "reachable (x::=a) = {x::=a, SKIP}"
nipkow@50050
    43
by(auto simp: reachable_def dest:Assign_starD)
nipkow@50050
    44
nipkow@50050
    45
nipkow@52046
    46
lemma Seq_stepsnD: "(c1;; c2, s) \<rightarrow>(n) (c', t) \<Longrightarrow>
nipkow@52046
    47
  (\<exists>c1' m. c' = c1';; c2 \<and> (c1, s) \<rightarrow>(m) (c1', t) \<and> m \<le> n) \<or>
nipkow@50050
    48
  (\<exists>s2 m1 m2. (c1,s) \<rightarrow>(m1) (SKIP,s2) \<and> (c2, s2) \<rightarrow>(m2) (c', t) \<and> m1+m2 < n)"
nipkow@50050
    49
proof(induction n arbitrary: c1 c2 s)
nipkow@50050
    50
  case 0 thus ?case by auto
nipkow@50050
    51
next
nipkow@50050
    52
  case (Suc n)
nipkow@52046
    53
  from Suc.prems obtain s' c12' where "(c1;;c2, s) \<rightarrow> (c12', s')"
nipkow@50050
    54
    and n: "(c12',s') \<rightarrow>(n) (c',t)" by auto
nipkow@50050
    55
  from this(1) show ?case
nipkow@50050
    56
  proof
nipkow@50050
    57
    assume "c1 = SKIP" "(c12', s') = (c2, s)"
nipkow@50050
    58
    hence "(c1,s) \<rightarrow>(0) (SKIP, s') \<and> (c2, s') \<rightarrow>(n) (c', t) \<and> 0 + n < Suc n"
nipkow@50050
    59
      using n by auto
nipkow@50050
    60
    thus ?case by blast
nipkow@50050
    61
  next
nipkow@52046
    62
    fix c1' s'' assume 1: "(c12', s') = (c1';; c2, s'')" "(c1, s) \<rightarrow> (c1', s'')"
nipkow@52046
    63
    hence n': "(c1';;c2,s') \<rightarrow>(n) (c',t)" using n by auto
nipkow@50050
    64
    from Suc.IH[OF n'] show ?case
nipkow@50050
    65
    proof
nipkow@52046
    66
      assume "\<exists>c1'' m. c' = c1'';; c2 \<and> (c1', s') \<rightarrow>(m) (c1'', t) \<and> m \<le> n"
nipkow@50050
    67
        (is "\<exists> a b. ?P a b")
nipkow@50050
    68
      then obtain c1'' m where 2: "?P c1'' m" by blast
nipkow@52046
    69
      hence "c' = c1'';;c2 \<and> (c1, s) \<rightarrow>(Suc m) (c1'',t) \<and> Suc m \<le> Suc n"
nipkow@50050
    70
        using 1 by auto
nipkow@50050
    71
      thus ?case by blast
nipkow@50050
    72
    next
nipkow@50050
    73
      assume "\<exists>s2 m1 m2. (c1',s') \<rightarrow>(m1) (SKIP,s2) \<and>
nipkow@50050
    74
        (c2,s2) \<rightarrow>(m2) (c',t) \<and> m1+m2 < n" (is "\<exists>a b c. ?P a b c")
nipkow@50050
    75
      then obtain s2 m1 m2 where "?P s2 m1 m2" by blast
nipkow@50050
    76
      hence "(c1,s) \<rightarrow>(Suc m1) (SKIP,s2) \<and> (c2,s2) \<rightarrow>(m2) (c',t) \<and>
nipkow@50050
    77
        Suc m1 + m2 < Suc n"  using 1 by auto
nipkow@50050
    78
      thus ?case by blast
nipkow@50050
    79
    qed
nipkow@50050
    80
  qed
nipkow@50050
    81
qed
nipkow@50050
    82
nipkow@52046
    83
corollary Seq_starD: "(c1;; c2, s) \<rightarrow>* (c', t) \<Longrightarrow>
nipkow@52046
    84
  (\<exists>c1'. c' = c1';; c2 \<and> (c1, s) \<rightarrow>* (c1', t)) \<or>
nipkow@50050
    85
  (\<exists>s2. (c1,s) \<rightarrow>* (SKIP,s2) \<and> (c2, s2) \<rightarrow>* (c', t))"
nipkow@50050
    86
by(metis Seq_stepsnD star_if_stepsn stepsn_if_star)
nipkow@50050
    87
nipkow@52046
    88
lemma reachable_Seq: "reachable (c1;;c2) \<subseteq>
nipkow@52046
    89
  (\<lambda>c1'. c1';;c2) ` reachable c1 \<union> reachable c2"
nipkow@50050
    90
by(auto simp: reachable_def image_def dest!: Seq_starD)
nipkow@50050
    91
nipkow@50050
    92
nipkow@50050
    93
lemma If_starD: "(IF b THEN c1 ELSE c2, s) \<rightarrow>* (c,t) \<Longrightarrow>
nipkow@50050
    94
  c = IF b THEN c1 ELSE c2 \<or> (c1,s) \<rightarrow>* (c,t) \<or> (c2,s) \<rightarrow>* (c,t)"
nipkow@50050
    95
by(induction "IF b THEN c1 ELSE c2" s c t rule: star_induct) auto
nipkow@50050
    96
nipkow@50050
    97
lemma reachable_If: "reachable (IF b THEN c1 ELSE c2) \<subseteq>
nipkow@50050
    98
  {IF b THEN c1 ELSE c2} \<union> reachable c1 \<union> reachable c2"
nipkow@50050
    99
by(auto simp: reachable_def dest!: If_starD)
nipkow@50050
   100
nipkow@50050
   101
nipkow@50050
   102
lemma While_stepsnD: "(WHILE b DO c, s) \<rightarrow>(n) (c2,t) \<Longrightarrow>
nipkow@52046
   103
  c2 \<in> {WHILE b DO c, IF b THEN c ;; WHILE b DO c ELSE SKIP, SKIP}
nipkow@52046
   104
  \<or> (\<exists>c1. c2 = c1 ;; WHILE b DO c \<and> (\<exists> s1 s2. (c,s1) \<rightarrow>* (c1,s2)))"
nipkow@50050
   105
proof(induction n arbitrary: s rule: less_induct)
nipkow@50050
   106
  case (less n1)
nipkow@50050
   107
  show ?case
nipkow@50050
   108
  proof(cases n1)
nipkow@50050
   109
    case 0 thus ?thesis using less.prems by (simp)
nipkow@50050
   110
  next
nipkow@50050
   111
    case (Suc n2)
nipkow@50050
   112
    let ?w = "WHILE b DO c"
nipkow@52046
   113
    let ?iw = "IF b THEN c ;; ?w ELSE SKIP"
nipkow@50050
   114
    from Suc less.prems have n2: "(?iw,s) \<rightarrow>(n2) (c2,t)" by(auto elim!: WhileE)
nipkow@50050
   115
    show ?thesis
nipkow@50050
   116
    proof(cases n2)
nipkow@50050
   117
      case 0 thus ?thesis using n2 by auto
nipkow@50050
   118
    next
nipkow@50050
   119
      case (Suc n3)
nipkow@50050
   120
      then obtain iw' s' where "(?iw,s) \<rightarrow> (iw',s')"
nipkow@50050
   121
        and n3: "(iw',s') \<rightarrow>(n3) (c2,t)"  using n2 by auto
nipkow@50050
   122
      from this(1)
nipkow@50050
   123
      show ?thesis
nipkow@50050
   124
      proof
nipkow@52046
   125
        assume "(iw', s') = (c;; WHILE b DO c, s)"
nipkow@52046
   126
        with n3 have "(c;;?w, s) \<rightarrow>(n3) (c2,t)" by auto
nipkow@50050
   127
        from Seq_stepsnD[OF this] show ?thesis
nipkow@50050
   128
        proof
nipkow@52046
   129
          assume "\<exists>c1' m. c2 = c1';; ?w \<and> (c,s) \<rightarrow>(m) (c1', t) \<and> m \<le> n3"
nipkow@50050
   130
          thus ?thesis by (metis star_if_stepsn)
nipkow@50050
   131
        next
nipkow@50050
   132
          assume "\<exists>s2 m1 m2. (c, s) \<rightarrow>(m1) (SKIP, s2) \<and>
nipkow@50050
   133
            (WHILE b DO c, s2) \<rightarrow>(m2) (c2, t) \<and> m1 + m2 < n3" (is "\<exists>x y z. ?P x y z")
nipkow@50050
   134
          then obtain s2 m1 m2 where "?P s2 m1 m2" by blast
nipkow@50050
   135
          with `n2 = Suc n3` `n1 = Suc n2`have "m2 < n1" by arith
nipkow@50050
   136
          from less.IH[OF this] `?P s2 m1 m2` show ?thesis by blast
nipkow@50050
   137
        qed
nipkow@50050
   138
      next
nipkow@50050
   139
        assume "(iw', s') = (SKIP, s)"
nipkow@50050
   140
        thus ?thesis using star_if_stepsn[OF n3] by(auto dest!: SKIP_starD)
nipkow@50050
   141
      qed
nipkow@50050
   142
    qed
nipkow@50050
   143
  qed
nipkow@50050
   144
qed
nipkow@50050
   145
nipkow@50050
   146
lemma reachable_While: "reachable (WHILE b DO c) \<subseteq>
nipkow@52046
   147
  {WHILE b DO c, IF b THEN c ;; WHILE b DO c ELSE SKIP, SKIP} \<union>
nipkow@52046
   148
  (\<lambda>c'. c' ;; WHILE b DO c) ` reachable c"
nipkow@50050
   149
apply(auto simp: reachable_def image_def)
nipkow@50050
   150
by (metis While_stepsnD insertE singletonE stepsn_if_star)
nipkow@50050
   151
nipkow@50050
   152
nipkow@50050
   153
theorem finite_reachable: "finite(reachable c)"
nipkow@50050
   154
apply(induction c)
nipkow@50050
   155
apply(auto simp: reachable_SKIP reachable_Assign
nipkow@50050
   156
  finite_subset[OF reachable_Seq] finite_subset[OF reachable_If]
nipkow@50050
   157
  finite_subset[OF reachable_While])
nipkow@50050
   158
done
nipkow@50050
   159
nipkow@50050
   160
nipkow@62390
   161
end