# HG changeset patch
# User mueller
# Date 884792284 -3600
# Node ID 674b0b354febe555f1cd41d633ad015d669e11c2
# Parent  be6b5edbca9ffeb3bace5f4bac5c6478bf8cbdb2
added thms wrt weakening and strengthening in Abstraction;

diff -r be6b5edbca9f -r 674b0b354feb src/HOLCF/IOA/meta_theory/Abstraction.ML
--- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Wed Jan 14 11:22:03 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Wed Jan 14 16:38:04 1998 +0100
@@ -365,49 +365,210 @@
 (* ---------------------------------------------------------------- *)
 (*             Localizing Temproal Strengthenings - 2               *)
 (* ---------------------------------------------------------------- *)
-(*
+
+
+(* ------------------ Box ----------------------------*)
+
+(* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
+goal thy "(UU = x @@ y) = (((x::'a Seq)= UU) | (x=nil & y=UU))";
+by (Seq_case_simp_tac "x" 1);
+by Auto_tac;
+qed"UU_is_Conc";
+
+goal thy 
+"Finite s1 --> \
+\ (! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))";
+by (rtac impI 1);
+by (Seq_Finite_induct_tac 1);
+(* main case *)
+by (Blast_tac 1);
+by (clarify_tac set_cs 1);
+by (pair_tac "ex" 1);
+by (Seq_case_simp_tac "y" 1);
+(* UU case *)
+by (clarify_tac set_cs 1);
+by (asm_full_simp_tac (simpset() addsimps [UU_is_Conc])1);
+by (hyp_subst_tac 1);
+by (Asm_full_simp_tac 1);
+(* nil case *)
+by (clarify_tac set_cs 1);
+by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc])1);
+(* cons case *)
+by (pair_tac "aa" 1);
+auto();
+qed_spec_mp"ex2seqConc";
+
+(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
+
+goalw thy [tsuffix_def,suffix_def]
+"!!s. tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')";
+auto();
+bd ex2seqConc 1;
+auto();
+qed"ex2seq_tsuffix";
+
+
+goal thy "(Map f`s = nil) = (s=nil)";
+by (Seq_case_simp_tac "s" 1);
+qed"Mapnil";
+
+goal thy "(Map f`s = UU) = (s=UU)";
+by (Seq_case_simp_tac "s" 1);
+qed"MapUU";
+
+
+(* important property of cex_absSeq: As it is a 1to1 correspondence, 
+  properties carry over *)
+
+goalw thy [tsuffix_def,suffix_def,cex_absSeq_def]
+"!! s. tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)";
+auto();
+by (asm_full_simp_tac (simpset() addsimps [Mapnil])1);
+by (asm_full_simp_tac (simpset() addsimps [MapUU])1);
+by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))`s1")] exI 1);
+by (asm_full_simp_tac (simpset() addsimps [Map2Finite,MapConc])1);
+qed"cex_absSeq_tsuffix";
+
+
+goalw thy [temp_strengthening_def,state_strengthening_def, temp_sat_def,
+satisfies_def,Box_def]
+"!! h. [| temp_strengthening P Q h |]\
+\      ==> temp_strengthening ([] P) ([] Q) h";
+by (clarify_tac set_cs 1);
+by (forward_tac [ex2seq_tsuffix] 1);
+by (clarify_tac set_cs 1);
+by (dres_inst_tac [("h","h")] cex_absSeq_tsuffix 1);
+by (asm_full_simp_tac (simpset() addsimps [ex2seq_abs_cex])1);
+qed"strength_Box";
+
+
+(* ------------------ Init ----------------------------*)
+
 goalw thy [temp_strengthening_def,state_strengthening_def,
-temp_sat_def,satisfies_def,Init_def]
+temp_sat_def,satisfies_def,Init_def,unlift_def]
 "!! h. [| state_strengthening P Q h |]\
 \      ==> temp_strengthening (Init P) (Init Q) h";
 by (safe_tac set_cs);
 by (pair_tac "ex" 1);
 by (Seq_case_simp_tac "y" 1);
+by (pair_tac "a" 1);
+qed"strength_Init";
+
+
+(* ------------------ Next ----------------------------*)
+
+goal thy 
+"(TL`(ex2seq (cex_abs h ex))=UU) = (TL`(ex2seq ex)=UU)";
+by (pair_tac "ex" 1);
+by (Seq_case_simp_tac "y" 1);
+by (pair_tac "a" 1);
+by (Seq_case_simp_tac "s" 1);
+by (pair_tac "a" 1);
+qed"TL_ex2seq_UU";
+
+goal thy 
+"(TL`(ex2seq (cex_abs h ex))=nil) = (TL`(ex2seq ex)=nil)";
+by (pair_tac "ex" 1);
+by (Seq_case_simp_tac "y" 1);
+by (pair_tac "a" 1);
+by (Seq_case_simp_tac "s" 1);
+by (pair_tac "a" 1);
+qed"TL_ex2seq_nil";
+
+(* FIX: put to Sequence Lemmas *)
+goal thy "Map f`(TL`s) = TL`(Map f`s)";
+by (Seq_induct_tac "s" [] 1);
+qed"MapTL";
+
+(* important property of cex_absSeq: As it is a 1to1 correspondence, 
+  properties carry over *)
+
+goalw thy [cex_absSeq_def]
+"cex_absSeq h (TL`s) = (TL`(cex_absSeq h s))";
+by (simp_tac (simpset() addsimps [MapTL]) 1);
+qed"cex_absSeq_TL";
+
+(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
+
+goal thy "!!ex. [| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL`(ex2seq ex) = ex2seq ex')";
+by (pair_tac "ex" 1);
+by (Seq_case_simp_tac "y" 1);
+by (pair_tac "a" 1);
+auto();
+qed"TLex2seq";
+
+
+goal thy "(TL`(ex2seq ex)~=UU) = ((snd ex)~=UU)";
+by (pair_tac "ex" 1);
+by (Seq_case_simp_tac "y" 1);
+by (pair_tac "a" 1);
+by (Seq_case_simp_tac "s" 1);
+by (pair_tac "a" 1);
+qed"ex2seqUUTL";
+
+goal thy "(TL`(ex2seq ex)~=nil) = ((snd ex)~=nil)";
+by (pair_tac "ex" 1);
+by (Seq_case_simp_tac "y" 1);
+by (pair_tac "a" 1);
+by (Seq_case_simp_tac "s" 1);
+by (pair_tac "a" 1);
+qed"ex2seqnilTL";
+
+
+goalw thy [temp_strengthening_def,state_strengthening_def,
+temp_sat_def, satisfies_def,Next_def]
+"!! h. [| temp_strengthening P Q h |]\
+\      ==> temp_strengthening (Next P) (Next Q) h";
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (safe_tac set_cs);
+by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
+by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
+by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
+by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
+(* cons case *)
+by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU,
+        ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqUUTL,ex2seqnilTL])1);
+bd TLex2seq 1;
+ba 1;
+auto();
+qed"strength_Next";
 
 
 
-goalw thy [temp_strengthening_def,state_strengthening_def]
-"!! h. [| temp_strengthening P Q h |]\
-\      ==> temp_strengthening ([] P) ([] Q) h";
-
-goalw thy [temp_strengthening_def,state_strengthening_def]
-"!! h. [| temp_strengthening P Q h |]\
-\      ==> temp_strengthening (Next P) (Next Q) h";
-
-*)
-
 (* ---------------------------------------------------------------- *)
-(*             Localizing Temproal Weakenings     - 2               *)
+(*             Localizing Temporal Weakenings     - 2               *)
 (* ---------------------------------------------------------------- *)
 
-(*
-goalw thy [temp_weakening_def,state_weakening_def,
-temp_sat_def,satisfies_def,Init_def]
+
+goal thy 
 "!! h. [| state_weakening P Q h |]\
 \      ==> temp_weakening (Init P) (Init Q) h";
+by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2,
+      state_weakening_def2, temp_sat_def,satisfies_def,Init_def,unlift_def])1);
 by (safe_tac set_cs);
 by (pair_tac "ex" 1);
 by (Seq_case_simp_tac "y" 1);
-
+by (pair_tac "a" 1);
+qed"weak_Init";
 
 
-goalw thy [temp_weakening_def,state_weakening_def]
+(*
+
+(* analog to strengthening thm above, with analog lemmas used  *)
+
+goalw thy [state_weakening_def]
 "!! h. [| temp_weakening P Q h |]\
 \      ==> temp_weakening ([] P) ([] Q) h";
+by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2,
+         temp_sat_def,satisfies_def,Box_def])1);
 
-goalw thy [temp_weakening_def,state_weakening_def]
+(* analog to strengthening thm above, with analog lemmas used  *)
+
+goalw thy [state_weakening_def]
 "!! h. [| temp_weakening P Q h |]\
 \      ==> temp_weakening (Next P) (Next Q) h";
+by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2,
+         temp_sat_def,satisfies_def,Next_def])1);
 
 *)
 
diff -r be6b5edbca9f -r 674b0b354feb src/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Wed Jan 14 11:22:03 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Wed Jan 14 16:38:04 1998 +0100
@@ -14,7 +14,8 @@
 
 consts
 
-  cex_abs   ::"('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution"
+  cex_abs      ::"('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution"
+  cex_absSeq   ::"('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq"
 
   is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
 
@@ -44,6 +45,10 @@
 cex_abs_def
   "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))`(snd ex))"
 
+(* equals cex_abs on Sequneces -- after ex2seq application -- *)
+cex_absSeq_def
+  "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))`s"
+
 weakeningIOA_def
    "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A"
 
@@ -61,26 +66,16 @@
 
 rules
 
-strength_Init
- "state_strengthening P Q h 
-  ==> temp_strengthening (Init P) (Init Q) h"
-
-strength_Box
-"temp_strengthening P Q h 
- ==> temp_strengthening ([] P) ([] Q) h"
+(* thm about ex2seq which is not provable by induction as ex2seq is not continous *)
+ex2seq_abs_cex
+  "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)" 
 
-strength_Next
-"temp_strengthening P Q h 
- ==> temp_strengthening (Next P) (Next Q) h"
-
-weak_Init
- "state_weakening P Q h 
-  ==> temp_weakening (Init P) (Init Q) h"
-
+(* analog to the proved thm strength_Box  *)
 weak_Box
 "temp_weakening P Q h 
  ==> temp_weakening ([] P) ([] Q) h"
 
+(* analog to the proved thm strength_Next  *)
 weak_Next
 "temp_weakening P Q h 
  ==> temp_weakening (Next P) (Next Q) h"
diff -r be6b5edbca9f -r 674b0b354feb src/HOLCF/IOA/meta_theory/LiveIOA.thy
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Jan 14 11:22:03 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Jan 14 16:38:04 1998 +0100
@@ -39,7 +39,7 @@
 
 SF_def
   "SF A acts ==  [] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
-
+ 
 
 liveexecutions_def
    "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
diff -r be6b5edbca9f -r 674b0b354feb src/HOLCF/IOA/meta_theory/TL.ML
--- a/src/HOLCF/IOA/meta_theory/TL.ML	Wed Jan 14 11:22:03 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.ML	Wed Jan 14 16:38:04 1998 +0100
@@ -113,6 +113,8 @@
 be STL1b 1;
 qed"STL1";
 
+
+
 (* Note that unlift and HD is not at all used !!! *)
 goal thy "!! P. valid (P .--> Q)  ==> validT ([] (Init P) .--> [] (Init Q))";
 by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1);
@@ -177,3 +179,13 @@
 auto();
 
 
+
+
+goal thy "!! P. [| validT (P .--> Q); validT P |] ==> validT Q";
+by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,IMPLIES_def])1);
+qed"ModusPonens";
+
+(* works only if validT is defined without restriction to s~=UU, s~=nil *)
+goal thy "!! P. validT P ==> validT (Next P)";
+by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1);
+(* qed"NextTauto"; *)
\ No newline at end of file
diff -r be6b5edbca9f -r 674b0b354feb src/HOLCF/IOA/meta_theory/TL.thy
--- a/src/HOLCF/IOA/meta_theory/TL.thy	Wed Jan 14 11:22:03 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.thy	Wed Jan 14 16:38:04 1998 +0100
@@ -54,12 +54,9 @@
 Init_def
   "Init P s ==  (P (unlift (HD`s)))" 
 
-
-(* FIX: Introduce nice symbol infix suntax *)
 suffix_def
   "suffix s2 s == ? s1. (Finite s1  & s = s1 @@ s2)" 
 
-(* FIX: Introduce nice symbol infix suntax *)
 tsuffix_def
   "tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s"
 
@@ -67,7 +64,7 @@
   "([] P) s == ! s2. tsuffix s2 s --> P s2"
 
 Next_def
-  "(Next P) s == if TL`s=UU then (P s) else P (TL`s)"
+  "(Next P) s == if (TL`s=UU | TL`s=nil) then (P s) else P (TL`s)"
 
 Diamond_def
   "<> P == .~ ([] (.~ P))"
diff -r be6b5edbca9f -r 674b0b354feb src/HOLCF/IOA/meta_theory/TLS.ML
--- a/src/HOLCF/IOA/meta_theory/TLS.ML	Wed Jan 14 11:22:03 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Wed Jan 14 16:38:04 1998 +0100
@@ -58,7 +58,7 @@
 qed"ex2seq_cons";
 
 Delsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons]; 
-Addsimps [ex2seq_UU,ex2seq_nil, ex2seq_cons];  
+Addsimps [ex2seq_UUAlt,ex2seq_nil, ex2seq_cons];  
 
 
 
diff -r be6b5edbca9f -r 674b0b354feb src/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Jan 14 11:22:03 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Jan 14 16:38:04 1998 +0100
@@ -75,6 +75,11 @@
 validIOA_def
   "validIOA A P == ! ex : executions A . (ex |== P)"
 
+rules
+
+ex2seq_UUAlt
+  "ex2seq (s,UU) = (s,None,s)>>UU"
+
 
 end