author  wenzelm 
Wed, 19 Mar 2008 22:47:35 +0100  
changeset 26339  7825c83c9eff 
parent 19741  f65265d71426 
child 26359  6d437bde2f1d 
permissions  rwrr 
4559  1 
(* Title: HOLCF/IOA/meta_theory/TLS.thy 
2 
ID: $Id$ 

12218  3 
Author: Olaf Müller 
17233  4 
*) 
4559  5 

17233  6 
header {* Temporal Logic of Steps  tailored for I/O automata *} 
4559  7 

17233  8 
theory TLS 
9 
imports IOA TL 

10 
begin 

4559  11 

17233  12 
defaultsort type 
4559  13 

14 
types 

17233  15 
('a, 's) ioa_temp = "('a option,'s)transition temporal" 
16 
('a, 's) step_pred = "('a option,'s)transition predicate" 

17 
's state_pred = "'s predicate" 

4559  18 

19 
consts 

20 

21 
option_lift :: "('a => 'b) => 'b => ('a option => 'b)" 

22 
plift :: "('a => bool) => ('a option => bool)" 

17233  23 

4559  24 
temp_sat :: "('a,'s)execution => ('a,'s)ioa_temp => bool" (infixr "==" 22) 
25 
xt1 :: "'s predicate => ('a,'s)step_pred" 

26 
xt2 :: "'a option predicate => ('a,'s)step_pred" 

27 

28 
validTE :: "('a,'s)ioa_temp => bool" 

29 
validIOA :: "('a,'s)ioa => ('a,'s)ioa_temp => bool" 

30 

5677
4feffde494cf
another little bug ;) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset

31 
mkfin :: "'a Seq => 'a Seq" 
4559  32 

33 
ex2seq :: "('a,'s)execution => ('a option,'s)transition Seq" 

17233  34 
ex2seqC :: "('a,'s)pairs > ('s => ('a option,'s)transition Seq)" 
4559  35 

36 

37 
defs 

38 

17233  39 
mkfin_def: 
5677
4feffde494cf
another little bug ;) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset

40 
"mkfin s == if Partial s then @t. Finite t & s = t @@ UU 
4feffde494cf
another little bug ;) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset

41 
else s" 
4feffde494cf
another little bug ;) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset

42 

17233  43 
option_lift_def: 
4559  44 
"option_lift f s y == case y of None => s  Some x => (f x)" 
45 

17233  46 
(* plift is used to determine that None action is always false in 
4559  47 
transition predicates *) 
17233  48 
plift_def: 
4559  49 
"plift P == option_lift P False" 
50 

17233  51 
temp_sat_def: 
4559  52 
"ex == P == ((ex2seq ex) = P)" 
53 

17233  54 
xt1_def: 
4559  55 
"xt1 P tr == P (fst tr)" 
56 

17233  57 
xt2_def: 
4559  58 
"xt2 P tr == P (fst (snd tr))" 
59 

17233  60 
ex2seq_def: 
10835  61 
"ex2seq ex == ((ex2seqC $(mkfin (snd ex))) (fst ex))" 
4559  62 

17233  63 
ex2seqC_def: 
64 
"ex2seqC == (fix$(LAM h ex. (%s. case ex of 

4559  65 
nil => (s,None,s)>>nil 
66 
 x##xs => (flift1 (%pr. 

17233  67 
(s,Some (fst pr), snd pr)>> (h$xs) (snd pr)) 
10835  68 
$x) 
4559  69 
)))" 
70 

17233  71 
validTE_def: 
4559  72 
"validTE P == ! ex. (ex == P)" 
73 

17233  74 
validIOA_def: 
4559  75 
"validIOA A P == ! ex : executions A . (ex == P)" 
76 

5976  77 

17233  78 
axioms 
5976  79 

17233  80 
mkfin_UU: 
5677
4feffde494cf
another little bug ;) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset

81 
"mkfin UU = nil" 
4feffde494cf
another little bug ;) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset

82 

17233  83 
mkfin_nil: 
5677
4feffde494cf
another little bug ;) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset

84 
"mkfin nil =nil" 
4feffde494cf
another little bug ;) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset

85 

17233  86 
mkfin_cons: 
5677
4feffde494cf
another little bug ;) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset

87 
"(mkfin (a>>s)) = (a>>(mkfin s))" 
4feffde494cf
another little bug ;) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset

88 

19741  89 

90 
lemmas [simp del] = ex_simps all_simps split_paired_Ex 

91 
declare Let_def [simp] 

92 

26339  93 
declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *} 
19741  94 

95 

96 
subsection {* ex2seqC *} 

97 

98 
lemma ex2seqC_unfold: "ex2seqC = (LAM ex. (%s. case ex of 

99 
nil => (s,None,s)>>nil 

100 
 x##xs => (flift1 (%pr. 

101 
(s,Some (fst pr), snd pr)>> (ex2seqC$xs) (snd pr)) 

102 
$x) 

103 
))" 

104 
apply (rule trans) 

105 
apply (rule fix_eq2) 

106 
apply (rule ex2seqC_def) 

107 
apply (rule beta_cfun) 

108 
apply (simp add: flift1_def) 

109 
done 

110 

111 
lemma ex2seqC_UU: "(ex2seqC $UU) s=UU" 

112 
apply (subst ex2seqC_unfold) 

113 
apply simp 

114 
done 

115 

116 
lemma ex2seqC_nil: "(ex2seqC $nil) s = (s,None,s)>>nil" 

117 
apply (subst ex2seqC_unfold) 

118 
apply simp 

119 
done 

120 

121 
lemma ex2seqC_cons: "(ex2seqC $((a,t)>>xs)) s = 

122 
(s,Some a,t)>> ((ex2seqC$xs) t)" 

123 
apply (rule trans) 

124 
apply (subst ex2seqC_unfold) 

125 
apply (simp add: Consq_def flift1_def) 

126 
apply (simp add: Consq_def flift1_def) 

127 
done 

128 

129 
declare ex2seqC_UU [simp] ex2seqC_nil [simp] ex2seqC_cons [simp] 

130 

131 

132 

133 
declare mkfin_UU [simp] mkfin_nil [simp] mkfin_cons [simp] 

134 

135 
lemma ex2seq_UU: "ex2seq (s, UU) = (s,None,s)>>nil" 

136 
apply (simp add: ex2seq_def) 

137 
done 

138 

139 
lemma ex2seq_nil: "ex2seq (s, nil) = (s,None,s)>>nil" 

140 
apply (simp add: ex2seq_def) 

141 
done 

142 

143 
lemma ex2seq_cons: "ex2seq (s, (a,t)>>ex) = (s,Some a,t) >> ex2seq (t, ex)" 

144 
apply (simp add: ex2seq_def) 

145 
done 

146 

147 
declare ex2seqC_UU [simp del] ex2seqC_nil [simp del] ex2seqC_cons [simp del] 

148 
declare ex2seq_UU [simp] ex2seq_nil [simp] ex2seq_cons [simp] 

149 

150 

151 
lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil" 

152 
apply (tactic {* pair_tac "exec" 1 *}) 

153 
apply (tactic {* Seq_case_simp_tac "y" 1 *}) 

154 
apply (tactic {* pair_tac "a" 1 *}) 

155 
done 

156 

157 

158 
subsection {* Interface TL  TLS *} 

159 

160 
(* uses the fact that in executions states overlap, which is lost in 

161 
after the translation via ex2seq !! *) 

162 

163 
lemma TL_TLS: 

164 
"[ ! s a t. (P s) & saA> t > (Q t) ] 

165 
==> ex == (Init (%(s,a,t). P s) .& Init (%(s,a,t). s aA> t) 

166 
.> (Next (Init (%(s,a,t).Q s))))" 

167 
apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def) 

168 

169 
apply (tactic "clarify_tac set_cs 1") 

170 
apply (simp split add: split_if) 

171 
(* TL = UU *) 

172 
apply (rule conjI) 

173 
apply (tactic {* pair_tac "ex" 1 *}) 

174 
apply (tactic {* Seq_case_simp_tac "y" 1 *}) 

175 
apply (tactic {* pair_tac "a" 1 *}) 

176 
apply (tactic {* Seq_case_simp_tac "s" 1 *}) 

177 
apply (tactic {* pair_tac "a" 1 *}) 

178 
(* TL = nil *) 

179 
apply (rule conjI) 

180 
apply (tactic {* pair_tac "ex" 1 *}) 

181 
apply (tactic {* Seq_case_tac "y" 1 *}) 

182 
apply (simp add: unlift_def) 

183 
apply fast 

184 
apply (simp add: unlift_def) 

185 
apply fast 

186 
apply (simp add: unlift_def) 

187 
apply (tactic {* pair_tac "a" 1 *}) 

188 
apply (tactic {* Seq_case_simp_tac "s" 1 *}) 

189 
apply (tactic {* pair_tac "a" 1 *}) 

190 
(* TL =cons *) 

191 
apply (simp add: unlift_def) 

192 

193 
apply (tactic {* pair_tac "ex" 1 *}) 

194 
apply (tactic {* Seq_case_simp_tac "y" 1 *}) 

195 
apply (tactic {* pair_tac "a" 1 *}) 

196 
apply (tactic {* Seq_case_simp_tac "s" 1 *}) 

197 
apply blast 

198 
apply fastsimp 

199 
apply (tactic {* pair_tac "a" 1 *}) 

200 
apply fastsimp 

201 
done 

4559  202 

203 
end 