21 lemma int_add_LC: "x + (y + (z::int)) = y + (x + z)" |
21 lemma int_add_LC: "x + (y + (z::int)) = y + (x + z)" |
22 by simp |
22 by simp |
23 |
23 |
24 lemmas int_add_ac = int_add_A int_add_C int_add_LC |
24 lemmas int_add_ac = int_add_A int_add_C int_add_LC |
25 |
25 |
26 method_setup prune = {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} |
26 method_setup prune = |
27 "pruning parameters" |
27 {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} |
|
28 "pruning parameters" |
28 |
29 |
29 ML {* |
30 ML {* |
30 structure StepRules = Named_Thms |
31 structure StepRules = Named_Thms |
31 (val name = @{binding "step"} |
32 (val name = @{binding "step"} |
32 val description = "Theorems for hoare rules for every step") |
33 val description = "Theorems for hoare rules for every step") |
108 where "trset_of (faults, prog, pc, pos, m) = |
109 where "trset_of (faults, prog, pc, pos, m) = |
109 tprog_set prog \<union> tpc_set pc \<union> tpos_set pos \<union> tmem_set m \<union> tfaults_set faults" |
110 tprog_set prog \<union> tpc_set pc \<union> tpos_set pos \<union> tmem_set m \<union> tfaults_set faults" |
110 |
111 |
111 interpretation tm: sep_exec tstep trset_of . |
112 interpretation tm: sep_exec tstep trset_of . |
112 |
113 |
113 section {* Assembly language and its program logic *} |
114 section {* Assembly language for TMs and its program logic *} |
114 |
115 |
115 subsection {* The assembly language *} |
116 subsection {* The assembly language *} |
116 |
117 |
117 datatype tpg = |
118 datatype tpg = |
118 TInstr tm_inst |
119 TInstr tm_inst |
119 | TLabel nat |
120 | TLabel nat |
120 | TSeq tpg tpg |
121 | TSeq tpg tpg |
121 | TLocal "(nat \<Rightarrow> tpg)" |
122 | TLocal "nat \<Rightarrow> tpg" |
122 |
123 |
123 notation TLocal (binder "TL " 10) |
124 notation TLocal (binder "TL " 10) |
124 |
125 |
125 abbreviation tprog_instr :: "tm_inst \<Rightarrow> tpg" ("\<guillemotright> _" [61] 61) |
126 abbreviation tprog_instr :: "tm_inst \<Rightarrow> tpg" ("\<guillemotright> _" [61] 61) |
126 where "\<guillemotright> i \<equiv> TInstr i" |
127 where "\<guillemotright> i \<equiv> TInstr i" |
130 |
131 |
131 definition "sg e = (\<lambda> s. s = e)" |
132 definition "sg e = (\<lambda> s. s = e)" |
132 |
133 |
133 type_synonym tassert = "tresource set \<Rightarrow> bool" |
134 type_synonym tassert = "tresource set \<Rightarrow> bool" |
134 |
135 |
135 abbreviation t_hoare :: |
136 abbreviation t_hoare :: "tassert \<Rightarrow> tassert \<Rightarrow> tassert \<Rightarrow> bool" ("(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50) |
136 "tassert \<Rightarrow> tassert \<Rightarrow> tassert \<Rightarrow> bool" ("(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50) |
137 where "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace> == sep_exec.Hoare_gen tstep trset_of p c q" |
137 where "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace> == sep_exec.Hoare_gen tstep trset_of p c q" |
|
138 |
138 |
139 abbreviation it_hoare :: |
139 abbreviation it_hoare :: |
140 "(('a::sep_algebra) \<Rightarrow> tresource set \<Rightarrow> bool) \<Rightarrow> |
140 "('a::sep_algebra \<Rightarrow> tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> (tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
141 ('a \<Rightarrow> bool) \<Rightarrow> (tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
141 ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50) |
142 ("(1_).(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50) |
|
143 where "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> == sep_exec.IHoare tstep trset_of I P c Q" |
142 where "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> == sep_exec.IHoare tstep trset_of I P c Q" |
144 |
143 |
145 (* |
144 (* |
146 primrec tpg_len :: "tpg \<Rightarrow> nat" where |
145 primrec tpg_len :: "tpg \<Rightarrow> nat" where |
147 "tpg_len (TInstr ai) = 1" | |
146 "tpg_len (TInstr ai) = 1" | |
148 "tpg_len (TSeq p1 p2) = tpg_len p1 + tpg_len " | |
147 "tpg_len (TSeq p1 p2) = tpg_len p1 + tpg_len " | |
149 "tpg_len (TLocal fp) = tpg_len (fp 0)" | |
148 "tpg_len (TLocal fp) = tpg_len (fp 0)" | |
150 "tpg_len (TLabel l) = 0" *) |
149 "tpg_len (TLabel l) = 0" |
|
150 *) |
151 |
151 |
152 primrec tassemble_to :: "tpg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> tassert" |
152 primrec tassemble_to :: "tpg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> tassert" |
153 where |
153 where |
154 "tassemble_to (TInstr ai) i j = (sg ({TC i ai}) ** <(j = i + 1)>)" | |
154 "tassemble_to (TInstr ai) i j = (sg ({TC i ai}) ** <(j = i + 1)>)" | |
155 "tassemble_to (TSeq p1 p2) i j = (EXS j'. (tassemble_to p1 i j') ** (tassemble_to p2 j' j))" | |
155 "tassemble_to (TSeq p1 p2) i j = (EXS j'. (tassemble_to p1 i j') ** (tassemble_to p2 j' j))" | |
163 abbreviation tasmb_to :: "nat \<Rightarrow> tpg \<Rightarrow> nat \<Rightarrow> tassert" ("_ :[ _ ]: _" [60, 60, 60] 60) |
163 abbreviation tasmb_to :: "nat \<Rightarrow> tpg \<Rightarrow> nat \<Rightarrow> tassert" ("_ :[ _ ]: _" [60, 60, 60] 60) |
164 where "i :[ tpg ]: j \<equiv> tassemble_to tpg i j" |
164 where "i :[ tpg ]: j \<equiv> tassemble_to tpg i j" |
165 |
165 |
166 lemma EXS_intro: |
166 lemma EXS_intro: |
167 assumes h: "(P x) s" |
167 assumes h: "(P x) s" |
168 shows "((EXS x. P(x))) s" |
168 shows "(EXS x. P(x)) s" |
169 by (smt h pred_ex_def sep_conj_impl) |
169 by (smt h pred_ex_def sep_conj_impl) |
170 |
170 |
171 lemma EXS_elim: |
171 lemma EXS_elim: |
172 assumes "(EXS x. P x) s" |
172 assumes "(EXS x. P x) s" |
173 obtains x where "P x s" |
173 obtains x where "P x s" |