src/HOL/IMP/Collecting_Examples.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 52019 a4cbca8f7342
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
     1 theory Collecting_Examples
     2 imports Collecting Vars
     3 begin
     4 
     5 subsection "Pretty printing state sets"
     6 
     7 text{* Tweak code generation to work with sets of non-equality types: *}
     8 declare insert_code[code del] union_coset_filter[code del]
     9 lemma insert_code [code]:  "insert x (set xs) = set (x#xs)"
    10 by simp
    11 
    12 text{* Compensate for the fact that sets may now have duplicates: *}
    13 definition compact :: "'a set \<Rightarrow> 'a set" where
    14 "compact X = X"
    15 
    16 lemma [code]: "compact(set xs) = set(remdups xs)"
    17 by(simp add: compact_def)
    18 
    19 definition "vars_acom = compact o vars o strip"
    20 
    21 text{* In order to display commands annotated with state sets, states must be
    22 translated into a printable format as sets of variable-state pairs, for the
    23 variables in the command: *}
    24 
    25 definition show_acom :: "state set acom \<Rightarrow> (vname*val)set set acom" where
    26 "show_acom C =
    27    annotate (\<lambda>p. (\<lambda>s. (\<lambda>x. (x, s x)) ` (vars_acom C)) ` anno C p) (strip C)"
    28 
    29 
    30 subsection "Examples"
    31 
    32 definition "c0 = WHILE Less (V ''x'') (N 3)
    33                 DO ''x'' ::= Plus (V ''x'') (N 2)"
    34 definition C0 :: "state set acom" where "C0 = annotate (%p. {}) c0"
    35 
    36 text{* Collecting semantics: *}
    37 
    38 value "show_acom (((step {<>}) ^^ 1) C0)"
    39 value "show_acom (((step {<>}) ^^ 2) C0)"
    40 value "show_acom (((step {<>}) ^^ 3) C0)"
    41 value "show_acom (((step {<>}) ^^ 4) C0)"
    42 value "show_acom (((step {<>}) ^^ 5) C0)"
    43 value "show_acom (((step {<>}) ^^ 6) C0)"
    44 value "show_acom (((step {<>}) ^^ 7) C0)"
    45 value "show_acom (((step {<>}) ^^ 8) C0)"
    46 
    47 text{* Small-step semantics: *}
    48 value "show_acom (((step {}) ^^ 0) (step {<>} C0))"
    49 value "show_acom (((step {}) ^^ 1) (step {<>} C0))"
    50 value "show_acom (((step {}) ^^ 2) (step {<>} C0))"
    51 value "show_acom (((step {}) ^^ 3) (step {<>} C0))"
    52 value "show_acom (((step {}) ^^ 4) (step {<>} C0))"
    53 value "show_acom (((step {}) ^^ 5) (step {<>} C0))"
    54 value "show_acom (((step {}) ^^ 6) (step {<>} C0))"
    55 value "show_acom (((step {}) ^^ 7) (step {<>} C0))"
    56 value "show_acom (((step {}) ^^ 8) (step {<>} C0))"
    57 
    58 end