adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

c-parser: more pair-like setup for DTPair (splitting, collapsing)

This commit is contained in:
Gerwin Klein 2019-05-24 20:33:10 +10:00 committed by Matthew Brecknell
parent 512c134761
commit 3ebeaeffab
1 changed files with 23 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
tools/c-parser/umm_heap/CTypesBase.thy
View File

@ -171,6 +171,29 @@ primrec
where
"dt_snd (DTPair a b) = b"
lemma split_DTPair_All:
"(\<forall>x. P x) = (\<forall>a b. P (DTPair a b))"
by (rule iffI; clarsimp) (case_tac x, simp)
lemma surjective_dt_pair:
"p = DTPair (dt_fst p) (dt_snd p)"
by (cases p) simp
lemmas dt_pair_collapse [simp] = surjective_dt_pair[symmetric]
lemma split_DTPair_all[no_atp]: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (DTPair a b))"
proof
fix a b
assume "\<And>x. PROP P x"
then show "PROP P (DTPair a b)" .
next
fix x
assume "\<And>a b. PROP P (DTPair a b)"
from \<open>PROP P (DTPair (dt_fst x) (dt_snd x))\<close> show "PROP P x" by simp
qed
type_synonym normalisor = "byte list \<Rightarrow> byte list"