src/HOL/IMP/Abs_Int_Tests.thy
changeset 46432 ce8f7944fd6b
parent 45623 f682f3f7b726
child 49095 7df19036392e
equal deleted inserted replaced
46431:26c2e053ab96 46432:ce8f7944fd6b
    50  ''x'' ::= N 7;
    50  ''x'' ::= N 7;
    51  WHILE Less (V ''x'') (N 100)
    51  WHILE Less (V ''x'') (N 100)
    52  DO ''x'' ::= Plus (V ''x'') (N 1)"
    52  DO ''x'' ::= Plus (V ''x'') (N 1)"
    53 
    53 
    54 definition "test4_ivl =
    54 definition "test4_ivl =
    55  ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
    55  ''x'' ::= N 0; ''y'' ::= N 0;
    56  WHILE Less (V ''x'') (N 11)
    56  WHILE Less (V ''x'') (N 11)
    57  DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
    57  DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N 1))"
    58 
    58 
    59 definition "test5_ivl =
    59 definition "test5_ivl =
    60  ''x'' ::= N 0; ''y'' ::= N 0;
    60  ''x'' ::= N 0; ''y'' ::= N 0;
    61  WHILE Less (V ''x'') (N 1000)
    61  WHILE Less (V ''x'') (N 1000)
    62  DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
    62  DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"