392 by (ALLGOALS (simp_tac (red_ss addsimps ext_ss @ compat_ss))); |
392 by (ALLGOALS (simp_tac (red_ss addsimps ext_ss @ compat_ss))); |
393 |
393 |
394 qed "system_refinement"; |
394 qed "system_refinement"; |
395 |
395 |
396 |
396 |
397 |
|
398 (************************************************************************ |
|
399 I n t e r a c t i v e A b s t r a c t i o n |
|
400 *************************************************************************) |
|
401 |
|
402 goal Correctness.thy |
|
403 "ioa_implements system_ioa system_fin_ioa"; |
|
404 |
|
405 (* ------------------- Rewriting ----------------------------*) |
|
406 by (simp_tac (impl_ss addsimps [ioa_implements_def]) 1); |
|
407 by (rtac conjI 1); |
|
408 by (simp_tac (sys_ss addsimps ext_ss) 1); |
|
409 |
|
410 (* ------------------- Lemmata ------------------------------*) |
|
411 by (rtac trace_inclusion 1); |
|
412 by (rtac system_refinement 4); |
|
413 |
|
414 (* -------------------- Rewriting ---------------------------*) |
|
415 by (ALLGOALS (simp_tac impl_ss)); |
|
416 by (simp_tac (sys_ss addsimps ext_ss) 1); |
|
417 |
|
418 qed"interactive_abstraction"; |
|
419 |
|
420 |
|
421 |
|
422 |
|
423 |
|
424 (*********************************************************************** |
|
425 Illustrative ISABELLE Examples |
|
426 ************************************************************************) |
|
427 |
|
428 (*** Cantor's Theorem: There is no surjection from a set to its powerset. ***) |
|
429 |
|
430 goal Set.thy |
|
431 "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)"; |
|
432 |
|
433 by (best_tac (set_cs addSEs [equalityCE]) 1); |
|
434 qed "cantor1"; |
|
435 |
|
436 (***** Theorem 2 *) |
|
437 val prems = goalw Lfp.thy [image_def] "inj(f) ==> Inv(f)``(f``X) = X"; |
|
438 by (cut_facts_tac prems 1); |
|
439 by (rtac equalityI 1); |
|
440 by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1); |
|
441 by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1); |
|
442 qed "inv_image_comp"; |
|