theory ex15_examples imports VC Abs_Int1_parity Parity begin (* Exercise 15.1 *) definition "Q \ \ s. s ''a'' = 0 \ even (s ''x'')" definition "I \ \ s. s ''a'' \ 0 \ (\ i. i \ 0 \ s ''a'' = s ''x'' - 2 * i)" abbreviation "Sannot \ ''x'' ::= V ''a'' ; {I} WHILE Less (N 1) (V ''a'') DO ''a'' ::= Plus (V ''a'') (N (-2))" lemma "pre Sannot Q = blah" (* see the predicate in terms of I: *) apply simp (* it amounts to: *) unfolding I_def apply simp oops lemma "\ s. vc Sannot Q s" (* see the predicate in terms of I and Q: *)unfolding vc.simps apply simp unfolding I_def Q_def by auto arith (* Exercise 15.2 *) definition "test_parity = ''r'' ::= N 11; ''a'' ::= Plus (N 11) (N 11); WHILE Less (N 1) (V ''a'') DO ( ''r'' ::= Plus (V ''r'') (N 1); ''a'' ::= Plus (V ''a'') (N (-2)) ); ''r'' ::= Plus (V ''a'') (N 1)" term step_parity value "show_acom (steps test_parity 0)" value "show_acom (steps test_parity 1)" value "show_acom (steps test_parity 2)" value "show_acom (steps test_parity 3)" value "show_acom (steps test_parity 4)" value "show_acom (steps test_parity 5)" value "show_acom (steps test_parity 6)" value "show_acom (steps test_parity 7)" value "show_acom (steps test_parity 8)" value "show_acom (steps test_parity 9)" value "show_acom (steps test_parity 10)" value "show_acom (steps test_parity 11)" value "show_acom (the(AI_parity test_parity))" end