# Theory Solve

Up to index of Isabelle/HOL/IOA

theory Solve
imports IOA
uses [Solve.ML]
begin

    (*  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)