kleing@44070: header "Semantic Equivalence up to a Condition" kleing@44070: kleing@44070: theory Sem_Equiv kleing@44070: imports Hoare_Sound_Complete kleing@44070: begin kleing@44070: kleing@44070: definition kleing@44070: equiv_up_to :: "assn \ com \ com \ bool" ("_ \ _ \ _" [60,0,10] 60) kleing@44070: where kleing@44070: "P \ c \ c' \ \s s'. P s \ (c,s) \ s' \ (c',s) \ s'" kleing@44070: kleing@44070: definition kleing@44070: bequiv_up_to :: "assn \ bexp \ bexp \ bool" ("_ \ _ <\> _" [60,0,10] 60) kleing@44070: where kleing@44070: "P \ b <\> b' \ \s. P s \ bval b s = bval b' s" kleing@44070: kleing@44070: lemma equiv_up_to_True: kleing@44070: "((\_. True) \ c \ c') = (c \ c')" kleing@44070: by (simp add: equiv_def equiv_up_to_def) kleing@44070: kleing@44070: lemma equiv_up_to_weaken: kleing@44070: "P \ c \ c' \ (\s. P' s \ P s) \ P' \ c \ c'" kleing@44070: by (simp add: equiv_up_to_def) kleing@44070: kleing@44070: lemma equiv_up_toI: kleing@44070: "(\s s'. P s \ (c, s) \ s' = (c', s) \ s') \ P \ c \ c'" kleing@44070: by (unfold equiv_up_to_def) blast kleing@44070: kleing@44070: lemma equiv_up_toD1: kleing@44070: "P \ c \ c' \ P s \ (c, s) \ s' \ (c', s) \ s'" kleing@44070: by (unfold equiv_up_to_def) blast kleing@44070: kleing@44070: lemma equiv_up_toD2: kleing@44070: "P \ c \ c' \ P s \ (c', s) \ s' \ (c, s) \ s'" kleing@44070: by (unfold equiv_up_to_def) blast kleing@44070: kleing@44070: kleing@44070: lemma equiv_up_to_refl [simp, intro!]: kleing@44070: "P \ c \ c" kleing@44070: by (auto simp: equiv_up_to_def) kleing@44070: kleing@44070: lemma equiv_up_to_sym: kleing@44070: "(P \ c \ c') = (P \ c' \ c)" kleing@44070: by (auto simp: equiv_up_to_def) kleing@44070: kleing@44070: lemma equiv_up_to_trans [trans]: kleing@44070: "P \ c \ c' \ P \ c' \ c'' \ P \ c \ c''" kleing@44070: by (auto simp: equiv_up_to_def) kleing@44070: kleing@44070: kleing@44070: lemma bequiv_up_to_refl [simp, intro!]: kleing@44070: "P \ b <\> b" kleing@44070: by (auto simp: bequiv_up_to_def) kleing@44070: kleing@44070: lemma bequiv_up_to_sym: kleing@44070: "(P \ b <\> b') = (P \ b' <\> b)" kleing@44070: by (auto simp: bequiv_up_to_def) kleing@44070: kleing@44070: lemma bequiv_up_to_trans [trans]: kleing@44070: "P \ b <\> b' \ P \ b' <\> b'' \ P \ b <\> b''" kleing@44070: by (auto simp: bequiv_up_to_def) kleing@44070: kleing@44070: kleing@44070: lemma equiv_up_to_hoare: kleing@44070: "P' \ c \ c' \ (\s. P s \ P' s) \ (\ {P} c {Q}) = (\ {P} c' {Q})" kleing@44070: unfolding hoare_valid_def equiv_up_to_def by blast kleing@44070: kleing@44070: lemma equiv_up_to_hoare_eq: kleing@44070: "P \ c \ c' \ (\ {P} c {Q}) = (\ {P} c' {Q})" kleing@44070: by (rule equiv_up_to_hoare) kleing@44070: kleing@44070: kleing@44070: lemma equiv_up_to_semi: kleing@44070: "P \ c \ c' \ Q \ d \ d' \ \ {P} c {Q} \ kleing@44070: P \ (c; d) \ (c'; d')" kleing@44070: by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast kleing@44070: kleing@44070: lemma equiv_up_to_while_lemma: kleing@44070: shows "(d,s) \ s' \ kleing@44070: P \ b <\> b' \ kleing@44070: (\s. P s \ bval b s) \ c \ c' \ kleing@44070: \ {\s. P s \ bval b s} c {P} \ kleing@44070: P s \ kleing@44070: d = WHILE b DO c \ kleing@44070: (WHILE b' DO c', s) \ s'" kleing@44070: proof (induct rule: big_step_induct) kleing@44070: case (WhileTrue b s1 c s2 s3) kleing@44070: note IH = WhileTrue.hyps(5) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)] kleing@44070: kleing@44070: from WhileTrue.prems kleing@44070: have "P \ b <\> b'" by simp kleing@44070: with `bval b s1` `P s1` kleing@44070: have "bval b' s1" by (simp add: bequiv_up_to_def) kleing@44070: moreover kleing@44070: from WhileTrue.prems kleing@44070: have "(\s. P s \ bval b s) \ c \ c'" by simp kleing@44070: with `bval b s1` `P s1` `(c, s1) \ s2` kleing@44070: have "(c', s1) \ s2" by (simp add: equiv_up_to_def) kleing@44070: moreover kleing@44070: from WhileTrue.prems kleing@44070: have "\ {\s. P s \ bval b s} c {P}" by simp kleing@44070: with `P s1` `bval b s1` `(c, s1) \ s2` kleing@44070: have "P s2" by (simp add: hoare_valid_def) kleing@44070: hence "(WHILE b' DO c', s2) \ s3" by (rule IH) kleing@44070: ultimately kleing@44070: show ?case by blast kleing@44070: next kleing@44070: case WhileFalse kleing@44070: thus ?case by (auto simp: bequiv_up_to_def) kleing@44070: qed (fastsimp simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+ kleing@44070: kleing@44070: lemma bequiv_context_subst: kleing@44070: "P \ b <\> b' \ (P s \ bval b s) = (P s \ bval b' s)" kleing@44070: by (auto simp: bequiv_up_to_def) kleing@44070: kleing@44070: lemma equiv_up_to_while: kleing@44070: "P \ b <\> b' \ (\s. P s \ bval b s) \ c \ c' \ kleing@44070: \ {\s. P s \ bval b s} c {P} \ kleing@44070: P \ WHILE b DO c \ WHILE b' DO c'" kleing@44070: apply (safe intro!: equiv_up_toI) kleing@44070: apply (auto intro: equiv_up_to_while_lemma)[1] kleing@44070: apply (simp add: equiv_up_to_hoare_eq bequiv_context_subst) kleing@44070: apply (drule equiv_up_to_sym [THEN iffD1]) kleing@44070: apply (drule bequiv_up_to_sym [THEN iffD1]) kleing@44070: apply (auto intro: equiv_up_to_while_lemma)[1] kleing@44070: done kleing@44070: kleing@44070: lemma equiv_up_to_while_weak: kleing@44070: "P \ b <\> b' \ P \ c \ c' \ \ {P} c {P} \ kleing@44070: P \ WHILE b DO c \ WHILE b' DO c'" kleing@44070: by (fastsimp elim!: equiv_up_to_while equiv_up_to_weaken kleing@44070: simp: hoare_valid_def) kleing@44070: kleing@44070: lemma equiv_up_to_if: huffman@44261: "P \ b <\> b' \ (\s. P s \ bval b s) \ c \ c' \ (\s. P s \ \bval b s) \ d \ d' \ kleing@44070: P \ IF b THEN c ELSE d \ IF b' THEN c' ELSE d'" kleing@44070: by (auto simp: bequiv_up_to_def equiv_up_to_def) kleing@44070: kleing@44070: lemma equiv_up_to_if_weak: kleing@44070: "P \ b <\> b' \ P \ c \ c' \ P \ d \ d' \ kleing@44070: P \ IF b THEN c ELSE d \ IF b' THEN c' ELSE d'" kleing@44070: by (fastsimp elim!: equiv_up_to_if equiv_up_to_weaken) kleing@44070: kleing@44070: lemma equiv_up_to_if_True [intro!]: kleing@44070: "(\s. P s \ bval b s) \ P \ IF b THEN c1 ELSE c2 \ c1" kleing@44070: by (auto simp: equiv_up_to_def) kleing@44070: kleing@44070: lemma equiv_up_to_if_False [intro!]: kleing@44070: "(\s. P s \ \ bval b s) \ P \ IF b THEN c1 ELSE c2 \ c2" kleing@44070: by (auto simp: equiv_up_to_def) kleing@44070: kleing@44070: lemma equiv_up_to_while_False [intro!]: kleing@44070: "(\s. P s \ \ bval b s) \ P \ WHILE b DO c \ SKIP" kleing@44070: by (auto simp: equiv_up_to_def) kleing@44070: kleing@44070: lemma while_never: "(c, s) \ u \ c \ WHILE (B True) DO c'" kleing@44070: by (induct rule: big_step_induct) auto kleing@44070: kleing@44070: lemma equiv_up_to_while_True [intro!,simp]: kleing@44070: "P \ WHILE B True DO c \ WHILE B True DO SKIP" kleing@44070: unfolding equiv_up_to_def kleing@44070: by (blast dest: while_never) kleing@44070: kleing@44070: huffman@44261: end