Up to index of Isabelle/HOL/Tables
theory Inversion = Tables2:
header {* Inversion of Normal Tables *}
theory Inversion = Tables2:
subsection {* One-Dimensional Inversion *}
consts
inverse1 :: "('a,('b,'c) T) T \<Rightarrow> ('b,('a,'c) T) T"
defs
inverse1_def: "inverse1 == tFold addH2 hConc"
lemma inverse1_addH[simp]:
"inverse1 (addH h t) = addH2 h t"
by (unfold inverse1_def, simp)
lemma inverse1_hConc[simp]:
"inverse1 (hConc t1 t2) = hConc (inverse1 t1) (inverse1 t2)"
by (unfold inverse1_def, simp)
lemma tFold_tFold_inverse1:
"\<lbrakk> assoc c2; assoc c4;
\<And> h2 h1 t . a2 h2 (a1 h1 t) = a3 h1 (a4 h2 t);
\<And> h t u . a3 h (c4 t u) = c2 (a3 h t) (a3 h u)
\<rbrakk> \<Longrightarrow>
tFold a2 c2 (tMap (tFold a1 c1) (inverse1 t)) =
tFold a3 c2 (tMap (tFold a4 c4) t)"
apply (induct_tac t rule: T_induct)
apply (induct_tac t0 rule: T_induct, simp)
apply (induct_tac t1 rule: T_induct, simp)
apply simp
apply (subgoal_tac "tFold (\<lambda>ha t0. a3 h (a4 ha t0)) c2 t1a = a3 h (tFold a4 c4 t1a)", simp)
apply (induct_tac t1a rule: T_induct, simp, simp)
txt {* original induction, second case: *}
apply (simp del: tFold_tMap)
done
lemma tFold_tFold0_inverse1:
"\<lbrakk> assoc c2; assoc c4;
\<And> h t u . a2 (c4 t u) h = c2 (a2 t h) (a2 u h)
\<rbrakk> \<Longrightarrow>
tFold a2 c2 (tMap (tFold0 c1) (inverse1 t)) =
tFold (flip a2) c2 (tMap (tFold0 c4) t)"
by (unfold tFold0_def, rule tFold_tFold_inverse1, simp_all)
subsection {* spread1 *}
consts spread1 :: "'a neList \<Rightarrow> 'b \<Rightarrow> ('a, 'b) T"
defs spread1_def: "spread1 hs t == foldr1 hConc (map1 (\<lambda>h. addH h t) hs)"
lemma regSkelOuter2_spread1[simp]:
"regSkelOuter2 (spread1 hs t) = Some (hs, headers t)"
apply (subst neList_append_induct [of "% hs . regSkelOuter2 (spread1 hs t) = Some (hs, headers t)"], simp_all)
txt {* WHy does standard induction not work here?! *}
apply (unfold spread1_def, simp_all)
done
lemma spread1_singleton[simp]: "spread1 (singleton h) t = addH h t"
by (simp add: spread1_def)
lemma spread1_append[simp]:
"spread1 (append hs1 hs2) t = hConc (spread1 hs1 t) (spread1 hs2 t)"
by (simp add: spread1_def)
lemma spread1_tFold_append:
"spread1 (tFold f append t1) t = tFold (% h0 t0 . spread1 (f h0 t0) t) hConc t1"
by (induct_tac t1 rule: T_induct, simp_all)
lemma spread1_hConc_0:
"ALL t1 . spread1 hs (hConc t1 t2) = vConc (spread1 hs t1) (spread1 hs t2)"
apply (induct_tac hs rule: neList_append_induct, simp)
apply simp
apply (rule allI)
apply (subst vConc_hConc)
apply simp
apply (rule conjI, simp, simp)
apply simp
apply simp
apply simp
apply simp
done
lemma spread1_hConc:
"spread1 hs (hConc t1 t2) = vConc (spread1 hs t1) (spread1 hs t2)"
by (insert spread1_hConc_0 [of hs t2], auto)
lemma tMap_f_spread1:
"tMap f (spread1 hs t) = spread1 hs (f t)"
by (induct_tac hs rule: neList_append_induct, simp_all)
lemma tFold_spread1:
"assoc c \<Longrightarrow> tFold a c (spread1 hs t) = foldr1 c (map1 (% h . a h t) hs)"
by (induct_tac hs rule: neList_append_induct, simp_all)
subsection {* spread2 *}
text {* This was used in the previous definition of @{text "dconc"}. *}
consts
spread2 :: "'a neList \<Rightarrow> ('b,'c) T \<Rightarrow> ('b,('a,'c) T) T"
defs
spread2_def: "spread2 hs t == foldr1 vConc (map1 (% h . addH2 h t) hs)"
lemma spread2_singleton[simp]:
"spread2 (singleton h) t = addH2 h t"
by (unfold spread2_def, simp)
lemma spread2_append[simp]:
"spread2 (append hs1 hs2) t = vConc (spread2 hs1 t) (spread2 hs2 t)"
by (unfold spread2_def, simp)
lemma spread2_cons1[simp]:
"spread2 (cons1 h hs) t = vCons (h,t) (spread2 hs t)"
by (simp add: cons1 vCons)
lemma headers_spread2[simp]:
"headers (spread2 hs t) = headers t"
by (induct_tac hs rule: neList_cons_induct, simp_all)
lemma regSkelOuter2_spread2_0:
"ALL hs2 . regSkelOuter2 (spread2 hs2 t) = Some (headers t,hs2)"
apply (induct_tac t rule: T_cons_induct, simp)
apply (rule allI, induct_tac hs2 rule: neList_append_induct)
apply simp
apply simp
apply (rule allI)
apply (erule mp1)
apply (rule_tac x=t2 in spec)
apply (induct_tac hs2 rule: neList_cons_induct)
apply (intro strip, simp)
txt {* @{text "hs2 = cons1 x xs"} *}
apply (intro strip, simp)
apply (drule_tac x=xa in spec)
apply simp
apply (subst regSkelOuter2_vCons, simp)
apply (simp add: cons1)
done
lemma regSkelOuter2_spread2[simp]:
"regSkelOuter2 (spread2 hs2 t) = Some (headers t,hs2)"
by (rule regSkelOuter2_spread2_0 [THEN spec])
lemma spread2_hConc_0:
"ALL t1 t2 . spread2 hs2 (hConc t1 t2) = hConc (spread2 hs2 t1) (spread2 hs2 t2)"
apply (induct_tac hs2 rule: neList_append_induct)
apply simp
apply simp
apply (intro strip)
apply (subst vConc_hConc)
apply simp
apply (rule conjI)
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
done
lemma spread2_hConc[simp]:
"spread2 hs2 (hConc t1 t2) = hConc (spread2 hs2 t1) (spread2 hs2 t2)"
by (insert spread2_hConc_0, auto)
lemma spread2_addH:
"spread2 hs (addH h t) = addH h (foldr1 hConc (map1 (% h2 . addH h2 t) hs))"
by (induct_tac hs rule: neList_append_induct, simp_all)
lemma spread2_tFold_hConc:
"spread2 hs2 (tFold a hConc t) = tFold (% h t . spread2 hs2 (a h t)) hConc t"
by (induct_tac t rule: T_induct, simp_all)
lemma tMap_tFold_spread2:
"assoc c \<Longrightarrow>
tMap (tFold a c) (spread2 hs t) =
tMap (% t0 . foldr1 c (map1 (\<lambda>h2. a h2 t0) hs)) t"
by (induct_tac t rule: T_induct, simp_all add: spread2_addH map1_contract_comp tFold_foldr1_hConc o_def)
subsection {* delH1 *}
consts delH1 :: "('a,'b) T \<Rightarrow> 'b"
defs delH1_def: "delH1 == tFold (% h t . t) const"
lemma delH1_hConc[simp]:
"delH1 (hConc t1 t2) = delH1 t1"
by (simp add: delH1_def)
lemma delH1_addH[simp]:
"delH1 (addH h t) = t"
by (simp add: delH1_def)
lemma delH1_hCons[simp]:
"delH1 (hCons (h,t0) t) = t0"
by (simp add: hCons)
lemma delH1_tFold_hConc[simp]:
"delH1 (tFold f hConc t) = delH1 (uncurry f (hHead t))"
by (induct_tac t rule: T_induct, simp_all)
lemma headers_delH1__reg2_0:
"ALL hs1 hs2 . regSkelOuter2 t1 = Some (hs1, hs2) \<longrightarrow> headers (delH1 t1) = hs2"
apply (induct_tac t1 rule: T_induct, simp_all)
apply (intro strip)
apply (drule optThen_result_Some, erule exE, erule conjE)
apply (drule optThen_result_Some, erule exE, erule conjE)
apply (split split_if_asm, simp_all)
apply (case_tac y, case_tac ya, simp)
done
lemma headers_delH1__reg2[simp]:
"regSkelOuter2 t1 = Some (hs1, hs2) \<Longrightarrow> headers (delH1 t1) = hs2"
by (insert headers_delH1__reg2_0, auto)
lemma delH1_addH2[simp]: "delH1 (addH2 h t) = addH h (delH1 t)"
by (induct_tac t rule: T_induct, simp_all)
lemma delH1_vConc_0:
"ALL hs1a hs1b hs2a hs2b .
regSkelOuter2 t1 = Some (hs1a, hs1b) \<longrightarrow>
regSkelOuter2 t2 = Some (hs2a, hs2b) \<longrightarrow>
delH1 (vConc t1 t2) = hConc (delH1 t1) (delH1 t2)"
apply (induct_tac t1 rule: T_cons_induct, simp_all)
apply (induct_tac t2 rule: T_cons_induct, simp_all)
apply (intro strip, erule exE, erule exE)
apply (drule optThen_result_Some, erule exE, erule conjE)
apply (split split_if_asm, simp_all)
apply (case_tac p, case_tac y, simp)
apply (induct_tac t2 rule: T_cons_induct, simp_all)
apply (intro strip, erule exE, erule exE)
apply (drule optThen_result_Some, erule exE, erule conjE)
apply (split split_if_asm, simp_all)
apply (case_tac p, case_tac y, simp)
apply (intro strip, erule exE, erule exE, erule exE, erule exE)
apply simp
apply (case_tac p, case_tac pa, simp)
done
lemma delH1_vConc:
"\<lbrakk> regSkelOuter2 t1 = Some (hs1a, hs1b);
regSkelOuter2 t2 = Some (hs2a, hs2b)
\<rbrakk> \<Longrightarrow>
delH1 (vConc t1 t2) = hConc (delH1 t1) (delH1 t2)"
by (insert delH1_vConc_0, auto)
lemma delH1_tMap_const[simp]: "delH1 (tMap (const t2) t1) = t2"
by (induct_tac t1 rule: T_induct, simp_all)
lemma delH1_tMap_CONST[simp]: "delH1 (tMap (% x . t2) t1) = t2"
by (induct_tac t1 rule: T_induct, simp_all)
subsection {* delH2 *}
consts delH2 :: "('a,('b,'c) T) T \<Rightarrow> ('a,'c) T"
defs delH2_def: "delH2 == tMap delH1"
lemma delH2_hConc[simp]:
"delH2 (hConc t1 t2) = hConc (delH2 t1) (delH2 t2)"
by (simp add: delH2_def)
lemma delH2_addH[simp]:
"delH2 (addH h t) = addH h (delH1 t)"
by (simp add: delH2_def)
lemma delH2_hCons[simp]:
"delH2 (hCons (h,t0) t) = hCons (h, delH1 t0) (delH2 t)"
by (simp add: hCons)
lemma delH2_addH2[simp]:
"delH2 (addH2 h t) = t"
by (induct_tac t rule: T_induct, simp_all)
lemma headers_delH2[simp]: "headers (delH2 t) = headers t"
by (induct_tac t rule: T_induct, simp_all)
lemma delH2_vConc_0:
"ALL hs1 hs2a t2 hs2b .
regSkelOuter2 t1 = Some (hs1, hs2a) \<longrightarrow>
regSkelOuter2 t2 = Some (hs1, hs2b) \<longrightarrow>
delH2 (vConc t1 t2) = delH2 t1"
apply (induct_tac t1 rule: T_cons_induct, simp_all)
apply (rule allI)
apply (rule impI)
apply (rule allI)
apply (erule exE)+
apply (drule optThen_result_Some, erule exE, erule conjE, simp)
apply (split split_if_asm, simp_all)
apply (erule conjE, case_tac y, simp)
apply (induct_tac t2a rule: T_cons_induct, simp_all)
apply (rule impI, rotate_tac -1, drule sym, simp)
apply (intro strip)
apply (erule exE)+
apply (drule optThen_result_Some, erule exE, erule conjE, simp)
apply (split split_if_asm, simp_all)
apply (erule conjE, case_tac p, case_tac pa, case_tac ya, simp)
apply (drule_tac x=t2b in spec, simp)
apply (rotate_tac 2, drule sym, simp, drule cons1_inj, simp)
done
lemma delH2_vConc[simp]:
"\<lbrakk> regSkelOuter2 t1 = Some (hs1, hs2a);
regSkelOuter2 t2 = Some (hs1, hs2b) \<rbrakk> \<Longrightarrow>
delH2 (vConc t1 t2) = delH2 t1"
by (insert delH2_vConc_0 [of t1], auto)
lemma delH2_spread2[simp]:
"delH2 (spread2 hs t) = t"
apply (induct_tac t rule: T_induct, simp_all)
apply (induct_tac hs rule: neList_append_induct, simp_all)
apply (subst delH2_vConc, simp_all)
apply (rule conjI, simp_all)
apply (rule conjI, simp_all)
done
lemma delH2_tMap_const:
"delH2 (tMap (const t2) t1) = tMap (const (delH1 t2)) t1"
by (induct_tac t1 rule: T_induct, simp_all)
lemma delH2_tMap_CONST:
"delH2 (tMap (% x . t2) t1) = tMap (const (delH1 t2)) t1"
by (induct_tac t1 rule: T_induct, simp_all)
subsection {* Third Dimension Operators *}
consts addH3 :: "'c \<Rightarrow> ('a, ('b,'d) T) T \<Rightarrow> ('a, ('b, ('c, 'd) T) T) T"
defs addH3_def: "addH3 == tMap \<circ> addH2"
lemma delH1_addH3[simp]: "delH1 (addH3 h t) = addH2 h (delH1 t)"
by (unfold addH3_def, induct_tac t rule: T_induct, simp_all)
consts delH3 :: "('a, ('b, ('c , 'd) T) T) T \<Rightarrow> ('a, ('b,'d) T) T"
defs delH3_def: "delH3 == tMap delH2"
subsection {* Slimming Operators *}
text {* These operators slim down a selected dimension
in the regular table skeleton
to a singleton containing a supplied entry @{text "u"}. *}
consts slimH1 :: "'a \<Rightarrow> ('c,'b) T \<Rightarrow> ('a,'b) T"
defs slimH1_def[simp]: "slimH1 h1 t == addH h1 (delH1 t)"
lemma tFold_slimH1:
"assoc c \<Longrightarrow> tFold a c (slimH1 u t) = tFold (% h0 t0 . a u t0) const t"
apply (induct_tac t rule: T_induct, simp_all del: const)
apply (subst const)
apply (simp (no_asm_simp) del: const)
done
lemma headers_slimH1[simp]: "headers (slimH1 u t) = singleton u"
by simp
consts slimH2 :: "'b \<Rightarrow> ('a,('d,'c) T) T \<Rightarrow> ('a,('b,'c) T) T"
defs slimH2_def[simp]: "slimH2 h2 t == addH2 h2 (delH2 t)"
lemma slimH2_tMap: "slimH2 h2 = tMap (slimH1 h2)"
by (rule ext, induct_tac x rule: T_induct, simp_all)
lemma slimH2_slimH2[simp]: "slimH2 u (slimH2 v t) = slimH2 u t"
by simp
lemma slimH2_addH[simp]: "slimH2 u (addH h t) = addH h (slimH1 u t)"
by simp
lemma slimH2_hConc[simp]:
"slimH2 u (hConc t1 t2) = hConc (slimH2 u t1) (slimH2 u t2)"
by simp
lemma slimH2_as_tFold[simp]:
"tFold (\<lambda>h t. addH h (slimH1 u t)) hConc t = slimH2 u t"
by (induct_tac t rule: T_induct, simp_all)
lemma slimH2_addH2[simp]: "slimH2 u (addH2 h2 t) = addH2 u t"
by simp
lemma headers_slimH2[simp]: "headers (slimH2 u t) = headers t"
by (induct_tac t rule: T_induct, simp_all)
lemma regSkelOuter2_slimH2[simp]:
"regSkelOuter2 (slimH2 u t) = Some (headers t, singleton u)"
by (induct_tac t rule: T_induct, simp_all)
lemma slimH2_tFold_hConc[simp]:
"slimH2 u (tFold f hConc t) = tFold (% h t . slimH2 u (f h t)) hConc t"
by (induct_tac t rule: T_induct, simp_all del: slimH2_def)
lemma slimH2_tFold_addH2_hConc[simp]:
"slimH2 u (tFold (% h . addH2 v) hConc t) = tFold (% h . addH2 u) hConc t"
by (induct_tac t rule: T_induct, simp_all del: slimH2_def)
lemma del1_slimH2_isConst[simp]:
"delH1 (slimH2 u (t1 :: ('a, ('b, unit) T) T)) = delH1 (slimH2 u t2)"
by simp
lemma tFold_slimH2:
"assoc c \<Longrightarrow> tFold a c (slimH2 u t) = tFold (% h0 t0 . a h0 (slimH1 u t0)) c t"
by (induct_tac t rule: T_induct, simp_all)
consts slimH3 :: "'c \<Rightarrow> ('a, ('b, ('e , 'd) T) T) T \<Rightarrow> ('a, ('b, ('c, 'd) T) T) T"
defs slimH3_def: "slimH3 == tMap \<circ> slimH2"
lemma slimH3_expand: "slimH3 u t = addH3 u (delH3 t)"
by (induct_tac t rule: T_induct, simp_all add: delH3_def addH3_def slimH3_def)
lemma slimH3_addH[simp]: "slimH3 u (addH h t) = addH h (slimH2 u t)"
by (simp add: slimH3_def del: slimH2_def)
lemma slimH3_hConc[simp]: "slimH3 u (hConc t1 t2) = hConc (slimH3 u t1) (slimH3 u t2)"
by (simp add: slimH3_def del: slimH2_def)
lemma spread1_slimH2: "spread1 hs (slimH2 u t) = slimH3 u (spread1 hs t)"
by (induct_tac hs rule: neList_append_induct, simp_all del: slimH2_def slimH3_def)
lemma tFold_slimH3:
"assoc c \<Longrightarrow> tFold a c (slimH3 u t) = tFold (% h0 t0 . a h0 (slimH2 u t0)) c t"
by (induct_tac t rule: T_induct, simp_all del: slimH2_def slimH3_def)
lemma tMap_f_slimH3:
"tMap f (slimH3 u t) = tMap (% t0 . f (slimH2 u t0)) t"
apply (unfold slimH3_def)
apply (unfold comp_def)
apply (subst tMap_tMap)
apply (unfold comp_def)
apply (rule refl)
done
subsection {* Right-Updating Horizontal Concatenation *}
consts hConcU :: "('c \<Rightarrow> ('a,'b) T) \<Rightarrow> ('a,'b) T \<Rightarrow> 'c \<Rightarrow> ('a,'b) T"
defs hConcU_def[simp]: "hConcU u t1 t2 == hConc t1 (u t2)"
lemma hConcU_assoc[simp]:
"\<lbrakk> \<And> t . u (u t) = u t;
\<And> t1 t2 . u (hConc t1 t2) = hConc (u t1) (u t2)
\<rbrakk> \<Longrightarrow> assoc (hConcU u)"
by (rule assoc_intro, simp)
lemma U_hConcU[simp]:
"\<lbrakk> \<And> t . u (u t) = u t;
\<And> t1 t2 . u (hConc t1 t2) = hConc (u t1) (u t2)
\<rbrakk> \<Longrightarrow> u (hConcU u t1 t2) = hConc (u t1) (u t2)"
by simp
lemma U_tFold_hConcU[simp]:
"\<lbrakk> \<And> t . u (u t) = u t;
\<And> t1 t2 . u (hConc t1 t2) = hConc (u t1) (u t2)
\<rbrakk> \<Longrightarrow> u (tFold f (hConcU u) t) = tFold (% h0 t0 . u (f h0 t0)) hConc t"
by (induct_tac t rule: T_induct, simp_all del: hConcU_def)
consts hConcSH2 :: "'b \<Rightarrow> ('a,('b,'c) T) T \<Rightarrow> ('a,('d,'c) T) T \<Rightarrow> ('a,('b,'c) T) T"
defs hConcSH2_def: "hConcSH2 u == hConcU (slimH2 u)"
lemma hConcSH2_assoc[simp]: "assoc (hConcSH2 u)"
by (rule assoc_intro, simp add: hConcSH2_def)
lemma slimH2_hConcSH2[simp]:
"slimH2 u (hConcSH2 u t1 t2) = hConc (slimH2 u t1) (slimH2 u t2)"
by (unfold hConcSH2_def, simp del: slimH2_def)
lemma slimH2_tFold_hConcSH2[simp]:
"slimH2 u (tFold f (hConcSH2 u) t) = tFold (% h t . slimH2 u (f h t)) hConc t"
by (induct_tac t rule: T_induct, simp_all del: slimH2_def)
subsection {* Diagonal Table Concatenation *}
text {* Diagonal concatenation allocates the two last arguments
as blocks on the main diagonal and fills the remainder with
``empty'' tables created using the first argument.
Since we shall use this as combinator of a table fold,
we need its associativity, but that holds only on tables
that are regular in their outer two dimensions.
For this reason we define diagonal concatenation
on the subtype @{text "regT2"}.
*}
consts dConc :: "(('b,'c) T \<Rightarrow> ('b,'c) T) \<Rightarrow>
('a,'b,'c) regT2 \<Rightarrow>
('a,'b,'c) regT2 \<Rightarrow>
('a,'b,'c) regT2"
defs dConc_def: "dConc h t1 t2 ==
let t1' = Rep_regT2 t1;
t2' = Rep_regT2 t2
in Abs_regT2
(hConc (vConc t1' (tMap (const (h (delH1 t2'))) t1'))
(vConc (tMap (const (h (delH1 t1'))) t2') t2' )
)"
lemma dConc[simp]:
"\<lbrakk> regSkelOuter2 t1 = Some (cs1, hs1);
regSkelOuter2 t2 = Some (cs2, hs2)
\<rbrakk> \<Longrightarrow>
dConc h (Abs_regT2 t1) (Abs_regT2 t2)
= Abs_regT2
(hConc (vConc t1 (tMap (const (h (delH1 t2))) t1))
(vConc (tMap (const (h (delH1 t1))) t2) t2)
)"
apply (unfold dConc_def, simp only: Let_def regT2_def)
apply (subst Abs_regT2_inverse, simp add: regT2_def, fast)+
apply simp
done
lemma dConc1:
"\<lbrakk> regSkelOuter2 (Rep_regT2 t1) = Some (cs1, hs1);
regSkelOuter2 (Rep_regT2 t2) = Some (cs2, hs2)
\<rbrakk> \<Longrightarrow>
dConc h t1 t2
= Abs_regT2
(hConc (vConc (Rep_regT2 t1) (tMap (const (h (delH1 (Rep_regT2 t2)))) (Rep_regT2 t1)))
(vConc (tMap (const (h (delH1 (Rep_regT2 t1)))) (Rep_regT2 t2)) (Rep_regT2 t2))
)"
apply (frule_tac h=h and "t2.0"="Rep_regT2 t2" in dConc, assumption)
apply (simp only: Rep_regT2_inverse)
done
lemma regSkelOuter2_dConcDef[simp]:
"\<lbrakk> \<And> t . headers (h t) = headers t;
regSkelOuter2 t1 = Some (cs1, hs1);
regSkelOuter2 t2 = Some (cs2, hs2)
\<rbrakk> \<Longrightarrow>
regSkelOuter2
(hConc (vConc t1 (tMap (const (h (delH1 t2))) t1))
(vConc (tMap (const (h (delH1 t1))) t2) t2))
= Some (append cs1 cs2, append hs1 hs2)"
apply (rotate_tac -1, frule regSkelOuter2_eq_Some)
apply (rotate_tac -2, frule regSkelOuter2_eq_Some)
apply (cut_tac "t1.0"="t1" and "t2.0"="tMap (const (h (delH1 t2))) t1" in regSkelOuter2_vConc)
apply assumption
apply (simp (no_asm_simp))
apply (rule conjI)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (rotate_tac -1, frule regSkelOuter2_eq_Some)
apply (cut_tac "t1.0"="tMap (const (h (delH1 t1))) t2" and "t2.0"="t2" in regSkelOuter2_vConc)
apply (simp (no_asm_simp))
apply (rule conjI)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply (simp (no_asm_simp))
apply (rotate_tac -1, frule regSkelOuter2_eq_Some)
apply (simp (no_asm_simp))
apply (subst headers_delH1__reg2, assumption)
apply (subst headers_delH1__reg2, assumption)
apply (simp (no_asm_simp))
done
lemma regSkelOuter2_dConc[simp]:
"\<lbrakk> \<And> t . headers (h t) = headers t;
regSkelOuter2 t1 = Some (cs1, hs1);
regSkelOuter2 t2 = Some (cs2, hs2)
\<rbrakk> \<Longrightarrow>
regSkelOuter2 (Rep_regT2 (dConc h (Abs_regT2 t1) (Abs_regT2 t2)))
= Some (append cs1 cs2, append hs1 hs2)"
apply (subst dConc)
apply assumption
apply assumption
apply (subst Abs_regT2_inverse, rule regT2)
apply (subst regSkelOuter2_dConcDef)
apply simp
apply assumption
apply assumption
apply simp
apply (rule conjI, simp, simp)
apply (subst regSkelOuter2_dConcDef)
apply simp
apply assumption
apply assumption
apply simp
done
lemma dConc2[simp]:
"\<lbrakk> \<And> t . headers (h t) = headers t;
regSkelOuter2 (Rep_regT2 t1) = Some (cs1, hs1);
regSkelOuter2 (Rep_regT2 t2) = Some (cs2, hs2)
\<rbrakk> \<Longrightarrow>
Rep_regT2 (dConc h t1 t2)
= hConc (vConc (Rep_regT2 t1) (tMap (const (h (delH1 (Rep_regT2 t2)))) (Rep_regT2 t1)))
(vConc (tMap (const (h (delH1 (Rep_regT2 t1)))) (Rep_regT2 t2)) (Rep_regT2 t2))"
apply (subst dConc1)
apply assumption+
apply (subst Abs_regT2_inverse, rule regT2)
apply (subst regSkelOuter2_dConcDef)
apply simp
apply assumption
apply assumption
apply simp
apply (rule conjI, simp, simp)
apply (simp del: const)
done
lemma regSkelOuter2_dConc1[simp]:
"\<lbrakk> \<And> t . headers (h t) = headers t;
regSkelOuter2 (Rep_regT2 t1) = Some (cs1, hs1);
regSkelOuter2 (Rep_regT2 t2) = Some (cs2, hs2)
\<rbrakk> \<Longrightarrow>
regSkelOuter2 (Rep_regT2 (dConc h t1 t2))
= Some (append cs1 cs2, append hs1 hs2)"
apply (subst dConc2)
apply simp
apply assumption
apply assumption
apply (subst regSkelOuter2_dConcDef)
apply simp
apply assumption
apply assumption
apply simp
done
lemma headers_dConc[simp]:
"\<lbrakk> \<And> t . headers (h t) = headers t
\<rbrakk> \<Longrightarrow>
headers (Rep_regT2 (dConc h t1 t2)) = append (headers (Rep_regT2 t1)) (headers (Rep_regT2 t2))"
apply (cut_tac x=t1 in Rep_regT2)
apply (cut_tac x=t2 in Rep_regT2)
apply (simp add: regT2_def)
apply (drule regularOuter2, erule exE, erule exE)
apply (drule regularOuter2, erule exE, erule exE)
apply (subst dConc2)
apply simp
apply assumption
apply assumption
apply simp
apply (subst headers_vConc)
apply simp
apply (rule conjI)
apply simp
apply simp
apply simp
apply (rule conjI)
apply (rule sym, simp)
apply simp
apply (subst headers_vConc)
apply simp
apply (rule conjI)
apply simp
apply simp
apply (simp del: const)
apply (simp del: const)
done
lemma reg2dim2_dConc[simp]:
"\<lbrakk> \<And> t . headers (h t) = headers t;
regSkelOuter2 (Rep_regT2 t1) = Some (cs1, hs1);
regSkelOuter2 (Rep_regT2 t2) = Some (cs2, hs2)
\<rbrakk> \<Longrightarrow>
reg2dim2 (dConc h t1 t2) = append hs1 hs2"
apply (cut_tac h=h and "t1.0"="Rep_regT2 t1" and "t2.0"="Rep_regT2 t2" in regSkelOuter2_dConc)
apply (simp (no_asm_simp))
apply assumption+
apply (simp only: Rep_regT2_inverse)
apply (subst Rep_regT2_inverse [THEN sym])
apply (rule reg2dim2)
apply assumption
done
lemma cs_dConc[simp]:
"\<lbrakk> \<And> t . headers (h t) = headers t;
\<And> t . h (h t) = h t;
\<And> t1 t2 . h (hConc t1 t2) = hConc (h t1) (h t2);
regSkelOuter2 (Rep_regT2 t1) = Some (cs1, hs1);
regSkelOuter2 (Rep_regT2 t2) = Some (cs2, hs2)
\<rbrakk> \<Longrightarrow>
h (delH1 (Rep_regT2 (dConc h t1 t2))) =
hConc (h (delH1 (Rep_regT2 t1)))
(h (delH1 (Rep_regT2 t2)))"
apply (cut_tac h=h and "t1.0"="Rep_regT2 t1" and "t2.0"="Rep_regT2 t2" in regSkelOuter2_dConc)
apply (simp (no_asm_simp))
apply assumption+
apply (subst dConc1)
apply assumption+
apply (subst Abs_regT2_inverse, rule regT2)
apply (subst regSkelOuter2_dConcDef)
apply simp
apply assumption
apply assumption
apply (simp (no_asm_simp))
apply (rule conjI)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (subst delH1_vConc)
apply (simp (no_asm_simp))
apply (rule conjI)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (rule conjI)
apply (rule sym, simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp del: const)
done
lemma dConc_assoc[simp]:
"\<lbrakk> \<And> t . headers (h t) = headers t;
\<And> t . h (h t) = h t;
\<And> t1 t2 . h (hConc t1 t2) = hConc (h t1) (h t2)
\<rbrakk> \<Longrightarrow> assoc (dConc h)"
apply (rule assoc_intro)
apply (cut_tac x=x in Rep_regT2)
apply (cut_tac x=y in Rep_regT2)
apply (cut_tac x=z in Rep_regT2)
apply (simp add: regT2_def)
apply (drule regularOuter2, erule exE, erule exE)
apply (drule regularOuter2, erule exE, erule exE)
apply (drule regularOuter2, erule exE, erule exE)
apply (cut_tac h=h and "t1.0"="Rep_regT2 x" and "t2.0"="Rep_regT2 y" in regSkelOuter2_dConc)
apply (simp (no_asm_simp))
apply assumption+
apply (cut_tac h=h and "t1.0"="Rep_regT2 y" and "t2.0"="Rep_regT2 z" in regSkelOuter2_dConc)
apply (simp (no_asm_simp))
apply assumption+
apply (simp only: Rep_regT2_inverse)
apply (cut_tac h=h and "t1.0"="Rep_regT2 (dConc h x y)" and "t2.0"="Rep_regT2 z" in regSkelOuter2_dConc)
apply (simp (no_asm_simp))
apply assumption+
apply (cut_tac h=h and "t1.0"="Rep_regT2 x" and "t2.0"="Rep_regT2 (dConc h y z)" in regSkelOuter2_dConc)
apply (simp (no_asm_simp))
apply assumption+
apply (simp only: Rep_regT2_inverse)
apply (rotate_tac -1, frule regSkelOuter2_eq_Some)
apply (rotate_tac -1, frule regSkelOuter2_eq_Some)
apply (rotate_tac -1, frule regSkelOuter2_eq_Some)
apply (rotate_tac -1, frule regSkelOuter2_eq_Some)
apply (rotate_tac -1, frule regSkelOuter2_eq_Some)
apply (rotate_tac -1, frule regSkelOuter2_eq_Some)
apply (rotate_tac -1, frule regSkelOuter2_eq_Some)
apply (cut_tac h=h and "t1.0"="dConc h x y" and "t2.0"="z" in dConc1)
apply assumption
apply assumption
apply (cut_tac h=h and "t1.0"="x" and "t2.0"="dConc h y z" in dConc1)
apply assumption
apply assumption
apply (simp (no_asm_simp))
apply (subst cs_dConc [of h])
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply assumption
apply (subst cs_dConc [of h])
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply assumption
apply (subst dConc2 [of h])
apply (simp (no_asm_simp))
apply assumption
apply assumption
apply (subst dConc2 [of h])
apply (simp (no_asm_simp))
apply assumption
apply assumption
txt {* Lots of preparations *}
apply (frule_tac t="Rep_regT2 x" in reg2dim2)
apply (frule_tac t="Rep_regT2 y" in reg2dim2)
apply (frule_tac t="Rep_regT2 z" in reg2dim2)
apply (simp only: Rep_regT2_inverse)
apply (cut_tac "t1.0"="Rep_regT2 y" and "t2.0"="(tMap (const (h (delH1 (Rep_regT2 z)))) (Rep_regT2 y))" in regSkelOuter2_vConc)
apply assumption
apply (simp (no_asm_simp))
apply (rule conjI)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (rule sym, simp (no_asm_simp))
apply (rotate_tac -1, frule regSkelOuter2_eq_Some)
apply (cut_tac "t1.0"="(tMap (const (h (delH1 (Rep_regT2 y)))) (Rep_regT2 z))" and "t2.0"="Rep_regT2 z" in regSkelOuter2_vConc)
apply (simp (no_asm_simp))
apply (rule conjI)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply (simp (no_asm_simp))
apply (rotate_tac -1, frule regSkelOuter2_eq_Some)
apply (cut_tac "t1.0"="Rep_regT2 x" and "t2.0"="(tMap (const (h (delH1 (Rep_regT2 y)))) (Rep_regT2 x))" in regSkelOuter2_vConc)
apply assumption
apply (simp (no_asm_simp))
apply (rule conjI)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (rule sym, simp (no_asm_simp))
apply (rotate_tac -1, frule regSkelOuter2_eq_Some)
apply (cut_tac "t1.0"="(tMap (const (h (delH1 (Rep_regT2 x)))) (Rep_regT2 y))" and "t2.0"="Rep_regT2 y" in regSkelOuter2_vConc)
apply (simp (no_asm_simp))
apply (rule conjI)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply (simp (no_asm_simp))
apply (rotate_tac -1, frule regSkelOuter2_eq_Some)
txt {* end of preparations *}
txt {* The remainder is rewriting to normal form with @{text "vConc_hConc"}. *}
apply (simp (no_asm_simp) del: const)
apply (subst vConc_hConc)
apply (simp (no_asm_simp))
apply (rule conjI)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply (simp (no_asm_simp))
apply (subst headers_delH1__reg2, assumption)
apply (subst headers_delH1__reg2, assumption)
apply (simp (no_asm_simp))
apply (subst vConc_hConc)
apply assumption
apply (simp (no_asm_simp) del: const)
apply (rule conjI)
apply (simp (no_asm_simp))
apply (subst headers_delH1__reg2, assumption)
apply (subst headers_delH1__reg2, assumption)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp) del: const)
apply (simp (no_asm_simp) del: const)
apply (simp (no_asm_simp) del: const)
apply (subst tMap_const_vConc)
apply (simp (no_asm_simp) del: const)
apply (rule conjI)
apply (simp (no_asm_simp))
apply (subst headers_delH1__reg2, assumption)
apply (simp (no_asm_simp))
apply assumption
apply (simp (no_asm_simp))
apply (subst tMap_const_vConc)
apply (simp (no_asm_simp) del: const)
apply (rule conjI)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp) del: const)
apply (rule conjI)
apply (simp (no_asm_simp))
apply (subst headers_delH1__reg2, assumption)
apply (simp (no_asm_simp))
apply (rule sym, simp (no_asm_simp))
apply (subst tMap_const_vConc)
apply (simp (no_asm_simp) del: const)
apply (rule conjI)
apply (simp (no_asm_simp))
apply (subst headers_delH1__reg2, assumption)
apply (simp (no_asm_simp))
apply assumption
apply (simp (no_asm_simp))
apply (subst tMap_const_vConc)
apply (simp (no_asm_simp) del: const)
apply (rule conjI)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp) del: const)
apply (rule conjI)
apply (simp (no_asm_simp))
apply (subst headers_delH1__reg2, assumption)
apply (simp (no_asm_simp))
apply (rule sym, simp (no_asm_simp))
apply (subst tMap_const_hConc)+
apply (simp (no_asm_simp) del: const)
done
subsection {* Lifting of Inversion Combinators to the Next Dimension *}
text {* The initial inversion operator is @{text "addH2"},
as used in the definition of @{text "inverse1"}.
The first argument @{text "u"} is the contents of ``empty'' cells
created by inversion.
The second argument @{text "h"} converts @{text "u"}
into an update function for @{text "dConc"},
and the third argument @{text "g"} is the
inversion operator of the next-lower dimension.
*}
consts invLift0 ::
"'a \<Rightarrow>
('a \<Rightarrow> ('e,'d) T \<Rightarrow> ('e,'d) T) \<Rightarrow>
('a \<Rightarrow> 'b \<Rightarrow> ('c,'d) T) \<Rightarrow>
('a \<Rightarrow> ('e,'b) T \<Rightarrow> ('c,'e,'d) regT2)"
defs invLift0_def:
"invLift0 u h g h1 ==
tFold (% h2 t2 . Abs_regT2 (addH2 h2 (g h1 t2))) (dConc (h u))"
lemma invLift0_addH[simp]:
"invLift0 u h g h1 (addH h2 t2) = Abs_regT2 (addH2 h2 (g h1 t2))"
by (unfold invLift0_def, simp)
lemma invLift0_addH1[simp]:
"Rep_regT2 (invLift0 u h g h1 (addH h2 t2)) = addH2 h2 (g h1 t2)"
apply simp
apply (subst Abs_regT2_inverse, rule regT2, simp)
apply (rule conjI, simp_all)
done
lemma reg2dim2_invLift0_addH[simp]:
"reg2dim2 (invLift0 u h g h1 (addH h2 t2)) = singleton h2"
by simp
lemma cs_invLift0_addH[simp]:
"\<lbrakk> \<And> u v t . h u (g v t) = g u t \<rbrakk> \<Longrightarrow>
h u (delH2 (Rep_regT2 (invLift0 u h g h1 (addH h2 t2)))) = g u t2"
apply simp
apply (subst Abs_regT2_inverse, rule regT2, simp)
apply (rule conjI, simp_all)
done
lemma invLift0_hConc[simp]:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t . h u (h u t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2)
\<rbrakk> \<Longrightarrow> invLift0 u h g h1 (hConc t1 t2) =
dConc (h u) (invLift0 u h g h1 t1) (invLift0 u h g h1 t2)"
by (unfold invLift0_def, simp)
lemma reg2dim2_invLift0:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t . h u (h u t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2);
\<And> x t . headers (g x t) = headers t \<rbrakk> \<Longrightarrow>
reg2dim2 (invLift0 u h g h1 t) = headers t"
apply (unfold invLift0_def, induct_tac t rule: T_induct, simp_all)
apply (fold invLift0_def)
apply (cut_tac x="invLift0 u h g h1 t1" in Rep_regT2)
apply (cut_tac x="invLift0 u h g h1 t2" in Rep_regT2)
apply (subst reg2dim2_dConc)
apply simp
apply (simp add: regT2_def)
apply (drule regularOuter2, erule exE, erule exE, simp)
apply (rule conjI)
apply (rule sym, erule regSkelOuter2_eq_Some)
apply (drule reg2dim2)
apply (rule sym, assumption)
apply (simp add: regT2_def)
apply (rotate_tac -1, drule regularOuter2, erule exE, erule exE, simp)
apply (rule conjI)
apply (rule sym, erule regSkelOuter2_eq_Some)
apply (drule reg2dim2)
apply (rule sym, assumption)
apply (simp add: Rep_regT2_inverse)
done
lemma regSkelOuter2_invLift0_EX:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t . h u (h u t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2);
\<And> x y t . headers (g x t) = headers (g y t) \<rbrakk> \<Longrightarrow>
EX hs1 .
regSkelOuter2 (Rep_regT2 (invLift0 u h g h1 t)) = Some (hs1, headers t)"
apply (unfold invLift0_def, induct_tac t rule: T_induct, simp_all)
apply (subst Abs_regT2_inverse, rule regT2, simp)
apply (rule conjI)
apply simp
apply simp
apply simp
apply (fold invLift0_def)
apply (erule exE, erule exE)
apply (subst regSkelOuter2_dConc1)
apply simp
apply assumption
apply assumption
apply (rule_tac x="append hs1 hs1a" in exI, simp)
done
lemma cs_invLift0_hConc[simp]:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t . h u (h u t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2)
\<rbrakk> \<Longrightarrow>
h u (delH1 (Rep_regT2 (invLift0 u h g h1 (hConc t1 t2)))) =
hConc (h u (delH1 (Rep_regT2 (invLift0 u h g h1 t1))))
(h u (delH1 (Rep_regT2 (invLift0 u h g h1 t2))))"
apply (cut_tac x="invLift0 u h g h1 t1" in Rep_regT2)
apply (cut_tac x="invLift0 u h g h1 t2" in Rep_regT2)
apply (simp add: regT2_def)
apply (drule regularOuter2, erule exE, erule exE)
apply (drule regularOuter2, erule exE, erule exE)
apply (subst cs_dConc [of "h u"])
apply simp
apply simp
apply simp
apply simp
apply (rule conjI)
apply simp
apply simp
apply simp
apply (rule conjI)
apply simp
apply simp
apply simp
done
consts invLift ::
"'a \<Rightarrow>
('a \<Rightarrow> ('e,'d) T \<Rightarrow> ('e,'d) T) \<Rightarrow>
('a \<Rightarrow> 'b \<Rightarrow> ('c,'d) T) \<Rightarrow>
('a \<Rightarrow> ('e,'b) T \<Rightarrow> ('c,('e,'d) T) T)"
defs invLift_def: "invLift u h g h1 t == Rep_regT2 (invLift0 u h g h1 t)"
lemma invLift_addH[simp]:
"\<lbrakk> \<And> x y t . headers (g x t) = headers (g y t) \<rbrakk> \<Longrightarrow>
invLift u h g h1 (addH h2 t2) = addH2 h2 (g h1 t2)"
apply (unfold invLift_def, simp)
apply (subst Abs_regT2_inverse, simp_all add: regT2_def)
apply (rule regularOuter2I, auto)
done
lemma headers_invLift0_invariant:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t . h u (h u t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2);
\<And>x y t. headers (g x t) = headers (g y t) \<rbrakk> \<Longrightarrow>
headers (Rep_regT2 (invLift0 u h g x t)) =
headers (Rep_regT2 (invLift0 u h g y t))"
apply (induct_tac t rule: T_induct)
apply (subst invLift0_addH1)
apply (subst invLift0_addH1)
apply simp
apply simp
done
text {* The following lemma justifies the build-up
for higher-dimensional inversion functions. *}
lemma headers_invLift_invariant:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t . h u (h u t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2);
\<And> x y t . headers (g x t) = headers (g y t) \<rbrakk> \<Longrightarrow>
headers (invLift u h g x t) = headers (invLift u h g y t)"
apply (unfold invLift_def)
apply (cut_tac x="invLift0 u h g x t" in Rep_regT2)
apply (cut_tac x="invLift0 u h g y t" in Rep_regT2)
apply (unfold regT2_def, simp)
apply (drule regularOuter2, erule exE, erule exE)
apply (drule regularOuter2, erule exE, erule exE)
apply (drule regSkelOuter2_eq_Some)
apply (drule regSkelOuter2_eq_Some)
apply (rule headers_invLift0_invariant)
apply simp_all
done
lemma invLift_hConc[simp]:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t . h u (h u t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2);
\<And> x y t . headers (g x t) = headers (g y t);
regSkelOuter2 (invLift u h g h1 t1) = Some (hs1a, hs2a);
regSkelOuter2 (invLift u h g h1 t2) = Some (hs1b, hs2b)
\<rbrakk> \<Longrightarrow>
invLift u h g h1 (hConc t1 t2) =
hConc (vConc (invLift u h g h1 t1)
(tMap (const (h u (delH1 (invLift u h g h1 t2)))) (invLift u h g h1 t1)))
(vConc (tMap (const (h u (delH1 (invLift u h g h1 t1)))) (invLift u h g h1 t2))
(invLift u h g h1 t2))"
apply (unfold invLift_def, simp)
apply (subst dConc2 [THEN sym], auto)
done
lemma regSkelOuter2_invLift_EX:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t . h u (h u t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2);
\<And> x y t . headers (g x t) = headers (g y t) \<rbrakk> \<Longrightarrow>
EX hs1 . regSkelOuter2 (invLift u h g h1 t) = Some (hs1, headers t)"
apply (unfold invLift_def)
apply (rule regSkelOuter2_invLift0_EX)
apply simp_all
done
lemma delH1_invLift:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t . h u (h u t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2);
\<And> x y t . headers (g x t) = headers (g y t)
\<rbrakk> \<Longrightarrow>
delH1 (invLift u h g v t) = tFold (% h0 t0 . addH h0 (delH1 (g v t0))) (hConcU (h u)) t"
apply (induct_tac t rule: T_induct, simp_all del: const)
apply (cut_tac u=u and h=h and g=g and "h1.0"=v and t=t1 in regSkelOuter2_invLift_EX)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (erule exE)
apply (cut_tac u=u and h=h and g=g and "h1.0"=v and t=t2 in regSkelOuter2_invLift_EX)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (erule exE)
apply (subst invLift_hConc)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply assumption
apply (simp (no_asm_simp))
apply (subst delH1_vConc)
apply assumption
apply (simp (no_asm_simp))
apply (rule conjI, simp (no_asm_simp), simp (no_asm_simp))
apply (subst delH1_tMap_const)
apply (simp (no_asm_simp))
apply (fold hConcU_def)
apply (cut_tac u="h u" in hConcU_assoc)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp del: hConcU_def)
done
lemma h_u_delH1_invLift:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t x . h u (h x t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2);
\<And> x y t . headers (g x t) = headers (g y t);
\<And> h0 t0 . h u (addH h0 (delH1 (g v t0))) = addH h0 (delH1 (g u t0))
\<rbrakk> \<Longrightarrow>
h u (delH1 (invLift u h g v t)) = tFold (% h0 t0 . addH h0 (delH1 (g u t0))) hConc t"
apply (subst delH1_invLift)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
done
lemma headers_h_u_delH1_invLift[simp]:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t x . h u (h x t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2);
\<And> x y t . headers (g x t) = headers (g y t);
\<And> h0 t0 . h u (addH h0 (delH1 (g v t0))) = addH h0 (delH1 (g u t0))
\<rbrakk> \<Longrightarrow>
headers (h u (delH1 (invLift u h g v t))) = headers t"
apply (subst h_u_delH1_invLift [of h u g v t])
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (subst headers_def)
apply (simp (no_asm_simp))
done
lemma headers_delH1_invLift[simp]:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t x . h u (h x t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2);
\<And> x y t . headers (g x t) = headers (g y t);
\<And> h0 t0 . h u (addH h0 (delH1 (g v t0))) = addH h0 (delH1 (g u t0))
\<rbrakk> \<Longrightarrow>
headers (delH1 (invLift u h g v t)) = headers t"
apply (cut_tac headers_h_u_delH1_invLift [of h u g v t])
apply simp
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
done
lemma regSkelOuter2_dConcFill:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t x . h u (h x t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2);
\<And> x y t . headers (g x t) = headers (g y t);
regSkelOuter2 (invLift u h g h1 t1) = Some (hs1a, hs2a);
regSkelOuter2 (invLift u h g h1 t2) = Some (hs1b, hs2b)
\<rbrakk> \<Longrightarrow>
regSkelOuter2 (tMap (const (h u (delH1 (invLift u h g h1 t2))))
(invLift u h g h1 t1)) = Some (hs1a,hs2b)"
apply (cut_tac "t2.0"="h u (delH1 (invLift u h g h1 t2))" and "t1.0"="invLift u h g h1 t1" in regSkelOuter2_tMap_const)
apply simp
done
lemma headers_invLift_hConc[simp]:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t x . h u (h x t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2);
\<And> x y t . headers (g x t) = headers (g y t);
regSkelOuter2 (invLift u h g h1 t1) = Some (hs1a, hs2a);
regSkelOuter2 (invLift u h g h1 t2) = Some (hs1b, hs2b)
\<rbrakk> \<Longrightarrow>
headers (invLift u h g h1 (hConc t1 t2)) =
append (headers (invLift u h g h1 t1))
(headers (invLift u h g h1 t2))"
apply (subst invLift_hConc)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply assumption
apply (cut_tac h=h and u=u and g=g and "h1.0"=h1 and
"t1.0"=t1 and hs1a=hs1a and hs2a=hs2a and
"t2.0"=t2 and hs1b=hs1b and hs2b=hs2b in regSkelOuter2_dConcFill)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply assumption
apply (cut_tac h=h and u=u and g=g and "h1.0"=h1 and
"t1.0"=t2 and hs1a=hs1b and hs2a=hs2b and
"t2.0"=t1 and hs1b=hs1a and hs2b=hs2a in regSkelOuter2_dConcFill)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply assumption
apply (simp (no_asm_simp))
apply (subst headers_vConc)
apply assumption
apply assumption
apply (subst headers_vConc)
apply assumption
apply assumption
apply (simp (no_asm_simp))
done
lemma headers_invLift[simp]:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t x . h u (h x t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2);
\<And> x y t . headers (g x t) = headers (g y t)
\<rbrakk> \<Longrightarrow>
headers (invLift u h g h1 t) = tFold (% h2 t2 . headers (g h1 t2)) append t"
apply (induct_tac t rule: T_induct, simp)
apply (cut_tac u=u and h=h and g=g and "h1.0"=h1 and t=t1 in regSkelOuter2_invLift_EX)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (erule exE)
apply (cut_tac u=u and h=h and g=g and "h1.0"=h1 and t=t2 in regSkelOuter2_invLift_EX)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (erule exE)
apply (subst headers_invLift_hConc)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply assumption
apply (simp (no_asm_simp))
done
lemma regSkelOuter2_invLift[simp]:
"\<lbrakk> \<And> t . headers (h u t) = headers t;
\<And> t x . h u (h x t) = h u t;
\<And> t1 t2 . h u (hConc t1 t2) = hConc (h u t1) (h u t2);
\<And> x y t . headers (g x t) = headers (g y t);
\<And> h0 t0 . h u (addH h0 (delH1 (g h1 t0))) = addH h0 (delH1 (g u t0))
\<rbrakk> \<Longrightarrow>
regSkelOuter2 (invLift u h g h1 t) =
Some (tFold (% h2 t2 . headers (g h1 t2)) append t, headers t)"
apply (induct_tac t rule: T_induct, simp)
apply (cut_tac u=u and h=h and g=g and "h1.0"=h1 and t=t1 in regSkelOuter2_invLift_EX)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (erule exE)
apply (cut_tac u=u and h=h and g=g and "h1.0"=h1 and t=t2 in regSkelOuter2_invLift_EX)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (erule exE)
apply (subst invLift_hConc)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply assumption
apply (subst regSkelOuter2_hConc)
apply (cut_tac h=h and u=u and g=g and "h1.0"=h1 and
"t1.0"=t1 and hs1a=hs1 and hs2a="headers t1" and
"t2.0"=t2 and hs1b=hs1a and hs2b="headers t2" in regSkelOuter2_dConcFill)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply assumption
apply (cut_tac h=h and u=u and g=g and "h1.0"=h1 and
"t1.0"=t2 and hs1a=hs1a and hs2a="headers t2" and
"t2.0"=t1 and hs1b=hs1 and hs2b="headers t1" in regSkelOuter2_dConcFill)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply assumption
apply (subst regSkelOuter2_vConc)
apply (simp (no_asm_simp))
apply (rule conjI)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply (simp (no_asm_simp))
apply (subst regSkelOuter2_vConc)
apply assumption
apply (simp (no_asm_simp))
apply (rule conjI)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
done
subsection {* The Inversion Operator for Two Dimensions *}
consts invOp2 :: "'a \<Rightarrow> 'a \<Rightarrow> ('b,('c,'d) T) T \<Rightarrow> ('c,('b,('a,'d) T) T) T"
defs invOp2_def: "invOp2 u == invLift u slimH2 addH2"
lemma delH1_invOp2:
"delH1 (invOp2 u v t) = tFold (% h t . addH h (slimH1 v t)) (hConcSH2 u) t"
apply (unfold invOp2_def)
apply (subst delH1_invLift)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp del: tFold_hConc hConcU_def slimH2_def)
apply (fold hConcSH2_def)
apply (rule refl)
done
lemma headers_invOp2[simp]:
"headers (invOp2 u v t) = tFold (% h . headers) append t"
apply (unfold invOp2_def)
apply (subst headers_invLift)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
done
lemma cs_invOp2[simp]:
"slimH2 u (delH1 (invOp2 u v t)) = tFold (% h t . addH h (slimH1 u t)) hConc t"
apply (subst delH1_invOp2)
apply (induct_tac t rule: T_induct, simp_all del: slimH2_def)
done
lemma regSkelOuter2_invOp2:
"regSkelOuter2 (invOp2 u h1 t) = Some (tFold (% h . headers) append t, headers t)"
apply (cut_tac u=u and h=slimH2 and g=addH2 and "h1.0"=h1 and t=t in regSkelOuter2_invLift)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (fold invOp2_def)
apply (simp (no_asm_simp))
done
lemma invOp2_hConc[simp]:
"\<lbrakk>regSkelOuter2 (invOp2 u h1 t1) = Some (hs1a, hs2a);
regSkelOuter2 (invOp2 u h1 t2) = Some (hs1b, hs2b)
\<rbrakk> \<Longrightarrow>
invOp2 u h1 (hConc t1 t2) =
hConc (vConc (invOp2 u h1 t1)
(spread1 hs1a (slimH2 u t2)))
(vConc (spread1 hs1b (slimH2 u t1))
(invOp2 u h1 t2))"
apply (unfold invOp2_def, subst invLift_hConc)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply assumption
apply (fold invOp2_def)
apply (subst cs_invOp2)
apply (subst cs_invOp2)
apply (simp (no_asm_simp))
apply (subst tMap_CONST__headers)
apply (subst tMap_CONST__headers)
apply (subst regSkelOuter2_eq_Some [of "invOp2 u h1 t1" hs1a hs2a])
apply assumption
apply (subst regSkelOuter2_eq_Some [of "invOp2 u h1 t2"])
apply assumption
apply (fold slimH2_def)
apply (unfold spread1_def)
apply (fold slimH1_def)
apply (simp (no_asm_simp) only: slimH2_as_tFold)
done
subsection {* Two-Dimensional Inversion *}
consts inverse2 :: "'a \<Rightarrow> ('a,('b,('c,'d) T) T) T
\<Rightarrow> ('c,('b,('a,'d) T) T) T"
defs inverse2_def: "inverse2 u == tFold (invLift u slimH2 addH2) hConc"
lemma inverse2_addH[simp]: "inverse2 u (addH h t) = invLift u slimH2 addH2 h t"
by (unfold inverse2_def, simp)
lemma inverse2_hConc[simp]:
"inverse2 u (hConc t1 t2) = hConc (inverse2 u t1) (inverse2 u t2)"
by (unfold inverse2_def, simp)
lemma tFold_tFold_tFold_inverse2:
"\<lbrakk> assoc c2; assoc c3; assoc c1; assoc c5; assoc c6;
\<And> h ha hb t . a4 hb (a5 ha (a6 h t)) = a1 h (a2 ha (a3 hb t));
\<And> h ha t1 t2 .
c1 (a1 h (a2 ha t1)) (a1 h (a2 ha t2)) = a1 h (a2 ha (c3 t1 t2));
(* The next two are for tFold_tFold_vConc: *)
\<And> x y z . a4 x (c5 y z) = c5 (a4 x y) (a4 x z);
\<And> x1 x2 y1 y2 . c1 (c5 x1 y1) (c5 x2 y2) = c5 (c1 x1 x2) (c1 y1 y2);
(* units: *)
\<And> x . LRunit c1 (a1 u x);
\<And> x y . LRunit c5 (a5 y (a6 u x));
\<And> x y z . LRunit c1 (a1 z (a5 y (a6 u x)));
(* finishing 1.2: *)
\<And> h x1 x2 . c5 (a1 h x1) (a1 h x2) = a1 h (c2 x1 x2)
\<rbrakk> \<Longrightarrow>
tFold a4 c1 (tMap (tFold a5 c5 o (tMap (tFold a6 c6))) (inverse2 u t)) =
tFold a1 c1 (tMap (tFold a2 c2 o (tMap (tFold a3 c3))) t)"
apply (induct_tac t rule: T_induct)
txt {* 1: @{text "addH h t0"} *}
apply (induct_tac t0 rule: T_induct)
txt {* 1.1: @{text "t0 = addH ha t0a"} *}
apply (induct_tac t0a rule: T_induct, simp)
txt {* 1.1.2: @{text "t0a = hConc t1 t2"} *}
apply simp
txt {* 1.2: @{text "t0 = hConc t1 t2"} *}
apply (simp del: slimH2_def tFold_tMap)
apply (fold invOp2_def)
apply (cut_tac u=u and "h1.0"=h and t=t1 in regSkelOuter2_invOp2)
apply (cut_tac u=u and "h1.0"=h and t=t2 in regSkelOuter2_invOp2)
apply (subst invOp2_hConc)
apply assumption
apply assumption
apply (subgoal_tac "ALL t . tFold a5 c5 (tMap (tFold a6 c6) t) =
tFold (\<lambda>h t0. a5 h (tFold a6 c6 t0)) c5 t")
prefer 2
apply (rule allI, simp (no_asm_simp))
apply (simp (no_asm_simp) del: slimH2_def tFold_tMap)
apply (subst tFold_tFold_vConc [of c5 c1 a4])
apply assumption
apply assumption
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (rule conjI)
apply (rule refl)
apply (rule refl)
apply assumption
apply (rule refl)
apply (subst tFold_tFold_vConc [of c5 c1 a4])
apply assumption
apply assumption
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply (simp (no_asm_simp) del: slimH2_def)
apply (rule conjI)
apply (rule refl)
apply (rule refl)
apply (rule refl)
apply (simp (no_asm_simp) only: tMap_f_spread1)
apply (simp (no_asm_simp) only: tFold_slimH2 tFold_slimH1)
apply (simp (no_asm_simp) only: f_tFold_const)
apply (simp (no_asm_simp) only: tFold_spread1)
apply (subgoal_tac "(\<lambda>h. a4 h (tFold (\<lambda>h0. tFold (\<lambda>h0a t0. a5 h0 (a6 u t0)) const) c5 t1)) =
(\<lambda>h. a4 h (tFold (\<lambda>h0. tFold (\<lambda>h0a t0. a5 arbitrary (a6 u arbitrary)) const) c5 t1))")
prefer 2
apply (rule ext)
apply (rule_tac f="a4 ha" in arg_cong)
apply (rule_tac x=t1 in fun_cong)
apply (rule_tac x=c5 in fun_cong)
apply (rule_tac f=tFold in arg_cong)
apply (rule ext)
apply (rule fun_cong [of _ _ const])
apply (rule arg_cong [of _ _ tFold])
apply (rule ext)
apply (rule ext)
apply (cut_tac c=c5 and F="%x . a5 x (a6 u t0)" and x=h0 in LRunit_const)
apply (simp (no_asm_simp))
apply (cut_tac c=c5 and F="%x . a5 arbitrary (a6 u x)" and x=t0 in LRunit_const)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (subgoal_tac "(\<lambda>h. a4 h (tFold (\<lambda>h0. tFold (\<lambda>h0a t0. a5 h0 (a6 u t0)) const) c5 t2)) =
(\<lambda>h. a4 h (tFold (\<lambda>h0. tFold (\<lambda>h0a t0. a5 arbitrary (a6 u arbitrary)) const) c5 t2))")
prefer 2
apply (rule ext)
apply (rule_tac f="a4 ha" in arg_cong)
apply (rule_tac x=t2 in fun_cong)
apply (rule_tac x=c5 in fun_cong)
apply (rule_tac f=tFold in arg_cong)
apply (rule ext)
apply (rule fun_cong [of _ _ const])
apply (rule arg_cong [of _ _ tFold])
apply (rule ext)
apply (rule ext)
apply (cut_tac c=c5 and F="%x . a5 x (a6 u t0)" and x=h0 in LRunit_const)
apply (simp (no_asm_simp))
apply (cut_tac c=c5 and F="%x . a5 arbitrary (a6 u x)" and x=t0 in LRunit_const)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (rotate_tac -1, simp (no_asm_simp) del: slimH2_def tFold_tMap)
apply (thin_tac "ALL t . tFold a5 c5 (tMap (tFold a6 c6) t) =
tFold (\<lambda>h t0. a5 h (tFold a6 c6 t0)) c5 t")
apply (subgoal_tac "tFold (\<lambda>h t0. a5 h (tFold a6 c6 t0)) c5 = (% t . tFold a5 c5 (tMap (tFold a6 c6) t))")
prefer 2
apply (rule ext)
apply (subst tFold_tMap)
apply assumption
apply (rule refl)
apply (simp (no_asm_simp) del: tFold_tMap add: o_def)
apply (thin_tac "tFold (\<lambda>h t0. a5 h (tFold a6 c6 t0)) c5 = (% t . tFold a5 c5 (tMap (tFold a6 c6) t))")
apply (simp (no_asm_simp) add: o_def LRunit_left LRunit_right)
txt {* 2: @{text "t = hConc t1 t2"} *}
apply (simp del: slimH2_def tFold_tMap)
done
lemma tFold_tFold_tFold0_inverse2:
"\<lbrakk> assoc c2; assoc c3; assoc c1; assoc c5; assoc c6;
\<And> h ha hb t . a4 hb (a5 ha h) = a1 h (a2 ha hb);
\<And> h ha t1 t2 .
c1 (a1 h (a2 ha t1)) (a1 h (a2 ha t2)) = a1 h (a2 ha (c3 t1 t2));
(* The next two are for tFold_tFold_vConc: *)
\<And> x y z . a4 x (c5 y z) = c5 (a4 x y) (a4 x z);
\<And> x1 x2 y1 y2 . c1 (c5 x1 y1) (c5 x2 y2) = c5 (c1 x1 x2) (c1 y1 y2);
(* units: *)
\<And> x . LRunit c1 (a1 u x);
\<And> x y . LRunit c5 (a5 y u);
\<And> x y z . LRunit c1 (a1 z (a5 y u));
(* finishing 1.2: *)
\<And> h x1 x2 . c5 (a1 h x1) (a1 h x2) = a1 h (c2 x1 x2)
\<rbrakk> \<Longrightarrow>
tFold a4 c1 (tMap (tFold a5 c5 o (tMap (tFold0 c6))) (inverse2 u t)) =
tFold a1 c1 (tMap (tFold a2 c2 o (tMap (tFold0 c3))) t)"
apply (unfold tFold0_def)
apply (rule tFold_tFold_tFold_inverse2)
apply (simp_all (no_asm_simp))
done
text {* Adapting for cells at lowest level: *}
lemma tFold_tFold_tFoldC_inverse2:
"\<lbrakk> assoc c1; assoc c2; assoc c3; assoc c5; assoc c6;
\<And> h ha hb t . a4 hb (a5 ha (a6 h)) = a1 h (a2 ha (a3 hb));
\<And> h ha t1 t2 .
c1 (a1 h (a2 ha t1)) (a1 h (a2 ha t2)) = a1 h (a2 ha (c3 t1 t2));
(* The next two are for tFold_tFold_vConc: *)
\<And> x y z . a4 x (c5 y z) = c5 (a4 x y) (a4 x z);
\<And> x1 x2 y1 y2 . c1 (c5 x1 y1) (c5 x2 y2) = c5 (c1 x1 x2) (c1 y1 y2);
(* units: *)
\<And> x . LRunit c1 (a1 u x);
\<And> x y . LRunit c5 (a5 y (a6 u));
\<And> x y z . LRunit c1 (a1 z (a5 y (a6 u)));
(* finishing 1.2: *)
\<And> h x1 x2 . c5 (a1 h x1) (a1 h x2) = a1 h (c2 x1 x2)
\<rbrakk> \<Longrightarrow>
tFold a4 c1 (tMap (tFold a5 c5 o (tMap (tFoldC a6 c6))) (inverse2 u t)) =
tFold a1 c1 (tMap (tFold a2 c2 o (tMap (tFoldC a3 c3))) t)"
apply (unfold tFoldC_def)
apply (rule tFold_tFold_tFold_inverse2)
apply assumption+
apply (simp_all (no_asm_simp))
done
lemma tFold_tFold_tFold_inverse2_wrapped:
"\<lbrakk> assoc c1; assoc c2; assoc c3; assoc c4; assoc c5; assoc c6;
\<And> h ha hb t . w2 (a4 hb (a5 ha (a6 h t))) = w1 (a1 h (a2 ha (a3 hb t)));
\<And> x y . w2 (c4 x y) = c7 (w2 x) (w2 y);
\<And> x y . c7 (w1 x) (w1 y) = w1 (c1 x y);
\<And> x y . w2 (c5 x y) = c8 (w2 x) (w2 y);
\<And> h x y . c7 (w1 (a1 h x)) (w1 (a1 h y)) = w1 (a1 h (c2 x y));
\<And> h ha x y .
c7 (w1 (a1 h (a2 ha x))) (w1 (a1 h (a2 ha y))) =
w1 (a1 h (a2 ha (c3 x y)));
(* The next two are for tFold_tFold_vConc: *)
\<And> x y z . a4 x (c5 y z) = c5 (a4 x y) (a4 x z);
\<And> x1 x2 y1 y2 . c4 (c5 x1 y1) (c5 x2 y2) = c5 (c4 x1 x2) (c4 y1 y2);
(* units: *)
\<And> x . LRunit c8 (w1 (a1 u x));
\<And> x y . LRunit c5 (a5 y (a6 u x));
\<And> x y z . LRunit c4 (a4 z (a5 y (a6 u x)));
(* finishing 1.2: *)
\<And> h x1 x2 . c5 (a1 h x1) (a1 h x2) = a1 h (c2 x1 x2)
\<rbrakk> \<Longrightarrow>
w2 (tFold a4 c4 (tMap (tFold a5 c5 o (tMap (tFold a6 c6))) (inverse2 u t))) =
w1 (tFold a1 c1 (tMap (tFold a2 c2 o (tMap (tFold a3 c3))) t))"
apply (induct_tac t rule: T_induct)
txt {* 1: @{text "addH h t0"} *}
apply (induct_tac t0 rule: T_induct)
txt {* 1.1: @{text "t0 = addH ha t0a"} *}
apply (induct_tac t0a rule: T_induct, simp (no_asm_simp))
txt {* 1.1.2: @{text "t0a = hConc t1 t2"} *}
apply simp
txt {* 1.2: @{text "t0 = hConc t1 t2"} *}
apply (simp del: slimH2_def tFold_tMap)
apply (fold invOp2_def)
apply (cut_tac u=u and "h1.0"=h and t=t1 in regSkelOuter2_invOp2)
apply (cut_tac u=u and "h1.0"=h and t=t2 in regSkelOuter2_invOp2)
apply (subst invOp2_hConc)
apply assumption
apply assumption
apply (subgoal_tac "ALL t . tFold a5 c5 (tMap (tFold a6 c6) t) =
tFold (\<lambda>h t0. a5 h (tFold a6 c6 t0)) c5 t")
prefer 2
apply (rule allI, simp (no_asm_simp))
apply (simp (no_asm_simp) del: slimH2_def tFold_tMap)
apply (subst tFold_tFold_vConc [of c5 c4 a4])
apply assumption
apply assumption
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (rule conjI, rule refl, rule refl)
apply assumption
apply (rule refl)
apply (subst tFold_tFold_vConc [of c5 c4 a4])
apply assumption
apply assumption
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply (simp (no_asm_simp) del: slimH2_def)
apply (rule conjI, rule refl, rule refl)
apply (rule refl)
apply (simp (no_asm_simp) only: tMap_f_spread1)
apply (simp (no_asm_simp) only: tFold_slimH2 tFold_slimH1)
apply (simp (no_asm_simp) only: f_tFold_const)
apply (subgoal_tac "(\<lambda>h0 . tFold (\<lambda>h0a t0 . a5 h0 (a6 u t0)) const) = (\<lambda> h0 t0 . a5 arbitrary (a6 u arbitrary))")
prefer 2
apply (subgoal_tac "(\<lambda>h0 . tFold (\<lambda>h0a t0 . a5 h0 (a6 u t0)) const) = (\<lambda>h0 . tFold (\<lambda> h0 t0 . a5 arbitrary (a6 u arbitrary)) const)")
prefer 2
apply (rule ext)
apply (rule_tac x=const in fun_cong)
apply (rule_tac f=tFold in arg_cong)
apply (rule ext)
apply (rule ext)
apply (cut_tac c=c5 and F="%x . a5 x (a6 u t0)" and x=h0 in LRunit_const)
apply (simp (no_asm_simp))
apply (cut_tac c=c5 and F="%x . a5 arbitrary (a6 u x)" and x=t0 in LRunit_const)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (rotate_tac -1, erule trans)
apply (rule ext)
apply (rule ext)
apply (simp (no_asm_simp))
apply (rotate_tac -1, erule ssubst)
apply (simp (no_asm_simp) del: slimH2_def tFold_tMap)
apply (simp (no_asm_simp) only: tFold_spread1)
apply (subst foldr1_map1_LRunit)
apply (simp (no_asm_simp))
apply assumption
apply (subst foldr1_map1_LRunit)
apply (simp (no_asm_simp))
apply assumption
apply (thin_tac "ALL t . tFold a5 c5 (tMap (tFold a6 c6) t) =
tFold (\<lambda>h t0. a5 h (tFold a6 c6 t0)) c5 t")
apply (subgoal_tac "tFold (\<lambda>h t0. a5 h (tFold a6 c6 t0)) c5 = (% t . tFold a5 c5 (tMap (tFold a6 c6) t))")
prefer 2
apply (rule ext)
apply (subst tFold_tMap)
apply assumption
apply (rule refl)
apply (simp (no_asm_simp) del: tFold_tMap add: LRunit_left LRunit_right)
txt {* 2: @{text "t = hConc t1 t2"} *}
apply (simp del: slimH2_def tFold_tMap)
done
lemma tFold_tFold_tFoldC_inverse2_wrapped:
"\<lbrakk> assoc c1; assoc c2; assoc c3; assoc c4; assoc c5; assoc c6;
\<And> h ha hb t . w2 (a4 hb (a5 ha (a6 h))) = w1 (a1 h (a2 ha (a3 hb)));
\<And> x y . w2 (c4 x y) = c7 (w2 x) (w2 y);
\<And> x y . c7 (w1 x) (w1 y) = w1 (c1 x y);
\<And> x y . w2 (c5 x y) = c8 (w2 x) (w2 y);
\<And> h x y . c7 (w1 (a1 h x)) (w1 (a1 h y)) = w1 (a1 h (c2 x y));
\<And> h ha x y .
c7 (w1 (a1 h (a2 ha x))) (w1 (a1 h (a2 ha y))) =
w1 (a1 h (a2 ha (c3 x y)));
(* The next two are for tFold_tFold_vConc: *)
\<And> x y z . a4 x (c5 y z) = c5 (a4 x y) (a4 x z);
\<And> x1 x2 y1 y2 . c4 (c5 x1 y1) (c5 x2 y2) = c5 (c4 x1 x2) (c4 y1 y2);
(* units: *)
\<And> x . LRunit c8 (w1 (a1 u x));
\<And> x y . LRunit c5 (a5 y (a6 u));
\<And> x y z . LRunit c4 (a4 z (a5 y (a6 u)));
(* finishing 1.2: *)
\<And> h x1 x2 . c5 (a1 h x1) (a1 h x2) = a1 h (c2 x1 x2)
\<rbrakk> \<Longrightarrow>
w2 (tFold a4 c4 (tMap (tFold a5 c5 o (tMap (tFoldC a6 c6))) (inverse2 u t))) =
w1 (tFold a1 c1 (tMap (tFold a2 c2 o (tMap (tFoldC a3 c3))) t))"
apply (unfold tFoldC_def)
apply (rule tFold_tFold_tFold_inverse2_wrapped)
apply assumption+
apply (simp_all (no_asm_simp))
apply simp_all
txt {* Strange: Why doesn't the first @{text "simp_all"},
even without @{text "no_asm_simp"}, go through? *}
done
lemma wrapped_tFold:
"\<lbrakk> assoc c4; assoc c7; \<And> x y . w2 (c4 x y) = c7 (w2 x) (w2 y) \<rbrakk> \<Longrightarrow>
w2 (tFold a4 c4 t) = tFold (% h t . w2 (a4 h t)) c7 t"
by (induct_tac t rule: T_induct, simp_all)
lemma wrapped_foldr1:
"\<lbrakk> assoc c5; assoc c8; \<And> x y . f (c5 x y) = c8 (f x) (f y) \<rbrakk> \<Longrightarrow>
f (foldr1 c5 xs) = foldr1 c8 (map1 f xs)"
by (induct_tac xs rule: neList_append_induct, simp_all)
lemma wrapped2_tFold:
"\<lbrakk> assoc c5; assoc c7;
\<And> h x y . w2 (a4 h (c5 x y)) = c7 (w2 (a4 h x)) (w2 (a4 h y)) \<rbrakk> \<Longrightarrow>
(% x . w2 (a4 x (tFold a8 c5 t))) = (% x . tFold (% h t . w2 (a4 x (a8 h t))) c7 t)"
apply (rule ext)
apply (rule wrapped_tFold [of c5 c7])
apply assumption
apply assumption
apply (simp_all (no_asm_simp))
done
lemma tFold_tFold_tFold_inverse2_gen:
"\<lbrakk> assoc c1; assoc c2; assoc c3; assoc c4; assoc c5; assoc c6; assoc c7;
\<And> h ha hb t . w2 (a4 hb (a5 ha (a6 h t))) = w1 (a1 h (a2 ha (a3 hb t)));
(* finishing 2, and influencing the next rule: *)
\<And> x y . c7 (w1 x) (w1 y) = w1 (c1 x y);
(* finishing 1.1.2 *)
\<And> h ha x y .
w1 (c1 (a1 h (a2 ha x)) (a1 h (a2 ha y))) =
w1 (a1 h (a2 ha (c3 x y)));
(* The next few are for tFold_tFold_vConc_wrapped: *)
\<And> h x y . w2 (a4 h (c5 x y)) = w2 (c4 (a4 h x) (a4 h y));
\<And> x y . w2 (c4 x y) = c7 (w2 x) (w2 y);
\<And> x1 x2 y1 y2 . c7 (w2 (c4 x1 x2)) (w2 (c4 y1 y2)) =
w2 (c4 (c4 x1 y1) (c4 x2 y2));
(* stronger:
\<And> x1 x2 y1 y2 . c4 (c4 x1 x2) (c4 y1 y2) =
c4 (c4 x1 y1) (c4 x2 y2);
*)
(* units: *)
(*
\<And> x y . LRunit c5 (a5 y (a6 u x));
\<And> h x y . LRunit c4 (a4 h (a5 y (a6 u x)));
*)
\<And> x . LRunit c7 (w1 (a1 u x));
(* finishing 1.2: *)
\<And> h x y . w1 (c1 (a1 h x) (a1 h y)) = w1 (a1 h (c2 x y))
\<rbrakk> \<Longrightarrow>
w2 (tFold a4 c4 (tMap (tFold a5 c5 o (tMap (tFold a6 c6))) (inverse2 u t))) =
w1 (tFold a1 c1 (tMap (tFold a2 c2 o (tMap (tFold a3 c3))) t))"
apply (induct_tac t rule: T_induct)
txt {* 1: @{text "addH h t0"} *}
apply (induct_tac t0 rule: T_induct)
txt {* 1.1: @{text "t0 = addH ha t0a"} *}
apply (induct_tac t0a rule: T_induct, simp (no_asm_simp))
txt {* 1.1.2: @{text "t0a = hConc t1 t2"} *}
apply simp
txt {* 1.2: @{text "t0 = hConc t1 t2"} *} (*
apply (tactic "thin_tac \"!! x y. c7 (w1 x) (w1 y) = w1 (c1 x y)\" 1")
-- doesn't work. Why?
*)
apply (simp del: slimH2_def tFold_tMap)
apply (fold invOp2_def)
apply (cut_tac u=u and "h1.0"=h and t=t1 in regSkelOuter2_invOp2)
apply (cut_tac u=u and "h1.0"=h and t=t2 in regSkelOuter2_invOp2)
apply (subst invOp2_hConc)
apply assumption
apply assumption
apply (subgoal_tac "ALL t . tFold a5 c5 (tMap (tFold a6 c6) t) =
tFold (\<lambda>h t0. a5 h (tFold a6 c6 t0)) c5 t")
prefer 2
apply (rule allI, simp (no_asm_simp))
apply (simp (no_asm_simp) del: slimH2_def tFold_tMap)
apply (subst tFold_tFold_vConc_wrapped [of c4 c5 c4 w2 a4 w2 a4 c7])
apply assumption
apply assumption
apply assumption
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (rule conjI, rule refl, rule refl)
apply assumption
apply (subst tFold_tFold_vConc_wrapped [of c4 c5 c4 w2 a4 w2 a4 c7])
apply assumption
apply assumption
apply assumption
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply assumption
apply (simp (no_asm_simp) del: slimH2_def)
apply (simp (no_asm_simp) only: spread1_slimH2)
apply (simp (no_asm_simp) only: tMap_f_slimH3 tFold_slimH2 tFold_slimH1)
apply (subst tFold_tMap [of _ _ "(tFold (\<lambda>h0 t0. a5 h0 (tFold (\<lambda>h0. a6 u) const t0)) c5)"])
apply assumption
apply (subst tFold_tMap [of _ _ "(tFold (\<lambda>h0 t0. a5 h0 (tFold (\<lambda>h0. a6 u) const t0)) c5)"])
apply assumption
apply (subst wrapped_tFold [of c4 c7 w2 "(\<lambda>h t0. a4 h (tFold (\<lambda>h0 t0. a5 h0 (tFold (\<lambda>h0. a6 u) const t0)) c5 t0))"])
apply assumption
apply assumption
apply (simp (no_asm_simp))
apply (subst wrapped_tFold [of c4 c7 w2 "(\<lambda>h t0. a4 h (tFold (\<lambda>h0 t0. a5 h0 (tFold (\<lambda>h0. a6 u) const t0)) c5 t0))"])
apply assumption
apply assumption
apply (simp (no_asm_simp))
apply (subgoal_tac "(\<lambda>h t. w2 (a4 h (tFold (\<lambda>h0 t0. a5 h0 (tFold (\<lambda>h0. a6 u) const t0)) c5 t))) = (\<lambda> h t . w1 (a1 u arbitrary))")
prefer 2
apply (rule ext)
apply (rule ext)
apply (cut_tac "c4.0"=c5 and "c7.0"=c7 and "w2.0"="%z . w2 (a4 ha z)" in wrapped_tFold)
apply assumption
apply assumption
apply (simp (no_asm_simp))
apply (rotate_tac -1, erule ssubst)
apply (simp (no_asm_simp) only: f_tFold_const)
apply (cut_tac c=c7 and a="(\<lambda>h. tFold (\<lambda>h0 t0. w1 (a1 u (a2 h (a3 ha t0)))) const)" in tFold_LRunit)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp) only: f_tFold_const)
apply (simp (no_asm_simp) only: tFold_const_const)
apply assumption
apply (rotate_tac -1, erule ssubst)
apply (subgoal_tac "tFold (\<lambda>h0 t0. w1 (a1 u (a2 arbitrary (a3 ha t0)))) const = tFold (\<lambda>h0 t0. w1 (a1 u arbitrary)) const")
apply (rotate_tac -1, erule ssubst)
apply (simp (no_asm_simp) only: tFold_const_const)
apply (rule_tac x=const in fun_cong)
apply (rule_tac f=tFold in arg_cong)
apply (rule ext)
apply (rule ext)
apply (rule_tac c=c7 and F="%x . w1 (a1 u x)" in LRunit_const)
apply (simp (no_asm_simp))
apply (rotate_tac -1, erule ssubst)
apply (simp (no_asm_simp) del: slimH2_def tFold_tMap)
apply (thin_tac "ALL t . tFold a5 c5 (tMap (tFold a6 c6) t) =
tFold (\<lambda>h t0. a5 h (tFold a6 c6 t0)) c5 t")
apply (subgoal_tac "tFold (\<lambda>h t0. a5 h (tFold a6 c6 t0)) c5 = (% t . tFold a5 c5 (tMap (tFold a6 c6) t))")
prefer 2
apply (rule ext)
apply (subst tFold_tMap)
apply assumption
apply (rule refl)
apply (simp (no_asm_simp) del: tFold_tMap add: LRunit_left LRunit_right)
txt {* Now we expand some extra effort to be able to work with a single, wrapped-only unit assumption. *}
apply (subgoal_tac "w1 (c1 (a1 h (tFold a2 c2 (tMap (tFold a3 c3) t1)))
(c1 (a1 u arbitrary)
(c1 (a1 u arbitrary)
(a1 h (tFold a2 c2 (tMap (tFold a3 c3) t2)))))) =
c7 (w1 (a1 h (tFold a2 c2 (tMap (tFold a3 c3) t1))))
(c7 (w1 (a1 u arbitrary))
(c7 (w1 (a1 u arbitrary))
(w1 (a1 h (tFold a2 c2 (tMap (tFold a3 c3) t2))))))")
prefer 2
apply (simp (no_asm_simp))
apply (rotate_tac -1, erule trans)
apply (subst LRunit_left [of c7 "w1 (a1 u arbitrary)"])
apply (simp (no_asm_simp))
apply (subst LRunit_left [of c7 "w1 (a1 u arbitrary)"])
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
txt {* 2: @{text "t = hConc t1 t2"} *}
apply (simp del: slimH2_def tFold_tMap)
done
lemma tFold_tFold_tFoldC_inverse2_gen:
"\<lbrakk> assoc c1; assoc c2; assoc c3; assoc c4; assoc c5; assoc c6; assoc c7;
\<And> h ha hb . w2 (a4 hb (a5 ha (a6 h))) = w1 (a1 h (a2 ha (a3 hb)));
(* finishing 2, and influencing the next rule: *)
\<And> x y . c7 (w1 x) (w1 y) = w1 (c1 x y);
(* finishing 1.1.2 *)
\<And> h ha x y .
w1 (c1 (a1 h (a2 ha x)) (a1 h (a2 ha y))) =
w1 (a1 h (a2 ha (c3 x y)));
(* The next few are for tFold_tFold_vConc_wrapped: *)
\<And> h x y . w2 (a4 h (c5 x y)) = w2 (c4 (a4 h x) (a4 h y));
\<And> x y . w2 (c4 x y) = c7 (w2 x) (w2 y);
\<And> x1 x2 y1 y2 . c7 (w2 (c4 x1 x2)) (w2 (c4 y1 y2)) =
w2 (c4 (c4 x1 y1) (c4 x2 y2));
(* stronger:
\<And> x1 x2 y1 y2 . c4 (c4 x1 x2) (c4 y1 y2) =
c4 (c4 x1 y1) (c4 x2 y2);
*)
(* units: *)
(*
\<And> x y . LRunit c5 (a5 y (a6 u));
\<And> h x y . LRunit c4 (a4 h (a5 y (a6 u)));
*)
\<And> x . LRunit c7 (w1 (a1 u x));
(* finishing 1.2: *)
\<And> h x y . w1 (c1 (a1 h x) (a1 h y)) = w1 (a1 h (c2 x y))
\<rbrakk> \<Longrightarrow>
w2 (tFold a4 c4 (tMap (tFold a5 c5 o (tMap (tFoldC a6 c6))) (inverse2 u t))) =
w1 (tFold a1 c1 (tMap (tFold a2 c2 o (tMap (tFoldC a3 c3))) t))"
apply (unfold tFoldC_def)
apply (rule tFold_tFold_tFold_inverse2_gen)
apply assumption+
apply (simp_all (no_asm_simp))
apply simp
apply (subgoal_tac "c7 (c7 (w2 x1) (w2 x2)) (c7 (w2 y1) (w2 y2)) =
c7 (w2 (c4 x1 x2)) (w2 (c4 y1 y2))")
prefer 2
apply (simp (no_asm_simp))
apply simp
done
lemma id_tFold_tFold_tFoldC_inverse2_gen:
"\<lbrakk> assoc c1; assoc c2; assoc c3; assoc c5; assoc c6;
\<And> h ha hb . a4 hb (a5 ha (a6 h)) = a1 h (a2 ha (a3 hb));
(* finishing 1.1.2 *)
\<And> h ha x y .
c1 (a1 h (a2 ha x)) (a1 h (a2 ha y)) = a1 h (a2 ha (c3 x y));
(* The next few are for tFold_tFold_vConc_wrapped: *)
\<And> h x y . a4 h (c5 x y) = c1 (a4 h x) (a4 h y);
\<And> x1 x2 y1 y2 . c1 (c1 x1 x2) (c1 y1 y2) =
c1 (c1 x1 y1) (c1 x2 y2);
(* units: *)
\<And> x . LRunit c1 (a1 u x);
(* finishing 1.2: *)
\<And> h x y . c1 (a1 h x) (a1 h y) = a1 h (c2 x y)
\<rbrakk> \<Longrightarrow>
id (tFold a4 c1 (tMap (tFold a5 c5 o (tMap (tFoldC a6 c6))) (inverse2 u t))) =
id (tFold a1 c1 (tMap (tFold a2 c2 o (tMap (tFoldC a3 c3))) t))"
apply (rule tFold_tFold_tFoldC_inverse2_gen)
apply assumption+
apply (simp_all (no_asm_simp))
apply (subgoal_tac "a1 h (c2 (a2 ha x) (a2 ha y)) = c1 (a1 h (a2 ha x)) (a1 h (a2 ha y))")
prefer 2
apply simp
apply (erule trans)
apply (rotate_tac -1, simp)
done
end
lemma inverse1_addH:
inverse1 (addH h t) = addH2 h t
lemma inverse1_hConc:
inverse1 (hConc t1 t2) = hConc (inverse1 t1) (inverse1 t2)
lemma tFold_tFold_inverse1:
[| assoc c2; assoc c4; !!h2 h1 t. a2 h2 (a1 h1 t) = a3 h1 (a4 h2 t);
!!h t u. a3 h (c4 t u) = c2 (a3 h t) (a3 h u) |]
==> tFold a2 c2 (tMap (tFold a1 c1) (inverse1 t)) =
tFold a3 c2 (tMap (tFold a4 c4) t)
lemma tFold_tFold0_inverse1:
[| assoc c2; assoc c4; !!h t u. a2 (c4 t u) h = c2 (a2 t h) (a2 u h) |]
==> tFold a2 c2 (tMap (tFold0 c1) (inverse1 t)) =
tFold (flip a2) c2 (tMap (tFold0 c4) t)
lemma regSkelOuter2_spread1:
regSkelOuter2 (spread1 hs t) = Some (hs, headers t)
lemma spread1_singleton:
spread1 (singleton h) t = addH h t
lemma spread1_append:
spread1 (append hs1 hs2) t = hConc (spread1 hs1 t) (spread1 hs2 t)
lemma spread1_tFold_append:
spread1 (tFold f append t1) t = tFold (%h0 t0. spread1 (f h0 t0) t) hConc t1
lemma spread1_hConc_0:
ALL t1. spread1 hs (hConc t1 t2) = vConc (spread1 hs t1) (spread1 hs t2)
lemma spread1_hConc:
spread1 hs (hConc t1 t2) = vConc (spread1 hs t1) (spread1 hs t2)
lemma tMap_f_spread1:
tMap f (spread1 hs t) = spread1 hs (f t)
lemma tFold_spread1:
assoc c ==> tFold a c (spread1 hs t) = foldr1 c (map1 (%h. a h t) hs)
lemma spread2_singleton:
spread2 (singleton h) t = addH2 h t
lemma spread2_append:
spread2 (append hs1 hs2) t = vConc (spread2 hs1 t) (spread2 hs2 t)
lemma spread2_cons1:
spread2 (cons1 h hs) t = vCons (h, t) (spread2 hs t)
lemma headers_spread2:
headers (spread2 hs t) = headers t
lemma regSkelOuter2_spread2_0:
ALL hs2. regSkelOuter2 (spread2 hs2 t) = Some (headers t, hs2)
lemma regSkelOuter2_spread2:
regSkelOuter2 (spread2 hs2 t) = Some (headers t, hs2)
lemma spread2_hConc_0:
ALL t1 t2. spread2 hs2 (hConc t1 t2) = hConc (spread2 hs2 t1) (spread2 hs2 t2)
lemma spread2_hConc:
spread2 hs2 (hConc t1 t2) = hConc (spread2 hs2 t1) (spread2 hs2 t2)
lemma spread2_addH:
spread2 hs (addH h t) = addH h (foldr1 hConc (map1 (%h2. addH h2 t) hs))
lemma spread2_tFold_hConc:
spread2 hs2 (tFold a hConc t) = tFold (%h t. spread2 hs2 (a h t)) hConc t
lemma tMap_tFold_spread2:
assoc c
==> tMap (tFold a c) (spread2 hs t) =
tMap (%t0. foldr1 c (map1 (%h2. a h2 t0) hs)) t
lemma delH1_hConc:
delH1 (hConc t1 t2) = delH1 t1
lemma delH1_addH:
delH1 (addH h t) = t
lemma delH1_hCons:
delH1 (hCons (h, t0) t) = t0
lemma delH1_tFold_hConc:
delH1 (tFold f hConc t) = delH1 (uncurry f (hHead t))
lemma headers_delH1__reg2_0:
ALL hs1 hs2. regSkelOuter2 t1 = Some (hs1, hs2) --> headers (delH1 t1) = hs2
lemma headers_delH1__reg2:
regSkelOuter2 t1 = Some (hs1, hs2) ==> headers (delH1 t1) = hs2
lemma delH1_addH2:
delH1 (addH2 h t) = addH h (delH1 t)
lemma delH1_vConc_0:
ALL hs1a hs1b hs2a hs2b.
regSkelOuter2 t1 = Some (hs1a, hs1b) -->
regSkelOuter2 t2 = Some (hs2a, hs2b) -->
delH1 (vConc t1 t2) = hConc (delH1 t1) (delH1 t2)
lemma delH1_vConc:
[| regSkelOuter2 t1 = Some (hs1a, hs1b); regSkelOuter2 t2 = Some (hs2a, hs2b) |] ==> delH1 (vConc t1 t2) = hConc (delH1 t1) (delH1 t2)
lemma delH1_tMap_const:
delH1 (tMap (const t2) t1) = t2
lemma delH1_tMap_CONST:
delH1 (tMap (%x. t2) t1) = t2
lemma delH2_hConc:
delH2 (hConc t1 t2) = hConc (delH2 t1) (delH2 t2)
lemma delH2_addH:
delH2 (addH h t) = addH h (delH1 t)
lemma delH2_hCons:
delH2 (hCons (h, t0) t) = hCons (h, delH1 t0) (delH2 t)
lemma delH2_addH2:
delH2 (addH2 h t) = t
lemma headers_delH2:
headers (delH2 t) = headers t
lemma delH2_vConc_0:
ALL hs1 hs2a t2 hs2b.
regSkelOuter2 t1 = Some (hs1, hs2a) -->
regSkelOuter2 t2 = Some (hs1, hs2b) --> delH2 (vConc t1 t2) = delH2 t1
lemma delH2_vConc:
[| regSkelOuter2 t1 = Some (hs1, hs2a); regSkelOuter2 t2 = Some (hs1, hs2b) |] ==> delH2 (vConc t1 t2) = delH2 t1
lemma delH2_spread2:
delH2 (spread2 hs t) = t
lemma delH2_tMap_const:
delH2 (tMap (const t2) t1) = tMap (const (delH1 t2)) t1
lemma delH2_tMap_CONST:
delH2 (tMap (%x. t2) t1) = tMap (const (delH1 t2)) t1
lemma delH1_addH3:
delH1 (addH3 h t) = addH2 h (delH1 t)
lemma tFold_slimH1:
assoc c ==> tFold a c (slimH1 u t) = tFold (%h0. a u) const t
lemma headers_slimH1:
headers (slimH1 u t) = singleton u
lemma slimH2_tMap:
slimH2 h2 = tMap (slimH1 h2)
lemma slimH2_slimH2:
slimH2 u (slimH2 v t) = slimH2 u t
lemma slimH2_addH:
slimH2 u (addH h t) = addH h (slimH1 u t)
lemma slimH2_hConc:
slimH2 u (hConc t1 t2) = hConc (slimH2 u t1) (slimH2 u t2)
lemma slimH2_as_tFold:
tFold (%h t. addH h (slimH1 u t)) hConc t = slimH2 u t
lemma slimH2_addH2:
slimH2 u (addH2 h2 t) = addH2 u t
lemma headers_slimH2:
headers (slimH2 u t) = headers t
lemma regSkelOuter2_slimH2:
regSkelOuter2 (slimH2 u t) = Some (headers t, singleton u)
lemma slimH2_tFold_hConc:
slimH2 u (tFold f hConc t) = tFold (%h t. slimH2 u (f h t)) hConc t
lemma slimH2_tFold_addH2_hConc:
slimH2 u (tFold (%h. addH2 v) hConc t) = tFold (%h. addH2 u) hConc t
lemma del1_slimH2_isConst:
delH1 (slimH2 u t1) = delH1 (slimH2 u t2)
lemma tFold_slimH2:
assoc c ==> tFold a c (slimH2 u t) = tFold (%h0 t0. a h0 (slimH1 u t0)) c t
lemma slimH3_expand:
slimH3 u t = addH3 u (delH3 t)
lemma slimH3_addH:
slimH3 u (addH h t) = addH h (slimH2 u t)
lemma slimH3_hConc:
slimH3 u (hConc t1 t2) = hConc (slimH3 u t1) (slimH3 u t2)
lemma spread1_slimH2:
spread1 hs (slimH2 u t) = slimH3 u (spread1 hs t)
lemma tFold_slimH3:
assoc c ==> tFold a c (slimH3 u t) = tFold (%h0 t0. a h0 (slimH2 u t0)) c t
lemma tMap_f_slimH3:
tMap f (slimH3 u t) = tMap (%t0. f (slimH2 u t0)) t
lemma hConcU_assoc:
[| !!t. u (u t) = u t; !!t1 t2. u (hConc t1 t2) = hConc (u t1) (u t2) |] ==> assoc (hConcU u)
lemma U_hConcU:
[| !!t. u (u t) = u t; !!t1 t2. u (hConc t1 t2) = hConc (u t1) (u t2) |] ==> u (hConcU u t1 t2) = hConc (u t1) (u t2)
lemma U_tFold_hConcU:
[| !!t. u (u t) = u t; !!t1 t2. u (hConc t1 t2) = hConc (u t1) (u t2) |] ==> u (tFold f (hConcU u) t) = tFold (%h0 t0. u (f h0 t0)) hConc t
lemma hConcSH2_assoc:
assoc (hConcSH2 u)
lemma slimH2_hConcSH2:
slimH2 u (hConcSH2 u t1 t2) = hConc (slimH2 u t1) (slimH2 u t2)
lemma slimH2_tFold_hConcSH2:
slimH2 u (tFold f (hConcSH2 u) t) = tFold (%h t. slimH2 u (f h t)) hConc t
lemma dConc:
[| regSkelOuter2 t1 = Some (cs1, hs1); regSkelOuter2 t2 = Some (cs2, hs2) |]
==> dConc h (Abs_regT2 t1) (Abs_regT2 t2) =
Abs_regT2
(hConc (vConc t1 (tMap (const (h (delH1 t2))) t1))
(vConc (tMap (const (h (delH1 t1))) t2) t2))
lemma dConc1:
[| regSkelOuter2 (Rep_regT2 t1) = Some (cs1, hs1);
regSkelOuter2 (Rep_regT2 t2) = Some (cs2, hs2) |]
==> dConc h t1 t2 =
Abs_regT2
(hConc
(vConc (Rep_regT2 t1)
(tMap (const (h (delH1 (Rep_regT2 t2)))) (Rep_regT2 t1)))
(vConc (tMap (const (h (delH1 (Rep_regT2 t1)))) (Rep_regT2 t2))
(Rep_regT2 t2)))
lemma regSkelOuter2_dConcDef:
[| !!t. headers (h t) = headers t; regSkelOuter2 t1 = Some (cs1, hs1);
regSkelOuter2 t2 = Some (cs2, hs2) |]
==> regSkelOuter2
(hConc (vConc t1 (tMap (const (h (delH1 t2))) t1))
(vConc (tMap (const (h (delH1 t1))) t2) t2)) =
Some (append cs1 cs2, append hs1 hs2)
lemma regSkelOuter2_dConc:
[| !!t. headers (h t) = headers t; regSkelOuter2 t1 = Some (cs1, hs1);
regSkelOuter2 t2 = Some (cs2, hs2) |]
==> regSkelOuter2 (Rep_regT2 (dConc h (Abs_regT2 t1) (Abs_regT2 t2))) =
Some (append cs1 cs2, append hs1 hs2)
lemma dConc2:
[| !!t. headers (h t) = headers t;
regSkelOuter2 (Rep_regT2 t1) = Some (cs1, hs1);
regSkelOuter2 (Rep_regT2 t2) = Some (cs2, hs2) |]
==> Rep_regT2 (dConc h t1 t2) =
hConc
(vConc (Rep_regT2 t1)
(tMap (const (h (delH1 (Rep_regT2 t2)))) (Rep_regT2 t1)))
(vConc (tMap (const (h (delH1 (Rep_regT2 t1)))) (Rep_regT2 t2))
(Rep_regT2 t2))
lemma regSkelOuter2_dConc1:
[| !!t. headers (h t) = headers t;
regSkelOuter2 (Rep_regT2 t1) = Some (cs1, hs1);
regSkelOuter2 (Rep_regT2 t2) = Some (cs2, hs2) |]
==> regSkelOuter2 (Rep_regT2 (dConc h t1 t2)) =
Some (append cs1 cs2, append hs1 hs2)
lemma headers_dConc:
(!!t. headers (h t) = headers t)
==> headers (Rep_regT2 (dConc h t1 t2)) =
append (headers (Rep_regT2 t1)) (headers (Rep_regT2 t2))
lemma reg2dim2_dConc:
[| !!t. headers (h t) = headers t;
regSkelOuter2 (Rep_regT2 t1) = Some (cs1, hs1);
regSkelOuter2 (Rep_regT2 t2) = Some (cs2, hs2) |]
==> reg2dim2 (dConc h t1 t2) = append hs1 hs2
lemma cs_dConc:
[| !!t. headers (h t) = headers t; !!t. h (h t) = h t;
!!t1 t2. h (hConc t1 t2) = hConc (h t1) (h t2);
regSkelOuter2 (Rep_regT2 t1) = Some (cs1, hs1);
regSkelOuter2 (Rep_regT2 t2) = Some (cs2, hs2) |]
==> h (delH1 (Rep_regT2 (dConc h t1 t2))) =
hConc (h (delH1 (Rep_regT2 t1))) (h (delH1 (Rep_regT2 t2)))
lemma dConc_assoc:
[| !!t. headers (h t) = headers t; !!t. h (h t) = h t;
!!t1 t2. h (hConc t1 t2) = hConc (h t1) (h t2) |]
==> assoc (dConc h)
lemma invLift0_addH:
invLift0 u h g h1 (addH h2 t2) = Abs_regT2 (addH2 h2 (g h1 t2))
lemma invLift0_addH1:
Rep_regT2 (invLift0 u h g h1 (addH h2 t2)) = addH2 h2 (g h1 t2)
lemma reg2dim2_invLift0_addH:
reg2dim2 (invLift0 u h g h1 (addH h2 t2)) = singleton h2
lemma cs_invLift0_addH:
(!!u v t. h u (g v t) = g u t) ==> h u (delH2 (Rep_regT2 (invLift0 u h g h1 (addH h2 t2)))) = g u t2
lemma invLift0_hConc:
[| !!t. headers (h u t) = headers t; !!t. h u (h u t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2) |]
==> invLift0 u h g h1 (hConc t1 t2) =
dConc (h u) (invLift0 u h g h1 t1) (invLift0 u h g h1 t2)
lemma reg2dim2_invLift0:
[| !!t. headers (h u t) = headers t; !!t. h u (h u t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2);
!!x t. headers (g x t) = headers t |]
==> reg2dim2 (invLift0 u h g h1 t) = headers t
lemma regSkelOuter2_invLift0_EX:
[| !!t. headers (h u t) = headers t; !!t. h u (h u t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2);
!!x y t. headers (g x t) = headers (g y t) |]
==> EX hs1.
regSkelOuter2 (Rep_regT2 (invLift0 u h g h1 t)) = Some (hs1, headers t)
lemma cs_invLift0_hConc:
[| !!t. headers (h u t) = headers t; !!t. h u (h u t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2) |]
==> h u (delH1 (Rep_regT2 (invLift0 u h g h1 (hConc t1 t2)))) =
hConc (h u (delH1 (Rep_regT2 (invLift0 u h g h1 t1))))
(h u (delH1 (Rep_regT2 (invLift0 u h g h1 t2))))
lemma invLift_addH:
(!!x y t. headers (g x t) = headers (g y t)) ==> invLift u h g h1 (addH h2 t2) = addH2 h2 (g h1 t2)
lemma headers_invLift0_invariant:
[| !!t. headers (h u t) = headers t; !!t. h u (h u t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2);
!!x y t. headers (g x t) = headers (g y t) |]
==> headers (Rep_regT2 (invLift0 u h g x t)) =
headers (Rep_regT2 (invLift0 u h g y t))
lemma headers_invLift_invariant:
[| !!t. headers (h u t) = headers t; !!t. h u (h u t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2);
!!x y t. headers (g x t) = headers (g y t) |]
==> headers (invLift u h g x t) = headers (invLift u h g y t)
lemma invLift_hConc:
[| !!t. headers (h u t) = headers t; !!t. h u (h u t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2);
!!x y t. headers (g x t) = headers (g y t);
regSkelOuter2 (invLift u h g h1 t1) = Some (hs1a, hs2a);
regSkelOuter2 (invLift u h g h1 t2) = Some (hs1b, hs2b) |]
==> invLift u h g h1 (hConc t1 t2) =
hConc
(vConc (invLift u h g h1 t1)
(tMap (const (h u (delH1 (invLift u h g h1 t2)))) (invLift u h g h1 t1)))
(vConc
(tMap (const (h u (delH1 (invLift u h g h1 t1)))) (invLift u h g h1 t2))
(invLift u h g h1 t2))
lemma regSkelOuter2_invLift_EX:
[| !!t. headers (h u t) = headers t; !!t. h u (h u t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2);
!!x y t. headers (g x t) = headers (g y t) |]
==> EX hs1. regSkelOuter2 (invLift u h g h1 t) = Some (hs1, headers t)
lemma delH1_invLift:
[| !!t. headers (h u t) = headers t; !!t. h u (h u t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2);
!!x y t. headers (g x t) = headers (g y t) |]
==> delH1 (invLift u h g v t) =
tFold (%h0 t0. addH h0 (delH1 (g v t0))) (hConcU (h u)) t
lemma h_u_delH1_invLift:
[| !!t. headers (h u t) = headers t; !!t x. h u (h x t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2);
!!x y t. headers (g x t) = headers (g y t);
!!h0 t0. h u (addH h0 (delH1 (g v t0))) = addH h0 (delH1 (g u t0)) |]
==> h u (delH1 (invLift u h g v t)) =
tFold (%h0 t0. addH h0 (delH1 (g u t0))) hConc t
lemma headers_h_u_delH1_invLift:
[| !!t. headers (h u t) = headers t; !!t x. h u (h x t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2);
!!x y t. headers (g x t) = headers (g y t);
!!h0 t0. h u (addH h0 (delH1 (g v t0))) = addH h0 (delH1 (g u t0)) |]
==> headers (h u (delH1 (invLift u h g v t))) = headers t
lemma headers_delH1_invLift:
[| !!t. headers (h u t) = headers t; !!t x. h u (h x t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2);
!!x y t. headers (g x t) = headers (g y t);
!!h0 t0. h u (addH h0 (delH1 (g v t0))) = addH h0 (delH1 (g u t0)) |]
==> headers (delH1 (invLift u h g v t)) = headers t
lemma regSkelOuter2_dConcFill:
[| !!t. headers (h u t) = headers t; !!t x. h u (h x t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2);
!!x y t. headers (g x t) = headers (g y t);
regSkelOuter2 (invLift u h g h1 t1) = Some (hs1a, hs2a);
regSkelOuter2 (invLift u h g h1 t2) = Some (hs1b, hs2b) |]
==> regSkelOuter2
(tMap (const (h u (delH1 (invLift u h g h1 t2)))) (invLift u h g h1 t1)) =
Some (hs1a, hs2b)
lemma headers_invLift_hConc:
[| !!t. headers (h u t) = headers t; !!t x. h u (h x t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2);
!!x y t. headers (g x t) = headers (g y t);
regSkelOuter2 (invLift u h g h1 t1) = Some (hs1a, hs2a);
regSkelOuter2 (invLift u h g h1 t2) = Some (hs1b, hs2b) |]
==> headers (invLift u h g h1 (hConc t1 t2)) =
append (headers (invLift u h g h1 t1)) (headers (invLift u h g h1 t2))
lemma headers_invLift:
[| !!t. headers (h u t) = headers t; !!t x. h u (h x t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2);
!!x y t. headers (g x t) = headers (g y t) |]
==> headers (invLift u h g h1 t) = tFold (%h2 t2. headers (g h1 t2)) append t
lemma regSkelOuter2_invLift:
[| !!t. headers (h u t) = headers t; !!t x. h u (h x t) = h u t;
!!t1 t2. h u (hConc t1 t2) = hConc (h u t1) (h u t2);
!!x y t. headers (g x t) = headers (g y t);
!!h0 t0. h u (addH h0 (delH1 (g h1 t0))) = addH h0 (delH1 (g u t0)) |]
==> regSkelOuter2 (invLift u h g h1 t) =
Some (tFold (%h2 t2. headers (g h1 t2)) append t, headers t)
lemma delH1_invOp2:
delH1 (invOp2 u v t) = tFold (%h t. addH h (slimH1 v t)) (hConcSH2 u) t
lemma headers_invOp2:
headers (invOp2 u v t) = tFold (%h. headers) append t
lemma cs_invOp2:
slimH2 u (delH1 (invOp2 u v t)) = tFold (%h t. addH h (slimH1 u t)) hConc t
lemma regSkelOuter2_invOp2:
regSkelOuter2 (invOp2 u h1 t) = Some (tFold (%h. headers) append t, headers t)
lemma invOp2_hConc:
[| regSkelOuter2 (invOp2 u h1 t1) = Some (hs1a, hs2a);
regSkelOuter2 (invOp2 u h1 t2) = Some (hs1b, hs2b) |]
==> invOp2 u h1 (hConc t1 t2) =
hConc (vConc (invOp2 u h1 t1) (spread1 hs1a (slimH2 u t2)))
(vConc (spread1 hs1b (slimH2 u t1)) (invOp2 u h1 t2))
lemma inverse2_addH:
inverse2 u (addH h t) = invLift u slimH2 addH2 h t
lemma inverse2_hConc:
inverse2 u (hConc t1 t2) = hConc (inverse2 u t1) (inverse2 u t2)
lemma tFold_tFold_tFold_inverse2:
[| assoc c2; assoc c3; assoc c1; assoc c5; assoc c6;
!!h ha hb t. a4 hb (a5 ha (a6 h t)) = a1 h (a2 ha (a3 hb t));
!!h ha t1 t2.
c1 (a1 h (a2 ha t1)) (a1 h (a2 ha t2)) = a1 h (a2 ha (c3 t1 t2));
!!x y z. a4 x (c5 y z) = c5 (a4 x y) (a4 x z);
!!x1 x2 y1 y2. c1 (c5 x1 y1) (c5 x2 y2) = c5 (c1 x1 x2) (c1 y1 y2);
!!x. LRunit c1 (a1 u x); !!x y. LRunit c5 (a5 y (a6 u x));
!!x y z. LRunit c1 (a1 z (a5 y (a6 u x)));
!!h x1 x2. c5 (a1 h x1) (a1 h x2) = a1 h (c2 x1 x2) |]
==> tFold a4 c1 (tMap (tFold a5 c5 o tMap (tFold a6 c6)) (inverse2 u t)) =
tFold a1 c1 (tMap (tFold a2 c2 o tMap (tFold a3 c3)) t)
lemma tFold_tFold_tFold0_inverse2:
[| assoc c2; assoc c3; assoc c1; assoc c5; assoc c6;
!!h ha hb t. a4 hb (a5 ha h) = a1 h (a2 ha hb);
!!h ha t1 t2.
c1 (a1 h (a2 ha t1)) (a1 h (a2 ha t2)) = a1 h (a2 ha (c3 t1 t2));
!!x y z. a4 x (c5 y z) = c5 (a4 x y) (a4 x z);
!!x1 x2 y1 y2. c1 (c5 x1 y1) (c5 x2 y2) = c5 (c1 x1 x2) (c1 y1 y2);
!!x. LRunit c1 (a1 u x); !!x y. LRunit c5 (a5 y u);
!!x y z. LRunit c1 (a1 z (a5 y u));
!!h x1 x2. c5 (a1 h x1) (a1 h x2) = a1 h (c2 x1 x2) |]
==> tFold a4 c1 (tMap (tFold a5 c5 o tMap (tFold0 c6)) (inverse2 u t)) =
tFold a1 c1 (tMap (tFold a2 c2 o tMap (tFold0 c3)) t)
lemma tFold_tFold_tFoldC_inverse2:
[| assoc c1; assoc c2; assoc c3; assoc c5; assoc c6;
!!h ha hb t. a4 hb (a5 ha (a6 h)) = a1 h (a2 ha (a3 hb));
!!h ha t1 t2.
c1 (a1 h (a2 ha t1)) (a1 h (a2 ha t2)) = a1 h (a2 ha (c3 t1 t2));
!!x y z. a4 x (c5 y z) = c5 (a4 x y) (a4 x z);
!!x1 x2 y1 y2. c1 (c5 x1 y1) (c5 x2 y2) = c5 (c1 x1 x2) (c1 y1 y2);
!!x. LRunit c1 (a1 u x); !!x y. LRunit c5 (a5 y (a6 u));
!!x y z. LRunit c1 (a1 z (a5 y (a6 u)));
!!h x1 x2. c5 (a1 h x1) (a1 h x2) = a1 h (c2 x1 x2) |]
==> tFold a4 c1 (tMap (tFold a5 c5 o tMap (tFoldC a6 c6)) (inverse2 u t)) =
tFold a1 c1 (tMap (tFold a2 c2 o tMap (tFoldC a3 c3)) t)
lemma tFold_tFold_tFold_inverse2_wrapped:
[| assoc c1; assoc c2; assoc c3; assoc c4; assoc c5; assoc c6;
!!h ha hb t. w2 (a4 hb (a5 ha (a6 h t))) = w1 (a1 h (a2 ha (a3 hb t)));
!!x y. w2 (c4 x y) = c7 (w2 x) (w2 y); !!x y. c7 (w1 x) (w1 y) = w1 (c1 x y);
!!x y. w2 (c5 x y) = c8 (w2 x) (w2 y);
!!h x y. c7 (w1 (a1 h x)) (w1 (a1 h y)) = w1 (a1 h (c2 x y));
!!h ha x y.
c7 (w1 (a1 h (a2 ha x))) (w1 (a1 h (a2 ha y))) =
w1 (a1 h (a2 ha (c3 x y)));
!!x y z. a4 x (c5 y z) = c5 (a4 x y) (a4 x z);
!!x1 x2 y1 y2. c4 (c5 x1 y1) (c5 x2 y2) = c5 (c4 x1 x2) (c4 y1 y2);
!!x. LRunit c8 (w1 (a1 u x)); !!x y. LRunit c5 (a5 y (a6 u x));
!!x y z. LRunit c4 (a4 z (a5 y (a6 u x)));
!!h x1 x2. c5 (a1 h x1) (a1 h x2) = a1 h (c2 x1 x2) |]
==> w2 (tFold a4 c4 (tMap (tFold a5 c5 o tMap (tFold a6 c6)) (inverse2 u t))) =
w1 (tFold a1 c1 (tMap (tFold a2 c2 o tMap (tFold a3 c3)) t))
lemma tFold_tFold_tFoldC_inverse2_wrapped:
[| assoc c1; assoc c2; assoc c3; assoc c4; assoc c5; assoc c6;
!!h ha hb t. w2 (a4 hb (a5 ha (a6 h))) = w1 (a1 h (a2 ha (a3 hb)));
!!x y. w2 (c4 x y) = c7 (w2 x) (w2 y); !!x y. c7 (w1 x) (w1 y) = w1 (c1 x y);
!!x y. w2 (c5 x y) = c8 (w2 x) (w2 y);
!!h x y. c7 (w1 (a1 h x)) (w1 (a1 h y)) = w1 (a1 h (c2 x y));
!!h ha x y.
c7 (w1 (a1 h (a2 ha x))) (w1 (a1 h (a2 ha y))) =
w1 (a1 h (a2 ha (c3 x y)));
!!x y z. a4 x (c5 y z) = c5 (a4 x y) (a4 x z);
!!x1 x2 y1 y2. c4 (c5 x1 y1) (c5 x2 y2) = c5 (c4 x1 x2) (c4 y1 y2);
!!x. LRunit c8 (w1 (a1 u x)); !!x y. LRunit c5 (a5 y (a6 u));
!!x y z. LRunit c4 (a4 z (a5 y (a6 u)));
!!h x1 x2. c5 (a1 h x1) (a1 h x2) = a1 h (c2 x1 x2) |]
==> w2 (tFold a4 c4 (tMap (tFold a5 c5 o tMap (tFoldC a6 c6)) (inverse2 u t))) =
w1 (tFold a1 c1 (tMap (tFold a2 c2 o tMap (tFoldC a3 c3)) t))
lemma wrapped_tFold:
[| assoc c4; assoc c7; !!x y. w2 (c4 x y) = c7 (w2 x) (w2 y) |] ==> w2 (tFold a4 c4 t) = tFold (%h t. w2 (a4 h t)) c7 t
lemma wrapped_foldr1:
[| assoc c5; assoc c8; !!x y. f (c5 x y) = c8 (f x) (f y) |] ==> f (foldr1 c5 xs) = foldr1 c8 (map1 f xs)
lemma wrapped2_tFold:
[| assoc c5; assoc c7;
!!h x y. w2 (a4 h (c5 x y)) = c7 (w2 (a4 h x)) (w2 (a4 h y)) |]
==> (%x. w2 (a4 x (tFold a8 c5 t))) =
(%x. tFold (%h t. w2 (a4 x (a8 h t))) c7 t)
lemma tFold_tFold_tFold_inverse2_gen:
[| assoc c1; assoc c2; assoc c3; assoc c4; assoc c5; assoc c6; assoc c7;
!!h ha hb t. w2 (a4 hb (a5 ha (a6 h t))) = w1 (a1 h (a2 ha (a3 hb t)));
!!x y. c7 (w1 x) (w1 y) = w1 (c1 x y);
!!h ha x y.
w1 (c1 (a1 h (a2 ha x)) (a1 h (a2 ha y))) = w1 (a1 h (a2 ha (c3 x y)));
!!h x y. w2 (a4 h (c5 x y)) = w2 (c4 (a4 h x) (a4 h y));
!!x y. w2 (c4 x y) = c7 (w2 x) (w2 y);
!!x1 x2 y1 y2.
c7 (w2 (c4 x1 x2)) (w2 (c4 y1 y2)) = w2 (c4 (c4 x1 y1) (c4 x2 y2));
!!x. LRunit c7 (w1 (a1 u x));
!!h x y. w1 (c1 (a1 h x) (a1 h y)) = w1 (a1 h (c2 x y)) |]
==> w2 (tFold a4 c4 (tMap (tFold a5 c5 o tMap (tFold a6 c6)) (inverse2 u t))) =
w1 (tFold a1 c1 (tMap (tFold a2 c2 o tMap (tFold a3 c3)) t))
lemma tFold_tFold_tFoldC_inverse2_gen:
[| assoc c1; assoc c2; assoc c3; assoc c4; assoc c5; assoc c6; assoc c7;
!!h ha hb. w2 (a4 hb (a5 ha (a6 h))) = w1 (a1 h (a2 ha (a3 hb)));
!!x y. c7 (w1 x) (w1 y) = w1 (c1 x y);
!!h ha x y.
w1 (c1 (a1 h (a2 ha x)) (a1 h (a2 ha y))) = w1 (a1 h (a2 ha (c3 x y)));
!!h x y. w2 (a4 h (c5 x y)) = w2 (c4 (a4 h x) (a4 h y));
!!x y. w2 (c4 x y) = c7 (w2 x) (w2 y);
!!x1 x2 y1 y2.
c7 (w2 (c4 x1 x2)) (w2 (c4 y1 y2)) = w2 (c4 (c4 x1 y1) (c4 x2 y2));
!!x. LRunit c7 (w1 (a1 u x));
!!h x y. w1 (c1 (a1 h x) (a1 h y)) = w1 (a1 h (c2 x y)) |]
==> w2 (tFold a4 c4 (tMap (tFold a5 c5 o tMap (tFoldC a6 c6)) (inverse2 u t))) =
w1 (tFold a1 c1 (tMap (tFold a2 c2 o tMap (tFoldC a3 c3)) t))
lemma id_tFold_tFold_tFoldC_inverse2_gen:
[| assoc c1; assoc c2; assoc c3; assoc c5; assoc c6;
!!h ha hb. a4 hb (a5 ha (a6 h)) = a1 h (a2 ha (a3 hb));
!!h ha x y. c1 (a1 h (a2 ha x)) (a1 h (a2 ha y)) = a1 h (a2 ha (c3 x y));
!!h x y. a4 h (c5 x y) = c1 (a4 h x) (a4 h y);
!!x1 x2 y1 y2. c1 (c1 x1 x2) (c1 y1 y2) = c1 (c1 x1 y1) (c1 x2 y2);
!!x. LRunit c1 (a1 u x); !!h x y. c1 (a1 h x) (a1 h y) = a1 h (c2 x y) |]
==> id (tFold a4 c1 (tMap (tFold a5 c5 o tMap (tFoldC a6 c6)) (inverse2 u t))) =
id (tFold a1 c1 (tMap (tFold a2 c2 o tMap (tFoldC a3 c3)) t))