theory WhileLang imports Main begin datatype var = V nat (".v_" 90) datatype iexp = Var var | Const int | Plus iexp iexp | Mult iexp iexp datatype bexp = Le iexp iexp ("_ .\. _" [80, 80] 10) datatype com = SKIP | Asgn var iexp ("_::= _" [80, 80] 10) | Semi com com ("_; _" [70, 60] 10) | Cond bexp com com ("IF _ THEN _ ELSE _" 60) | While bexp com ("WHILE _ DO _" 60) type_synonym state = "var \ int" fun ieval :: "state \ iexp \ int" where "ieval s (Var v) = (s v)" | "ieval s (Const i) = i" | "ieval s (Plus li ri) = (ieval s li) + (ieval s ri)" | "ieval s (Mult li ri) = (ieval s li) * (ieval s ri)" fun beval :: "state \ bexp \ bool" where "beval s (Le li ri) = ((ieval s li) \ (ieval s ri))" inductive exec :: "state \ com \ state \ bool" ("_/ -_\/ _" [50,0,50] 50) where Skip: "s -SKIP\ s" | Asgn: "s -x::=e\ s(x:= ieval s e)" | Semi: "\ s0 -c1\ s1; s1 -c2\ s2 \ \ s0 -c1;c2\ s2" | IfT: "\ (beval s b); s -c1\ t \ \ s -IF b THEN c1 ELSE c2\ t" | IfF: "\ \(beval s b); s -c2\ t \ \ s -IF b THEN c1 ELSE c2\ t" | WhileF: "\(beval s b) \ s -WHILE b DO c\ s" | WhileT: "\ (beval s b); s -c\ t; t -WHILE b DO c\ u \ \ s -WHILE b DO c\ u" lemma [iff]: "(s -SKIP\ t) = (s=t)" by(best elim: exec.cases intro:exec.intros) lemma [iff]: "(s -x::=e\ t) = (s(x:= ieval s e)=t)" by(best elim: exec.cases intro:exec.intros) lemma semic_eqv: "(s -c;d\ u) = (\t. s -c\ t \ t -d\ u)" by(best elim: exec.cases intro:exec.intros) lemma [iff]: "(s -IF b THEN c ELSE d\ t) = (s -if (beval s b) then c else d\ t)" apply auto apply(blast elim: exec.cases intro:exec.intros) apply(blast elim: exec.cases intro:exec.intros) apply(blast elim: exec.cases intro:exec.intros) apply(blast elim: exec.cases intro:exec.intros) done (*apply(blast elim: exec.cases intro:exec.intros)+ *) lemma unfold_while: "(s -WHILE b DO c\ u) = (s -IF b THEN c;WHILE b DO c ELSE SKIP \ u)" by(auto elim: exec.cases intro:exec.intros split:split_if_asm) lemma while_lemma[rule_format]: "s -w\ t \ \b c. w = (WHILE b DO c) \ P s \ (\s s'. P s \ (beval s b) \ s -c\ s' \ P s') \ P t \ \(beval t b)" apply(erule exec.induct) apply clarify+ apply(subgoal_tac "P t") apply blast+ done lemma while_rule: "\s -WHILE b DO c\ t; P s; \s s'. P s \ (beval s b) \ s -c\ s' \ P s'\ \ P t \ \(beval t b)" apply(drule while_lemma) prefer 2 apply assumption apply blast done lemma hoare_skip: "\s t. P s \ s -SKIP\ t \ P t" by( blast ) lemma hoare_assign [rule_format]: "\s t. P (s(x:= ieval s e)) \ s -x::=e\ t \ P t" by( blast ) lemma hoare_semic [rule_format]: "\ \s t. P s \ s -c1\ t \ Q t; \s t. Q s \ s -c2\ t \ R t \ \ \s t. P s \ s -c1;c2\ t \ R t" apply (simp add: semic_eqv) apply blast done lemma hoare_cond [rule_format]: "\ \s t. (beval s b) \ P s \ s -c1\ t \ Q t; \s t. \(beval s b) \ P s \ s -c2\ t \ Q t \ \ \s t. P s \ s -IF b THEN c1 ELSE c2\ t \ Q t" apply clarify apply (auto elim: exec.cases intro:exec.intros split:split_if_asm) done lemma my_conj_commute: "A \ B \ B \ A" by blast lemma hoare_while [rule_format]: "\ \s t. (beval s b) \ INV s \ s -c\ t \ INV t \ \ \s t. INV s \ s -WHILE b DO c\ t \ \(beval t b) \ INV t" apply clarify apply (rule my_conj_commute) apply (rule while_rule) by(blast)+ (* The considered program with specification: {x >= 0} c = 0 s = 1 while( sq <= x ) c = c +1 sq = sq + (2*c+1) } { c*c <= x & x < (c+1)*(c+1) } *) definition x :: "var" where "x == .v0" definition c :: "var" where "c == .v1" definition sq :: "var" where "sq == .v2" definition a1 :: "com" where "a1 == (c ::= (Const 0))" definition a2 :: "com" where "a2 == (sq ::= (Const 1))" definition a3 :: "com" where "a3 == (c ::= (Plus (Var c)) (Const 1))" definition a4 :: "com" where "a4 == (sq ::= Plus (Var sq) (Plus (Mult (Const 2) (Var c))(Const 1)))" definition wb :: "com" where "wb == (a3 ; a4)" definition w :: "com" where "w == (WHILE ( (Var sq).\. (Var x) ) DO wb)" definition c1 :: "com" where "c1 == (a2 ; w)" definition c0 :: "com" where "c0 == (a1 ; c1)" definition myProg :: "com" where "myProg == (c ::= (Const 0)) ; ((sq ::= (Const 1)) ; (WHILE ( Le (Var sq) (Var x) ) DO ( (c ::= (Plus (Var c) (Const 1))) ; (sq ::= Plus (Var sq) (Plus (Mult (Const 2) (Var c))(Const 1))) ) ) )" lemmas var_def = x_def c_def sq_def lemma [iff]: "myProg == c0" apply (simp add: myProg_def a1_def a2_def a3_def a4_def wb_def w_def c1_def c0_def) done lemma a1Prop [rule_format]: "\s t. 0 \ (s x) \ (s -a1\ t) \ (t c)*(t c) \ (t x) \ 1 = ((t c)+1)*((t c)+1)" by (simp add: a1_def) lemma a2Prop [rule_format]: "\s t. ((s c)*(s c) \ (s x) \ 1 = ((s c)+1)*((s c)+1)) \ (s -a2\ t) \ (t c)*(t c) \ (t x) \ (t sq) = ((t c)+1)*((t c)+1)" apply (simp add: a2_def var_def) done lemma a3Prop [rule_format]: "\s t. (((s sq) \ (s x) \ (s c)*(s c) \ (s x)) \ (s sq) = ((s c)+1)*((s c)+1)) \ (s -a3\ t) \ (t c)*(t c) \ (t x) \ (t sq) = (t c)*(t c)" apply (simp add: a3_def var_def) done lemma a4Prop [rule_format]: "\s t. ((s c)*(s c) \ (s x) \ (s sq)+(2*(s c)+1) = ((s c)+1)*((s c)+1)) \ (s -a4\ t) \ (t c)*(t c) \ (t x) \ (t sq) = ((t c)+1)*((t c)+1)" apply (simp add: a4_def var_def) done thm add thm mult lemma binom1: "((i::int)+1)*(i+1) = i*i + 2*i + 1" apply (simp add: add mult ring_distribs) done lemma a4WeakProp [rule_format]: "\s t. ((s c)*(s c) \ (s x) \ (s sq) = (s c)*(s c)) \ (s -a4\ t) \ (t c)*(t c) \ (t x) \ (t sq) = ((t c)+1)*((t c)+1)" apply clarify apply (rule a4Prop) apply auto apply (insert binom1) apply simp done lemma wbProp [rule_format]: "\s t. (s sq) \ (s x) \ ((s c)*(s c) \ (s x) \ ((s sq) = ((s c)+1)*((s c)+1) \ (s -wb\ t))) \ (t c)*(t c) \ (t x) \ (t sq) = ((t c)+1)*((t c)+1)" apply (simp (no_asm) add: wb_def ) apply clarify thm hoare_semic apply (rule_tac ?P="%s.((s sq) \ (s x) \ (s c)*(s c) \ (s x)) \ (s sq) = ((s c)+1)*((s c)+1)" and ?c1.0="a3" and ?c2.0="a4" and ?Q="%t.(t c)*(t c) \ (t x) \ (t sq) = (t c)*(t c)" and ?R="%t.(t c)*(t c) \ (t x) \ (t sq) = ((t c)+1)*((t c)+1)" and ?s=s and ?t=t in hoare_semic) apply (rotate_tac -1) thm a3Prop apply (erule a3Prop) thm a4WeakProp apply (erule a4WeakProp) apply auto done lemma wProp [rule_format]: "\s t. ((s c)*(s c) \ (s x) \ (s sq) = ((s c)+1)*((s c)+1)) \ s -w\ t \ \(beval t (Le (Var sq) (Var x))) \ ((t c)*(t c) \ (t x) \ (t sq) = ((t c)+1)*((t c)+1))" apply (unfold w_def ) apply (rule allI)+ apply (rule impI) thm hoare_while apply (rule_tac ?INV="%s. (s c * s c \ s x \ s sq = (s c + 1) * (s c + 1))" and ?b="(Le (Var sq) (Var x))" and ?c="wb" and ?s=s and ?t=t in hoare_while) apply (rotate_tac -1) apply simp thm wbProp apply (erule wbProp) apply auto done lemma wStrengthProp [rule_format]: "\s t. ((s c)*(s c) \ (s x) \ (s sq) = ((s c)+1)*((s c)+1)) \ s -w\ t \ (t c)*(t c) \ (t x) \ (t x) < ((t c)+1)*((t c)+1)" apply clarify thm wProp apply (cut_tac ?s="s" and ?t="t" in wProp) apply clarify apply simp done lemma c1Prop [rule_format]: "\s t. ((s c)*(s c) \ (s x) \ 1 = ((s c)+1)*((s c)+1)) \ (s -c1\ t) \ (t c)*(t c) \ (t x) \ (t x) < ((t c)+1)*((t c)+1)" apply (simp (no_asm) add: c1_def ) apply (rule allI)+ apply clarify thm hoare_semic apply (rule_tac ?P="%s.(s c)*(s c) \ (s x) \ 1 = ((s c)+1)*((s c)+1)" and ?c1.0="a2" and ?c2.0="w" and ?Q="%t.(t c)*(t c) \ (t x) \ (t sq) = ((t c)+1)*((t c)+1)" and ?R="%t.(t c)*(t c) \ (t x) \ (t x) < ((t c)+1)*((t c)+1)" and ?s=s and ?t=t in hoare_semic) apply (rotate_tac -1) thm a2Prop apply (erule a2Prop) apply (rotate_tac -1) thm wStrengthProp apply (erule wStrengthProp) apply auto done lemma c0Prop [rule_format]: "\s t. 0 \ (s x) \ (s -c0\ t) \ (t c)*(t c) \ (t x) \ (t x) < ((t c)+1)*((t c)+1)" apply (simp (no_asm) add: c0_def ) apply (rule allI)+ apply clarify thm hoare_semic apply (rule_tac ?P="%s. 0 \ s x" and ?c1.0="a1" and ?c2.0="c1" and ?Q="%s.((s c)*(s c) \ (s x) \ 1 = ((s c)+1)*((s c)+1))" and ?R="%t.(t c)*(t c) \ (t x) \ (t x) < ((t c)+1)*((t c)+1)" and ?s=s and ?t=t in hoare_semic) apply (rotate_tac -1) thm a1Prop apply (erule a1Prop) apply (rotate_tac -1) thm c1Prop apply (erule c1Prop) apply auto done lemma myProgProp: "\s t. 0 \ (s x) \ (s -myProg\ t) \ (t c)*(t c) \ (t x) \ (t x) < ((t c)+1)*((t c)+1)" apply (insert c0Prop) apply simp done end