theory ex09 imports "HOL-IMP.Hoare_Sound_Complete" begin paragraph "Step 1" definition Max :: com where "None = undefined" paragraph "Step 2" lemma [simp]: "(a::int) max a b = b" sorry lemma [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 where "None = 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)" where "None = undefined" 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