(* Title: HOL/IOA/Solve.thy ID: $Id: Solve.thy,v 1.3 2005/09/06 17:03:39 wenzelm Exp $ Author: Tobias Nipkow & Konrad Slind Copyright 1994 TU Muenchen *) header {* Weak possibilities mapping (abstraction) *} theory Solve imports IOA begin constdefs is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool" "is_weak_pmap f C A == (!s:starts_of(C). f(s):starts_of(A)) & (!s t a. reachable C s & (s,a,t):trans_of(C) --> (if a:externals(asig_of(C)) then (f(s),a,f(t)):trans_of(A) else f(s)=f(t)))" ML {* use_legacy_bindings (the_context ()) *} end
theorem trace_inclusion:
[| IOA C; IOA A; externals (asig_of C) = externals (asig_of A); is_weak_pmap f C A |] ==> traces C ⊆ traces A
theorem comp1_reachable:
reachable (C1.0 || C2.0) s ==> reachable C1.0 (fst s)
theorem comp2_reachable:
reachable (C1.0 || C2.0) s ==> reachable C2.0 (snd s)
theorem fxg_is_weak_pmap_of_product_IOA:
[| is_weak_pmap f C1.0 A1.0; externals (asig_of A1.0) = externals (asig_of C1.0); is_weak_pmap g C2.0 A2.0; externals (asig_of A2.0) = externals (asig_of C2.0); compat_ioas C1.0 C2.0; compat_ioas A1.0 A2.0 |] ==> is_weak_pmap (%p. (f (fst p), g (snd p))) (C1.0 || C2.0) (A1.0 || A2.0)
theorem reachable_rename_ioa:
reachable (rename C g) s ==> reachable C s
theorem rename_through_pmap:
is_weak_pmap f C A ==> is_weak_pmap f (rename C g) (rename A g)