Theory System

(*  Title:      NI/System.thy
    Id:         $Id: System.thy,v 1.6 2004/01/29 17:36:47 dvo Exp $
    Author:     David von Oheimb
    License:    (C) 2003 Siemens AG; any non-commercial use is granted

*)
header {* Automata *}

(*<*)
theory System = Main:
ML {* Pretty.setmargin 169; quick_and_dirty:=true *}

syntax (xsymbols)
  "op <->" :: "bool => bool => bool" (infixr "<->" 25)
translations
  "P <-> Q" \<rightharpoonup> "P = Q"
(*>*)

typedecl "state" 
typedecl "action"
typedecl "output"
typedecl "domain"

text {* System described as Moore (rather than Mealy) automaton *}

consts   step :: "action =>  state => state"
         Step :: "action => (state × state) set" --{* non-deterministic step *}
        "output" :: "domain => state => output set" --{* all observations of a domain *}
         run  :: "action list =>  state => state"
         Run  :: "action list => (state × state) set" --{* non-deterministic run *}

primrec "run []     = (λs. s)"
        "run (a#as) = run as ˆ step a" 
primrec "Run []     = Id"
        "Run (a#as) = Run as O Step a" 

consts s0 :: "state"

(*<*)
lemma foldl_init_func [rule_format]:
  "∀g. foldl (λf a u. h a (f u)) g as (h a x) = 
       foldl (λf a u. h a (f u)) (g o h a) as x"
by (rule induct, auto)

lemma "run = foldl (λf a. step a ˆ f) (λs. s)"
apply (rule ext)
apply (rule ext)
apply (rule_tac x = xa in spec)
apply (rule induct, auto simp add: foldl_init_func o_def)
done

lemma run_append [simp]: "run (as @ bs) = run bs ˆ run as"
by (induct "as", auto)

lemma Run_append [simp]: "Run (as @ bs) = Run bs O Run as"
by (induct "as", auto)

end
(*>*)