theory week08A_sol imports Main begin -- "Syntax and State Space" type_synonym vname = string type_synonym state = "vname \ nat" type_synonym aexp = "state \ nat" type_synonym bexp = "state \ bool" datatype com = SKIP | Assign vname aexp ("_ :== _ " [60,60] 60) | Semi com com ("_;; _" [50, 51] 50) | Cond bexp com com ("IF _ THEN _ ELSE _" [0,0,59] 60) | While bexp com ("WHILE _ DO _ OD" [0,45] 60) -- "Example Program" definition A :: vname where "A \ ''A''" definition B :: vname where "B \ ''B''" lemma [simp]: "A \ B" by (simp add: A_def B_def) lemma [simp]: "B \ A" by (simp add: A_def B_def) definition factorial :: com where "factorial \ B :== (\s. 1);; WHILE (\s. s A \ 0) DO B :== (\s. s B * s A);; A :== (\s. s A - 1) OD" -- "Execution" inductive eval :: "com \ state \ state \ bool" ("_/ \ _" [60,60] 61) where Skip [intro!,simp]: "(SKIP, s) \ s" | Assign [intro!,simp]: "(x :== a, s) \ s (x := a s)" | Semi [intro!]: "\ (c\<^sub>1,s) \ s''; (c\<^sub>2,s'') \ s' \ \ (c\<^sub>1;; c\<^sub>2, s) \ s'" | IfTrue: "\ b s; (c\<^sub>1,s) \ s' \ \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \ s'" | IfFalse: "\ \b s; (c\<^sub>2,s) \ s' \ \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \ s'" | WhileFalse: "\b s \ (WHILE b DO c OD, s) \ s" | WhileTrue: "\b s; (c,s) \ s''; (WHILE b DO c OD, s'') \ s'\ \ (WHILE b DO c OD, s) \ s'" (* Isabelle provides eval.induct which allows the elimination of terms cs \ t. In practice, we will have cs as a tuple (c,s). To avoid to manually have to split cs every time, we can use split_format as below to define an induction rule that will work on terms of the form (c, s) \ t.*) thm eval.induct lemmas eval_induct = eval.induct [split_format (complete)] thm eval_induct (* In practice, it is also useful to have elimination rules for precisely when e.g. c=SKIP, or c= c1;;c2, etc. (If c=SKIP, eval_induct has many useless cases). The command inductive_cases allows exactly this.*) inductive_cases skip [elim!]: "(SKIP, s) \ s'" and assign [elim!]: "(x :== a, s) \ s'" and semi [elim!]: "(c\<^sub>1;; c\<^sub>2, s) \ s'" and "if" [elim!]: "(IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \ s'" and while: "(WHILE b DO c OD, s) \ s'" thm skip assign semi "if" while lemma skip_eq [simp]: "(SKIP, s) \ s' = (s' = s)" by blast lemma assign_eq [simp]: "(x :== a, s) \ s' = (s' = s (x := a s))" by blast -- --------------------------------------------------------------------- -- "Example Proof" primrec fac :: "nat \ nat" where "fac 0 = 1" |"fac (Suc n) = (Suc n) * fac n" (* Need to relate the final state of B to values of A and B *at each iteration* of the loop *) lemma factorial_partial_correct_helper: "(prog, s) \ s' \ prog = WHILE \s. 0 < s A DO B :== (\s. s B * s A) ;; A :== (\s. s A - Suc 0) OD \ s' B = s B * fac (s A)" apply(induct rule: eval_induct) apply(simp_all) apply (case_tac "s A") apply(simp) apply clarsimp (*sledgehammer*) by (simp add: distrib_left distrib_right) lemma factorial_partial_correct: "(factorial, s) \ s' \ s' B = fac (s A)" apply (unfold factorial_def) apply clarsimp apply (clarsimp simp: factorial_partial_correct_helper) done -- --------------------------------------------------------------------- type_synonym assn = "state => bool" definition hoare_valid :: "assn \ com \ assn \ bool" ("\ {(1_)}/ (_)/ {(1_)}" 50) where "\ {P} c {Q} \ \s s'. P s \ (c,s) \ s' \ Q s'" inductive hoare :: "assn \ com \ assn \ bool" ("\ ({(1_)}/ (_)/ {(1_)})" 50) where h_skip: "\ {P} SKIP {P}" | h_assign: "\ {\s. P (s(x:= a s))} x:==a {P}" | h_semi: "\ \ {P} c\<^sub>1 {R}; \ {R} c\<^sub>2 {Q} \ \ \ {P} c\<^sub>1;;c\<^sub>2 {Q}" | h_if: "\ \ {\s. P s \ b s} c\<^sub>1 {Q}; \ {\s. P s \ \b s} c\<^sub>2 {Q} \ \ \ {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" | h_while: "\ \ {\s. P s \ b s} c {P}; \s. P s \ \b s \ Q s \ \ \ {P} WHILE b DO c OD {Q}" | conseq: "\ \s. P s \ P' s; \ {P'} c {Q'}; \s. Q' s \ Q s \ \ \ {P} c {Q}" -- "Soundness Proof" lemma skip_sound: "\ {P} SKIP {P}" by(simp add: hoare_valid_def) lemma assign_sound: "\ {\b. P (b(x := a b))} x :== a {P}" by(simp add: hoare_valid_def) lemma semi_sound: " \\ {P} c\<^sub>1 {R}; \ {R} c\<^sub>2 {Q}\ \ \ {P} c\<^sub>1;; c\<^sub>2 {Q}" apply(clarsimp simp: hoare_valid_def) by blast lemma if_sound: "\\ {\a. P a \ b a} c\<^sub>1 {Q}; \ {\a. P a \ \ b a} c\<^sub>2 {Q}\ \ \ {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" apply(clarsimp simp: hoare_valid_def) by blast (* When a while loop is fully executed to a state s', then the loop condition is false in s' (otherwise there would have been another iteration). Moreover, if the loop satisfies an invariant P, then P is true when the loop exits. *) lemma while_final: "\(prog, s) \ s'; \s. P s \ b s \ (\s'. (c, s) \ s' \ P s'); P s; prog = WHILE b DO c OD\ \ P s' \ \ b s'" apply(induct rule: eval_induct) apply(simp_all) done (* To show that a postcondition Q holds after a While loop, we need to find a predicate P that is an invariant of the loop (i.e. preserved by the loop body at each iteration) and is "enough" to prove the postcondition when the proof exits.*) lemma while_sound: "\\ {\a. P a \ b a} c {P}; \s. P s \ \ b s \ Q s\ \ \ {P} WHILE b DO c OD {Q}" apply(clarsimp simp: hoare_valid_def) apply(subgoal_tac "P s' \ \ b s'") apply blast apply(rule while_final) apply(simp_all) done lemma conseq_sound: "\\s. P s \ P' s; \ {P'} c {Q'}; \s. Q' s \ Q s\ \ \ {P} c {Q}" apply(simp add: hoare_valid_def) by blast theorem hoare_sound: "\ {P} c {Q} \ \ {P} c {Q}" apply(induct rule: hoare.induct) by(auto intro: skip_sound assign_sound semi_sound if_sound while_sound conseq_sound) (*OR*) theorem hoare_sound2: "\ {P} c {Q} \ \ {P} c {Q}" apply (induct rule:hoare.induct) apply (clarsimp simp: hoare_valid_def) apply (clarsimp simp: hoare_valid_def) apply (clarsimp simp: hoare_valid_def, blast) apply (clarsimp simp: hoare_valid_def, blast) defer apply (clarsimp simp: hoare_valid_def, blast) apply (rule while_sound, assumption, assumption) done -- -------------------------------------------------------------------------------------- -- "derived rules" lemma h_ass: "(\s. P s \ Q (s(x := a s))) \ \ {P} x :== a {Q}" apply(rule_tac Q'=Q in conseq) prefer 2 apply(rule h_assign) apply(blast)+ done -- "example proof" lemma "\ {\s. True} x :== (\s. 2) {\s. s x = 2}" apply(rule h_ass) apply simp done lemma "\ {\s. s A = n} factorial {\s. s B = fac n}" apply(unfold factorial_def) apply(rule h_semi) prefer 2 apply(rule_tac P="\s. s B * fac (s A) = fac n" in h_while) apply(rule h_semi) prefer 2 apply(rule h_assign) apply(rule h_ass) apply clarsimp apply(case_tac "s A", simp) apply clarsimp apply (simp add: add_mult_distrib2 comm_semiring_class.distrib) apply clarsimp apply(rule h_ass) apply clarsimp done end