theory tut11 imports "~~/src/HOL/IMP/Hoare_Sound_Complete" begin term "V ''x''" term "V ''y''" definition "MAX \ IF Less (V ''x'') (V ''y'') THEN ''z'' ::= V ''y'' ELSE ''z'' ::= V ''x'' " lemma [simp]: "(a::int) max a b = b" by linarith lemma [simp]: "\(a::int) max a b = a" by linarith lemma "\ {\s. True} MAX {\s. s ''z'' = max (s ''x'') (s ''y'')}" unfolding MAX_def by (rule If Assign' | simp)+ definition "MUL \ ''z'' ::= N 0;; ''i'' ::= N 0;; WHILE Less (V ''i'') (V ''x'') DO ( ''z'' ::= Plus (V ''z'') (V ''y'');; ''i'' ::= Plus (V ''i'') (N 1) ) " thm While[where P = "\ s. True"] lemma "\ {\s. 0 \ s ''x''} MUL {\s. s ''z'' = s ''x'' * s ''y''}" unfolding MUL_def thm Seq Seq[rotated] apply (rule Seq[rotated]) thm While' apply (rule While'[where P = "\ s. s ''z'' = s ''y'' * s ''i'' \ s ''i'' \ s ''x''"]) apply (rule Seq[rotated]) apply (rule Assign) apply simp apply (rule Assign') apply (simp add: algebra_simps) apply (rule Seq[rotated] Assign Assign' | simp)+ done definition "MAX_wrong = (''a''::=N 0;;''b''::=N 0;;''c''::= N 0)" lemma "\ {\s. True} MAX_wrong {\s. s ''c'' = max (s ''a'') (s ''b'')}" unfolding MAX_wrong_def by (rule Seq[rotated] Assign Assign' | simp)+ lemma "\ {\s. a = s ''a'' \ b = s ''b''} MAX_wrong {\s. s ''c'' = max a b}" unfolding MAX_wrong_def by (rule Seq[rotated] Assign Assign' | simp)+ lemma "\ {\s. x = s ''x'' \ y = s ''y''} MAX {\s. s ''z'' = max x y}" unfolding MAX_def by (rule If Assign' | simp)+ term "\ {P} x::=a {\ s'. \ s. P s \ s' = s[a/x]}" lemma fwd_Assign: "\ {P} x::=a {\ s'. \ s. P s \ s' = s[a/x]}" apply (rule hoare_complete) unfolding hoare_valid_def by auto end