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