1(* Title: HOL/HOLCF/IOA/Abstraction.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>Abstraction Theory -- tailored for I/O automata\<close> 6 7theory Abstraction 8imports LiveIOA 9begin 10 11default_sort type 12 13definition cex_abs :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) execution \<Rightarrow> ('a, 's2) execution" 14 where "cex_abs f ex = (f (fst ex), Map (\<lambda>(a, t). (a, f t)) \<cdot> (snd ex))" 15 16text \<open>equals cex_abs on Sequences -- after ex2seq application\<close> 17definition cex_absSeq :: 18 "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a option, 's1) transition Seq \<Rightarrow> ('a option, 's2)transition Seq" 19 where "cex_absSeq f = (\<lambda>s. Map (\<lambda>(s, a, t). (f s, a, f t)) \<cdot> s)" 20 21definition is_abstraction :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool" 22 where "is_abstraction f C A \<longleftrightarrow> 23 ((\<forall>s \<in> starts_of C. f s \<in> starts_of A) \<and> 24 (\<forall>s t a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<longrightarrow> f s \<midarrow>a\<midarrow>A\<rightarrow> f t))" 25 26definition weakeningIOA :: "('a, 's2) ioa \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> bool" 27 where "weakeningIOA A C h \<longleftrightarrow> (\<forall>ex. ex \<in> executions C \<longrightarrow> cex_abs h ex \<in> executions A)" 28 29definition temp_strengthening :: "('a, 's2) ioa_temp \<Rightarrow> ('a, 's1) ioa_temp \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> bool" 30 where "temp_strengthening Q P h \<longleftrightarrow> (\<forall>ex. (cex_abs h ex \<TTurnstile> Q) \<longrightarrow> (ex \<TTurnstile> P))" 31 32definition temp_weakening :: "('a, 's2) ioa_temp \<Rightarrow> ('a, 's1) ioa_temp \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> bool" 33 where "temp_weakening Q P h \<longleftrightarrow> temp_strengthening (\<^bold>\<not> Q) (\<^bold>\<not> P) h" 34 35definition state_strengthening :: "('a, 's2) step_pred \<Rightarrow> ('a, 's1) step_pred \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> bool" 36 where "state_strengthening Q P h \<longleftrightarrow> (\<forall>s t a. Q (h s, a, h t) \<longrightarrow> P (s, a, t))" 37 38definition state_weakening :: "('a, 's2) step_pred \<Rightarrow> ('a, 's1) step_pred \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> bool" 39 where "state_weakening Q P h \<longleftrightarrow> state_strengthening (\<^bold>\<not> Q) (\<^bold>\<not> P) h" 40 41definition is_live_abstraction :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) live_ioa \<Rightarrow> ('a, 's2) live_ioa \<Rightarrow> bool" 42 where "is_live_abstraction h CL AM \<longleftrightarrow> 43 is_abstraction h (fst CL) (fst AM) \<and> temp_weakening (snd AM) (snd CL) h" 44 45 46(* thm about ex2seq which is not provable by induction as ex2seq is not continous *) 47axiomatization where 48 ex2seq_abs_cex: "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)" 49 50(* analog to the proved thm strength_Box - proof skipped as trivial *) 51axiomatization where 52 weak_Box: "temp_weakening P Q h \<Longrightarrow> temp_weakening (\<box>P) (\<box>Q) h" 53 54(* analog to the proved thm strength_Next - proof skipped as trivial *) 55axiomatization where 56 weak_Next: "temp_weakening P Q h \<Longrightarrow> temp_weakening (\<circle>P) (\<circle>Q) h" 57 58 59subsection \<open>\<open>cex_abs\<close>\<close> 60 61lemma cex_abs_UU [simp]: "cex_abs f (s, UU) = (f s, UU)" 62 by (simp add: cex_abs_def) 63 64lemma cex_abs_nil [simp]: "cex_abs f (s,nil) = (f s, nil)" 65 by (simp add: cex_abs_def) 66 67lemma cex_abs_cons [simp]: 68 "cex_abs f (s, (a, t) \<leadsto> ex) = (f s, (a, f t) \<leadsto> (snd (cex_abs f (t, ex))))" 69 by (simp add: cex_abs_def) 70 71 72subsection \<open>Lemmas\<close> 73 74lemma temp_weakening_def2: "temp_weakening Q P h \<longleftrightarrow> (\<forall>ex. (ex \<TTurnstile> P) \<longrightarrow> (cex_abs h ex \<TTurnstile> Q))" 75 apply (simp add: temp_weakening_def temp_strengthening_def NOT_def temp_sat_def satisfies_def) 76 apply auto 77 done 78 79lemma state_weakening_def2: "state_weakening Q P h \<longleftrightarrow> (\<forall>s t a. P (s, a, t) \<longrightarrow> Q (h s, a, h t))" 80 apply (simp add: state_weakening_def state_strengthening_def NOT_def) 81 apply auto 82 done 83 84 85subsection \<open>Abstraction Rules for Properties\<close> 86 87lemma exec_frag_abstraction [rule_format]: 88 "is_abstraction h C A \<Longrightarrow> 89 \<forall>s. reachable C s \<and> is_exec_frag C (s, xs) \<longrightarrow> is_exec_frag A (cex_abs h (s, xs))" 90 apply (simp add: cex_abs_def) 91 apply (pair_induct xs simp: is_exec_frag_def) 92 txt \<open>main case\<close> 93 apply (auto dest: reachable.reachable_n simp add: is_abstraction_def) 94 done 95 96lemma abs_is_weakening: "is_abstraction h C A \<Longrightarrow> weakeningIOA A C h" 97 apply (simp add: weakeningIOA_def) 98 apply auto 99 apply (simp add: executions_def) 100 txt \<open>start state\<close> 101 apply (rule conjI) 102 apply (simp add: is_abstraction_def cex_abs_def) 103 txt \<open>is-execution-fragment\<close> 104 apply (erule exec_frag_abstraction) 105 apply (simp add: reachable.reachable_0) 106 done 107 108 109lemma AbsRuleT1: 110 "is_abstraction h C A \<Longrightarrow> validIOA A Q \<Longrightarrow> temp_strengthening Q P h \<Longrightarrow> validIOA C P" 111 apply (drule abs_is_weakening) 112 apply (simp add: weakeningIOA_def validIOA_def temp_strengthening_def) 113 apply (auto simp add: split_paired_all) 114 done 115 116 117lemma AbsRuleT2: 118 "is_live_abstraction h (C, L) (A, M) \<Longrightarrow> validLIOA (A, M) Q \<Longrightarrow> temp_strengthening Q P h 119 \<Longrightarrow> validLIOA (C, L) P" 120 apply (unfold is_live_abstraction_def) 121 apply auto 122 apply (drule abs_is_weakening) 123 apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def) 124 apply (auto simp add: split_paired_all) 125 done 126 127 128lemma AbsRuleTImprove: 129 "is_live_abstraction h (C, L) (A, M) \<Longrightarrow> validLIOA (A,M) (H1 \<^bold>\<longrightarrow> Q) \<Longrightarrow> 130 temp_strengthening Q P h \<Longrightarrow> temp_weakening H1 H2 h \<Longrightarrow> validLIOA (C, L) H2 \<Longrightarrow> 131 validLIOA (C, L) P" 132 apply (unfold is_live_abstraction_def) 133 apply auto 134 apply (drule abs_is_weakening) 135 apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def) 136 apply (auto simp add: split_paired_all) 137 done 138 139 140subsection \<open>Correctness of safe abstraction\<close> 141 142lemma abstraction_is_ref_map: "is_abstraction h C A \<Longrightarrow> is_ref_map h C A" 143 apply (auto simp: is_abstraction_def is_ref_map_def) 144 apply (rule_tac x = "(a,h t) \<leadsto>nil" in exI) 145 apply (simp add: move_def) 146 done 147 148lemma abs_safety: "inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> is_abstraction h C A \<Longrightarrow> C =<| A" 149 apply (simp add: ioa_implements_def) 150 apply (rule trace_inclusion) 151 apply (simp (no_asm) add: externals_def) 152 apply (auto)[1] 153 apply (erule abstraction_is_ref_map) 154 done 155 156 157subsection \<open>Correctness of life abstraction\<close> 158 159text \<open> 160 Reduces to \<open>Filter (Map fst x) = Filter (Map fst (Map (\<lambda>(a, t). (a, x)) x)\<close>, 161 that is to special Map Lemma. 162\<close> 163lemma traces_coincide_abs: 164 "ext C = ext A \<Longrightarrow> mk_trace C \<cdot> xs = mk_trace A \<cdot> (snd (cex_abs f (s, xs)))" 165 apply (unfold cex_abs_def mk_trace_def filter_act_def) 166 apply simp 167 apply (pair_induct xs) 168 done 169 170 171text \<open> 172 Does not work with \<open>abstraction_is_ref_map\<close> as proof of \<open>abs_safety\<close>, because 173 \<open>is_live_abstraction\<close> includes \<open>temp_strengthening\<close> which is necessarily based 174 on \<open>cex_abs\<close> and not on \<open>corresp_ex\<close>. Thus, the proof is redone in a more specific 175 way for \<open>cex_abs\<close>. 176\<close> 177lemma abs_liveness: 178 "inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> is_live_abstraction h (C, M) (A, L) \<Longrightarrow> 179 live_implements (C, M) (A, L)" 180 apply (simp add: is_live_abstraction_def live_implements_def livetraces_def liveexecutions_def) 181 apply auto 182 apply (rule_tac x = "cex_abs h ex" in exI) 183 apply auto 184 text \<open>Traces coincide\<close> 185 apply (pair ex) 186 apply (rule traces_coincide_abs) 187 apply (simp (no_asm) add: externals_def) 188 apply (auto)[1] 189 190 text \<open>\<open>cex_abs\<close> is execution\<close> 191 apply (pair ex) 192 apply (simp add: executions_def) 193 text \<open>start state\<close> 194 apply (rule conjI) 195 apply (simp add: is_abstraction_def cex_abs_def) 196 text \<open>\<open>is_execution_fragment\<close>\<close> 197 apply (erule exec_frag_abstraction) 198 apply (simp add: reachable.reachable_0) 199 200 text \<open>Liveness\<close> 201 apply (simp add: temp_weakening_def2) 202 apply (pair ex) 203 done 204 205 206subsection \<open>Abstraction Rules for Automata\<close> 207 208lemma AbsRuleA1: 209 "inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> inp Q = inp P \<Longrightarrow> out Q = out P \<Longrightarrow> 210 is_abstraction h1 C A \<Longrightarrow> A =<| Q \<Longrightarrow> is_abstraction h2 Q P \<Longrightarrow> C =<| P" 211 apply (drule abs_safety) 212 apply assumption+ 213 apply (drule abs_safety) 214 apply assumption+ 215 apply (erule implements_trans) 216 apply (erule implements_trans) 217 apply assumption 218 done 219 220lemma AbsRuleA2: 221 "inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> inp Q = inp P \<Longrightarrow> out Q = out P \<Longrightarrow> 222 is_live_abstraction h1 (C, LC) (A, LA) \<Longrightarrow> live_implements (A, LA) (Q, LQ) \<Longrightarrow> 223 is_live_abstraction h2 (Q, LQ) (P, LP) \<Longrightarrow> live_implements (C, LC) (P, LP)" 224 apply (drule abs_liveness) 225 apply assumption+ 226 apply (drule abs_liveness) 227 apply assumption+ 228 apply (erule live_implements_trans) 229 apply (erule live_implements_trans) 230 apply assumption 231 done 232 233 234declare split_paired_All [simp del] 235 236 237subsection \<open>Localizing Temporal Strengthenings and Weakenings\<close> 238 239lemma strength_AND: 240 "temp_strengthening P1 Q1 h \<Longrightarrow> temp_strengthening P2 Q2 h \<Longrightarrow> 241 temp_strengthening (P1 \<^bold>\<and> P2) (Q1 \<^bold>\<and> Q2) h" 242 by (auto simp: temp_strengthening_def) 243 244lemma strength_OR: 245 "temp_strengthening P1 Q1 h \<Longrightarrow> temp_strengthening P2 Q2 h \<Longrightarrow> 246 temp_strengthening (P1 \<^bold>\<or> P2) (Q1 \<^bold>\<or> Q2) h" 247 by (auto simp: temp_strengthening_def) 248 249lemma strength_NOT: "temp_weakening P Q h \<Longrightarrow> temp_strengthening (\<^bold>\<not> P) (\<^bold>\<not> Q) h" 250 by (auto simp: temp_weakening_def2 temp_strengthening_def) 251 252lemma strength_IMPLIES: 253 "temp_weakening P1 Q1 h \<Longrightarrow> temp_strengthening P2 Q2 h \<Longrightarrow> 254 temp_strengthening (P1 \<^bold>\<longrightarrow> P2) (Q1 \<^bold>\<longrightarrow> Q2) h" 255 by (simp add: temp_weakening_def2 temp_strengthening_def) 256 257 258lemma weak_AND: 259 "temp_weakening P1 Q1 h \<Longrightarrow> temp_weakening P2 Q2 h \<Longrightarrow> 260 temp_weakening (P1 \<^bold>\<and> P2) (Q1 \<^bold>\<and> Q2) h" 261 by (simp add: temp_weakening_def2) 262 263lemma weak_OR: 264 "temp_weakening P1 Q1 h \<Longrightarrow> temp_weakening P2 Q2 h \<Longrightarrow> 265 temp_weakening (P1 \<^bold>\<or> P2) (Q1 \<^bold>\<or> Q2) h" 266 by (simp add: temp_weakening_def2) 267 268lemma weak_NOT: 269 "temp_strengthening P Q h \<Longrightarrow> temp_weakening (\<^bold>\<not> P) (\<^bold>\<not> Q) h" 270 by (auto simp add: temp_weakening_def2 temp_strengthening_def) 271 272lemma weak_IMPLIES: 273 "temp_strengthening P1 Q1 h \<Longrightarrow> temp_weakening P2 Q2 h \<Longrightarrow> 274 temp_weakening (P1 \<^bold>\<longrightarrow> P2) (Q1 \<^bold>\<longrightarrow> Q2) h" 275 by (simp add: temp_weakening_def2 temp_strengthening_def) 276 277 278subsubsection \<open>Box\<close> 279 280(* FIXME: should be same as nil_is_Conc2 when all nils are turned to right side! *) 281lemma UU_is_Conc: "(UU = x @@ y) = (((x::'a Seq)= UU) | (x = nil \<and> y = UU))" 282 by (Seq_case_simp x) 283 284lemma ex2seqConc [rule_format]: 285 "Finite s1 \<longrightarrow> (\<forall>ex. (s \<noteq> nil \<and> s \<noteq> UU \<and> ex2seq ex = s1 @@ s) \<longrightarrow> (\<exists>ex'. s = ex2seq ex'))" 286 apply (rule impI) 287 apply Seq_Finite_induct 288 apply blast 289 text \<open>main case\<close> 290 apply clarify 291 apply (pair ex) 292 apply (Seq_case_simp x2) 293 text \<open>\<open>UU\<close> case\<close> 294 apply (simp add: nil_is_Conc) 295 text \<open>\<open>nil\<close> case\<close> 296 apply (simp add: nil_is_Conc) 297 text \<open>cons case\<close> 298 apply (pair aa) 299 apply auto 300 done 301 302(* important property of ex2seq: can be shiftet, as defined "pointwise" *) 303lemma ex2seq_tsuffix: "tsuffix s (ex2seq ex) \<Longrightarrow> \<exists>ex'. s = (ex2seq ex')" 304 apply (unfold tsuffix_def suffix_def) 305 apply auto 306 apply (drule ex2seqConc) 307 apply auto 308 done 309 310 311(*important property of cex_absSeq: As it is a 1to1 correspondence, 312 properties carry over *) 313lemma cex_absSeq_tsuffix: "tsuffix s t \<Longrightarrow> tsuffix (cex_absSeq h s) (cex_absSeq h t)" 314 apply (unfold tsuffix_def suffix_def cex_absSeq_def) 315 apply auto 316 apply (simp add: Mapnil) 317 apply (simp add: MapUU) 318 apply (rule_tac x = "Map (% (s,a,t) . (h s,a, h t))\<cdot>s1" in exI) 319 apply (simp add: Map2Finite MapConc) 320 done 321 322 323lemma strength_Box: "temp_strengthening P Q h \<Longrightarrow> temp_strengthening (\<box>P) (\<box>Q) h" 324 apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Box_def) 325 apply clarify 326 apply (frule ex2seq_tsuffix) 327 apply clarify 328 apply (drule_tac h = "h" in cex_absSeq_tsuffix) 329 apply (simp add: ex2seq_abs_cex) 330 done 331 332 333subsubsection \<open>Init\<close> 334 335lemma strength_Init: 336 "state_strengthening P Q h \<Longrightarrow> temp_strengthening (Init P) (Init Q) h" 337 apply (unfold temp_strengthening_def state_strengthening_def 338 temp_sat_def satisfies_def Init_def unlift_def) 339 apply auto 340 apply (pair ex) 341 apply (Seq_case_simp x2) 342 apply (pair a) 343 done 344 345 346subsubsection \<open>Next\<close> 347 348lemma TL_ex2seq_UU: "TL \<cdot> (ex2seq (cex_abs h ex)) = UU \<longleftrightarrow> TL \<cdot> (ex2seq ex) = UU" 349 apply (pair ex) 350 apply (Seq_case_simp x2) 351 apply (pair a) 352 apply (Seq_case_simp s) 353 apply (pair a) 354 done 355 356lemma TL_ex2seq_nil: "TL \<cdot> (ex2seq (cex_abs h ex)) = nil \<longleftrightarrow> TL \<cdot> (ex2seq ex) = nil" 357 apply (pair ex) 358 apply (Seq_case_simp x2) 359 apply (pair a) 360 apply (Seq_case_simp s) 361 apply (pair a) 362 done 363 364(*important property of cex_absSeq: As it is a 1to1 correspondence, 365 properties carry over*) 366lemma cex_absSeq_TL: "cex_absSeq h (TL \<cdot> s) = TL \<cdot> (cex_absSeq h s)" 367 by (simp add: MapTL cex_absSeq_def) 368 369(* important property of ex2seq: can be shiftet, as defined "pointwise" *) 370lemma TLex2seq: "snd ex \<noteq> UU \<Longrightarrow> snd ex \<noteq> nil \<Longrightarrow> \<exists>ex'. TL\<cdot>(ex2seq ex) = ex2seq ex'" 371 apply (pair ex) 372 apply (Seq_case_simp x2) 373 apply (pair a) 374 apply auto 375 done 376 377lemma ex2seqnilTL: "TL \<cdot> (ex2seq ex) \<noteq> nil \<longleftrightarrow> snd ex \<noteq> nil \<and> snd ex \<noteq> UU" 378 apply (pair ex) 379 apply (Seq_case_simp x2) 380 apply (pair a) 381 apply (Seq_case_simp s) 382 apply (pair a) 383 done 384 385lemma strength_Next: "temp_strengthening P Q h \<Longrightarrow> temp_strengthening (\<circle>P) (\<circle>Q) h" 386 apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Next_def) 387 apply simp 388 apply auto 389 apply (simp add: TL_ex2seq_nil TL_ex2seq_UU) 390 apply (simp add: TL_ex2seq_nil TL_ex2seq_UU) 391 apply (simp add: TL_ex2seq_nil TL_ex2seq_UU) 392 apply (simp add: TL_ex2seq_nil TL_ex2seq_UU) 393 text \<open>cons case\<close> 394 apply (simp add: TL_ex2seq_nil TL_ex2seq_UU ex2seq_abs_cex cex_absSeq_TL [symmetric] ex2seqnilTL) 395 apply (erule conjE) 396 apply (drule TLex2seq) 397 apply assumption 398 apply auto 399 done 400 401 402text \<open>Localizing Temporal Weakenings - 2\<close> 403 404lemma weak_Init: "state_weakening P Q h \<Longrightarrow> temp_weakening (Init P) (Init Q) h" 405 apply (simp add: temp_weakening_def2 state_weakening_def2 406 temp_sat_def satisfies_def Init_def unlift_def) 407 apply auto 408 apply (pair ex) 409 apply (Seq_case_simp x2) 410 apply (pair a) 411 done 412 413 414text \<open>Localizing Temproal Strengthenings - 3\<close> 415 416lemma strength_Diamond: "temp_strengthening P Q h \<Longrightarrow> temp_strengthening (\<diamond>P) (\<diamond>Q) h" 417 apply (unfold Diamond_def) 418 apply (rule strength_NOT) 419 apply (rule weak_Box) 420 apply (erule weak_NOT) 421 done 422 423lemma strength_Leadsto: 424 "temp_weakening P1 P2 h \<Longrightarrow> temp_strengthening Q1 Q2 h \<Longrightarrow> 425 temp_strengthening (P1 \<leadsto> Q1) (P2 \<leadsto> Q2) h" 426 apply (unfold Leadsto_def) 427 apply (rule strength_Box) 428 apply (erule strength_IMPLIES) 429 apply (erule strength_Diamond) 430 done 431 432 433text \<open>Localizing Temporal Weakenings - 3\<close> 434 435lemma weak_Diamond: "temp_weakening P Q h \<Longrightarrow> temp_weakening (\<diamond>P) (\<diamond>Q) h" 436 apply (unfold Diamond_def) 437 apply (rule weak_NOT) 438 apply (rule strength_Box) 439 apply (erule strength_NOT) 440 done 441 442lemma weak_Leadsto: 443 "temp_strengthening P1 P2 h \<Longrightarrow> temp_weakening Q1 Q2 h \<Longrightarrow> 444 temp_weakening (P1 \<leadsto> Q1) (P2 \<leadsto> Q2) h" 445 apply (unfold Leadsto_def) 446 apply (rule weak_Box) 447 apply (erule weak_IMPLIES) 448 apply (erule weak_Diamond) 449 done 450 451lemma weak_WF: 452 "(\<And>s. Enabled A acts (h s) \<Longrightarrow> Enabled C acts s) 453 \<Longrightarrow> temp_weakening (WF A acts) (WF C acts) h" 454 apply (unfold WF_def) 455 apply (rule weak_IMPLIES) 456 apply (rule strength_Diamond) 457 apply (rule strength_Box) 458 apply (rule strength_Init) 459 apply (rule_tac [2] weak_Box) 460 apply (rule_tac [2] weak_Diamond) 461 apply (rule_tac [2] weak_Init) 462 apply (auto simp add: state_weakening_def state_strengthening_def 463 xt2_def plift_def option_lift_def NOT_def) 464 done 465 466lemma weak_SF: 467 "(\<And>s. Enabled A acts (h s) \<Longrightarrow> Enabled C acts s) 468 \<Longrightarrow> temp_weakening (SF A acts) (SF C acts) h" 469 apply (unfold SF_def) 470 apply (rule weak_IMPLIES) 471 apply (rule strength_Box) 472 apply (rule strength_Diamond) 473 apply (rule strength_Init) 474 apply (rule_tac [2] weak_Box) 475 apply (rule_tac [2] weak_Diamond) 476 apply (rule_tac [2] weak_Init) 477 apply (auto simp add: state_weakening_def state_strengthening_def 478 xt2_def plift_def option_lift_def NOT_def) 479 done 480 481 482lemmas weak_strength_lemmas = 483 weak_OR weak_AND weak_NOT weak_IMPLIES weak_Box weak_Next weak_Init 484 weak_Diamond weak_Leadsto strength_OR strength_AND strength_NOT 485 strength_IMPLIES strength_Box strength_Next strength_Init 486 strength_Diamond strength_Leadsto weak_WF weak_SF 487 488ML \<open> 489fun abstraction_tac ctxt = 490 SELECT_GOAL (auto_tac 491 (ctxt addSIs @{thms weak_strength_lemmas} 492 addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}])) 493\<close> 494 495method_setup abstraction = \<open>Scan.succeed (SIMPLE_METHOD' o abstraction_tac)\<close> 496 497end 498