(*  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 imports Main begin
ML {* Pretty.setmargin 169; quick_and_dirty:=true *}

(*>*)
record "state" =
  HighData :: nat
  LowData :: nat

datatype "action" = INPUTHIGH nat | INPUTLOW nat | OUTPUTHIGH | OUTPUTLOW
types "output" = nat
datatype "domain" = H | L
(*
(* the original system had this: *)
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 \<times> state) set" --{* non-deterministic step *}
        "output" :: "domain => state => output set" --{* all observations of a domain *}
         run  :: "action list =>  state => state"
         Run  :: "action list => (state \<times> state) set" --{* non-deterministic run *}

primrec "run []     = (\<lambda>s. s)"
        "run (a#as) = run as \<circ> step a" 
primrec "Run []     = Id"
        "Run (a#as) = Run as O Step a" 

consts s0 :: "state"

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

lemma "run = foldl (\<lambda>f a. step a \<circ> f) (\<lambda>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 \<circ> run as"
by (induct "as", auto)

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

end
(*>*)