src/HOL/Hoare_Parallel/RG_Tran.thy
changeset 35416 d8d7d1b785af
parent 32621 a073cb249a06
child 41842 d8f76db6a207
     1.1 --- a/src/HOL/Hoare_Parallel/RG_Tran.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Hoare_Parallel/RG_Tran.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -81,8 +81,7 @@
     1.4  | CptnEnv: "(P, t)#xs \<in> cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> cptn"
     1.5  | CptnComp: "\<lbrakk>(P,s) -c\<rightarrow> (Q,t); (Q, t)#xs \<in> cptn \<rbrakk> \<Longrightarrow> (P,s)#(Q,t)#xs \<in> cptn"
     1.6  
     1.7 -constdefs
     1.8 -  cp :: "('a com) option \<Rightarrow> 'a \<Rightarrow> ('a confs) set"
     1.9 +definition cp :: "('a com) option \<Rightarrow> 'a \<Rightarrow> ('a confs) set" where
    1.10    "cp P s \<equiv> {l. l!0=(P,s) \<and> l \<in> cptn}"  
    1.11  
    1.12  subsubsection {* Parallel computations *}
    1.13 @@ -95,14 +94,12 @@
    1.14  | ParCptnEnv: "(P,t)#xs \<in> par_cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> par_cptn"
    1.15  | ParCptnComp: "\<lbrakk> (P,s) -pc\<rightarrow> (Q,t); (Q,t)#xs \<in> par_cptn \<rbrakk> \<Longrightarrow> (P,s)#(Q,t)#xs \<in> par_cptn"
    1.16  
    1.17 -constdefs
    1.18 -  par_cp :: "'a par_com \<Rightarrow> 'a \<Rightarrow> ('a par_confs) set"
    1.19 +definition par_cp :: "'a par_com \<Rightarrow> 'a \<Rightarrow> ('a par_confs) set" where
    1.20    "par_cp P s \<equiv> {l. l!0=(P,s) \<and> l \<in> par_cptn}"  
    1.21  
    1.22  subsection{* Modular Definition of Computation *}
    1.23  
    1.24 -constdefs 
    1.25 -  lift :: "'a com \<Rightarrow> 'a conf \<Rightarrow> 'a conf"
    1.26 +definition lift :: "'a com \<Rightarrow> 'a conf \<Rightarrow> 'a conf" where
    1.27    "lift Q \<equiv> \<lambda>(P, s). (if P=None then (Some Q,s) else (Some(Seq (the P) Q), s))"
    1.28  
    1.29  inductive_set cptn_mod :: "('a confs) set"
    1.30 @@ -380,38 +377,36 @@
    1.31  
    1.32  types 'a rgformula = "'a com \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
    1.33  
    1.34 -constdefs
    1.35 -  assum :: "('a set \<times> ('a \<times> 'a) set) \<Rightarrow> ('a confs) set"
    1.36 +definition assum :: "('a set \<times> ('a \<times> 'a) set) \<Rightarrow> ('a confs) set" where
    1.37    "assum \<equiv> \<lambda>(pre, rely). {c. snd(c!0) \<in> pre \<and> (\<forall>i. Suc i<length c \<longrightarrow> 
    1.38                 c!i -e\<rightarrow> c!(Suc i) \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> rely)}"
    1.39  
    1.40 -  comm :: "(('a \<times> 'a) set \<times> 'a set) \<Rightarrow> ('a confs) set"
    1.41 +definition comm :: "(('a \<times> 'a) set \<times> 'a set) \<Rightarrow> ('a confs) set" where
    1.42    "comm \<equiv> \<lambda>(guar, post). {c. (\<forall>i. Suc i<length c \<longrightarrow> 
    1.43                 c!i -c\<rightarrow> c!(Suc i) \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> guar) \<and> 
    1.44                 (fst (last c) = None \<longrightarrow> snd (last c) \<in> post)}"
    1.45  
    1.46 -  com_validity :: "'a com \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool" 
    1.47 -                 ("\<Turnstile> _ sat [_, _, _, _]" [60,0,0,0,0] 45)
    1.48 +definition com_validity :: "'a com \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool" 
    1.49 +                 ("\<Turnstile> _ sat [_, _, _, _]" [60,0,0,0,0] 45) where
    1.50    "\<Turnstile> P sat [pre, rely, guar, post] \<equiv> 
    1.51     \<forall>s. cp (Some P) s \<inter> assum(pre, rely) \<subseteq> comm(guar, post)"
    1.52  
    1.53  subsection {* Validity for Parallel Programs. *}
    1.54  
    1.55 -constdefs
    1.56 -  All_None :: "(('a com) option) list \<Rightarrow> bool"
    1.57 +definition All_None :: "(('a com) option) list \<Rightarrow> bool" where
    1.58    "All_None xs \<equiv> \<forall>c\<in>set xs. c=None"
    1.59  
    1.60 -  par_assum :: "('a set \<times> ('a \<times> 'a) set) \<Rightarrow> ('a par_confs) set"
    1.61 +definition par_assum :: "('a set \<times> ('a \<times> 'a) set) \<Rightarrow> ('a par_confs) set" where
    1.62    "par_assum \<equiv> \<lambda>(pre, rely). {c. snd(c!0) \<in> pre \<and> (\<forall>i. Suc i<length c \<longrightarrow> 
    1.63               c!i -pe\<rightarrow> c!Suc i \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> rely)}"
    1.64  
    1.65 -  par_comm :: "(('a \<times> 'a) set \<times> 'a set) \<Rightarrow> ('a par_confs) set"
    1.66 +definition par_comm :: "(('a \<times> 'a) set \<times> 'a set) \<Rightarrow> ('a par_confs) set" where
    1.67    "par_comm \<equiv> \<lambda>(guar, post). {c. (\<forall>i. Suc i<length c \<longrightarrow>   
    1.68          c!i -pc\<rightarrow> c!Suc i \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> guar) \<and> 
    1.69           (All_None (fst (last c)) \<longrightarrow> snd( last c) \<in> post)}"
    1.70  
    1.71 -  par_com_validity :: "'a  par_com \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set 
    1.72 -\<Rightarrow> 'a set \<Rightarrow> bool"  ("\<Turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45)
    1.73 +definition par_com_validity :: "'a  par_com \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set 
    1.74 +\<Rightarrow> 'a set \<Rightarrow> bool"  ("\<Turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45) where
    1.75    "\<Turnstile> Ps SAT [pre, rely, guar, post] \<equiv> 
    1.76     \<forall>s. par_cp Ps s \<inter> par_assum(pre, rely) \<subseteq> par_comm(guar, post)"
    1.77  
    1.78 @@ -419,23 +414,22 @@
    1.79  
    1.80  subsubsection {* Definition of the conjoin operator *}
    1.81  
    1.82 -constdefs
    1.83 -  same_length :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"
    1.84 +definition same_length :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool" where
    1.85    "same_length c clist \<equiv> (\<forall>i<length clist. length(clist!i)=length c)"
    1.86   
    1.87 -  same_state :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"
    1.88 +definition same_state :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool" where
    1.89    "same_state c clist \<equiv> (\<forall>i <length clist. \<forall>j<length c. snd(c!j) = snd((clist!i)!j))"
    1.90  
    1.91 -  same_program :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"
    1.92 +definition same_program :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool" where
    1.93    "same_program c clist \<equiv> (\<forall>j<length c. fst(c!j) = map (\<lambda>x. fst(nth x j)) clist)"
    1.94  
    1.95 -  compat_label :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"
    1.96 +definition compat_label :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool" where
    1.97    "compat_label c clist \<equiv> (\<forall>j. Suc j<length c \<longrightarrow> 
    1.98           (c!j -pc\<rightarrow> c!Suc j \<and> (\<exists>i<length clist. (clist!i)!j -c\<rightarrow> (clist!i)! Suc j \<and> 
    1.99                         (\<forall>l<length clist. l\<noteq>i \<longrightarrow> (clist!l)!j -e\<rightarrow> (clist!l)! Suc j))) \<or> 
   1.100           (c!j -pe\<rightarrow> c!Suc j \<and> (\<forall>i<length clist. (clist!i)!j -e\<rightarrow> (clist!i)! Suc j)))"
   1.101  
   1.102 -  conjoin :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"  ("_ \<propto> _" [65,65] 64)
   1.103 +definition conjoin :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"  ("_ \<propto> _" [65,65] 64) where
   1.104    "c \<propto> clist \<equiv> (same_length c clist) \<and> (same_state c clist) \<and> (same_program c clist) \<and> (compat_label c clist)"
   1.105  
   1.106  subsubsection {* Some previous lemmas *}