equal
deleted
inserted
replaced
5 begin |
5 begin |
6 |
6 |
7 type_synonym assn = "state \<Rightarrow> bool" |
7 type_synonym assn = "state \<Rightarrow> bool" |
8 |
8 |
9 definition |
9 definition |
10 equiv_up_to :: "assn \<Rightarrow> com \<Rightarrow> com \<Rightarrow> bool" ("_ \<Turnstile> _ \<sim> _" [60,0,10] 60) |
10 equiv_up_to :: "assn \<Rightarrow> com \<Rightarrow> com \<Rightarrow> bool" ("_ \<Turnstile> _ \<sim> _" [50,0,10] 50) |
11 where |
11 where |
12 "P \<Turnstile> c \<sim> c' \<equiv> \<forall>s s'. P s \<longrightarrow> (c,s) \<Rightarrow> s' \<longleftrightarrow> (c',s) \<Rightarrow> s'" |
12 "P \<Turnstile> c \<sim> c' \<equiv> \<forall>s s'. P s \<longrightarrow> (c,s) \<Rightarrow> s' \<longleftrightarrow> (c',s) \<Rightarrow> s'" |
13 |
13 |
14 definition |
14 definition |
15 bequiv_up_to :: "assn \<Rightarrow> bexp \<Rightarrow> bexp \<Rightarrow> bool" ("_ \<Turnstile> _ <\<sim>> _" [60,0,10] 60) |
15 bequiv_up_to :: "assn \<Rightarrow> bexp \<Rightarrow> bexp \<Rightarrow> bool" ("_ \<Turnstile> _ <\<sim>> _" [50,0,10] 50) |
16 where |
16 where |
17 "P \<Turnstile> b <\<sim>> b' \<equiv> \<forall>s. P s \<longrightarrow> bval b s = bval b' s" |
17 "P \<Turnstile> b <\<sim>> b' \<equiv> \<forall>s. P s \<longrightarrow> bval b s = bval b' s" |
18 |
18 |
19 lemma equiv_up_to_True: |
19 lemma equiv_up_to_True: |
20 "((\<lambda>_. True) \<Turnstile> c \<sim> c') = (c \<sim> c')" |
20 "((\<lambda>_. True) \<Turnstile> c \<sim> c') = (c \<sim> c')" |