From 3ebeaeffab74cabebd0d93f4c63a097ca6314ab1 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@data61.csiro.au>
Date: Fri, 24 May 2019 20:33:10 +1000
Subject: [PATCH] c-parser: more pair-like setup for DTPair (splitting,
 collapsing)

---
 tools/c-parser/umm_heap/CTypesBase.thy | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/tools/c-parser/umm_heap/CTypesBase.thy b/tools/c-parser/umm_heap/CTypesBase.thy
index 092caef40..f5927ceae 100644
--- a/tools/c-parser/umm_heap/CTypesBase.thy
+++ b/tools/c-parser/umm_heap/CTypesBase.thy
@@ -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"