equal
deleted
inserted
replaced
82 ))" |
82 ))" |
83 |
83 |
84 "app (i,G,rT,s) = False" |
84 "app (i,G,rT,s) = False" |
85 |
85 |
86 |
86 |
87 text {* \isa{p_count} of successor instructions *} |
87 text {* \verb,p_count, of successor instructions *} |
88 |
88 |
89 consts |
89 consts |
90 succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count set" |
90 succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count set" |
91 |
91 |
92 primrec |
92 primrec |
131 have "length a = 2 \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0) |
131 have "length a = 2 \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0) |
132 with * show ?thesis by (auto dest: 0) |
132 with * show ?thesis by (auto dest: 0) |
133 qed |
133 qed |
134 |
134 |
135 text {* |
135 text {* |
136 \mdeskip |
136 \medskip |
137 simp rules for \isa{app} without patterns, better suited for proofs |
137 simp rules for @{term app} without patterns, better suited for proofs |
138 \medskip |
138 \medskip |
139 *} |
139 *} |
140 |
140 |
141 lemma appStore[simp]: |
141 lemma appStore[simp]: |
142 "app (Store idx, G, rT, s) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)" |
142 "app (Store idx, G, rT, s) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)" |