Theory CTypes
theory CTypes
imports
CTypesDefs "HOL-Eisbach.Eisbach_Tools"
begin
section ‹‹super_update_bs››
lemma length_super_update_bs [simp]:
"n + length v ≤ length bs ⟹ length (super_update_bs v bs n) = length bs"
by (clarsimp simp: super_update_bs_def)
lemma drop_super_update_bs:
"⟦ k ≤ n; n ≤ length bs ⟧ ⟹ drop k (super_update_bs v bs n) = super_update_bs v (drop k bs) (n - k)"
by (simp add: super_update_bs_def take_drop)
lemma drop_super_update_bs2:
"⟦ n ≤ length bs; n + length v ≤ k ⟧ ⟹
drop k (super_update_bs v bs n) = drop k bs"
by (clarsimp simp: super_update_bs_def min_def split: if_split_asm)
lemma take_super_update_bs:
"⟦ k ≤ n; n ≤ length bs ⟧ ⟹ take k (super_update_bs v bs n) = take k bs"
by (clarsimp simp: super_update_bs_def min_def split: if_split_asm)
lemma take_super_update_bs2:
"⟦ n ≤ length bs; n + length v ≤ k ⟧ ⟹
take k (super_update_bs v bs n) = super_update_bs v (take k bs) n"
apply (clarsimp simp: super_update_bs_def min_def split: if_split_asm)
apply (cases "n=k"; simp add: drop_take)
done
lemma take_drop_super_update_bs:
"length v = n ⟹ m ≤ length bs ⟹ take n (drop m (super_update_bs v bs m)) = v"
by (simp add: super_update_bs_def)
lemma super_update_bs_take_drop:
"n + m ≤ length bs ⟹ super_update_bs (take m (drop n bs)) bs n = bs"
by (simp add: super_update_bs_def) (metis append.assoc append_take_drop_id take_add)
lemma super_update_bs_same_length: "length bs = length xbs ⟹ super_update_bs bs xbs 0 = bs"
by (simp add: super_update_bs_def)
lemma super_update_bs_append_drop_first:
"length xbs = m ⟹ n + length bs ≤ m ⟹ drop m (super_update_bs bs (xbs @ ybs) n) = ybs"
by (simp add: super_update_bs_def)
lemma super_update_bs_append_take_first:
"length xbs = m ⟹ n + length bs ≤ m ⟹ take m (super_update_bs bs (xbs @ ybs) n) = (super_update_bs bs xbs n)"
by (simp add: super_update_bs_def)
lemma super_update_bs_append_drop_second:
"length xbs = m ⟹ m ≤ n ⟹
drop m (super_update_bs bs (xbs @ ybs) n) = (super_update_bs bs ybs (n - m))"
by (simp add: super_update_bs_def)
lemma super_update_bs_append_take_second:
"length xbs = m ⟹ m ≤ n ⟹
take m (super_update_bs bs (xbs @ ybs) n) = xbs"
by (simp add: super_update_bs_def)
lemma super_update_bs_length: "length bs + n ≤ length xbs ==> length (super_update_bs bs xbs n) = length xbs"
by (simp add: super_update_bs_def)
lemma super_update_bs_append2: "length xbs ≤ n ⟹
super_update_bs bs (xbs @ ybs) n = xbs @ super_update_bs bs ybs (n - length xbs)"
by (simp add: super_update_bs_def)
lemma super_update_bs_append1: "n + length bs ≤ length xbs ⟹
super_update_bs bs (xbs @ ybs) n = super_update_bs bs xbs n @ ybs"
by (simp add: super_update_bs_def)
section ‹Rest›
lemma fu_commutes:
"fu_commutes f g ⟹ f bs (g bs' v) = g bs' (f bs v)"
by (simp add: fu_commutes_def)
lemma size_td_list_append [simp]:
"size_td_list (xs@ys) = size_td_list xs + size_td_list ys"
by (induct xs) (auto)
lemma access_ti_append:
"⋀bs. length bs = size_td_list (xs@ys) ⟹
access_ti_list (xs@ys) t bs =
access_ti_list xs t (take (size_td_list xs) bs) @
access_ti_list ys t (drop (size_td_list xs) bs)"
proof (induct xs)
case Nil show ?case by simp
next
case (Cons x xs) thus ?case by (simp add: min_def ac_simps drop_take)
qed
lemma update_ti_append [simp]:
"⋀bs. update_ti_list (xs@ys) bs v =
update_ti_list xs (take (size_td_list xs) bs)
(update_ti_list ys (drop (size_td_list xs) bs) v)"
proof (induct xs)
case Nil show ?case by simp
next
case (Cons x xs) thus ?case by (simp add: drop_take ac_simps min_def)
qed
lemma update_ti_struct_t_typscalar [simp]:
"update_ti_struct_t (TypScalar n algn d) =
(λbs. if length bs = n then field_update d bs else id)"
by (rule ext, simp add: update_ti_struct_t_def)
lemma update_ti_list_t_empty [simp]:
"update_ti_list_t [] = (λx. id)"
by (rule ext, simp add: update_ti_list_t_def)
lemma update_ti_list_t_cons [simp]:
"update_ti_list_t (x#xs) = (λbs v.
if length bs = size_td_tuple x + size_td_list xs then
update_ti_tuple_t x (take (size_td_tuple x) bs)
(update_ti_list_t xs (drop (size_td_tuple x) bs) v) else
v)"
by (force simp: update_ti_list_t_def update_ti_tuple_t_def min_def)
lemma update_ti_append_s [simp]:
"⋀bs. update_ti_list_t (xs@ys) bs v = (
if length bs = size_td_list xs + size_td_list ys then
update_ti_list_t xs (take (size_td_list xs) bs)
(update_ti_list_t ys (drop (size_td_list xs) bs) v) else
v)"
proof (induct xs)
case Nil show ?case by (simp add: update_ti_list_t_def)
next
case (Cons x xs) thus ?case by (simp add: min_def drop_take ac_simps)
qed
lemma update_ti_tuple_t_dtuple [simp]:
"update_ti_tuple_t (DTuple t f d) = update_ti_t t"
by (rule ext, simp add: update_ti_tuple_t_def update_ti_t_def)
text ‹---------------------------------------------------------------›
lemma field_desc_empty [simp]:
"field_desc (TypDesc algn (TypAggregate []) nm) =
⦇ field_access = λx bs. [],
field_update = λx. id, field_sz = 0 ⦈"
by (force simp: update_ti_t_def)
lemma export_uinfo_typdesc_simp [simp]:
"export_uinfo (TypDesc algn st nm) = map_td field_norm (λ_. ()) (TypDesc algn st nm)"
by (simp add: export_uinfo_def)
lemma map_td_list_append [simp]:
"map_td_list f g (xs@ys) = map_td_list f g xs @ map_td_list f g ys"
by (induct xs) auto
lemma map_td_id:
"map_td (λn algn. id) id t = (t::('a, 'b) typ_desc)"
"map_td_struct (λn algn. id) id st = (st::('a, 'b) typ_struct)"
"map_td_list (λn algn. id) id ts = (ts::('a, 'b) typ_tuple list)"
"map_td_tuple (λn algn. id) id x = (x::('a, 'b) typ_tuple)"
by (induction t and st and ts and x) simp_all
lemma dt_snd_map_td_list:
"dt_snd ` set (map_td_list f g ts) = dt_snd ` set ts"
proof (induct ts)
case (Cons x xs) thus ?case by (cases x) auto
qed simp
lemma wf_desc_map:
shows "wf_desc (map_td f g t) = wf_desc t" and
"wf_desc_struct (map_td_struct f g st) = wf_desc_struct st" and
"wf_desc_list (map_td_list f g ts) = wf_desc_list ts" and
"wf_desc_tuple (map_td_tuple f g x) = wf_desc_tuple x"
proof (induct t and st and ts and x)
case (Cons_typ_desc x xs) thus ?case
by (cases x, auto simp: dt_snd_map_td_list)
qed auto
lemma wf_desc_list_append [simp]:
"wf_desc_list (xs@ys) =
(wf_desc_list xs ∧ wf_desc_list ys ∧ dt_snd ` set xs ∩ dt_snd ` set ys = {})"
by (induct xs) auto
lemma wf_size_desc_list_append [simp]:
"wf_size_desc_list (xs@ys) = (wf_size_desc_list xs ∧ wf_size_desc_list ys)"
by (induct xs) auto
lemma norm_tu_list_append [simp]:
"norm_tu_list (xs@ys) bs =
norm_tu_list xs (take (size_td_list xs) bs) @ norm_tu_list ys (drop (size_td_list xs) bs)"
by (induct xs arbitrary: bs, auto simp: min_def ac_simps drop_take)
lemma wf_size_desc_gt:
shows "wf_size_desc (t::('a, 'b) typ_desc) ⟹ 0 < size_td t" and
"wf_size_desc_struct st ⟹ 0 < size_td_struct (st::('a,'b) typ_struct)" and
"⟦ ts ≠ []; wf_size_desc_list ts ⟧ ⟹ 0 < size_td_list (ts::('a,'b) typ_tuple list)" and
"wf_size_desc_tuple x ⟹ 0 < size_td_tuple (x::('a,'b) typ_tuple)"
by (induct t and st and ts and x rule: typ_desc_typ_struct_inducts, auto)
lemma field_lookup_empty [simp]:
"field_lookup t [] n = Some (t,n)"
by (cases t) clarsimp
lemma field_lookup_tuple_empty [simp]:
"field_lookup_tuple x [] n = None"
by (cases x) clarsimp
lemma field_lookup_list_empty [simp]:
"field_lookup_list ts [] n = None"
by (induct ts arbitrary: n) auto
lemma field_lookup_struct_empty [simp]:
"field_lookup_struct st [] n = None"
by (cases st) auto
lemma field_lookup_list_append:
"field_lookup_list (xs@ys) f n = (case field_lookup_list xs f n of
None ⇒ field_lookup_list ys f (n + size_td_list xs)
| Some y ⇒ Some y)"
proof (induct xs arbitrary: n)
case Nil show ?case by simp
next
case (Cons x xs) thus ?case
by (cases x) (auto simp: ac_simps split: option.splits)
qed
lemma field_lookup_list_None:
"f ∉ dt_snd ` set ts ⟹ field_lookup_list ts (f#fs) m = None"
proof (induct ts arbitrary: f fs m)
case (Cons x _) thus ?case by (cases x) auto
qed simp
lemma field_lookup_list_Some:
"f ∈ dt_snd ` set ts ⟹ field_lookup_list ts [f] m ≠ None"
proof (induct ts arbitrary: f m)
case (Cons x _) thus ?case by (cases x) auto
qed simp
lemma field_lookup_offset_le:
shows "⋀s m n f. field_lookup t f m = Some ((s::('a,'b) typ_desc),n) ⟹ m ≤ n" and
"⋀s m n f. field_lookup_struct st f m = Some ((s::('a,'b) typ_desc),n) ⟹ m ≤ n" and
"⋀s m n f. field_lookup_list ts f m = Some ((s::('a, 'b) typ_desc),n) ⟹ m ≤ n" and
"⋀s m n f. field_lookup_tuple x f m = Some ((s::('a, 'b) typ_desc),n) ⟹ m ≤ n"
proof (induct t and st and ts and x)
case (Cons_typ_desc x xs) thus ?case by (fastforce split: option.splits)
qed (auto split: if_split_asm)
lemma field_lookup_offset':
shows "⋀f m m' n t'. (field_lookup t f m = Some ((t'::('a,'b) typ_desc),m + n)) =
(field_lookup t f m' = Some (t',m' + n))" and
"⋀f m m' n t'. (field_lookup_struct st f m = Some ((t'::('a,'b) typ_desc),m + n)) =
(field_lookup_struct st f m' = Some (t',m' + n))" and
"⋀f m m' n t'. (field_lookup_list ts f m = Some ((t'::('a,'b) typ_desc),m + n)) =
(field_lookup_list ts f m' = Some (t',m' + n))" and
"⋀f m m' n t'. (field_lookup_tuple x f m = Some ((t'::('a,'b) typ_desc),m + n)) =
(field_lookup_tuple x f m' = Some (t',m' + n))"
proof (induct t and st and ts and x)
case (Cons_typ_desc x xs)
show ?case
proof
assume ls: "field_lookup_list (x # xs) f m = Some (t', m + n)"
show "field_lookup_list (x # xs) f m' = Some (t', m' + n)" (is "?X")
proof cases
assume ps: "field_lookup_tuple x f m = None"
moreover from this ls have "∃k. n = size_td (dt_fst x) + k"
by (clarsimp dest!: field_lookup_offset_le, arith)
moreover have "field_lookup_tuple x f m' = None"
apply (rule ccontr)
using ps
apply clarsimp
subgoal premises prems for a b
proof -
obtain k where "b = m' + k"
using prems field_lookup_offset_le
by (metis less_eqE)
then show ?thesis
using prems
by (clarsimp simp: Cons_typ_desc [where m'=m])
qed
done
ultimately show "?X" using ls
by (clarsimp simp: add.assoc [symmetric])
(subst (asm) Cons_typ_desc [where m'="m' + size_td (dt_fst x)"], fast)
next
assume nps: "field_lookup_tuple x f m ≠ None"
moreover from this have "field_lookup_tuple x f m' ≠ None"
apply (clarsimp)
subgoal premises prems for a b
proof -
obtain k where "b = m + k"
using prems field_lookup_offset_le
by (metis less_eqE)
then show ?thesis
using prems
apply clarsimp
apply (subst (asm) Cons_typ_desc [where m'=m'])
apply fast
done
qed
done
ultimately show "?X" using ls
by (clarsimp, subst (asm) Cons_typ_desc [where m'=m'], simp)
qed
next
assume ls: "field_lookup_list (x # xs) f m' = Some (t', m' + n)"
show "field_lookup_list (x # xs) f m = Some (t', m + n)" (is "?X")
proof cases
assume ps: "field_lookup_tuple x f m' = None"
moreover from this ls have "∃k. n = size_td (dt_fst x) + k"
by (clarsimp dest!: field_lookup_offset_le, arith)
moreover have "field_lookup_tuple x f m = None"
apply (rule ccontr)
using ps
apply clarsimp
subgoal premises prems for a b
proof -
obtain k where "b = m + k"
using prems field_lookup_offset_le
by (metis less_eqE)
then show ?thesis using prems
by (clarsimp simp: Cons_typ_desc [where m'=m'])
qed
done
ultimately show "?X" using ls
by (clarsimp simp: add.assoc [symmetric])
(subst (asm) Cons_typ_desc [where m'="m + size_td (dt_fst x)"], fast)
next
assume nps: "field_lookup_tuple x f m' ≠ None"
moreover from this have "field_lookup_tuple x f m ≠ None"
apply clarsimp
subgoal premises prems for a b
proof -
obtain k where "b = m' + k"
using prems field_lookup_offset_le
by (metis less_eqE)
then show ?thesis using prems
apply clarsimp
apply (subst (asm) Cons_typ_desc [where m'=m])
apply fast
done
qed
done
ultimately show "?X" using ls
by (clarsimp, subst (asm) Cons_typ_desc [where m'=m], simp)
qed
qed
qed auto
lemma field_lookup_offset:
"(field_lookup t f m = Some (t',m + n)) = (field_lookup t f 0 = Some (t',n))"
by (simp add: field_lookup_offset' [where m'=0])
lemma field_lookup_offset2:
"field_lookup t f m = Some (t',n) ⟹ field_lookup t f 0 = Some (t',n - m)"
by (simp add: field_lookup_offset_le
flip: field_lookup_offset [where m=m])
lemma field_lookup_list_offset:
"(field_lookup_list ts f m = Some (t',m + n)) = (field_lookup_list ts f 0 = Some (t',n))"
by (simp add: field_lookup_offset' [where m'=0])
lemma field_lookup_list_offset2:
"field_lookup_list ts f m = Some (t',n) ⟹ field_lookup_list ts f 0 = Some (t',n - m)"
by (simp add: field_lookup_offset_le
flip: field_lookup_list_offset [where m=m])
lemma field_lookup_list_offset3:
"field_lookup_list ts f 0 = Some (t',n) ⟹ field_lookup_list ts f m = Some (t',m + n)"
by (simp add: field_lookup_list_offset)
lemma field_lookup_list_offsetD:
"⟦ field_lookup_list ts f 0 = Some (s,k);
field_lookup_list ts f m = Some (t,n) ⟧ ⟹ s=t ∧ n=m+k"
subgoal premises prems
proof -
have "∃k. n = m + k" using prems field_lookup_offset_le by (metis less_eqE)
then show ?thesis using prems
by (clarsimp simp: field_lookup_list_offset)
qed
done
lemma field_lookup_offset_None:
"(field_lookup t f m = None) = (field_lookup t f 0 = None)"
by (auto simp: field_lookup_offset2 field_lookup_offset [where m=m,symmetric]
intro: ccontr)
lemma field_lookup_list_offset_None:
"(field_lookup_list ts f m = None) = (field_lookup_list ts f 0 = None)"
by (auto simp: field_lookup_list_offset2 field_lookup_list_offset [where m=m,symmetric]
intro: ccontr)
lemma map_td_size [simp]:
shows "size_td (map_td f g t) = size_td t" and
"size_td_struct (map_td_struct f g st) = size_td_struct st" and
"size_td_list (map_td_list f g ts) = size_td_list ts" and
"size_td_tuple (map_td_tuple f g x) = size_td_tuple x"
by (induct t and st and ts and x, auto)
lemma td_set_map_td1:
"(s, n) ∈ td_set t k ⟹ (map_td f g s, n) ∈ td_set (map_td f g t) k" and
"(s, n) ∈ td_set_struct st k ⟹ (map_td f g s, n) ∈ td_set_struct (map_td_struct f g st) k" and
"(s, n) ∈ td_set_list ts k ⟹ (map_td f g s, n) ∈ td_set_list (map_td_list f g ts) k" and
"(s, n) ∈ td_set_tuple td k ⟹ (map_td f g s, n) ∈ td_set_tuple (map_td_tuple f g td) k"
apply (induct t and st and ts and td arbitrary: n k and n k and n k and n k)
by (auto, metis dt_tuple.collapse map_td_size(4) tz5)
lemma size_td_tuple_dt_fst:
"size_td_tuple p = size_td (dt_fst p)"
by (cases p, simp)
lemma td_set_map_td2:
"(s', n) ∈ td_set (map_td f g t) k ⟹ ∃s. (s, n) ∈ td_set t k ∧ s' = map_td f g s" and
"(s', n) ∈ td_set_struct (map_td_struct f g st) k ⟹ ∃s. (s, n) ∈ td_set_struct st k ∧ s' = map_td f g s" and
"(s', n) ∈ td_set_list (map_td_list f g ts) k ⟹ ∃s. (s, n) ∈ td_set_list ts k ∧ s' = map_td f g s" and
"(s', n) ∈ td_set_tuple (map_td_tuple f g td) k ⟹ ∃s. (s, n) ∈ td_set_tuple td k ∧ s' = map_td f g s"
proof (induct t and st and ts and td arbitrary: n k and n k and n k and n k )
case (TypDesc nat typ_struct list)
then show ?case by auto
next
case (TypScalar nat1 nat2 a)
then show ?case by auto
next
case (TypAggregate list)
then show ?case by auto
next
case Nil_typ_desc
then show ?case by auto
next
case (Cons_typ_desc dt_tuple list)
then show ?case
apply (clarsimp, safe)
apply blast
by (metis map_td_size(4) size_td_tuple_dt_fst)
next
case (DTuple_typ_desc typ_desc list b)
then show ?case by auto
qed
lemma td_set_offset1:
"(s, n) ∈ td_set t k ⟹ (s, n + l) ∈ td_set t (k + l)" and
"(s, n) ∈ td_set_struct st k ⟹ (s, n + l) ∈ td_set_struct st (k + l)" and
"(s, n) ∈ td_set_list xs k ⟹ (s, n + l) ∈ td_set_list xs (k + l)" and
"(s, n) ∈ td_set_tuple td k ⟹ (s, n + l) ∈ td_set_tuple td (k + l)"
apply (induct t and st and xs and td arbitrary: s n k l and s n k l and s n k l and s n k l)
by (auto, smt (verit, best) add.commute add.left_commute)
lemma td_set_offset2:
"(s, n + l) ∈ td_set t (k + l) ⟹ (s, n) ∈ td_set t k" and
"(s, n + l) ∈ td_set_struct st (k + l) ⟹ (s, n) ∈ td_set_struct st k" and
"(s, n + l) ∈ td_set_list xs (k + l) ⟹ (s, n) ∈ td_set_list xs k" and
"(s, n + l) ∈ td_set_tuple td (k + l) ⟹ (s, n) ∈ td_set_tuple td k"
apply (induct t and st and xs and td arbitrary: s n k l and s n k l and s n k l and s n k l)
by (auto, smt (verit, best) add.commute add.left_commute)
lemma td_set_offset_conv: "(s, n) ∈ td_set t k ⟷ (s, n + l) ∈ td_set t (k + l)"
using td_set_offset1 td_set_offset2 by blast
lemma td_set_offset_0_conv: "(s, n + k) ∈ td_set t k ⟷ (s, n) ∈ td_set t 0 "
using td_set_offset_conv [where k=0 and n=n and l=k and s=s and t =t]
by simp
lemma td_set_offset_le':
"∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set t m ⟶ m ≤ n"
"∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_struct st m ⟶ m ≤ n"
"∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_list ts m ⟶ m ≤ n"
"∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_tuple x m ⟶ m ≤ n"
by (induct t and st and ts and x) fastforce+
lemma td_set_offset_0_conv': "(s, n) ∈ td_set t k ⟷ (∃n'. (s, n') ∈ td_set t 0 ∧ n = n' + k) "
by (metis add.commute le_Suc_ex td_set_offset_0_conv td_set_offset_le'(1))
lemma td_set_list_set_td_set1: "(s, n) ∈ td_set_list ts k ⟹
(∃t n'. t ∈ set ts ∧ (s, n') ∈ td_set (dt_fst t) 0)"
apply (induct ts arbitrary: n k)
apply simp
apply simp
by (metis dt_tuple.collapse td_set_offset_0_conv' ts5)
lemma export_uinfo_size [simp]:
"size_td (export_uinfo t) = size_td (t::('a,'b) typ_info)"
by (simp add: export_uinfo_def)
lemma (in c_type) typ_uinfo_size [simp]:
"size_td (typ_uinfo_t TYPE('a)) = size_td (typ_info_t TYPE('a))"
by (simp add: typ_uinfo_t_def export_uinfo_def)
lemma wf_size_desc_map:
shows "wf_size_desc (map_td f g t) = wf_size_desc t" and
"wf_size_desc_struct (map_td_struct f g st) = wf_size_desc_struct st" and
"wf_size_desc_list (map_td_list f g ts) = wf_size_desc_list ts" and
"wf_size_desc_tuple (map_td_tuple f g x) = wf_size_desc_tuple x"
proof (induction t and st and ts and x)
case (TypAggregate list)
then show ?case by (cases list) auto
qed auto
lemma map_td_flr_Some [simp]:
"map_td_flr f g (Some (t,n)) = Some (map_td f g t,n)"
by (clarsimp simp: map_td_flr_def)
lemma map_td_flr_None [simp]:
"map_td_flr f g None = None"
by (clarsimp simp: map_td_flr_def)
lemma field_lookup_map:
shows "⋀f m s. field_lookup t f m = s ⟹
field_lookup (map_td fupd g t) f m = map_td_flr fupd g s" and
"⋀f m s. field_lookup_struct st f m = s ⟹
field_lookup_struct (map_td_struct fupd g st) f m = map_td_flr fupd g s" and
"⋀f m s. field_lookup_list ts f m = s ⟹
field_lookup_list (map_td_list fupd g ts) f m = map_td_flr fupd g s" and
"⋀f m s. field_lookup_tuple x f m = s ⟹
field_lookup_tuple (map_td_tuple fupd g x) f m = map_td_flr fupd g s"
proof (induct t and st and ts and x)
case (Cons_typ_desc x xs) thus ?case
by (clarsimp, cases x, auto simp: map_td_flr_def split: option.splits)
qed auto
lemma field_lookup_export_uinfo_Some:
"field_lookup (t::('a,'b) typ_info) f m = Some (s,n) ⟹
field_lookup (export_uinfo t) f m = Some (export_uinfo s,n)"
by (simp add: export_uinfo_def field_lookup_map)
lemma field_lookup_struct_export_Some:
"field_lookup_struct (st::('a,'b) typ_struct) f m = Some (s,n) ⟹
field_lookup_struct (map_td_struct fupd g st) f m = Some (map_td fupd g s,n)"
by (simp add: field_lookup_map)
lemma field_lookup_struct_export_None:
"field_lookup_struct (st::('a, 'b) typ_struct) f m = None ⟹
field_lookup_struct (map_td_struct fupd g st) f m = None"
by (simp add: field_lookup_map)
lemma field_lookup_list_export_Some:
"field_lookup_list (ts::('a, 'b) typ_tuple list) f m = Some (s,n) ⟹
field_lookup_list (map_td_list fupd g ts) f m = Some (map_td fupd g s,n)"
by (simp add: field_lookup_map)
lemma field_lookup_list_export_None:
"field_lookup_list (ts::('a, 'b) typ_tuple list) f m = None ⟹
field_lookup_list (map_td_list fupd g ts) f m = None"
by (simp add: field_lookup_map)
lemma field_lookup_tuple_export_Some:
"field_lookup_tuple (x::('a, 'b) typ_tuple) f m = Some (s,n) ⟹
field_lookup_tuple (map_td_tuple fupd g x) f m = Some (map_td fupd g s,n)"
by (simp add: field_lookup_map)
lemma field_lookup_tuple_export_None:
"field_lookup_tuple (x::('a, 'b) typ_tuple) f m = None ⟹
field_lookup_tuple (map_td_tuple fupd g x) f m = None"
by (simp add: field_lookup_map)
lemma import_flr_Some [simp]:
"import_flr f g (Some (map_td f g t,n)) (Some (t,n))"
by (clarsimp simp: import_flr_def)
lemma import_flr_None [simp]:
"import_flr f g None None"
by (clarsimp simp: import_flr_def)
lemma field_lookup_export_uinfo_rev'':
"⋀f m s. field_lookup (map_td fupd g t) f m = s ⟹
import_flr fupd g s ((field_lookup t f m)::('a,'b) flr)"
"⋀f m s. field_lookup_struct (map_td_struct fupd g st) f m = s ⟹
import_flr fupd g s ((field_lookup_struct st f m)::('a,'b) flr)"
"⋀f m s. field_lookup_list (map_td_list fupd g ts) f m = s ⟹
import_flr fupd g s ((field_lookup_list ts f m)::('a,'b) flr)"
"⋀f m s. field_lookup_tuple (map_td_tuple fupd g x) f m = s ⟹
import_flr fupd g s ((field_lookup_tuple x f m)::('a,'b) flr)"
proof (induct t and st and ts and x)
case (TypDesc nat typ_struct list)
then show ?case by (clarsimp simp: import_flr_def export_uinfo_def)
next
case (TypScalar nat1 nat2 a)
then show ?case by auto
next
case (TypAggregate list)
then show ?case by auto
next
case Nil_typ_desc
then show ?case by auto
next
case (Cons_typ_desc dt_tuple list)
then show ?case
apply clarsimp
apply(clarsimp split: option.splits)
apply(cases f, clarsimp+)
apply(rule conjI, clarsimp)
apply(cases dt_tuple, simp)
apply clarsimp
apply(drule field_lookup_tuple_export_Some [where fupd=fupd and g=g])
apply simp
apply(rule conjI; clarsimp)
apply(drule field_lookup_tuple_export_None [where fupd=fupd and g=g])
apply simp
apply metis
done
next
case (DTuple_typ_desc typ_desc list b)
then show ?case by (auto)
qed
lemma field_lookup_export_uinfo_rev':
"(∀f m s. field_lookup (map_td fupd g t) f m = s ⟶
import_flr fupd g s ((field_lookup t f m)::('a,'b) flr)) ∧
(∀f m s. field_lookup_struct (map_td_struct fupd g st) f m = s ⟶
import_flr fupd g s ((field_lookup_struct st f m)::('a,'b) flr)) ∧
(∀f m s. field_lookup_list (map_td_list fupd g ts) f m = s ⟶
import_flr fupd g s ((field_lookup_list ts f m)::('a,'b) flr)) ∧
(∀f m s. field_lookup_tuple (map_td_tuple fupd g x) f m = s ⟶
import_flr fupd g s ((field_lookup_tuple x f m)::('a,'b) flr))"
by (auto simp: field_lookup_export_uinfo_rev'')
lemma field_lookup_export_uinfo_Some_rev:
"field_lookup (export_uinfo (t::('a,'b) typ_info)) f m = Some (s,n) ⟹
∃k. field_lookup t f m = Some (k,n) ∧ export_uinfo k = s"
apply(insert field_lookup_export_uinfo_rev' [of field_norm "(λ_. ())" t undefined undefined undefined])
apply clarsimp
apply(drule spec [where x=f])
apply(drule spec [where x=m])
apply(clarsimp simp: import_flr_def export_uinfo_def split: option.splits)
done
lemma (in c_type) field_lookup_uinfo_Some_rev:
"field_lookup (typ_uinfo_t (TYPE('a))) f m = Some (s,n) ⟹
∃k. field_lookup (typ_info_t (TYPE('a))) f m = Some (k,n) ∧ export_uinfo k = s"
apply (simp add: typ_uinfo_t_def)
apply (rule field_lookup_export_uinfo_Some_rev)
apply assumption
done
lemma (in c_type) field_lookup_offset_untyped_eq [simp]:
"field_lookup (typ_info_t TYPE('a)) f 0 = Some (s,n) ⟹
field_offset_untyped (typ_uinfo_t TYPE('a)) f = n"
apply(simp add: field_offset_untyped_def typ_uinfo_t_def)
apply(drule field_lookup_export_uinfo_Some)
apply(simp add: typ_uinfo_t_def export_uinfo_def)
done
lemma (in c_type) field_lookup_offset_eq [simp]:
"field_lookup (typ_info_t TYPE('a)) f 0 = Some (s,n) ⟹
field_offset TYPE('a) f = n"
by(simp add: field_offset_def)
lemma field_offset_self [simp]:
"field_offset t [] = 0"
by (simp add: field_offset_def field_offset_untyped_def)
lemma (in c_type) field_ti_self [simp]:
"field_ti TYPE('a) [] = Some (typ_info_t TYPE('a))"
by (simp add: field_ti_def)
lemma (in c_type) field_size_self [simp]:
"field_size TYPE('a) [] = size_td (typ_info_t TYPE('a))"
by (simp add: field_size_def)
lemma field_lookup_prefix_None'':
"(∀f g m. field_lookup (t::('a,'b) typ_desc) f m = None ⟶ field_lookup t (f@g) m = None)"
"(∀f g m. field_lookup_struct (st::('a,'b) typ_struct) f m = None ⟶ f ≠ [] ⟶
field_lookup_struct st (f@g) m = None)"
"(∀f g m. field_lookup_list (ts::('a,'b) typ_tuple list) f m = None ⟶ f ≠ [] ⟶
field_lookup_list ts (f@g) m = None)"
"(∀f g m. field_lookup_tuple (x::('a,'b) typ_tuple) f m = None ⟶ f ≠ [] ⟶
field_lookup_tuple x (f@g) m = None)"
by (induct t and st and ts and x)
(clarsimp split: option.splits)+
lemma field_lookup_prefix_None':
"(∀f g m. field_lookup (t::('a,'b) typ_desc) f m = None ⟶ field_lookup t (f@g) m = None) ∧
(∀f g m. field_lookup_struct (st::('a,'b) typ_struct) f m = None ⟶ f ≠ [] ⟶
field_lookup_struct st (f@g) m = None) ∧
(∀f g m. field_lookup_list (ts::('a,'b) typ_tuple list) f m = None ⟶ f ≠ [] ⟶
field_lookup_list ts (f@g) m = None) ∧
(∀f g m. field_lookup_tuple (x::('a,'b) typ_tuple) f m = None ⟶ f ≠ [] ⟶
field_lookup_tuple x (f@g) m = None)"
by (auto simp: field_lookup_prefix_None'')
lemma field_lookup_prefix_Some'':
"(∀f g t' m n. field_lookup t f m = Some ((t'::('a,'b) typ_desc),n) ⟶ wf_desc t ⟶
field_lookup t (f@g) m = field_lookup t' g n)"
"(∀f g t' m n. field_lookup_struct st f m = Some ((t'::('a,'b) typ_desc),n) ⟶ wf_desc_struct st ⟶
field_lookup_struct st (f@g) m = field_lookup t' g n)"
"(∀f g t' m n. field_lookup_list ts f m = Some ((t'::('a,'b) typ_desc),n) ⟶ wf_desc_list ts ⟶
field_lookup_list ts (f@g) m = field_lookup t' g n)"
"(∀f g t' m n. field_lookup_tuple x f m = Some ((t'::('a,'b) typ_desc),n) ⟶ wf_desc_tuple x ⟶
field_lookup_tuple x (f@g) m = field_lookup t' g n)"
proof(induct t and st and ts and x)
case (TypDesc nat typ_struct list)
then show ?case by auto
next
case (TypScalar nat1 nat2 a)
then show ?case by auto
next
case (TypAggregate list)
then show ?case by auto
next
case Nil_typ_desc
then show ?case by auto
next
case (Cons_typ_desc dt_tuple list)
then show ?case
apply(clarsimp split: option.splits)
apply(cases dt_tuple)
subgoal for f
apply(cases f, clarsimp)
by (clarsimp simp: field_lookup_list_None split: if_split_asm)
done
next
case (DTuple_typ_desc typ_desc list b)
then show ?case by auto
qed
lemma field_lookup_prefix_Some':
"(∀f g t' m n. field_lookup t f m = Some ((t'::('a, 'b) typ_desc),n) ⟶ wf_desc t ⟶
field_lookup t (f@g) m = field_lookup t' g n) ∧
(∀f g t' m n. field_lookup_struct st f m = Some ((t'::('a,'b) typ_desc),n) ⟶ wf_desc_struct st ⟶
field_lookup_struct st (f@g) m = field_lookup t' g n) ∧
(∀f g t' m n. field_lookup_list ts f m = Some ((t'::('a,'b) typ_desc),n) ⟶ wf_desc_list ts ⟶
field_lookup_list ts (f@g) m = field_lookup t' g n) ∧
(∀f g t' m n. field_lookup_tuple x f m = Some ((t'::('a,'b) typ_desc),n) ⟶ wf_desc_tuple x ⟶
field_lookup_tuple x (f@g) m = field_lookup t' g n)"
by (auto simp: field_lookup_prefix_Some'')
lemma field_lookup_append_eq:
"wf_desc t ⟹
field_lookup t (f @ g) n =
Option.bind (field_lookup t f n) (λ(t', m). field_lookup t' g m)"
by (cases "field_lookup t f n")
(auto simp add: field_lookup_prefix_None''(1)[rule_format]
field_lookup_prefix_Some''(1)[rule_format])
lemma field_lookup_offset_shift:
"NO_MATCH 0 m ⟹ field_lookup t f 0 = Some (t', n) ⟹ field_lookup t f m = Some (t', m + n)"
by (simp add: field_lookup_offset)
lemma field_lookup_offset_shift':
"field_lookup t f m = Some (s, k) ⟹ field_lookup t f n = Some (s, k + n - m)"
by (metis CTypes.field_lookup_offset2 Nat.add_diff_assoc2 add.commute field_lookup_offset
field_lookup_offset_le(1))
lemma field_lookup_append:
assumes t: "wf_desc t"
and f: "field_lookup t f n = Some (u, m)" and g: "field_lookup u g l = Some (v, k)"
shows "field_lookup t (f @ g) n = Some (v, k + m - l)"
using field_lookup_prefix_Some''(1)[rule_format, OF f t, of g]
g[THEN field_lookup_offset_shift', of m]
by simp
lemma field_lvalue_empty_simp [simp]:
"Ptr &(p→[]) = p"
by (simp add: field_lvalue_def field_offset_def field_offset_untyped_def)
lemma map_td_align [simp]:
"align_td_wo_align (map_td f g t) = align_td_wo_align (t::('a,'b) typ_desc)"
"align_td_wo_align_struct (map_td_struct f g st) = align_td_wo_align_struct (st::('a,'b) typ_struct)"
"align_td_wo_align_list (map_td_list f g ts) = align_td_wo_align_list (ts::('a,'b) typ_tuple list)"
"align_td_wo_align_tuple (map_td_tuple f g x) = align_td_wo_align_tuple (x::('a,'b) typ_tuple)"
by (induct t and st and ts and x) auto
lemma map_td_align' [simp]:
"align_td (map_td f g t) = align_td (t::('a,'b) typ_desc)"
"align_td_struct (map_td_struct f g st) = align_td_struct (st::('a,'b) typ_struct)"
"align_td_list (map_td_list f g ts) = align_td_list (ts::('a,'b) typ_tuple list)"
"align_td_tuple (map_td_tuple f g x) = align_td_tuple (x::('a,'b) typ_tuple)"
by (induct t and st and ts and x) auto
lemma typ_uinfo_align [simp]:
"align_td_wo_align (export_uinfo t) = align_td_wo_align (t::('a,'b) typ_info)"
by (simp add: export_uinfo_def)
lemma ptr_aligned_Ptr_0 [simp]:
"ptr_aligned NULL"
by (simp add: ptr_aligned_def)
lemma td_set_self [simp]:
"(t,m) ∈ td_set t m"
by (cases t) simp
lemma td_set_wf_size_desc [rule_format]:
"(∀s m n. wf_size_desc t ⟶ ((s::('a,'b) typ_desc),m) ∈ td_set t n ⟶ wf_size_desc s)"
"(∀s m n. wf_size_desc_struct st ⟶ ((s::('a,'b) typ_desc),m) ∈ td_set_struct st n ⟶ wf_size_desc s)"
"(∀s m n. wf_size_desc_list ts ⟶ ((s::('a,'b) typ_desc),m) ∈ td_set_list ts n ⟶ wf_size_desc s)"
"(∀s m n. wf_size_desc_tuple x ⟶ ((s::('a,'b) typ_desc),m) ∈ td_set_tuple x n ⟶ wf_size_desc s)"
by (induct t and st and ts and x) force+
lemma td_set_size_lte':
"(∀s k m. ((s::('a,'b) typ_desc),k) ∈ td_set t m ⟶ size s = size t ∧ s=t ∧ k=m ∨ size s < size t)"
"(∀s k m. ((s::('a,'b) typ_desc),k) ∈ td_set_struct st m ⟶ size s < size st)"
"(∀s k m. ((s::('a,'b) typ_desc),k) ∈ td_set_list xs m ⟶ size s < size_list (size_dt_tuple size (λ_. 0) (λ_. 0)) xs)"
"(∀s k m. ((s::('a,'b) typ_desc),k) ∈ td_set_tuple x m ⟶ size s < size_dt_tuple size (λ_. 0) (λ_. 0) x)"
by (induct t and st and xs and x) force+
lemma td_set_size_lte:
"(s,k) ∈ td_set t m ⟹ size s = size t ∧ s=t ∧ k=m ∨
size s < size t"
by (simp add: td_set_size_lte')
lemma td_set_struct_size_lte:
"(s,k) ∈ td_set_struct st m ⟹ size s < size st"
by (simp add: td_set_size_lte')
lemma td_set_list_size_lte:
"(s,k) ∈ td_set_list ts m ⟹ size s < size_list (size_dt_tuple size (λ_. 0) (λ_. 0)) ts"
by (simp add: td_set_size_lte')
lemma td_aggregate_not_in_td_set_list [simp]:
"¬ (TypDesc algn (TypAggregate xs) tn,k) ∈ td_set_list xs m"
by (fastforce dest: td_set_list_size_lte simp: size_char_def)
lemma sub_size_td:
"(s::('a,'b) typ_desc) ≤ t ⟹ size s ≤ size t"
by (fastforce dest: td_set_size_lte simp: typ_tag_le_def)
lemma sub_tag_antisym:
"⟦ (s::('a,'b) typ_desc) ≤ t; t ≤ s ⟧ ⟹ s=t"
apply(frule sub_size_td)
apply(frule sub_size_td [where t=s])
apply(clarsimp simp: typ_tag_le_def)
apply(drule td_set_size_lte)
apply clarsimp
done
lemma sub_tag_refl:
"(s::('a,'b) typ_desc) ≤ s"
unfolding typ_tag_le_def by (cases s, fastforce)
lemma sub_tag_sub':
"∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set t m ⟶ td_set s n ⊆ td_set t m"
"∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_struct ts m ⟶ td_set s n ⊆ td_set_struct ts m"
"∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_list xs m ⟶ td_set s n ⊆ td_set_list xs m"
"∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_tuple x m ⟶ td_set s n ⊆ td_set_tuple x m"
by (induct t and ts and xs and x) fastforce+
lemma sub_tag_sub:
"(s,n) ∈ td_set t m ⟹ td_set s n ⊆ td_set t m"
by (simp add: sub_tag_sub')
lemma td_set_fst:
"∀m n. fst ` td_set (s::('a, 'b) typ_desc) m = fst ` td_set s n"
"∀m n. fst ` td_set_struct (st::('a,'b) typ_struct) m = fst ` td_set_struct st n"
"∀m n. fst ` td_set_list (xs::('a, 'b) typ_tuple list) m = fst ` td_set_list xs n"
"∀m n. fst ` td_set_tuple (x::('a, 'b) typ_tuple) m = fst ` td_set_tuple x n"
by (induct s and st and xs and x) (all ‹clarsimp›, fast, fast)
lemma sub_tag_trans:
"⟦ (s::('a,'b) typ_desc) ≤ t; t ≤ u ⟧ ⟹ s ≤ u"
apply(clarsimp simp: typ_tag_le_def)
by (meson sub_tag_sub'(1) subset_iff td_set_offset_0_conv)
instantiation typ_desc :: (type, type) order
begin
instance
apply intro_classes
apply(fastforce simp: typ_tag_lt_def typ_tag_le_def dest: td_set_size_lte)
apply(rule sub_tag_refl)
apply(erule (1) sub_tag_trans)
apply(erule (1) sub_tag_antisym)
done
end
lemma td_set_offset_size'':
"∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set t m ⟶ size_td s + (n - m) ≤ size_td t"
"∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_struct st m ⟶ size_td s + (n - m) ≤ size_td_struct st"
"∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_list ts m ⟶ size_td s + (n - m) ≤ size_td_list ts"
"∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_tuple x m ⟶ size_td s + (n - m) ≤ size_td_tuple x"
proof (induct t and st and ts and x)
case (Cons_typ_desc dt_tuple list)
then show ?case
apply (cases dt_tuple)
apply fastforce
done
qed auto
lemma td_set_offset_size':
"(∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set t m ⟶ size_td s + (n - m) ≤ size_td t) ∧
(∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_struct st m ⟶ size_td s + (n - m) ≤ size_td_struct st) ∧
(∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_list ts m ⟶ size_td s + (n - m) ≤ size_td_list ts) ∧
(∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_tuple x m ⟶ size_td s + (n - m) ≤ size_td_tuple x)"
by (auto simp: td_set_offset_size'')
lemma td_set_offset_size:
"(s,n) ∈ td_set t 0 ⟹ size_td s + n ≤ size_td t"
using td_set_offset_size' [of t undefined undefined undefined] by fastforce
lemma td_set_struct_offset_size:
"(s,n) ∈ td_set_struct st m ⟹ size_td s + (n - m) ≤ size_td_struct st"
using td_set_offset_size' [of undefined st undefined undefined] by clarsimp
lemma td_set_list_offset_size:
"(s,n) ∈ td_set_list ts 0 ⟹ size_td s + n ≤ size_td_list ts"
using td_set_offset_size' [of undefined undefined ts undefined]
by fastforce
lemma td_set_offset_size_m:
"(s,n) ∈ td_set t m ⟹ size_td s + (n - m) ≤ size_td t"
using insert td_set_offset_size' [of t undefined undefined undefined]
by clarsimp
lemma td_set_list_offset_size_m:
"(s,n) ∈ td_set_list t m ⟹ size_td s + (n - m) ≤ size_td_list t"
using insert td_set_offset_size' [of undefined undefined t undefined]
by clarsimp
lemma td_set_tuple_offset_size_m:
"(s,n) ∈ td_set_tuple t m ⟹ size_td s + (n - m) ≤ size_td_tuple t"
using td_set_offset_size' [of undefined undefined undefined t]
by clarsimp
lemma td_set_list_offset_le:
"(s,n) ∈ td_set_list ts m ⟹ m ≤ n"
by (simp add: td_set_offset_le')
lemma td_set_tuple_offset_le:
"(s,n) ∈ td_set_tuple ts m ⟹ m ≤ n"
by (simp add: td_set_offset_le')
lemma field_of_self [simp]:
"field_of 0 t t"
by (simp add: field_of_def)
lemma td_set_export_uinfo':
"∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set t m ⟶
(export_uinfo s,n) ∈ td_set (export_uinfo t) m"
"∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set_struct st m ⟶
(export_uinfo s,n) ∈ td_set_struct (map_td_struct field_norm (λ_. ()) st) m"
"∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set_list ts m ⟶
(export_uinfo s,n) ∈ td_set_list (map_td_list field_norm (λ_. ()) ts) m"
"∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set_tuple x m ⟶
(export_uinfo s,n) ∈ td_set_tuple (map_td_tuple field_norm (λ_. ()) x) m"
proof (induct t and st and ts and x)
case (Cons_typ_desc dt_tuple list)
then show ?case by(cases dt_tuple) (simp add: export_uinfo_def)
qed (auto simp add: export_uinfo_def)
lemma td_set_export_uinfo:
"(∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set t m ⟶
(export_uinfo s,n) ∈ td_set (export_uinfo t) m) ∧
(∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set_struct st m ⟶
(export_uinfo s,n) ∈ td_set_struct (map_td_struct field_norm (λ_. ()) st) m) ∧
(∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set_list ts m ⟶
(export_uinfo s,n) ∈ td_set_list (map_td_list field_norm (λ_. ()) ts) m) ∧
(∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set_tuple x m ⟶
(export_uinfo s,n) ∈ td_set_tuple (map_td_tuple field_norm (λ_. ()) x) m)"
by (auto simp: td_set_export_uinfo')
lemma td_set_export_uinfoD:
"(s,n) ∈ td_set t m ⟹ (export_uinfo s,n) ∈ td_set (export_uinfo t) m"
using td_set_export_uinfo [of t undefined undefined undefined] by clarsimp
lemma td_set_field_lookup'':
"∀s m n. wf_desc t ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set t m ⟶
(∃f. field_lookup t f m = Some (s,m+n)))"
"∀s m n. wf_desc_struct st ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set_struct st m ⟶
(∃f. field_lookup_struct st f m = Some (s,m+n)))"
"∀s m n. wf_desc_list ts ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set_list ts m ⟶
(∃f. field_lookup_list ts f m = Some (s,m+n)))"
"∀s m n. wf_desc_tuple x ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set_tuple x m ⟶
(∃f. field_lookup_tuple x f m = Some (s,m+n)))"
proof (induct t and st and ts and x)
case (TypDesc nat typ_struct list)
then show ?case
apply clarsimp
subgoal for s m n
apply(cases s, clarsimp)
apply (rule conjI)
apply clarsimp
apply(rule exI [where x="[]"])
apply clarsimp+
apply((erule allE)+, erule (1) impE)
apply clarsimp
subgoal for _ _ _ f
apply(cases f, clarsimp+)
subgoal for x xs
apply(rule exI [where x="x#xs"])
apply clarsimp
done
done
done
done
next
case (TypScalar nat1 nat2 a)
then show ?case by auto
next
case (TypAggregate list)
then show ?case by auto
next
case Nil_typ_desc
then show ?case by auto
next
case (Cons_typ_desc dt_tuple list)
then show ?case
apply clarsimp
apply(rule conjI, clarsimp)
apply((erule allE)+, erule (1) impE)
apply(clarsimp)
subgoal for s m n f
apply (cases f, clarsimp+)
subgoal for x xs
apply(rule exI [where x="x#xs"])
apply(clarsimp)
done
done
apply clarsimp
subgoal premises prems for s m n
using prems(1-3,6 )
prems(5)[rule_format, of s "m + size_td (dt_fst dt_tuple)" "n - size_td (dt_fst dt_tuple)"]
apply -
apply(frule td_set_list_offset_le)
apply clarsimp
subgoal for f
apply(rule exI [where x=f])
apply(clarsimp split: option.splits)
apply(cases dt_tuple, clarsimp split: if_split_asm)
apply(cases f, clarsimp+)
apply(simp add: field_lookup_list_None)
done
done
done
next
case (DTuple_typ_desc typ_desc list b)
then show ?case
apply clarsimp
apply((erule allE)+, erule (1) impE)
apply clarsimp
subgoal for s m n f
apply(rule exI [where x="list#f"])
apply clarsimp
done
done
qed
lemma td_set_field_lookup':
"(∀s m n. wf_desc t ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set t m ⟶
(∃f. field_lookup t f m = Some (s,m+n)))) ∧
(∀s m n. wf_desc_struct st ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set_struct st m ⟶
(∃f. field_lookup_struct st f m = Some (s,m+n)))) ∧
(∀s m n. wf_desc_list ts ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set_list ts m ⟶
(∃f. field_lookup_list ts f m = Some (s,m+n)))) ∧
(∀s m n. wf_desc_tuple x ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set_tuple x m ⟶
(∃f. field_lookup_tuple x f m = Some (s,m+n))))"
by (auto simp: td_set_field_lookup'')
lemma td_set_field_lookup_rev'':
"∀s m n. (∃f. field_lookup t f m = Some (s,m+n)) ⟶
((s::('a,'b) typ_desc),m + n) ∈ td_set t m"
"∀s m n. (∃f. field_lookup_struct st f m = Some (s,m+n)) ⟶
((s::('a,'b) typ_desc),m + n) ∈ td_set_struct st m"
"∀s m n. (∃f. field_lookup_list ts f m = Some (s,m+n)) ⟶
((s::('a,'b) typ_desc),m + n) ∈ td_set_list ts m"
"∀s m n. (∃f. field_lookup_tuple x f m = Some (s,m+n)) ⟶
((s::('a,'b) typ_desc),m + n) ∈ td_set_tuple x m"
proof(induct t and st and ts and x)
case (TypDesc nat typ_struct list)
then show ?case
apply clarsimp
subgoal for s m n f
apply(cases f, clarsimp)
apply clarsimp
apply((erule allE)+, erule impE, fast)
apply fast
done
done
next
case (TypScalar nat1 nat2 a)
then show ?case by auto
next
case (TypAggregate list)
then show ?case by auto
next
case Nil_typ_desc
then show ?case by auto
next
case (Cons_typ_desc dt_tuple list)
then show ?case
apply clarsimp
apply(clarsimp split: option.splits)
subgoal premises prems for s m n f
using prems (1, 4-5)
prems(3)[rule_format, where s = s and m = "m + size_td (dt_fst dt_tuple)" and n= "n - size_td (dt_fst dt_tuple)"]
apply -
apply(frule field_lookup_offset_le)
apply clarsimp
apply fast
done
subgoal by auto
done
next
case (DTuple_typ_desc typ_desc list b)
then show ?case
apply clarsimp
subgoal for s m n f
apply(cases f, clarsimp+)
apply((erule allE)+, erule impE, fast)
apply assumption
done
done
qed
lemma td_set_field_lookup_rev':
"(∀s m n. (∃f. field_lookup t f m = Some (s,m+n)) ⟶
((s::('a,'b) typ_desc),m + n) ∈ td_set t m) ∧
(∀s m n. (∃f. field_lookup_struct st f m = Some (s,m+n)) ⟶
((s::('a,'b) typ_desc),m + n) ∈ td_set_struct st m) ∧
(∀s m n. (∃f. field_lookup_list ts f m = Some (s,m+n)) ⟶
((s::('a,'b) typ_desc),m + n) ∈ td_set_list ts m) ∧
(∀s m n. (∃f. field_lookup_tuple x f m = Some (s,m+n)) ⟶
((s::('a,'b) typ_desc),m + n) ∈ td_set_tuple x m)"
by (auto simp: td_set_field_lookup_rev'')
lemma td_set_field_lookup:
"wf_desc t ⟹ k ∈ td_set t 0 = (∃f. field_lookup t f 0 = Some k)"
using td_set_field_lookup' [of t undefined undefined undefined]
td_set_field_lookup_rev' [of t undefined undefined undefined]
apply clarsimp
apply(cases k, clarsimp)
by (metis add_0)
lemma td_set_field_lookupD:
"field_lookup t f m = Some k ⟹ k ∈ td_set t m"
using td_set_field_lookup_rev' [of t undefined undefined undefined]
apply(cases k, clarsimp)
by (metis field_lookup_offset_le(1) le_iff_add)
lemma td_set_struct_field_lookup_structD:
"field_lookup_struct st f m = Some k ⟹ k ∈ td_set_struct st m"
using td_set_field_lookup_rev' [of undefined st undefined undefined]
apply(cases k, clarsimp)
by (metis field_lookup_offset_le(2) le_iff_add)
lemma field_lookup_struct_td_simp [simp]:
"field_lookup_struct ts f m ≠ Some (TypDesc algn ts nm, m)"
by (fastforce dest: td_set_struct_field_lookup_structD td_set_struct_size_lte)
lemma td_set_list_field_lookup_listD:
"field_lookup_list xs f m = Some k ⟹ k ∈ td_set_list xs m"
using td_set_field_lookup_rev' [of undefined undefined xs undefined]
apply(cases k, clarsimp)
by (metis field_lookup_offset_le(3) le_Suc_ex)
lemma td_set_tuple_field_lookup_tupleD:
"field_lookup_tuple x f m = Some k ⟹ k ∈ td_set_tuple x m"
using td_set_field_lookup_rev' [of undefined undefined undefined x]
apply(cases k, clarsimp)
by (metis field_lookup_offset_le(4) nat_le_iff_add)
lemma field_lookup_offset_size'':
"field_lookup t f n = Some (u, m) ⟹ size_td u + m ≤ size_td t + n"
by (metis Nat.add_diff_assoc field_lookup_offset_le(1)
le_diff_conv td_set_field_lookupD td_set_offset_size')
lemma field_lookup_offset_size':
assumes n: "field_lookup t f 0 = Some (t',n)" shows "size_td t' + n ≤ size_td t"
using field_lookup_offset_size''[OF n] by simp
lemma intvl_subset_of_field_lookup:
"field_lookup t f 0 = Some (u, n) ⟹
{a + of_nat n ..+ size_td u} ⊆ {a ..+ size_td t}"
by (simp add: field_lookup_offset_size' intvl_le)
lemma field_lookup_wf_size_desc_gt:
"⟦ field_lookup t f n = Some (a,b); wf_size_desc t ⟧ ⟹ 0 < size_td a"
by (fastforce simp: td_set_wf_size_desc wf_size_desc_gt dest!: td_set_field_lookupD)
lemma field_lookup_inject'':
"∀f g m s. wf_size_desc t ⟶ field_lookup (t::('a,'b) typ_desc) f m = Some s ∧ field_lookup t g m = Some s ⟶ f=g"
"∀f g m s. wf_size_desc_struct st ⟶ field_lookup_struct (st::('a,'b) typ_struct) f m = Some s ∧ field_lookup_struct st g m = Some s ⟶ f=g"
"∀f g m s. wf_size_desc_list ts ⟶ field_lookup_list (ts::('a,'b) typ_tuple list) f m = Some s ∧ field_lookup_list ts g m = Some s ⟶ f=g"
"∀f g m s. wf_size_desc_tuple x ⟶ field_lookup_tuple (x::('a,'b) typ_tuple) f m = Some s ∧ field_lookup_tuple x g m = Some s ⟶ f=g"
proof(induct t and st and ts and x)
case (TypDesc nat typ_struct list)
then show ?case by clarsimp fast
next
case (TypScalar nat1 nat2 a)
then show ?case by auto
next
case (TypAggregate list)
then show ?case by auto
next
case Nil_typ_desc
then show ?case by auto
next
case (Cons_typ_desc dt_tuple list)
then show ?case
apply clarsimp
subgoal for f g m a b
apply(clarsimp split: option.splits)
apply fast
subgoal
apply(frule td_set_tuple_field_lookup_tupleD)
apply(drule field_lookup_offset_le)
apply(drule td_set_tuple_offset_size_m)
subgoal premises prems
using prems(3-8)
apply(cases dt_tuple, simp)
subgoal premises prems
proof -
have "0 < size_td a"
using prems
apply -
apply(clarsimp split: if_split_asm; drule (2) field_lookup_wf_size_desc_gt)
done
then show ?thesis
using prems
by simp
qed
done
done
subgoal
apply(frule td_set_tuple_field_lookup_tupleD)
apply(drule field_lookup_offset_le)
apply(drule td_set_tuple_offset_size_m)
subgoal premises prems
using prems(3-8)
apply(cases dt_tuple, simp)
subgoal premises prems
proof -
have "0 < size_td a"
using prems
apply -
apply(clarsimp split: if_split_asm; drule (2) field_lookup_wf_size_desc_gt)
done
then show ?thesis
using prems
by simp
qed
done
done
subgoal by best
done
done
next
case (DTuple_typ_desc typ_desc list b)
then show ?case
apply clarsimp
subgoal for f g m a b
apply(drule spec [where x="tl f"])
apply(drule spec [where x="tl g"])
apply(cases f; simp)
apply(cases g; simp)
apply fastforce
done
done
qed
lemma field_lookup_inject':
"(∀f g m s. wf_size_desc t ⟶ field_lookup (t::('a,'b) typ_desc) f m = Some s ∧ field_lookup t g m = Some s ⟶ f=g) ∧
(∀f g m s. wf_size_desc_struct st ⟶ field_lookup_struct (st::('a,'b) typ_struct) f m = Some s ∧ field_lookup_struct st g m = Some s ⟶ f=g) ∧
(∀f g m s. wf_size_desc_list ts ⟶ field_lookup_list (ts::('a,'b) typ_tuple list) f m = Some s ∧ field_lookup_list ts g m = Some s ⟶ f=g) ∧
(∀f g m s. wf_size_desc_tuple x ⟶ field_lookup_tuple (x::('a,'b) typ_tuple) f m = Some s ∧ field_lookup_tuple x g m = Some s ⟶ f=g)"
by (auto simp: field_lookup_inject'')
lemma field_lookup_inject:
"⟦ field_lookup (t::('a,'b) typ_desc) f m = Some s;
field_lookup t g m = Some s; wf_size_desc t ⟧ ⟹ f=g"
using field_lookup_inject' [of t undefined undefined undefined]
apply(cases s)
apply clarsimp
apply(drule spec [where x=f])
apply(drule spec [where x=g])
apply fast
done
lemma fd_cons_update_normalise:
"⟦ fd_cons_update_access d n; fd_cons_access_update d n;
fd_cons_double_update d; fd_cons_length d n ⟧ ⟹
fd_cons_update_normalise d n"
apply(clarsimp simp: fd_cons_update_access_def fd_cons_update_normalise_def norm_desc_def)
subgoal for v bs
apply(drule spec [where x="field_update d bs v"])
apply(drule spec [where x="replicate (length bs) 0"])
apply clarsimp
apply(clarsimp simp: fd_cons_access_update_def)
apply(drule spec [where x=bs])
apply clarsimp
apply(drule spec [where x="replicate (length bs) 0"])
apply clarsimp
apply(drule spec [where x=v])
apply(drule spec [where x=undefined])
apply clarsimp
apply(clarsimp simp: fd_cons_double_update_def)
apply(drule spec [where x="v"])
apply(drule spec [where x="field_access d (field_update d bs undefined)
(replicate (length bs) 0)"])
apply(drule spec [where x=bs])
apply clarsimp
apply(erule impE)
apply(clarsimp simp: fd_cons_length_def)
apply clarsimp
done
done
lemma update_ti_t_update_ti_struct_t [simp]:
"update_ti_t (TypDesc algn st tn) = update_ti_struct_t st"
by (auto simp: update_ti_t_def update_ti_struct_t_def)
lemma fd_cons_fd_cons_struct [simp]:
"fd_cons (TypDesc algn st tn) = fd_cons_struct st"
by (clarsimp simp: fd_cons_def fd_cons_struct_def)
lemma update_ti_struct_t_update_ti_list_t [simp]:
"update_ti_struct_t (TypAggregate ts) = update_ti_list_t ts"
by (auto simp: update_ti_struct_t_def update_ti_list_t_def)
lemma fd_cons_struct_fd_cons_list [simp]:
"fd_cons_struct (TypAggregate ts) = fd_cons_list ts"
by (clarsimp simp: fd_cons_struct_def fd_cons_list_def)
lemma fd_cons_list_empty [simp]:
"fd_cons_list []"
by (clarsimp simp: fd_cons_list_def fd_cons_double_update_def
fd_cons_update_access_def fd_cons_access_update_def fd_cons_length_def
fd_cons_update_normalise_def update_ti_list_t_def fd_cons_desc_def)
lemma fd_cons_double_update_list_append:
"⟦ fd_cons_double_update (field_desc_list xs);
fd_cons_double_update (field_desc_list ys);
fu_commutes (field_update (field_desc_list xs)) (field_update (field_desc_list ys)) ⟧ ⟹
fd_cons_double_update (field_desc_list (xs@ys))"
by (auto simp: fd_cons_double_update_def fu_commutes_def)
lemma fd_cons_update_access_list_append:
"⟦ fd_cons_update_access (field_desc_list xs) (size_td_list xs);
fd_cons_update_access (field_desc_list ys) (size_td_list ys);
fd_cons_length (field_desc_list xs) (size_td_list xs);
fd_cons_length (field_desc_list ys) (size_td_list ys) ⟧ ⟹
fd_cons_update_access (field_desc_list (xs@ys)) (size_td_list (xs@ys))"
by (auto simp: fd_cons_update_access_def fd_cons_length_def access_ti_append)
lemma min_ll:
"min (x + y) x = (x::nat)"
by simp
lemma fd_cons_access_update_list_append:
"⟦ fd_cons_access_update (field_desc_list xs) (size_td_list xs);
fd_cons_access_update (field_desc_list ys) (size_td_list ys);
fu_commutes (field_update (field_desc_list xs)) (field_update (field_desc_list ys)) ⟧ ⟹
fd_cons_access_update (field_desc_list (xs@ys)) (size_td_list (xs@ys))"
apply(clarsimp simp: fd_cons_access_update_def)
subgoal for bs bs' v v'
apply(drule spec [where x="take (size_td_list xs) bs"])
apply clarsimp
apply(simp add: access_ti_append)
apply(drule spec [where x="drop (size_td_list xs) bs"])
apply clarsimp
apply(drule spec [where x="take (size_td_list xs) bs'"])
apply(simp add: min_ll)
apply(drule spec [where x="update_ti_list_t ys (drop (size_td_list xs) bs) v"])
apply(drule spec [where x="update_ti_list_t ys (drop (size_td_list xs) bs) v'"])
apply simp
apply(frule fu_commutes[where bs="take (size_td_list xs) bs" and
bs'="drop (size_td_list xs) bs" and v=v ])
apply clarsimp
apply(frule fu_commutes[where bs="take (size_td_list xs) bs" and
bs'="drop (size_td_list xs) bs" and v=v'])
apply clarsimp
done
done
lemma fd_cons_length_list_append:
"⟦ fd_cons_length (field_desc_list xs) (size_td_list xs);
fd_cons_length (field_desc_list ys) (size_td_list ys) ⟧ ⟹
fd_cons_length (field_desc_list (xs@ys)) (size_td_list (xs@ys))"
by (auto simp: fd_cons_length_def access_ti_append)
lemma wf_fdp_insert:
"wf_fdp (insert x xs) ⟹ wf_fdp {x} ∧ wf_fdp xs"
by (auto simp: wf_fdp_def)
lemma wf_fdp_fd_cons:
"⟦ wf_fdp X; (t,m) ∈ X ⟧ ⟹ fd_cons t"
by (auto simp: wf_fdp_def)
lemma wf_fdp_fu_commutes:
"⟦ wf_fdp X; (s,m) ∈ X; (t,n) ∈ X; ¬ m ≤ n; ¬ n ≤ m ⟧ ⟹
fu_commutes (field_update (field_desc s)) (field_update (field_desc t))"
by (auto simp: wf_fdp_def)
lemma wf_fdp_fa_fu_ind:
"⟦ wf_fdp X; (s,m) ∈ X; (t,n) ∈ X; ¬ m ≤ n; ¬ n ≤ m ⟧ ⟹
fa_fu_ind (field_desc s) (field_desc t) (size_td t) (size_td s)"
by (auto simp: wf_fdp_def)
lemma wf_fdp_mono:
"⟦ wf_fdp Y; X ⊆ Y ⟧ ⟹ wf_fdp X"
by (fastforce simp: wf_fdp_def)
lemma tf0 [simp]:
"tf_set (TypDesc algn st nm) = {(TypDesc algn st nm,[])} ∪ tf_set_struct st"
by (auto simp: tf_set_def tf_set_struct_def)
lemma tf1 [simp]: "tf_set_struct (TypScalar m algn d) = {}"
by (clarsimp simp: tf_set_struct_def)
lemma tf2 [simp]: "tf_set_struct (TypAggregate xs) = tf_set_list xs"
by (auto simp: tf_set_struct_def tf_set_list_def)
lemma tf3 [simp]: "tf_set_list [] = {}"
by (simp add: tf_set_list_def)
lemma tf4: "tf_set_list (x#xs) = tf_set_tuple x ∪ {t. t ∈ tf_set_list xs ∧ snd t ∉ snd ` tf_set_tuple x}"
apply(clarsimp simp: tf_set_list_def tf_set_tuple_def)
apply(cases x)
apply clarsimp
subgoal for x1 a b
apply(rule equalityI; clarsimp)
subgoal for a' b'
apply(cases b'; clarsimp)
apply(erule disjE; clarsimp?)