src/HOL/IOA/Asig.thy
changeset 62145 5b946c81dfbf
parent 58889 5b7a9633cfa8
child 63167 0909deb8059b
     1.1 --- a/src/HOL/IOA/Asig.thy	Mon Jan 11 21:20:44 2016 +0100
     1.2 +++ b/src/HOL/IOA/Asig.thy	Mon Jan 11 21:21:02 2016 +0100
     1.3 @@ -9,41 +9,31 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -type_synonym
     1.8 -  'a signature = "('a set * 'a set * 'a set)"
     1.9 +type_synonym 'a signature = "('a set * 'a set * 'a set)"
    1.10 +
    1.11 +definition "inputs" :: "'action signature => 'action set"
    1.12 +  where asig_inputs_def: "inputs == fst"
    1.13  
    1.14 -consts
    1.15 -  "actions" :: "'action signature => 'action set"
    1.16 -  "inputs" :: "'action signature => 'action set"
    1.17 -  "outputs" :: "'action signature => 'action set"
    1.18 -  "internals" :: "'action signature => 'action set"
    1.19 -  externals :: "'action signature => 'action set"
    1.20 +definition "outputs" :: "'action signature => 'action set"
    1.21 +  where asig_outputs_def: "outputs == (fst o snd)"
    1.22  
    1.23 -  is_asig       ::"'action signature => bool"
    1.24 -  mk_ext_asig   ::"'action signature => 'action signature"
    1.25 -
    1.26 -
    1.27 -defs
    1.28 +definition "internals" :: "'action signature => 'action set"
    1.29 +  where asig_internals_def: "internals == (snd o snd)"
    1.30  
    1.31 -asig_inputs_def:    "inputs == fst"
    1.32 -asig_outputs_def:   "outputs == (fst o snd)"
    1.33 -asig_internals_def: "internals == (snd o snd)"
    1.34 +definition "actions" :: "'action signature => 'action set"
    1.35 +  where actions_def: "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
    1.36  
    1.37 -actions_def:
    1.38 -   "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
    1.39 -
    1.40 -externals_def:
    1.41 -   "externals(asig) == (inputs(asig) Un outputs(asig))"
    1.42 +definition externals :: "'action signature => 'action set"
    1.43 +  where externals_def: "externals(asig) == (inputs(asig) Un outputs(asig))"
    1.44  
    1.45 -is_asig_def:
    1.46 -  "is_asig(triple) ==
    1.47 -      ((inputs(triple) Int outputs(triple) = {})    &
    1.48 -       (outputs(triple) Int internals(triple) = {}) &
    1.49 -       (inputs(triple) Int internals(triple) = {}))"
    1.50 +definition is_asig :: "'action signature => bool"
    1.51 +  where "is_asig(triple) ==
    1.52 +    ((inputs(triple) Int outputs(triple) = {})    &
    1.53 +     (outputs(triple) Int internals(triple) = {}) &
    1.54 +     (inputs(triple) Int internals(triple) = {}))"
    1.55  
    1.56 -
    1.57 -mk_ext_asig_def:
    1.58 -  "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
    1.59 +definition mk_ext_asig :: "'action signature => 'action signature"
    1.60 +  where "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
    1.61  
    1.62  
    1.63  lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def