Mercurial Mercurial > hg > tm2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/Hoare_gen.thy
changeset 3 545fef826fa9
parent 2 995eb45bbadc
child 5 6c722e960f2e
equal deleted inserted replaced
2:995eb45bbadc 3:545fef826fa9 
     5 theory Hoare_gen
 
     5 theory Hoare_gen
 
     6 imports Main  
     6 imports Main  
     7   "../Separation_Algebra/Sep_Tactics"
 
     7   "../Separation_Algebra/Sep_Tactics"
 
     8 begin
 
     8 begin
 
     9 
     9 
    10 definition pasrt :: "bool \<Rightarrow> (('a::sep_algebra) \<Rightarrow> bool)" ("<_>" [72] 71)
 
    10 definition 
       
    11   pasrt :: "bool \<Rightarrow> 'a::sep_algebra \<Rightarrow> bool" ("<_>" [72] 71)
 
    11 where "pasrt b = (\<lambda> s . s = 0 \<and> b)"
 
    12 where "pasrt b = (\<lambda> s . s = 0 \<and> b)"
 
    12 
    13 
    13 lemma sep_conj_cond1: "(p \<and>* <cond> \<and>* q) = (<cond> \<and>* p \<and>* q)"
 
    14 
    14   by(simp add: sep_conj_ac)
 
    15 (* smae as sep.mult.left_commute *)
 
    15 
    16 lemma sep_conj_cond1: 
    16 lemma sep_conj_cond2: "(p \<and>* <cond>) = (<cond> \<and>* p)"
 
    17   "(p \<and>* <cond> \<and>* q) = (<cond> \<and>* p \<and>* q)"
 
    17   by(simp add: sep_conj_ac)
 
    18   by (rule sep.mult.left_commute)
 
    18 
    19 
    19 lemma sep_conj_cond3: "((<cond> \<and>* p) \<and>* r) = (<cond> \<and>* p \<and>* r)"
 
    20 (* same as sep.mult.commute *)
 
    20   by (metis sep.mult_assoc)
 
    21 lemma sep_conj_cond2: 
       
    22   "(p \<and>* <cond>) = (<cond> \<and>* p)"
 
       
    23   by(rule sep.mult.commute)
 
       
    24 
       
    25 (* same as sep.mult_assoc *)
 
       
    26 lemma sep_conj_cond3: 
       
    27   "((<cond> \<and>* p) \<and>* r) = (<cond> \<and>* p \<and>* r)"
 
       
    28   by (rule sep.mult_assoc)
 
    21 
    29 
    22 lemmas sep_conj_cond = sep_conj_cond1 sep_conj_cond2 sep_conj_cond3
 
    30 lemmas sep_conj_cond = sep_conj_cond1 sep_conj_cond2 sep_conj_cond3
 
    23 
    31 
    24 lemma cond_true_eq[simp]: "<True> = \<box>"
 
    32 lemma cond_true_eq[simp]: "<True> = \<box>"
 
    25   by(unfold sep_empty_def pasrt_def, auto)
 
    33   by(unfold sep_empty_def pasrt_def, auto)
 
    31   by (simp add:pasrt_def)
 
    39   by (simp add:pasrt_def)
 
    32 
    40 
    33 lemma cond_true_eq2: "(p \<and>* <True>) = p"
 
    41 lemma cond_true_eq2: "(p \<and>* <True>) = p"
 
    34   by simp
 
    42   by simp
 
    35 
    43 
    36 lemma condD: "(<b> ** r) s \<Longrightarrow> b \<and> r s" 
    44 lemma condD: "(<b> \<and>* r) s \<Longrightarrow> b \<and> r s" 
    37 by (unfold sep_conj_def pasrt_def, auto)
 
    45 by (unfold sep_conj_def pasrt_def, auto)
 
    38 
    46 
    39 locale sep_exec = 
    47 locale sep_exec = 
    40    fixes step :: "'conf \<Rightarrow> 'conf"
 
    48    fixes step :: "'conf \<Rightarrow> 'conf"
 
    41     and  recse:: "'conf \<Rightarrow> 'a::sep_algebra"
 
    49     and  recse:: "'conf \<Rightarrow> 'a::sep_algebra"
 
    42 begin 
    50 begin 
    43 
    51 
    44 definition "run n = step ^^ n"
 
    52 definition "run n = step ^^ n"
 
    45 
    53 
    46 lemma run_add: "run (n1 + n2) s = run n1 (run n2 s)"
 
    54 lemma run_add: "run (n1 + n2) s = run n1 (run n2 s)"
 
    47   apply (unfold run_def)
 
    55   unfolding run_def
 
    48   by (metis funpow_add o_apply)
 
    56   by (simp add: funpow_add)
 
    49 
    57 
       
    58 (* separation Hoare tripple *)
 
    50 definition
 
    59 definition
 
    51   Hoare_gen :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" 
    60   Hoare_gen :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"  ("(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)
 
    52                   ("(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50)
 
       
    53 where
 
    61 where
 
    54   "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace> \<equiv> 
    62   "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace> \<equiv> 
    55       (\<forall> s r. (p**c**r) (recse s) \<longrightarrow> (\<exists> k. ((q ** c ** r) (recse (run (Suc k) s)))))"
 
    63       (\<forall>s r. (p \<and>* c \<and>* r) (recse s) \<longrightarrow> (\<exists>k. ((q \<and>* c \<and>* r) (recse (run (Suc k) s)))))"
 
    56 
    64 
    57 lemma HoareI [case_names Pre]: 
    65 lemma HoareI [case_names Pre]: 
    58   assumes h: "\<And> r s. (p**c**r) (recse s) \<Longrightarrow> (\<exists> k. ((q ** c ** r) (recse (run (Suc k) s))))"
 
    66   assumes h: "\<And> r s. (p \<and>* c \<and>* r) (recse s) \<Longrightarrow> (\<exists>k. ((q \<and>* c \<and>* r) (recse (run (Suc k) s))))"
 
    59   shows "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
 
    67   shows "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
 
    60   using h
 
    68   using h
 
    61   by (unfold Hoare_gen_def, auto)
 
    69   unfolding Hoare_gen_def
 
       
    70   by simp
 
    62 
    71 
    63 lemma frame_rule: 
    72 lemma frame_rule: 
    64   assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
 
    73   assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
 
    65   shows "\<lbrace> p ** r \<rbrace> c \<lbrace> q ** r \<rbrace>"
 
    74   shows "\<lbrace>p \<and>* r\<rbrace> c \<lbrace>q \<and>* r\<rbrace>"
 
    66 proof(induct rule: HoareI)
 
    75 using assms
 
    67   case (Pre r' s')
 
    76 unfolding Hoare_gen_def
 
    68   hence "(p \<and>* c \<and>* r \<and>* r') (recse s')" by (auto simp:sep_conj_ac)
 
    77 by (metis sep_conj_assoc sep_conj_left_commute)
 
    69   from h[unfolded Hoare_gen_def, rule_format, OF this]
 
       
    70   show ?case
 
       
    71     by (metis sep_conj_assoc sep_conj_left_commute)
 
       
    72 qed
 
       
    73 
    78 
    74 lemma sequencing: 
    79 lemma sequencing: 
    75   assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
 
    80   assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
 
    76   and h2: "\<lbrace>q\<rbrace> c \<lbrace>r\<rbrace>"
 
    81   and h2: "\<lbrace>q\<rbrace> c \<lbrace>r\<rbrace>"
 
    77   shows "\<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>"
 
    82   shows "\<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>"
 
    78 proof(induct rule:HoareI)
 
    83 proof(induct rule: HoareI)
 
    79   case (Pre r' s')
 
    84   case (Pre r' s')
 
    80   from h1[unfolded Hoare_gen_def, rule_format, OF Pre]
 
    85   have "(p \<and>* c \<and>* r') (recse s')" by fact
 
       
    86   with h1[unfolded Hoare_gen_def]
 
    81   obtain k1 where "(q \<and>* c \<and>* r') (recse (run (Suc k1) s'))" by auto
 
    87   obtain k1 where "(q \<and>* c \<and>* r') (recse (run (Suc k1) s'))" by auto
 
    82   from h2[unfolded Hoare_gen_def, rule_format, OF this]
 
    88   with h2[unfolded Hoare_gen_def]
 
    83   obtain k2 where "(r \<and>* c \<and>* r') (recse (run (Suc k2) (run (Suc k1) s')))" by auto
 
    89   obtain k2 where "(r \<and>* c \<and>* r') (recse (run (Suc k2) (run (Suc k1) s')))" by auto
 
    84   thus ?case
 
    90   thus "\<exists>k. (r \<and>* c \<and>* r') (recse (run (Suc k) s'))"
 
    85     apply (rule_tac x = "Suc (k1 + k2)" in exI)
 
    91     by (auto simp add: run_add[symmetric])
 
    86     by (metis add_Suc_right nat_add_commute sep_exec.run_add)
 
       
    87 qed
 
    92 qed
 
    88 
    93 
    89 lemma pre_stren: 
    94 lemma pre_stren: 
    90   assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
 
    95   assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
 
    91   and h2:  "\<And>s. r s \<Longrightarrow> p s"
 
    96   and h2: "\<And>s. r s \<Longrightarrow> p s"
 
    92   shows "\<lbrace>r\<rbrace> c \<lbrace>q\<rbrace>"
 
    97   shows "\<lbrace>r\<rbrace> c \<lbrace>q\<rbrace>"
 
    93 proof(induct rule:HoareI)
 
    98 using assms
 
    94   case (Pre r' s')
 
    99 unfolding Hoare_gen_def
 
    95   with h2
 
   100 by (metis sep_globalise)
 
    96   have "(p \<and>* c \<and>* r') (recse s')"
 
       
    97     by (metis sep_conj_impl1)
 
       
    98   from h1[unfolded Hoare_gen_def, rule_format, OF this]
 
       
    99   show ?case .
 
       
   100 qed
 
       
   101 
   101 
   102 lemma post_weaken: 
   102 lemma post_weaken: 
   103   assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
 
   103   assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
 
   104     and h2: "\<And> s. q s \<Longrightarrow> r s"
 
   104     and h2: "\<And> s. q s \<Longrightarrow> r s"
 
   105   shows "\<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>"
 
   105   shows "\<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>"
 
   106 proof(induct rule:HoareI)
 
   106 using assms
 
   107   case (Pre r' s')
 
   107 unfolding Hoare_gen_def
 
   108   from h1[unfolded Hoare_gen_def, rule_format, OF this]
 
   108 by (metis sep_globalise)
 
   109   obtain k where "(q \<and>* c \<and>* r') (recse (run (Suc k) s'))" by blast
 
       
   110   with h2
 
       
   111   show ?case
 
       
   112     by (metis sep_conj_impl1)
 
       
   113 qed
 
       
   114 
   109 
   115 lemma hoare_adjust:
 
   110 lemma hoare_adjust:
 
   116   assumes h1: "\<lbrace>p1\<rbrace> c \<lbrace>q1\<rbrace>"
 
   111   assumes h1: "\<lbrace>p1\<rbrace> c \<lbrace>q1\<rbrace>"
 
   117   and h2: "\<And>s. p s \<Longrightarrow> p1 s"
 
   112   and h2: "\<And>s. p s \<Longrightarrow> p1 s"
 
   118   and h3: "\<And>s. q1 s \<Longrightarrow> q s"
 
   113   and h3: "\<And>s. q1 s \<Longrightarrow> q s"
 
   119   shows "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
 
   114   shows "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
 
   120   using h1 h2 h3 post_weaken pre_stren
 
   115   using h1 h2 h3 post_weaken pre_stren
 
   121   by (metis)
 
   116   by (blast)
 
   122 
   117 
   123 lemma code_exI: 
   118 lemma code_exI: 
   124   assumes h: "\<And> k. \<lbrace>p\<rbrace> c(k) \<lbrace>q\<rbrace>"
 
   119   assumes h: "\<And> k. \<lbrace>p\<rbrace> c(k) \<lbrace>q\<rbrace>"
 
   125   shows "\<lbrace>p\<rbrace> EXS k. c(k) \<lbrace>q\<rbrace>"
 
   120   shows "\<lbrace>p\<rbrace> EXS k. c(k) \<lbrace>q\<rbrace>"
 
   126 proof(unfold pred_ex_def, induct rule:HoareI)
 
   121 unfolding pred_ex_def
 
       
   122 proof(induct rule:HoareI)
 
   127   case (Pre r' s')
 
   123   case (Pre r' s')
 
   128   then obtain k where "(p \<and>* (\<lambda> s. c k s) \<and>* r') (recse s')"
 
   124   then obtain k where "(p \<and>* (\<lambda> s. c k s) \<and>* r') (recse s')"
 
   129     by (auto elim!:sep_conjE intro!:sep_conjI)
 
   125     by (auto elim!: sep_conjE intro!: sep_conjI)
 
   130   from h[unfolded Hoare_gen_def, rule_format, OF this]
 
   126   from h[unfolded Hoare_gen_def, rule_format, OF this]
 
   131   show ?case
 
   127   show "\<exists>k. (q \<and>* (\<lambda>s. \<exists>x. c x s) \<and>* r') (recse (run (Suc k) s'))"
 
   132    by (auto elim!:sep_conjE intro!:sep_conjI)
 
   128     by (auto elim!: sep_conjE intro!: sep_conjI)
 
   133 qed
 
   129 qed
 
   134 
   130 
   135 lemma code_extension: 
   131 lemma code_extension: 
   136   assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
 
   132   assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
 
   137   shows "\<lbrace> p \<rbrace> c ** e \<lbrace> q \<rbrace>"
 
   133   shows "\<lbrace>p\<rbrace> c \<and>* e \<lbrace>q\<rbrace>"
 
   138 proof(induct rule:HoareI)
 
   134 using assms
 
   139   case (Pre r' s')
 
   135 unfolding Hoare_gen_def
 
   140   hence "(p \<and>* c \<and>* e \<and>* r') (recse s')" by (auto simp:sep_conj_ac)
 
   136 by (metis sep_conj_assoc)
 
   141   from h[unfolded Hoare_gen_def, rule_format, OF this]
 
       
   142   show ?case
 
       
   143     by (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)
 
       
   144 qed
 
       
   145 
   137 
   146 lemma code_extension1: 
   138 lemma code_extension1: 
   147   assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
 
   139   assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
 
   148   shows "\<lbrace> p \<rbrace> e ** c \<lbrace> q \<rbrace>"
 
   140   shows "\<lbrace>p\<rbrace> e \<and>* c \<lbrace>q\<rbrace>"
 
   149   by (metis code_extension h sep.mult_commute)
 
   141 using assms
 
       
   142 unfolding Hoare_gen_def
 
       
   143 by (metis sep_conj_commute sep_conj_left_commute)
 
   150 
   144 
   151 lemma composition: 
   145 lemma composition: 
   152   assumes h1: "\<lbrace>p\<rbrace> c1 \<lbrace>q\<rbrace>"
 
   146   assumes h1: "\<lbrace>p\<rbrace> c1 \<lbrace>q\<rbrace>"
 
   153     and h2: "\<lbrace>q\<rbrace> c2 \<lbrace>r\<rbrace>"
 
   147     and h2: "\<lbrace>q\<rbrace> c2 \<lbrace>r\<rbrace>"
 
   154   shows "\<lbrace>p\<rbrace> c1 ** c2 \<lbrace>r\<rbrace>"
 
   148   shows "\<lbrace>p\<rbrace> c1 \<and>* c2 \<lbrace>r\<rbrace>"
 
   155 proof(induct rule:HoareI)
 
   149 using assms
 
   156   case (Pre r' s')
 
   150 by (auto intro: sequencing code_extension code_extension1)
 
   157   hence "(p \<and>* c1 \<and>* c2 \<and>* r') (recse s')" by (auto simp:sep_conj_ac)
 
       
   158   from h1[unfolded Hoare_gen_def, rule_format, OF this]
 
       
   159   obtain k1 where "(q \<and>* c2 \<and>* c1 \<and>* r') (recse (run (Suc k1) s'))" 
       
   160     by (auto simp:sep_conj_ac)
 
       
   161   from h2[unfolded Hoare_gen_def, rule_format, OF this, folded run_add]
 
       
   162   show ?case
 
       
   163     by (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)
 
       
   164 qed
 
       
   165 
   151 
   166 
   152 
   167 definition
 
   153 definition
 
   168   IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 
   154   IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" 
   169                 ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" 
   155              ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)
 
   170                   ("(1_).(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50)
 
       
   171 where
 
   156 where
 
   172   "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> = (\<forall>s'. \<lbrace> EXS s. <P s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace> c 
   157   "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> = (\<forall>s'. \<lbrace> EXS s. <P s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace> c 
   173                          \<lbrace> EXS s. <Q s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace>)"
 
   158                         \<lbrace> EXS s. <Q s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace>)"
 
   174 
   159 
   175 lemma IHoareI [case_names IPre]: 
   160 lemma IHoareI [case_names IPre]: 
   176   assumes h: "\<And>s' s r cnf .  (<P s> \<and>* <(s ## s')> \<and>* I(s + s') \<and>* c \<and>* r) (recse cnf) \<Longrightarrow> 
   161   assumes h: "\<And>s' s r cnf .  (<P s> \<and>* <(s ## s')> \<and>* I(s + s') \<and>* c \<and>* r) (recse cnf) \<Longrightarrow> 
   177                    (\<exists>k t. (<Q t> \<and>* <(t ## s')>  \<and>* I(t + s') \<and>* c \<and>* r) (recse (run (Suc k) cnf)))"
 
   162                    (\<exists>k t. (<Q t> \<and>* <(t ## s')>  \<and>* I(t + s') \<and>* c \<and>* r) (recse (run (Suc k) cnf)))"
 
   178   shows "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"
 
   163   shows "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"
 
   179   unfolding IHoare_def
 
   164 unfolding IHoare_def
 
   180 proof
 
   165 proof
 
   181   fix s'
 
   166   fix s'
 
   182   show " \<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  c
 
   167   show " \<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  c
 
   183          \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>"
 
   168          \<lbrace>EXS s. <Q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>"
 
   184   proof(unfold pred_ex_def, induct rule:HoareI)
 
   169   proof(unfold pred_ex_def, induct rule:HoareI)
tm2