theory Ex09_Tut imports "HOL-IMP.Hoare_Sound_Complete" begin paragraph "Step 1" definition Max :: "com" where "Max = undefined" paragraph "Step 2" lemma max_right[simp]: "(a::int) max a b = b" sorry lemma max_left[simp]: "\(a::int) max a b = a" sorry lemma "\ {\s. True} Max {\s. s ''c'' = max (s ''a'') (s ''b'')}" sorry paragraph "Step 3" definition MUL :: "com" where "MUL = undefined" paragraph "Step 4" lemma "\ {\s. 0 \ s ''y''} MUL {\s. s ''z'' = s ''x'' * s ''y''}" sorry lemmas Seq_bwd = Seq[rotated] lemmas hoare_rule[intro?] = Seq_bwd Assign Assign' If paragraph "Step 5" 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'')}" sorry lemma "\ {\s. a=s ''a'' \ b=s ''b''} Max {\s. s ''c'' = max a b \ a = s ''a'' \ b = s ''b''}" sorry lemmas fwd_Assign' = weaken_post[OF fwd_Assign] lemma "\ {\s. True} Max {\s. s ''c'' = max (s ''a'') (s ''b'')}" sorry lemma "\ {\s. 0 \ s ''y''} MUL {\s. s ''z'' = s ''x'' * s ''y''}" sorry end