--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Sat Nov 27 16:08:10 2010 -0800
@@ -0,0 +1,201 @@
+(* Title: HOLCF/IOA/meta_theory/TLS.thy
+ Author: Olaf Müller
+*)
+
+header {* Temporal Logic of Steps -- tailored for I/O automata *}
+
+theory TLS
+imports IOA TL
+begin
+
+default_sort type
+
+types
+ ('a, 's) ioa_temp = "('a option,'s)transition temporal"
+ ('a, 's) step_pred = "('a option,'s)transition predicate"
+ 's state_pred = "'s predicate"
+
+consts
+
+option_lift :: "('a => 'b) => 'b => ('a option => 'b)"
+plift :: "('a => bool) => ('a option => bool)"
+
+temp_sat :: "('a,'s)execution => ('a,'s)ioa_temp => bool" (infixr "|==" 22)
+xt1 :: "'s predicate => ('a,'s)step_pred"
+xt2 :: "'a option predicate => ('a,'s)step_pred"
+
+validTE :: "('a,'s)ioa_temp => bool"
+validIOA :: "('a,'s)ioa => ('a,'s)ioa_temp => bool"
+
+mkfin :: "'a Seq => 'a Seq"
+
+ex2seq :: "('a,'s)execution => ('a option,'s)transition Seq"
+ex2seqC :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)"
+
+
+defs
+
+mkfin_def:
+ "mkfin s == if Partial s then @t. Finite t & s = t @@ UU
+ else s"
+
+option_lift_def:
+ "option_lift f s y == case y of None => s | Some x => (f x)"
+
+(* plift is used to determine that None action is always false in
+ transition predicates *)
+plift_def:
+ "plift P == option_lift P False"
+
+temp_sat_def:
+ "ex |== P == ((ex2seq ex) |= P)"
+
+xt1_def:
+ "xt1 P tr == P (fst tr)"
+
+xt2_def:
+ "xt2 P tr == P (fst (snd tr))"
+
+ex2seq_def:
+ "ex2seq ex == ((ex2seqC $(mkfin (snd ex))) (fst ex))"
+
+ex2seqC_def:
+ "ex2seqC == (fix$(LAM h ex. (%s. case ex of
+ nil => (s,None,s)>>nil
+ | x##xs => (flift1 (%pr.
+ (s,Some (fst pr), snd pr)>> (h$xs) (snd pr))
+ $x)
+ )))"
+
+validTE_def:
+ "validTE P == ! ex. (ex |== P)"
+
+validIOA_def:
+ "validIOA A P == ! ex : executions A . (ex |== P)"
+
+
+axioms
+
+mkfin_UU:
+ "mkfin UU = nil"
+
+mkfin_nil:
+ "mkfin nil =nil"
+
+mkfin_cons:
+ "(mkfin (a>>s)) = (a>>(mkfin s))"
+
+
+lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
+
+declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
+
+
+subsection {* ex2seqC *}
+
+lemma ex2seqC_unfold: "ex2seqC = (LAM ex. (%s. case ex of
+ nil => (s,None,s)>>nil
+ | x##xs => (flift1 (%pr.
+ (s,Some (fst pr), snd pr)>> (ex2seqC$xs) (snd pr))
+ $x)
+ ))"
+apply (rule trans)
+apply (rule fix_eq2)
+apply (rule ex2seqC_def)
+apply (rule beta_cfun)
+apply (simp add: flift1_def)
+done
+
+lemma ex2seqC_UU: "(ex2seqC $UU) s=UU"
+apply (subst ex2seqC_unfold)
+apply simp
+done
+
+lemma ex2seqC_nil: "(ex2seqC $nil) s = (s,None,s)>>nil"
+apply (subst ex2seqC_unfold)
+apply simp
+done
+
+lemma ex2seqC_cons: "(ex2seqC $((a,t)>>xs)) s =
+ (s,Some a,t)>> ((ex2seqC$xs) t)"
+apply (rule trans)
+apply (subst ex2seqC_unfold)
+apply (simp add: Consq_def flift1_def)
+apply (simp add: Consq_def flift1_def)
+done
+
+declare ex2seqC_UU [simp] ex2seqC_nil [simp] ex2seqC_cons [simp]
+
+
+
+declare mkfin_UU [simp] mkfin_nil [simp] mkfin_cons [simp]
+
+lemma ex2seq_UU: "ex2seq (s, UU) = (s,None,s)>>nil"
+apply (simp add: ex2seq_def)
+done
+
+lemma ex2seq_nil: "ex2seq (s, nil) = (s,None,s)>>nil"
+apply (simp add: ex2seq_def)
+done
+
+lemma ex2seq_cons: "ex2seq (s, (a,t)>>ex) = (s,Some a,t) >> ex2seq (t, ex)"
+apply (simp add: ex2seq_def)
+done
+
+declare ex2seqC_UU [simp del] ex2seqC_nil [simp del] ex2seqC_cons [simp del]
+declare ex2seq_UU [simp] ex2seq_nil [simp] ex2seq_cons [simp]
+
+
+lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil"
+apply (tactic {* pair_tac @{context} "exec" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+done
+
+
+subsection {* Interface TL -- TLS *}
+
+(* uses the fact that in executions states overlap, which is lost in
+ after the translation via ex2seq !! *)
+
+lemma TL_TLS:
+ "[| ! s a t. (P s) & s-a--A-> t --> (Q t) |]
+ ==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t)
+ .--> (Next (Init (%(s,a,t).Q s))))"
+apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
+
+apply clarify
+apply (simp split add: split_if)
+(* TL = UU *)
+apply (rule conjI)
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+(* TL = nil *)
+apply (rule conjI)
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_tac @{context} "y" 1 *})
+apply (simp add: unlift_def)
+apply fast
+apply (simp add: unlift_def)
+apply fast
+apply (simp add: unlift_def)
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+(* TL =cons *)
+apply (simp add: unlift_def)
+
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply blast
+apply fastsimp
+apply (tactic {* pair_tac @{context} "a" 1 *})
+ apply fastsimp
+done
+
+end