theory Demo12 imports Main begin find_theorems (100) "_ + _ + _" find_theorems "ALL _. _" find_theorems "_ + _ + (_::nat)" find_theorems "_ + _ + _" name: assoc find_theorems simp: "hd _" find_theorems "[]" simp: "hd _" find_theorems simp: "_ * (_ + _)" lemma "A \ B \ B \ A" find_theorems intro find_theorems dest find_theorems elim find_theorems intro name: "HOL." -dest by blast -- -------------------------------------------------------------------------------------- -- "Syntax and State Space" types loc = string state = "loc \ nat" aexp = "state \ nat" bexp = "state \ bool" datatype com = SKIP | Assign loc 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" constdefs A :: loc "A \ ''A''" B :: loc "B \ ''B''" lemma [simp]: "A \ B" by (simp add: A_def B_def) lemma [simp]: "B \ A" by (simp add: A_def B_def) constdefs factorial :: com "factorial \ B :== (\\. 1);; WHILE (\\. \ A \ 0) DO B :== (\\. \ B * \ A);; A :== (\\. \ A - 1) OD" -- "Execution" inductive eval :: "com \ state \ state \ bool" ("\_,_\/ \ _" [0,0,60] 61) where Skip [intro!,simp]: "\SKIP, \\ \ \" | Assign [intro!,simp]: "\x :== a, \\ \ \ (x := a \)" | Semi [intro!]: "\ \c\<^isub>1,\\ \ \''; \c\<^isub>2,\''\ \ \' \ \ \c\<^isub>1;; c\<^isub>2, \\ \ \'" | IfTrue: "\ b \; \c\<^isub>1,\\ \ \' \ \ \IF b THEN c\<^isub>1 ELSE c\<^isub>2, \\ \ \'" | IfFalse: "\ \b \; \c\<^isub>2,\\ \ \' \ \ \IF b THEN c\<^isub>1 ELSE c\<^isub>2, \\ \ \'" | WhileFalse: "\b \ \ \WHILE b DO c OD, \\ \ \" | WhileTrue: "\b \; \c,\\ \ \''; \WHILE b DO c OD, \''\ \ \'\ \ \WHILE b DO c OD, \\ \ \'" print_theorems inductive_cases skip [elim!]: "\SKIP, \\ \ \'" and assign [elim!]: "\x :== a, \\ \ \'" and semi [elim!]: "\c\<^isub>1;; c\<^isub>2, \\ \ \'" and "if" [elim!]: "\IF b THEN c\<^isub>1 ELSE c\<^isub>2, \\ \ \'" and while: "\WHILE b DO c OD, \\ \ \'" thm skip assign semi "if" while lemma skip_eq [simp]: "\SKIP, \\ \ \' = (\' = \)" by blast lemma assign_eq [simp]: "\x :== a, \\ \ \' = (\' = \ (x := a \))" by blast -- --------------------------------------------------------------------- -- "Example Proof" consts fac :: "nat \ nat" primrec "fac 0 = 1" "fac (Suc n) = (Suc n) * fac n" lemma factorial_helper: "\c,\\ \ \' \ (c = WHILE \\. 0 < \ A DO B :== (\\. \ B * \ A) ;; A :== (\\. \ A - Suc 0) OD) \ \' B = (\ B) * fac (\ A)" apply (erule eval.induct) apply simp_all apply clarsimp apply clarsimp apply (erule notE) apply (case_tac "\ A") apply simp apply simp done lemma factorial_partial_correct: "\factorial, \\ \ \' \ \' B = fac (\ A)" apply (unfold factorial_def) apply clarsimp apply (drule factorial_helper) apply simp done -- --------------------------------------------------------------------- term "x \ y" inductive foo :: "nat => bool" where "foo (Suc x)" lemma "foo x ==> x \ 0" apply (erule foo.induct) apply simp done types assn = "state => bool" constdefs hoare_valid :: "assn \ com \ assn \ bool" ("\ {(1_)}/ (_)/ {(1_)}" 50) "\ {P} c {Q} \ \\ \'. P \ \ \c,\\ \ \' \ Q \'" inductive hoare :: "assn \ com \ assn \ bool" ("\ ({(1_)}/ (_)/ {(1_)})" 50) where h_skip: "\ {P} SKIP {P}" | h_assign: "\ {\\. P (\(x:= a \))} x:==a {P}" | h_semi: "\ \ {P} c\<^isub>1 {R}; \ {R} c\<^isub>2 {Q} \ \ \ {P} c\<^isub>1;;c\<^isub>2 {Q}" | h_if: "\ \ {\\. P \ \ b \} c\<^isub>1 {Q}; \ {\\. P \ \ \b \} c\<^isub>2 {Q} \ \ \ {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" | h_while: "\ \ {\\. P \ \ b \} c {P}; \\. P \ \ \b \ \ Q \ \ \ \ {P} WHILE b DO c OD {Q}" | conseq: "\ \\. P \ \ P' \; \ {P'} c {Q'}; \\. Q' \ \ Q \ \ \ \ {P} c {Q}" -- "Soundness Proof" lemma invariant: assumes inv: "\\ \'. P \ \ b \ \ \c,\\ \ \' \ P \'" shows "\ \WHILE b DO c OD,\\ \ \'; P \ \ \ P \' \ \b \'" proof - { fix w assume "\w,\\ \ \'" hence "w = WHILE b DO c OD \ P \ \ P \' \ \b \'" proof induct case (WhileTrue b' \ c' \'' \') { assume "b = b'" and "c' = c" with WhileTrue have ?case by simp (insert inv, blast) } thus ?case by auto qed auto } thus "\ \WHILE b DO c OD,\\ \ \'; P \ \ \ P \' \ \b \'" by blast qed theorem hoare_sound: assumes deriv: "\ {P} c {Q}" shows "\ {P} c {Q}" using deriv proof induct fix P show "\ {P} SKIP {P}" by (simp add: hoare_valid_def) next fix P x a have "\\ \'. P (\(x := a \)) \ \x :== a, \\ \ \' \ P \'" by simp thus "\ { \\. P (\(x := a \)) } x :== a {P}" by (unfold hoare_valid_def) next fix P c\<^isub>1 c\<^isub>2 Q R assume "\ {P} c\<^isub>1 {R}" hence "\\ \'. P \ \ \c\<^isub>1, \\ \ \' \ R \'" by (unfold hoare_valid_def) moreover assume "\ {R} c\<^isub>2 {Q}" hence "\\ \'. R \ \ \c\<^isub>2, \\ \ \' \ Q \'" by (unfold hoare_valid_def) ultimately have "\\ \'. P \ \ \c\<^isub>1;;c\<^isub>2, \\ \ \' \ Q \'" by blast thus "\ {P} c\<^isub>1;; c\<^isub>2 {Q}" by (unfold hoare_valid_def) next case (h_if P b c\<^isub>1 Q c\<^isub>2) thus ?case by (unfold hoare_valid_def) (blast elim: "if") next fix P b c Q assume "\ {\\. P \ \ b \} c {P}" hence "\\ \'. P \ \ b \ \ \c,\\ \ \' \ P \'" by (unfold hoare_valid_def) hence "\\ \'. \ \WHILE b DO c OD,\\ \ \'; P \ \ \ P \' \ \b \'" by (rule invariant) moreover assume "\\. P \ \ \ b \ \ Q \" ultimately show "\ {P} WHILE b DO c OD {Q}" by (unfold hoare_valid_def) blast next case (conseq P P' c Q' Q) thus ?case by (unfold hoare_valid_def) blast qed -- -------------------------------------------------------------------------------------- -- "derived rules" lemma h_ass: "(\\. P \ \ Q (\(x := a \))) \ \ {P} x :== a {Q}" apply (rule conseq) prefer 2 apply (rule h_assign) prefer 2 apply clarify apply assumption apply blast done -- "example proof" lemma "\ {\\. True} x :== (\\. 2) {\\. \ x = 2}" apply (rule h_ass) apply simp done lemma "\ {\\. \ A = n} factorial {\\. \ B = fac n}" apply (unfold factorial_def) apply (rule h_semi) prefer 2 apply (rule_tac P="\\. fac n = (\ B) * fac (\ A)" in h_while) apply (rule h_semi) prefer 2 apply (rule h_assign) apply (rule h_ass) apply clarsimp apply (erule notE) apply (case_tac "\ A") apply simp apply simp apply clarsimp apply (rule h_ass) apply simp done end