added thms wrt weakening and strengthening in Abstraction;
authormueller
Wed Jan 14 16:38:04 1998 +0100 (1998-01-14)
changeset 4577674b0b354feb
parent 4576 be6b5edbca9f
child 4578 9f79e84ce00d
added thms wrt weakening and strengthening in Abstraction;
src/HOLCF/IOA/meta_theory/Abstraction.ML
src/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOLCF/IOA/meta_theory/LiveIOA.thy
src/HOLCF/IOA/meta_theory/TL.ML
src/HOLCF/IOA/meta_theory/TL.thy
src/HOLCF/IOA/meta_theory/TLS.ML
src/HOLCF/IOA/meta_theory/TLS.thy
     1.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Wed Jan 14 11:22:03 1998 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Wed Jan 14 16:38:04 1998 +0100
     1.3 @@ -365,49 +365,210 @@
     1.4  (* ---------------------------------------------------------------- *)
     1.5  (*             Localizing Temproal Strengthenings - 2               *)
     1.6  (* ---------------------------------------------------------------- *)
     1.7 -(*
     1.8 +
     1.9 +
    1.10 +(* ------------------ Box ----------------------------*)
    1.11 +
    1.12 +(* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
    1.13 +goal thy "(UU = x @@ y) = (((x::'a Seq)= UU) | (x=nil & y=UU))";
    1.14 +by (Seq_case_simp_tac "x" 1);
    1.15 +by Auto_tac;
    1.16 +qed"UU_is_Conc";
    1.17 +
    1.18 +goal thy 
    1.19 +"Finite s1 --> \
    1.20 +\ (! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))";
    1.21 +by (rtac impI 1);
    1.22 +by (Seq_Finite_induct_tac 1);
    1.23 +(* main case *)
    1.24 +by (Blast_tac 1);
    1.25 +by (clarify_tac set_cs 1);
    1.26 +by (pair_tac "ex" 1);
    1.27 +by (Seq_case_simp_tac "y" 1);
    1.28 +(* UU case *)
    1.29 +by (clarify_tac set_cs 1);
    1.30 +by (asm_full_simp_tac (simpset() addsimps [UU_is_Conc])1);
    1.31 +by (hyp_subst_tac 1);
    1.32 +by (Asm_full_simp_tac 1);
    1.33 +(* nil case *)
    1.34 +by (clarify_tac set_cs 1);
    1.35 +by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc])1);
    1.36 +(* cons case *)
    1.37 +by (pair_tac "aa" 1);
    1.38 +auto();
    1.39 +qed_spec_mp"ex2seqConc";
    1.40 +
    1.41 +(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
    1.42 +
    1.43 +goalw thy [tsuffix_def,suffix_def]
    1.44 +"!!s. tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')";
    1.45 +auto();
    1.46 +bd ex2seqConc 1;
    1.47 +auto();
    1.48 +qed"ex2seq_tsuffix";
    1.49 +
    1.50 +
    1.51 +goal thy "(Map f`s = nil) = (s=nil)";
    1.52 +by (Seq_case_simp_tac "s" 1);
    1.53 +qed"Mapnil";
    1.54 +
    1.55 +goal thy "(Map f`s = UU) = (s=UU)";
    1.56 +by (Seq_case_simp_tac "s" 1);
    1.57 +qed"MapUU";
    1.58 +
    1.59 +
    1.60 +(* important property of cex_absSeq: As it is a 1to1 correspondence, 
    1.61 +  properties carry over *)
    1.62 +
    1.63 +goalw thy [tsuffix_def,suffix_def,cex_absSeq_def]
    1.64 +"!! s. tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)";
    1.65 +auto();
    1.66 +by (asm_full_simp_tac (simpset() addsimps [Mapnil])1);
    1.67 +by (asm_full_simp_tac (simpset() addsimps [MapUU])1);
    1.68 +by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))`s1")] exI 1);
    1.69 +by (asm_full_simp_tac (simpset() addsimps [Map2Finite,MapConc])1);
    1.70 +qed"cex_absSeq_tsuffix";
    1.71 +
    1.72 +
    1.73 +goalw thy [temp_strengthening_def,state_strengthening_def, temp_sat_def,
    1.74 +satisfies_def,Box_def]
    1.75 +"!! h. [| temp_strengthening P Q h |]\
    1.76 +\      ==> temp_strengthening ([] P) ([] Q) h";
    1.77 +by (clarify_tac set_cs 1);
    1.78 +by (forward_tac [ex2seq_tsuffix] 1);
    1.79 +by (clarify_tac set_cs 1);
    1.80 +by (dres_inst_tac [("h","h")] cex_absSeq_tsuffix 1);
    1.81 +by (asm_full_simp_tac (simpset() addsimps [ex2seq_abs_cex])1);
    1.82 +qed"strength_Box";
    1.83 +
    1.84 +
    1.85 +(* ------------------ Init ----------------------------*)
    1.86 +
    1.87  goalw thy [temp_strengthening_def,state_strengthening_def,
    1.88 -temp_sat_def,satisfies_def,Init_def]
    1.89 +temp_sat_def,satisfies_def,Init_def,unlift_def]
    1.90  "!! h. [| state_strengthening P Q h |]\
    1.91  \      ==> temp_strengthening (Init P) (Init Q) h";
    1.92  by (safe_tac set_cs);
    1.93  by (pair_tac "ex" 1);
    1.94  by (Seq_case_simp_tac "y" 1);
    1.95 +by (pair_tac "a" 1);
    1.96 +qed"strength_Init";
    1.97 +
    1.98 +
    1.99 +(* ------------------ Next ----------------------------*)
   1.100 +
   1.101 +goal thy 
   1.102 +"(TL`(ex2seq (cex_abs h ex))=UU) = (TL`(ex2seq ex)=UU)";
   1.103 +by (pair_tac "ex" 1);
   1.104 +by (Seq_case_simp_tac "y" 1);
   1.105 +by (pair_tac "a" 1);
   1.106 +by (Seq_case_simp_tac "s" 1);
   1.107 +by (pair_tac "a" 1);
   1.108 +qed"TL_ex2seq_UU";
   1.109 +
   1.110 +goal thy 
   1.111 +"(TL`(ex2seq (cex_abs h ex))=nil) = (TL`(ex2seq ex)=nil)";
   1.112 +by (pair_tac "ex" 1);
   1.113 +by (Seq_case_simp_tac "y" 1);
   1.114 +by (pair_tac "a" 1);
   1.115 +by (Seq_case_simp_tac "s" 1);
   1.116 +by (pair_tac "a" 1);
   1.117 +qed"TL_ex2seq_nil";
   1.118 +
   1.119 +(* FIX: put to Sequence Lemmas *)
   1.120 +goal thy "Map f`(TL`s) = TL`(Map f`s)";
   1.121 +by (Seq_induct_tac "s" [] 1);
   1.122 +qed"MapTL";
   1.123 +
   1.124 +(* important property of cex_absSeq: As it is a 1to1 correspondence, 
   1.125 +  properties carry over *)
   1.126 +
   1.127 +goalw thy [cex_absSeq_def]
   1.128 +"cex_absSeq h (TL`s) = (TL`(cex_absSeq h s))";
   1.129 +by (simp_tac (simpset() addsimps [MapTL]) 1);
   1.130 +qed"cex_absSeq_TL";
   1.131 +
   1.132 +(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
   1.133 +
   1.134 +goal thy "!!ex. [| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL`(ex2seq ex) = ex2seq ex')";
   1.135 +by (pair_tac "ex" 1);
   1.136 +by (Seq_case_simp_tac "y" 1);
   1.137 +by (pair_tac "a" 1);
   1.138 +auto();
   1.139 +qed"TLex2seq";
   1.140 +
   1.141 +
   1.142 +goal thy "(TL`(ex2seq ex)~=UU) = ((snd ex)~=UU)";
   1.143 +by (pair_tac "ex" 1);
   1.144 +by (Seq_case_simp_tac "y" 1);
   1.145 +by (pair_tac "a" 1);
   1.146 +by (Seq_case_simp_tac "s" 1);
   1.147 +by (pair_tac "a" 1);
   1.148 +qed"ex2seqUUTL";
   1.149 +
   1.150 +goal thy "(TL`(ex2seq ex)~=nil) = ((snd ex)~=nil)";
   1.151 +by (pair_tac "ex" 1);
   1.152 +by (Seq_case_simp_tac "y" 1);
   1.153 +by (pair_tac "a" 1);
   1.154 +by (Seq_case_simp_tac "s" 1);
   1.155 +by (pair_tac "a" 1);
   1.156 +qed"ex2seqnilTL";
   1.157 +
   1.158 +
   1.159 +goalw thy [temp_strengthening_def,state_strengthening_def,
   1.160 +temp_sat_def, satisfies_def,Next_def]
   1.161 +"!! h. [| temp_strengthening P Q h |]\
   1.162 +\      ==> temp_strengthening (Next P) (Next Q) h";
   1.163 +by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   1.164 +by (safe_tac set_cs);
   1.165 +by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
   1.166 +by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
   1.167 +by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
   1.168 +by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
   1.169 +(* cons case *)
   1.170 +by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU,
   1.171 +        ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqUUTL,ex2seqnilTL])1);
   1.172 +bd TLex2seq 1;
   1.173 +ba 1;
   1.174 +auto();
   1.175 +qed"strength_Next";
   1.176  
   1.177  
   1.178  
   1.179 -goalw thy [temp_strengthening_def,state_strengthening_def]
   1.180 -"!! h. [| temp_strengthening P Q h |]\
   1.181 -\      ==> temp_strengthening ([] P) ([] Q) h";
   1.182 -
   1.183 -goalw thy [temp_strengthening_def,state_strengthening_def]
   1.184 -"!! h. [| temp_strengthening P Q h |]\
   1.185 -\      ==> temp_strengthening (Next P) (Next Q) h";
   1.186 -
   1.187 -*)
   1.188 -
   1.189  (* ---------------------------------------------------------------- *)
   1.190 -(*             Localizing Temproal Weakenings     - 2               *)
   1.191 +(*             Localizing Temporal Weakenings     - 2               *)
   1.192  (* ---------------------------------------------------------------- *)
   1.193  
   1.194 -(*
   1.195 -goalw thy [temp_weakening_def,state_weakening_def,
   1.196 -temp_sat_def,satisfies_def,Init_def]
   1.197 +
   1.198 +goal thy 
   1.199  "!! h. [| state_weakening P Q h |]\
   1.200  \      ==> temp_weakening (Init P) (Init Q) h";
   1.201 +by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2,
   1.202 +      state_weakening_def2, temp_sat_def,satisfies_def,Init_def,unlift_def])1);
   1.203  by (safe_tac set_cs);
   1.204  by (pair_tac "ex" 1);
   1.205  by (Seq_case_simp_tac "y" 1);
   1.206 -
   1.207 +by (pair_tac "a" 1);
   1.208 +qed"weak_Init";
   1.209  
   1.210  
   1.211 -goalw thy [temp_weakening_def,state_weakening_def]
   1.212 +(*
   1.213 +
   1.214 +(* analog to strengthening thm above, with analog lemmas used  *)
   1.215 +
   1.216 +goalw thy [state_weakening_def]
   1.217  "!! h. [| temp_weakening P Q h |]\
   1.218  \      ==> temp_weakening ([] P) ([] Q) h";
   1.219 +by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2,
   1.220 +         temp_sat_def,satisfies_def,Box_def])1);
   1.221  
   1.222 -goalw thy [temp_weakening_def,state_weakening_def]
   1.223 +(* analog to strengthening thm above, with analog lemmas used  *)
   1.224 +
   1.225 +goalw thy [state_weakening_def]
   1.226  "!! h. [| temp_weakening P Q h |]\
   1.227  \      ==> temp_weakening (Next P) (Next Q) h";
   1.228 +by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2,
   1.229 +         temp_sat_def,satisfies_def,Next_def])1);
   1.230  
   1.231  *)
   1.232  
     2.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Wed Jan 14 11:22:03 1998 +0100
     2.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Wed Jan 14 16:38:04 1998 +0100
     2.3 @@ -14,7 +14,8 @@
     2.4  
     2.5  consts
     2.6  
     2.7 -  cex_abs   ::"('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution"
     2.8 +  cex_abs      ::"('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution"
     2.9 +  cex_absSeq   ::"('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq"
    2.10  
    2.11    is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
    2.12  
    2.13 @@ -44,6 +45,10 @@
    2.14  cex_abs_def
    2.15    "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))`(snd ex))"
    2.16  
    2.17 +(* equals cex_abs on Sequneces -- after ex2seq application -- *)
    2.18 +cex_absSeq_def
    2.19 +  "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))`s"
    2.20 +
    2.21  weakeningIOA_def
    2.22     "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A"
    2.23  
    2.24 @@ -61,26 +66,16 @@
    2.25  
    2.26  rules
    2.27  
    2.28 -strength_Init
    2.29 - "state_strengthening P Q h 
    2.30 -  ==> temp_strengthening (Init P) (Init Q) h"
    2.31 -
    2.32 -strength_Box
    2.33 -"temp_strengthening P Q h 
    2.34 - ==> temp_strengthening ([] P) ([] Q) h"
    2.35 +(* thm about ex2seq which is not provable by induction as ex2seq is not continous *)
    2.36 +ex2seq_abs_cex
    2.37 +  "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)" 
    2.38  
    2.39 -strength_Next
    2.40 -"temp_strengthening P Q h 
    2.41 - ==> temp_strengthening (Next P) (Next Q) h"
    2.42 -
    2.43 -weak_Init
    2.44 - "state_weakening P Q h 
    2.45 -  ==> temp_weakening (Init P) (Init Q) h"
    2.46 -
    2.47 +(* analog to the proved thm strength_Box  *)
    2.48  weak_Box
    2.49  "temp_weakening P Q h 
    2.50   ==> temp_weakening ([] P) ([] Q) h"
    2.51  
    2.52 +(* analog to the proved thm strength_Next  *)
    2.53  weak_Next
    2.54  "temp_weakening P Q h 
    2.55   ==> temp_weakening (Next P) (Next Q) h"
     3.1 --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Jan 14 11:22:03 1998 +0100
     3.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Jan 14 16:38:04 1998 +0100
     3.3 @@ -39,7 +39,7 @@
     3.4  
     3.5  SF_def
     3.6    "SF A acts ==  [] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
     3.7 -
     3.8 + 
     3.9  
    3.10  liveexecutions_def
    3.11     "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
     4.1 --- a/src/HOLCF/IOA/meta_theory/TL.ML	Wed Jan 14 11:22:03 1998 +0100
     4.2 +++ b/src/HOLCF/IOA/meta_theory/TL.ML	Wed Jan 14 16:38:04 1998 +0100
     4.3 @@ -113,6 +113,8 @@
     4.4  be STL1b 1;
     4.5  qed"STL1";
     4.6  
     4.7 +
     4.8 +
     4.9  (* Note that unlift and HD is not at all used !!! *)
    4.10  goal thy "!! P. valid (P .--> Q)  ==> validT ([] (Init P) .--> [] (Init Q))";
    4.11  by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1);
    4.12 @@ -177,3 +179,13 @@
    4.13  auto();
    4.14  
    4.15  
    4.16 +
    4.17 +
    4.18 +goal thy "!! P. [| validT (P .--> Q); validT P |] ==> validT Q";
    4.19 +by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,IMPLIES_def])1);
    4.20 +qed"ModusPonens";
    4.21 +
    4.22 +(* works only if validT is defined without restriction to s~=UU, s~=nil *)
    4.23 +goal thy "!! P. validT P ==> validT (Next P)";
    4.24 +by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1);
    4.25 +(* qed"NextTauto"; *)
    4.26 \ No newline at end of file
     5.1 --- a/src/HOLCF/IOA/meta_theory/TL.thy	Wed Jan 14 11:22:03 1998 +0100
     5.2 +++ b/src/HOLCF/IOA/meta_theory/TL.thy	Wed Jan 14 16:38:04 1998 +0100
     5.3 @@ -54,12 +54,9 @@
     5.4  Init_def
     5.5    "Init P s ==  (P (unlift (HD`s)))" 
     5.6  
     5.7 -
     5.8 -(* FIX: Introduce nice symbol infix suntax *)
     5.9  suffix_def
    5.10    "suffix s2 s == ? s1. (Finite s1  & s = s1 @@ s2)" 
    5.11  
    5.12 -(* FIX: Introduce nice symbol infix suntax *)
    5.13  tsuffix_def
    5.14    "tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s"
    5.15  
    5.16 @@ -67,7 +64,7 @@
    5.17    "([] P) s == ! s2. tsuffix s2 s --> P s2"
    5.18  
    5.19  Next_def
    5.20 -  "(Next P) s == if TL`s=UU then (P s) else P (TL`s)"
    5.21 +  "(Next P) s == if (TL`s=UU | TL`s=nil) then (P s) else P (TL`s)"
    5.22  
    5.23  Diamond_def
    5.24    "<> P == .~ ([] (.~ P))"
     6.1 --- a/src/HOLCF/IOA/meta_theory/TLS.ML	Wed Jan 14 11:22:03 1998 +0100
     6.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Wed Jan 14 16:38:04 1998 +0100
     6.3 @@ -58,7 +58,7 @@
     6.4  qed"ex2seq_cons";
     6.5  
     6.6  Delsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons]; 
     6.7 -Addsimps [ex2seq_UU,ex2seq_nil, ex2seq_cons];  
     6.8 +Addsimps [ex2seq_UUAlt,ex2seq_nil, ex2seq_cons];  
     6.9  
    6.10  
    6.11  
     7.1 --- a/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Jan 14 11:22:03 1998 +0100
     7.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Jan 14 16:38:04 1998 +0100
     7.3 @@ -75,6 +75,11 @@
     7.4  validIOA_def
     7.5    "validIOA A P == ! ex : executions A . (ex |== P)"
     7.6  
     7.7 +rules
     7.8 +
     7.9 +ex2seq_UUAlt
    7.10 +  "ex2seq (s,UU) = (s,None,s)>>UU"
    7.11 +
    7.12  
    7.13  end
    7.14