1(* Title: HOL/HOLCF/IOA/TLS.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>Temporal Logic of Steps -- tailored for I/O automata\<close> 6 7theory TLS 8imports IOA TL 9begin 10 11default_sort type 12 13type_synonym ('a, 's) ioa_temp = "('a option, 's) transition temporal" 14 15type_synonym ('a, 's) step_pred = "('a option, 's) transition predicate" 16 17type_synonym 's state_pred = "'s predicate" 18 19definition mkfin :: "'a Seq \<Rightarrow> 'a Seq" 20 where "mkfin s = (if Partial s then SOME t. Finite t \<and> s = t @@ UU else s)" 21 22definition option_lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a option \<Rightarrow> 'b" 23 where "option_lift f s y = (case y of None \<Rightarrow> s | Some x \<Rightarrow> f x)" 24 25definition plift :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" 26(* plift is used to determine that None action is always false in 27 transition predicates *) 28 where "plift P = option_lift P False" 29 30definition xt1 :: "'s predicate \<Rightarrow> ('a, 's) step_pred" 31 where "xt1 P tr = P (fst tr)" 32 33definition xt2 :: "'a option predicate \<Rightarrow> ('a, 's) step_pred" 34 where "xt2 P tr = P (fst (snd tr))" 35 36definition ex2seqC :: "('a, 's) pairs \<rightarrow> ('s \<Rightarrow> ('a option, 's) transition Seq)" 37 where "ex2seqC = 38 (fix \<cdot> (LAM h ex. (\<lambda>s. case ex of 39 nil \<Rightarrow> (s, None, s) \<leadsto> nil 40 | x ## xs \<Rightarrow> (flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (h \<cdot> xs) (snd pr)) \<cdot> x))))" 41 42definition ex2seq :: "('a, 's) execution \<Rightarrow> ('a option, 's) transition Seq" 43 where "ex2seq ex = (ex2seqC \<cdot> (mkfin (snd ex))) (fst ex)" 44 45definition temp_sat :: "('a, 's) execution \<Rightarrow> ('a, 's) ioa_temp \<Rightarrow> bool" (infixr "\<TTurnstile>" 22) 46 where "(ex \<TTurnstile> P) \<longleftrightarrow> ((ex2seq ex) \<Turnstile> P)" 47 48definition validTE :: "('a, 's) ioa_temp \<Rightarrow> bool" 49 where "validTE P \<longleftrightarrow> (\<forall>ex. (ex \<TTurnstile> P))" 50 51definition validIOA :: "('a, 's) ioa \<Rightarrow> ('a, 's) ioa_temp \<Rightarrow> bool" 52 where "validIOA A P \<longleftrightarrow> (\<forall>ex \<in> executions A. (ex \<TTurnstile> P))" 53 54 55lemma IMPLIES_temp_sat [simp]: "(ex \<TTurnstile> P \<^bold>\<longrightarrow> Q) \<longleftrightarrow> ((ex \<TTurnstile> P) \<longrightarrow> (ex \<TTurnstile> Q))" 56 by (simp add: IMPLIES_def temp_sat_def satisfies_def) 57 58lemma AND_temp_sat [simp]: "(ex \<TTurnstile> P \<^bold>\<and> Q) \<longleftrightarrow> ((ex \<TTurnstile> P) \<and> (ex \<TTurnstile> Q))" 59 by (simp add: AND_def temp_sat_def satisfies_def) 60 61lemma OR_temp_sat [simp]: "(ex \<TTurnstile> P \<^bold>\<or> Q) \<longleftrightarrow> ((ex \<TTurnstile> P) \<or> (ex \<TTurnstile> Q))" 62 by (simp add: OR_def temp_sat_def satisfies_def) 63 64lemma NOT_temp_sat [simp]: "(ex \<TTurnstile> \<^bold>\<not> P) \<longleftrightarrow> (\<not> (ex \<TTurnstile> P))" 65 by (simp add: NOT_def temp_sat_def satisfies_def) 66 67 68axiomatization 69where mkfin_UU [simp]: "mkfin UU = nil" 70 and mkfin_nil [simp]: "mkfin nil = nil" 71 and mkfin_cons [simp]: "mkfin (a \<leadsto> s) = a \<leadsto> mkfin s" 72 73 74lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex 75 76setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close> 77 78 79subsection \<open>ex2seqC\<close> 80 81lemma ex2seqC_unfold: 82 "ex2seqC = 83 (LAM ex. (\<lambda>s. case ex of 84 nil \<Rightarrow> (s, None, s) \<leadsto> nil 85 | x ## xs \<Rightarrow> 86 (flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (ex2seqC \<cdot> xs) (snd pr)) \<cdot> x)))" 87 apply (rule trans) 88 apply (rule fix_eq4) 89 apply (rule ex2seqC_def) 90 apply (rule beta_cfun) 91 apply (simp add: flift1_def) 92 done 93 94lemma ex2seqC_UU [simp]: "(ex2seqC \<cdot> UU) s = UU" 95 apply (subst ex2seqC_unfold) 96 apply simp 97 done 98 99lemma ex2seqC_nil [simp]: "(ex2seqC \<cdot> nil) s = (s, None, s) \<leadsto> nil" 100 apply (subst ex2seqC_unfold) 101 apply simp 102 done 103 104lemma ex2seqC_cons [simp]: "(ex2seqC \<cdot> ((a, t) \<leadsto> xs)) s = (s, Some a,t ) \<leadsto> (ex2seqC \<cdot> xs) t" 105 apply (rule trans) 106 apply (subst ex2seqC_unfold) 107 apply (simp add: Consq_def flift1_def) 108 apply (simp add: Consq_def flift1_def) 109 done 110 111 112lemma ex2seq_UU: "ex2seq (s, UU) = (s, None, s) \<leadsto> nil" 113 by (simp add: ex2seq_def) 114 115lemma ex2seq_nil: "ex2seq (s, nil) = (s, None, s) \<leadsto> nil" 116 by (simp add: ex2seq_def) 117 118lemma ex2seq_cons: "ex2seq (s, (a, t) \<leadsto> ex) = (s, Some a, t) \<leadsto> ex2seq (t, ex)" 119 by (simp add: ex2seq_def) 120 121declare ex2seqC_UU [simp del] ex2seqC_nil [simp del] ex2seqC_cons [simp del] 122declare ex2seq_UU [simp] ex2seq_nil [simp] ex2seq_cons [simp] 123 124 125lemma ex2seq_nUUnnil: "ex2seq exec \<noteq> UU \<and> ex2seq exec \<noteq> nil" 126 apply (pair exec) 127 apply (Seq_case_simp x2) 128 apply (pair a) 129 done 130 131 132subsection \<open>Interface TL -- TLS\<close> 133 134(* uses the fact that in executions states overlap, which is lost in 135 after the translation via ex2seq !! *) 136 137lemma TL_TLS: 138 "\<forall>s a t. (P s) \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> (Q t) 139 \<Longrightarrow> ex \<TTurnstile> (Init (\<lambda>(s, a, t). P s) \<^bold>\<and> Init (\<lambda>(s, a, t). s \<midarrow>a\<midarrow>A\<rightarrow> t) 140 \<^bold>\<longrightarrow> (\<circle>(Init (\<lambda>(s, a, t). Q s))))" 141 apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def) 142 apply clarify 143 apply (simp split: if_split) 144 text \<open>\<open>TL = UU\<close>\<close> 145 apply (rule conjI) 146 apply (pair ex) 147 apply (Seq_case_simp x2) 148 apply (pair a) 149 apply (Seq_case_simp s) 150 apply (pair a) 151 text \<open>\<open>TL = nil\<close>\<close> 152 apply (rule conjI) 153 apply (pair ex) 154 apply (Seq_case x2) 155 apply (simp add: unlift_def) 156 apply fast 157 apply (simp add: unlift_def) 158 apply fast 159 apply (simp add: unlift_def) 160 apply (pair a) 161 apply (Seq_case_simp s) 162 apply (pair a) 163 text \<open>\<open>TL = cons\<close>\<close> 164 apply (simp add: unlift_def) 165 apply (pair ex) 166 apply (Seq_case_simp x2) 167 apply (pair a) 168 apply (Seq_case_simp s) 169 apply (pair a) 170 done 171 172end 173