Up to index of Isabelle/HOL/Tables
theory Tables2 = Tables:
header {* Functions Interacting Directly with the Second Table Dimension *}
theory Tables2 = Tables:
subsection {* Construction in the Second Dimension *}
constdefs
addH2 :: "'h2 \<Rightarrow> ('h1, 't) T \<Rightarrow> ('h1, ('h2, 't) T) T"
"addH2 h2 == tFold (% h1 t . addH h1 (addH h2 t)) hConc"
lemma addH2_addH[simp]: "addH2 h2 (addH h1 t) = addH h1 (addH h2 t)"
by (simp add: addH2_def)
lemma addH2_hConc[simp]: "addH2 h2 (hConc t1 t2) = hConc (addH2 h2 t1) (addH2 h2 t2)"
by (simp add: addH2_def)
lemma addH2_hCons[simp]: "addH2 h2 (hCons p t) = hCons (fst p, addH h2 (snd p)) (addH2 h2 t)"
by (simp add: addH2_def hCons)
lemma hHead_addH2[simp]: "hHead (addH2 h t) = (fst (hHead t), addH h (snd (hHead t)))"
apply (simp add: addH2_def)
apply (induct_tac t rule: T_cons_induct)
apply simp_all
done
lemma addH2_tMap: "addH2 h = tMap (addH h)"
by (simp add: addH2_def tMap_def)
lemma tFold_addH2[simp]:
"assoc c \<Longrightarrow> tFold a c (addH2 h t) = tFold (\<lambda>ha t0. a ha (addH h t0)) c t"
by (simp add: addH2_tMap)
lemma tFold_tFold_addH2:
"\<lbrakk> assoc c2 \<rbrakk> \<Longrightarrow>
tFold a2 c2 (tMap (tFold a1 c1) (addH2 h t)) =
tFold (\<lambda> h0 t0 . a2 h0 (a1 h t0)) c2 t"
by (induct_tac t rule: T_induct, simp_all)
lemma tMap_tFold_addH2:
"assoc c1 \<Longrightarrow>
tMap (tFold a1 c1) (addH2 h t) = tFold (\<lambda> h0 t0 . addH h0 (a1 h t0)) hConc t"
by (induct_tac t rule: T_induct, simp_all)
constdefs
vConc0 :: "('h1 * ('h2, 't) T) \<Rightarrow> ('h1 * ('h2, 't) T) \<Rightarrow> ('h1 * ('h2, 't) T)"
"vConc0 == % p1 p2 . (fst p1, hConc (snd p1) (snd p2))"
lemma vConc0[simp]: "vConc0 (h1,t1) (h2,t2) = (h1, hConc t1 t2)"
by (simp add: vConc0_def)
lemma fst_vConc0[simp]: "fst (vConc0 p1 p2) = fst p1"
by (simp add: vConc0_def)
lemma snd_vConc0[simp]: "snd (vConc0 p1 p2) = hConc (snd p1) (snd p2)"
by (simp add: vConc0_def)
lemma vConc0_assoc[simp]: "vConc0 (vConc0 p1 p2) p3 = vConc0 p1 (vConc0 p2 p3)"
proof -
have "vConc0 (vConc0 p1 p2) p3 = vConc0 (vConc0 (fst p1, snd p1) (fst p2, snd p2)) (fst p3, snd p3)" by simp
also have "\<dots> = vConc0 (fst p1, snd p1) (vConc0 (fst p2, snd p2) (fst p3, snd p3))" by (simp only: vConc0 hConc_assoc)
also have "\<dots> = vConc0 p1 (vConc0 p2 p3)" by simp
finally show ?thesis .
qed
lemma assoc_vConc0[simp]: "assoc vConc0"
by (rule assoc_intro, simp)
constdefs
vConc :: "('h1, ('h2, 't) T) T \<Rightarrow> ('h1, ('h2, 't) T) T \<Rightarrow> ('h1, ('h2, 't) T) T"
"vConc == tZipWith vConc0"
lemma assoc_vConc[simp]: "assoc vConc"
by (simp add: vConc_def)
lemma vConc_addH[simp]:
"vConc (addH h t1) t2 = uncurry addH (vConc0 (h, t1) (hHead t2))"
by (simp add: vConc_def)
lemma hHead_vConc_hCons[simp]:
"hHead (vConc (hCons p1 t1) t2) = vConc0 p1 (hHead t2)"
by (simp add: vConc_def)
lemma vConc__addH[simp]:
"vConc t1 (addH h t2) = uncurry addH (vConc0 (hHead t1) (h, t2))"
by (simp add: vConc_def)
lemma hHead_vConc__hCons[simp]:
"hHead (vConc t1 (hCons p2 t2)) = vConc0 (hHead t1) p2"
by (simp add: vConc_def)
lemma vConc_hCons_hCons[simp]:
"vConc (hCons p1 t1) (hCons p2 t2) = hCons (vConc0 p1 p2) (vConc t1 t2)"
by (simp add: vConc_def)
constdefs
vCons :: "('h2 * ('h1, 't) T) \<Rightarrow> ('h1, ('h2, 't) T) T \<Rightarrow> ('h1, ('h2, 't) T) T"
"vCons p t == vConc (uncurry addH2 p) t"
lemma vCons: "vCons (h,t0) t = vConc (addH2 h t0) t"
by (simp add: vCons_def)
lemma vCons_addH[simp]:
"vCons p (addH h t) = addH (fst (hHead (uncurry addH2 p)))
(hConc (snd (hHead (uncurry addH2 p))) t)"
by (simp add: vCons_def)
lemma hHead_vCons_hCons[simp]:
"hHead (vCons p1 (hCons p2 t2)) = vConc0 (hHead (uncurry addH2 p1)) p2"
by (simp add: vCons_def)
lemma vCons_hCons_hCons[simp]:
"vCons (h, hCons p1 t1) (hCons p2 t2) =
hCons (vConc0 (fst p1, addH h (snd p1)) p2) (vCons (h, t1) t2)"
by (simp add: vCons_def vConc_def)
lemma headers_addH2[simp]: "headers (addH2 h t) = headers t"
by (induct_tac t rule: T_induct, simp_all)
lemma headers_vCons_0:
"ALL t p . headers (snd p) = headers t \<longrightarrow> headers (vCons p t) = headers t"
apply (rule T_cons_inductA, simp_all)
apply (intro strip, drule headers_eq_singleton)
apply (erule exE, simp)
apply (intro strip, drule headers_eq_cons1)
apply (erule exE, erule exE, erule conjE, simp)
done
lemma headers_vCons[simp]:
"headers (snd p) = headers t \<Longrightarrow> headers (vCons p t) = headers t"
apply (insert headers_vCons_0)
apply (drule_tac x=t in spec)
apply (drule_tac x=p in spec)
apply simp
done
lemma tMap_h_vConc_0:
"\<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>
ALL t2 hs1 hs2a hs2b .
regSkelOuter2 t1 = Some (hs1, hs2a) \<longrightarrow>
regSkelOuter2 t2 = Some (hs1, hs2b) \<longrightarrow>
tMap h (vConc t1 t2) = vConc (tMap h t1) (tMap h t2)"
apply (induct_tac t1 rule: T_cons_induct, simp_all)
apply (rule allI)
apply (induct_tac t2 rule: T_cons_induct, simp_all)
apply (rule allI)
apply (induct_tac t2a rule: T_cons_induct, simp_all)
apply (intro strip, case_tac p, simp)
apply (erule exE, drule optThen_result_Some, erule exE, erule conjE)
apply (split split_if_asm) prefer 2 apply simp
apply (drule optThen_result_Some, erule exE, erule conjE)
apply (split split_if_asm) prefer 2 apply simp
apply (case_tac y, case_tac ya, case_tac pa, simp)
apply (erule conjE)+
apply (rotate_tac -2, drule sym, simp, drule cons1_inj, erule conjE, simp)
done
lemma tMap_h_vConc[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 t1 = Some (hs1, hs2a);
regSkelOuter2 t2 = Some (hs1, hs2b)
\<rbrakk> \<Longrightarrow>
tMap h (vConc t1 t2) = vConc (tMap h t1) (tMap h t2)"
by (insert tMap_h_vConc_0 [of h t1], auto)
lemma tMap_const_vConc_0:
"ALL t2 hs1a hs1b hs2a hs2b .
regSkelOuter2 t1 = Some (hs1a, hs2a) \<longrightarrow>
regSkelOuter2 t2 = Some (hs1b, hs2b) \<longrightarrow>
hs1a = hs1b \<longrightarrow>
tMap (const t) (vConc t1 t2) = tMap (const t) t1"
apply (induct_tac t1 rule: T_cons_induct, simp)
apply (rule allI)
apply (induct_tac t2a rule: T_cons_induct, simp_all)
apply (intro strip, erule exE)
apply (drule optThen_result_Some, erule exE, erule conjE)
apply (case_tac p, case_tac y, simp)
apply (split split_if_asm, simp, simp)
apply (intro strip, erule exE, erule exE)
apply (drule optThen_result_Some, erule exE, erule conjE)
apply (drule optThen_result_Some, erule exE, erule conjE)
apply (case_tac p, case_tac y, simp)
apply (case_tac pa, case_tac ya, simp)
apply (split split_if_asm, simp)
apply (split split_if_asm, simp)
apply (erule conjE, rotate_tac -2, drule sym, simp)
apply (drule cons1_inj, erule conjE, simp_all)
done
lemma tMap_const_vConc[simp]:
"\<lbrakk> regSkelOuter2 t1 = Some (hs1a, hs2a);
regSkelOuter2 t2 = Some (hs1b, hs2b);
hs1a = hs1b
\<rbrakk> \<Longrightarrow>
tMap (const t) (vConc t1 t2) = tMap (const t) t1"
by (insert tMap_const_vConc_0 [of t1 t], auto)
lemma tMap_const_hConc:
"tMap (const (hConc t1 t2)) t = vConc (tMap (const t1) t) (tMap (const t2) t)"
apply (cut_tac "t2.0"=t1 and "t1.0"=t in regSkelOuter2_tMap_const)
apply (cut_tac "t2.0"=t2 and "t1.0"=t in regSkelOuter2_tMap_const)
apply (erule mp1)
apply (erule mp1)
apply (induct_tac t rule: T_cons_induct, simp_all)
done
subsection {* Regular Skeletons and the Second Dimension *}
lemma regSkelOuter1_addH2[simp]:
"regSkelOuter1 (addH2 h t) = Some (headers t)"
by (simp add: regSkelOuter1_def)
lemma regSkelStep_addH2:
"regSkelStep rs (addH2 h t) = option_map (Pair (headers t)) (tFold (\<lambda>h. rs) optEq (addH2 h t))"
by (simp add: regSkelStep_def)
lemma regSkelStep_Some_0:
"ALL hs . regSkelStep rs t = Some (hs,r) \<longrightarrow> headers t = hs"
apply (induct_tac t rule: T_cons_induct, simp_all)
apply (intro strip)
apply (drule optThen_result_Some)
apply (erule exE, erule conjE)
apply (drule optThen_result_Some)
apply (erule exE, erule conjE)
apply (case_tac "y = snd ya", simp_all)
apply (erule conjE)
apply (rotate_tac -1, drule sym, simp)
apply (drule_tac x="fst ya" in spec)
apply (rotate_tac 3, drule sym, simp)
done
lemma regSkelStep_Some:
"regSkelStep rs t = Some (hs,r) \<Longrightarrow> headers t = hs"
apply (insert regSkelStep_Some_0 [of rs t r])
apply (drule_tac x=hs in spec, simp)
done
lemma regSkelOuter2_addH2[simp]:
"regSkelOuter2 (addH2 h t) = Some (headers t, singleton h)"
by (induct_tac t rule: T_induct, simp_all)
lemma regSkelOuter2_eq_Some:
"regSkelOuter2 t = Some (hs1,hs2) \<Longrightarrow> headers t = hs1"
by (simp add: regSkelStep_Some regSkelOuter2_def)
lemma regSkelOuter2_vCons_0:
"ALL t p . headers (snd p) = headers t \<longrightarrow>
regSkelOuter2 (vCons p t) =
optThen (tFold (\<lambda>h t . Some (headers t)) optEq (uncurry addH2 p)) (\<lambda> hs1 .
optThen (regSkelOuter2 t) (\<lambda> p2 . Some (headers t, append hs1 (snd p2))))"
apply (rule T_cons_inductA)
txt {* Case 1: @{text "t=addH"} *}
apply (simp add: regSkelOuter2_def)
apply (intro strip)
apply (drule headers_eq_singleton)
apply (erule exE)
apply (simp add: regSkelOuter1_def regSkelOuter2_def cons1 singleton_def append_def neList_def Abs_neList_inverse)
txt {* Case 2: @{text "t=hCons"} *}
apply (intro strip)
apply (simp add: regSkelOuter2_def)
apply (drule headers_eq_cons1)
apply (erule exE, erule exE, erule conjE)
apply (subgoal_tac "vCons pa = vCons (fst pa, hCons (fst p, t0) t2a)")
prefer 2
apply (drule sym, simp)
apply (rotate_tac -1, drule sym, rotate_tac -1, erule subst)
apply simp
apply (case_tac "regSkelStep regSkelOuter1 t2", simp)
apply (simp add: regSkelOuter1_def)
apply (case_tac "regSkelOuter1 (snd p)", simp)
txt {* Case 2.1: @{text "regSkelOuter1 (snd p) = None"} *}
apply (rule append_inj2_neq_conv)
apply (drule_tac x="fst pa" in spec)
apply (drule_tac x="t2a" in spec)
apply (simp add: regSkelOuter1_def)
txt {* Case 2.2: @{text "regSkelOuter1 (snd p) = Some aa"} *}
apply simp
apply (rule conjI)
txt {* Case 2.2.1: @{text "aa = snd a"} *}
apply (intro strip, rule append_inj2_conv)
apply (simp add: regSkelOuter1_def)
txt {* Case 2.2.2: @{text "aa \<noteq> snd a"} *}
apply (intro strip, rule append_inj2_neq_conv)
apply (simp add: regSkelOuter1_def)
done
lemma regSkelOuter2_vCons:
"headers (snd p) = headers t \<Longrightarrow>
regSkelOuter2 (vCons p t) =
optThen (tFold (\<lambda>h t . Some (headers t)) optEq (uncurry addH2 p)) (\<lambda> hs1 .
optThen (regSkelOuter2 t) (\<lambda> p2 . Some (headers t, append hs1 (snd p2))))"
apply (insert regSkelOuter2_vCons_0)
apply (drule_tac x=t in spec)
apply (drule_tac x=p in spec)
apply simp
done
lemma regSkelOuter2_Some_vCons:
"\<lbrakk> regSkelOuter2 t = Some (hs1, hs2); headers (snd p) = headers t \<rbrakk> \<Longrightarrow>
regSkelOuter2 (vCons p t) = Some (hs1, cons1 (fst p) hs2)"
by (simp add: regSkelOuter2_vCons cons1)
lemma regSkelOuter2_vConc_0:
"ALL t1 t2 hs1a hs2a hs1b hs2b . headers t1 = headers t2 \<longrightarrow>
regSkelOuter2 t1 = Some (hs1a, hs2a) \<longrightarrow>
regSkelOuter2 t2 = Some (hs1b, hs2b) \<longrightarrow>
hs1a = hs1b \<longrightarrow>
regSkelOuter2 (vConc t1 t2) = Some (hs1a, append hs2a hs2b)"
apply (rule T_cons_inductA)
apply (rule T_cons_inductA)
apply simp
apply (intro strip)
apply (simp add: regSkelOuter1_def regSkelOuter2_def)
apply (rule T_cons_inductA)
apply simp
apply simp
apply (intro strip, drule cons1_inj, erule conjE)
apply (drule_tac x="t2a" in spec)
apply (simp add: regSkelOuter1_def)
apply (case_tac "regSkelOuter2 t2", simp)
apply (case_tac "regSkelOuter2 t2a", simp_all)
apply (case_tac "headers (snd p) = snd a", simp_all)
apply (case_tac "headers (snd pa) = snd aa", simp_all)
apply (erule conjE, erule conjE)
apply (drule_tac x="fst a" in spec)
apply (drule_tac x="hs2a" in spec)
apply (drule mp, fastsimp)
apply (drule_tac x=hs2b in spec)
apply (drule mp)
apply (subgoal_tac "cons1 (fst pa) (fst a) = cons1 (fst pa) (fst aa)")
prefer 2
apply bestsimp
apply (drule cons1_inj, erule conjE, fastsimp)
apply simp
done
lemma regSkelOuter2_vConc[simp]:
"\<lbrakk> regSkelOuter2 t1 = Some (hs1a, hs2a);
regSkelOuter2 t2 = Some (hs1b, hs2b);
hs1a = hs1b
\<rbrakk> \<Longrightarrow> regSkelOuter2 (vConc t1 t2) = Some (hs1a, append hs2a hs2b)"
apply (insert regSkelOuter2_vConc_0)
apply (drule_tac x=t1 in spec)
apply (drule_tac x=t2 in spec)
apply (drule_tac x=hs1a in spec)
apply (drule_tac x=hs2a in spec)
apply (drule_tac x=hs1b in spec)
apply (drule_tac x=hs2b in spec)
apply (frule regSkelOuter2_eq_Some)
apply (rotate_tac 1, frule regSkelOuter2_eq_Some, simp)
done
(* The following incompletable proof attempt can be used to see why the
equality in this statement holds only for the Some case covered above:
lemma regSkelStep_vConc[simp]:
"ALL t1 t2 . headers t1 = headers t2 \<longrightarrow>
regSkelOuter2 (vConc t1 t2) =
optThen (regSkelOuter2 t1) (\<lambda> p1 .
optThen (regSkelOuter2 t2) (\<lambda> p2 .
if fst p1 = fst p2
then Some (fst p1, append (snd p1) (snd p2))
else None))"
apply (rule T_cons_inductA)
apply (rule T_cons_inductA)
apply (simp del: regSkelOuter2_def)
apply (intro strip)
apply (drule singleton_inj)
apply (simp add: regSkelOuter1_def)
apply (simp del: regSkelOuter2_def)
apply (rule T_cons_inductA)
apply (simp del: regSkelOuter2_def)
apply (simp del: regSkelOuter2_def)
apply (intro strip, drule cons1_inj, erule conjE)
apply (drule_tac x="t2a" in spec)
apply (simp add: regSkelOuter1_def del: regSkelOuter2_def)
apply (case_tac "regSkelOuter2 t2")
apply (simp del: regSkelOuter2_def)
apply (case_tac "regSkelOuter2 t2a")
apply (simp del: regSkelOuter2_def)
apply (simp del: regSkelOuter2_def)
apply (case_tac "fst a = fst aa")
apply (simp_all del: regSkelOuter2_def)
apply ((rule conjI)+, tactic "ALLGOALS strip_tac")+
apply (simp_all del: regSkelOuter2_def)
apply (erule append_inj1)
apply (erule append_inj2)
apply ((rule conjI)+, tactic "ALLGOALS strip_tac")
apply (erule append_inj1)
apply (drule append_inj1)
apply (simp del: regSkelOuter2_def)
apply ((rule conjI)+, tactic "ALLGOALS strip_tac")
apply (erule append_inj1)
apply (erule append_inj1)
apply ((rule conjI)+, tactic "ALLGOALS strip_tac")+
apply (erule append_inj2)
apply (drule append_inj2)
apply (simp del: regSkelOuter2_def)
apply (drule append_inj2_neq)
apply (drule append_inj1_neq)
apply (simp del: regSkelOuter2_def)
*)
lemma headers_vConc[simp]:
"\<lbrakk> regSkelOuter2 t1 = Some (hs1,hs2a);
regSkelOuter2 t2 = Some (hs1,hs2b)
\<rbrakk> \<Longrightarrow> headers (vConc t1 t2) = headers t1"
apply (frule_tac "t1.0"=t1 and "t2.0"=t2 in regSkelOuter2_vConc, assumption)
apply simp
apply (rotate_tac -1, drule regSkelOuter2_eq_Some)
apply (drule regSkelOuter2_eq_Some [THEN sym], simp)
done
lemma vConc_hConc_0:
"ALL t3 h1 v1 v2 t2 t4 h2 .
regSkelOuter2 t1 = Some (h1,v1) \<longrightarrow>
regSkelOuter2 t2 = Some (h2,v1) \<longrightarrow>
regSkelOuter2 t3 = Some (h1,v2) \<longrightarrow>
regSkelOuter2 t4 = Some (h2,v2) \<longrightarrow>
vConc (hConc t1 t2) (hConc t3 t4) = hConc (vConc t1 t3) (vConc t2 t4)"
apply (induct_tac t1 rule: T_cons_induct, simp add: regSkelOuter1_def)
apply (rule allI)
apply (induct_tac t3 rule: T_cons_induct, simp add: regSkelOuter1_def)
apply (intro strip, drule singleton_inj)
apply (simp add: hCons_p [THEN sym])
txt {* 1.2 *}
apply (intro strip, simp)
apply (drule optThen_result_Some, erule exE, erule conjE)
apply (simp add: regSkelOuter1_def)
apply (case_tac p, simp)
apply (split split_if_asm, simp, simp)
txt {* 2 *}
apply (rule allI)
apply (erule mp1)
apply (induct_tac t3 rule: T_cons_induct, simp add: regSkelOuter1_def)
apply (intro strip)
apply (drule optThen_result_Some, erule exE, erule conjE)
apply (split split_if_asm, simp)
apply (erule conjE, rotate_tac -2, drule sym, simp, simp)
txt {* 2.2 *}
apply (intro strip, simp add: regSkelOuter1_def del: vConc_hCons_hCons)
apply (drule optThen_result_Some, erule exE, erule conjE)+
apply (case_tac y)
apply (case_tac ya)
apply (case_tac p)
apply (case_tac pa)
apply (simp del: vConc_hCons_hCons)
apply (split split_if_asm, simp)
apply (split split_if_asm, simp)
apply (erule conjE, rotate_tac -2, drule sym, simp)
apply (drule cons1_inj, erule conjE, simp)
apply simp
apply simp
done
lemma vConc_hConc:
"\<lbrakk> regSkelOuter2 t1 = Some (h1,v1);
regSkelOuter2 t2 = Some (h2,v1);
regSkelOuter2 t3 = Some (h1,v2);
regSkelOuter2 t4 = Some (h2,v2) \<rbrakk> \<Longrightarrow>
vConc (hConc t1 t2) (hConc t3 t4) = hConc (vConc t1 t3) (vConc t2 t4)"
by (insert vConc_hConc_0 [of t1], auto)
subsection {* Table Transposition *}
constdefs
tTranspose :: "('h1, ('h2, 't) T) T \<Rightarrow> ('h2, ('h1, 't) T) T"
"tTranspose == tFold addH2 vConc"
lemma tTranspose_addH[simp]: "tTranspose (addH h t) = addH2 h t"
by (simp add: tTranspose_def)
lemma tTranspose_hConc[simp]: "tTranspose (hConc t1 t2) = vConc (tTranspose t1) (tTranspose t2)"
by (simp add: tTranspose_def)
lemma tTranspose_hCons[simp]: "tTranspose (hCons p t) = vCons p (tTranspose t)"
by (simp add: tTranspose_def hCons vCons_def)
lemma regSkelOuter2_tTranspose_via_T_cons_induct:
"ALL hs1 hs2 . regSkelOuter2 t = Some (hs1,hs2) \<longrightarrow>
regSkelOuter2 (tTranspose t) = Some (hs2,hs1)"
apply (induct_tac t rule: T_cons_induct)
apply (simp add: regSkelOuter1_def regSkelOuter2_def)
apply (induct_tac t0 rule: T_cons_induct, simp, simp)
apply (subst tTranspose_hCons)
apply (intro strip)
apply (simp only: regSkelOuter2_hCons)
apply (case_tac "regSkelOuter2 t2", simp, simp)
apply (split split_if_asm,simp_all, erule conjE)
apply (case_tac "a", simp)
apply (frule_tac p="p" in regSkelOuter2_Some_vCons)
apply (simp add: regSkelOuter2_def)
apply (drule regSkelStep_Some, simp, simp)
done
lemma regSkelOuter2_tTranspose_via_T_induct:
"ALL hs1 hs2 . regSkelOuter2 t = Some (hs1,hs2) \<longrightarrow>
regSkelOuter2 (tTranspose t) = Some (hs2,hs1)"
apply (induct_tac t rule: T_induct)
apply (simp add: regSkelOuter1_def regSkelOuter2_def)
apply (induct_tac t0 rule: T_induct, simp, simp)
apply (subst tTranspose_hConc)
apply (intro strip, simp only: regSkelOuter2_hConc)
apply (case_tac "regSkelOuter2 t1", simp, simp)
apply (drule optThen_result_Some, erule exE, erule conjE)
apply (case_tac "snd a = snd y", simp_all)
apply (erule conjE)
apply (drule_tac x="fst a" in spec)
apply (drule_tac x="hs2" in spec)
apply (drule mp, fastsimp)
apply (drule_tac x="fst y" in spec)
apply (drule_tac x="hs2" in spec)
apply (drule mp, fastsimp)
apply (rotate_tac -4, drule sym)
apply (simp add: regSkelOuter1_def)
done
theorem regSkelOuter2_tTranspose:
"regSkelOuter2 t = Some (hs1,hs2) \<Longrightarrow>
regSkelOuter2 (tTranspose t) = Some (hs2,hs1)"
by (insert regSkelOuter2_tTranspose_via_T_induct [of t], auto)
lemma tFold_tFold_vConc_0:
"\<lbrakk> assoc c1; assoc c2;
\<And> x y z . a2 x (c1 y z) = c1 (a2 x y) (a2 x z);
\<And> x1 x2 y1 y2 . c2 (c1 x1 y1) (c1 x2 y2) = c1 (c2 x1 x2) (c2 y1 y2)
\<rbrakk> \<Longrightarrow>
ALL t2 hs1a hs2a hs1b hs2b .
regSkelOuter2 t1 = Some (hs1a,hs2a) \<longrightarrow>
regSkelOuter2 t2 = Some (hs1b,hs2b) \<longrightarrow>
hs1a = hs1b \<longrightarrow>
tFold a2 c2 (tMap (tFold a1 c1) (vConc t1 t2)) =
c1 (tFold a2 c2 (tMap (tFold a1 c1) t1))
(tFold a2 c2 (tMap (tFold a1 c1) t2))"
apply (induct_tac t1 rule: T_cons_induct)
apply (rule T_cons_inductA)
txt {* Case 1.1: @{text "t1=addH, t2=addH"} *}
apply (intro strip)
apply (simp add: regSkelOuter1_def regSkelOuter2_def)
apply (erule conjE, erule conjE)
apply (subgoal_tac "singleton h = singleton ha", drule singleton_inj, simp)
apply fastsimp
txt {* Case 1.2: @{text "t1=addH, t2=hCons"} *}
apply (intro strip)
apply (drule regSkelOuter2_hCons_eq_Some)
apply (erule exE, erule exE, erule exE, erule conjE, erule conjE, erule conjE)
apply (simp add: regSkelOuter2_def)
txt {* Case 2: @{text "t1=hCons"} *}
apply (rule T_cons_inductA)
txt {* Case 2.1: @{text "t1=hCons, t2=addH"} *}
apply (intro strip)
apply (drule regSkelOuter2_hCons_eq_Some)
apply (erule exE, erule exE, erule exE, erule conjE, erule conjE, erule conjE)
apply (drule regSkelOuter2_addH_eq_Some, erule conjE)
apply simp
txt {* Case 2.2: @{text "t1=hCons, t2=hCons"} *}
apply (intro strip)
apply (drule regSkelOuter2_hCons_eq_Some)
apply (erule exE, erule exE, erule exE, erule conjE, erule conjE, erule conjE)
apply (drule regSkelOuter2_hCons_eq_Some)
apply (erule exE, erule exE, erule exE, erule conjE, erule conjE, erule conjE)
apply simp
apply (drule cons1_inj, erule conjE, simp)
done
lemma tFold_tFold_vConc:
"\<lbrakk> assoc c1; assoc c2;
\<And> x y z . a2 x (c1 y z) = c1 (a2 x y) (a2 x z);
\<And> x1 x2 y1 y2 . c2 (c1 x1 y1) (c1 x2 y2) = c1 (c2 x1 x2) (c2 y1 y2);
regSkelOuter2 t1 = Some (hs1a,hs2a);
regSkelOuter2 t2 = Some (hs1b,hs2b);
hs1a = hs1b
\<rbrakk> \<Longrightarrow>
tFold a2 c2 (tMap (tFold a1 c1) (vConc t1 t2)) =
c1 (tFold a2 c2 (tMap (tFold a1 c1) t1))
(tFold a2 c2 (tMap (tFold a1 c1) t2))"
by (insert tFold_tFold_vConc_0 [of c1 c2 a2 t1 a1], auto)
lemma tTranspose_tFold2_0:
"\<lbrakk> assoc c1; assoc c2;
\<And> x y z . a1 x (a2 y z) = a2 y (a1 x z);
\<And> x y z . a1 x (c2 y z) = c2 (a1 x y) (a1 x z);
\<And> x y z . a2 x (c1 y z) = c1 (a2 x y) (a2 x z);
\<And> x1 x2 y1 y2 . c2 (c1 x1 y1) (c1 x2 y2) = c1 (c2 x1 x2) (c2 y1 y2)
\<rbrakk> \<Longrightarrow>
ALL hs1 hs2 . regSkelOuter2 t = Some (hs1,hs2) \<longrightarrow>
tFold a2 c2 (tMap (tFold a1 c1) (tTranspose t)) =
tFold a1 c1 (tMap (tFold a2 c2) t)"
apply (induct_tac t rule: T_induct)
apply (induct_tac t0 rule: T_induct)
apply (intro strip, simp)
apply (intro strip, simp add: regSkelOuter1_def regSkelOuter2_def)
apply (intro strip)
apply (drule regSkelOuter2_hConc_eq_Some)
apply (erule exE, erule exE, erule conjE, erule conjE)
apply (simp del: tFold_tMap)
apply (subst tFold_tFold_vConc)
apply (assumption, assumption, simp, simp)
apply (erule regSkelOuter2_tTranspose)
apply (erule regSkelOuter2_tTranspose)
apply simp
apply simp
done
theorem tTranspose_tFold2:
"\<lbrakk> assoc c1; assoc c2;
\<And> x y z . a1 x (a2 y z) = a2 y (a1 x z);
\<And> x y z . a1 x (c2 y z) = c2 (a1 x y) (a1 x z);
\<And> x y z . a2 x (c1 y z) = c1 (a2 x y) (a2 x z);
\<And> x1 x2 y1 y2 . c2 (c1 x1 y1) (c1 x2 y2) = c1 (c2 x1 x2) (c2 y1 y2);
regSkelOuter2 t = Some (hs1,hs2)
\<rbrakk> \<Longrightarrow>
tFold a2 c2 (tMap (tFold a1 c1) (tTranspose t)) =
tFold a1 c1 (tMap (tFold a2 c2) t)"
by (insert tTranspose_tFold2_0 [of c1 c2 a1 a2 t], auto)
lemma tFold_tFold_vConc_gen_0:
"\<lbrakk> assoc c1; assoc c2; assoc c3;
\<And> x y z . a3 x (c2 y z) = c1 (a1 x y) (a1 x z);
\<And> x1 x2 y1 y2 . c3 (c1 x1 y1) (c1 x2 y2) = c1 (c1 x1 x2) (c1 y1 y2)
\<rbrakk> \<Longrightarrow>
ALL t2 hs1a hs2a hs1b hs2b .
regSkelOuter2 t1 = Some (hs1a,hs2a) \<longrightarrow>
regSkelOuter2 t2 = Some (hs1b,hs2b) \<longrightarrow>
hs1a = hs1b \<longrightarrow>
tFold a3 c3 (tMap (tFold a2 c2) (vConc t1 t2)) =
c1 (tFold a1 c1 (tMap (tFold a2 c2) t1))
(tFold a1 c1 (tMap (tFold a2 c2) t2))"
apply (induct_tac t1 rule: T_cons_induct)
apply (rule T_cons_inductA)
txt {* Case 1.1: @{text "t1=addH, t2=addH"} *}
apply (intro strip)
apply (simp add: regSkelOuter1_def regSkelOuter2_def)
apply (erule conjE, erule conjE)
apply (subgoal_tac "singleton h = singleton ha", drule singleton_inj, simp)
apply fastsimp
txt {* Case 1.2: @{text "t1=addH, t2=hCons"} *}
apply (intro strip)
apply (drule regSkelOuter2_hCons_eq_Some)
apply (erule exE, erule exE, erule exE, erule conjE, erule conjE, erule conjE)
apply (simp add: regSkelOuter2_def)
txt {* Case 2: @{text "t1=hCons"} *}
apply (rule T_cons_inductA)
txt {* Case 2.1: @{text "t1=hCons, t2=addH"} *}
apply (intro strip)
apply (drule regSkelOuter2_hCons_eq_Some)
apply (erule exE, erule exE, erule exE, erule conjE, erule conjE, erule conjE)
apply (drule regSkelOuter2_addH_eq_Some, erule conjE)
apply simp
txt {* Case 2.2: @{text "t1=hCons, t2=hCons"} *}
apply (intro strip)
apply (drule regSkelOuter2_hCons_eq_Some)
apply (erule exE, erule exE, erule exE, erule conjE, erule conjE, erule conjE)
apply (drule regSkelOuter2_hCons_eq_Some)
apply (erule exE, erule exE, erule exE, erule conjE, erule conjE, erule conjE)
apply simp
apply (drule cons1_inj, erule conjE, simp)
done
lemma tFold_tFold_vConc_gen:
"\<lbrakk> assoc c1; assoc c2; assoc c3;
\<And> x y z . a3 x (c2 y z) = c1 (a1 x y) (a1 x z);
\<And> x1 x2 y1 y2 . c3 (c1 x1 y1) (c1 x2 y2) = c1 (c1 x1 x2) (c1 y1 y2);
regSkelOuter2 t1 = Some (hs1a,hs2a);
regSkelOuter2 t2 = Some (hs1b,hs2b);
hs1a = hs1b
\<rbrakk> \<Longrightarrow>
tFold a3 c3 (tMap (tFold a2 c2) (vConc t1 t2)) =
c1 (tFold a1 c1 (tMap (tFold a2 c2) t1))
(tFold a1 c1 (tMap (tFold a2 c2) t2))"
by (insert tFold_tFold_vConc_gen_0 [of c1 c2 c3 a3 a1 t1], auto)
(* at least requires tFold a1 c1 = tFold a3 c3
lemma tTranspose_tFold2_gen_0:
"\<lbrakk> assoc c1; assoc c2; assoc c3;
\<And> x y z . a1 y (a2 x z) = a3 x (a2 y z);
\<And> x y z . a1 x (c2 y z) = c3 (a1 x y) (a1 x z);
\<And> x y z . a3 x (c2 y z) = c1 (a1 x y) (a1 x z);
\<And> x1 x2 y1 y2 . c3 (c1 x1 y1) (c1 x2 y2) = c1 (c1 x1 x2) (c1 y1 y2)
\<rbrakk> \<Longrightarrow>
ALL hs1 hs2 . regSkelOuter2 t = Some (hs1,hs2) \<longrightarrow>
tFold (% h t0 . a3 h (tFold a2 c2 t0)) c3 (tTranspose t) =
tFold (% h t0 . a1 h (tFold a2 c2 t0)) c1 t"
apply (induct_tac t rule: T_induct)
apply (induct_tac t0 rule: T_induct)
apply (intro strip)
apply simp
apply (intro strip)
apply (simp add: regSkelOuter1_def regSkelOuter2_def)
apply (intro strip)
apply (drule regSkelOuter2_hConc_eq_Some)
apply (erule exE, erule exE, erule conjE, erule conjE)
apply simp
apply (subst tFold_tFold_vConc_gen)
apply assumption
apply assumption
apply assumption
apply simp
apply simp
apply (erule regSkelOuter2_tTranspose)
apply (erule regSkelOuter2_tTranspose)
apply simp
apply simp
done
*)
lemma tFold_tFold_vConc_wrapped_0:
"\<lbrakk> assoc c1; assoc c2; assoc c3;
\<And> h x y . w1 (a3 h (c2 x y)) = w2 (c1 (a1 h x) (a1 h y));
\<And> x y . w1 (c3 x y) = c4 (w1 x) (w1 y);
\<And> x1 x2 y1 y2 . c4 (w2 (c1 x1 x2)) (w2 (c1 y1 y2)) =
w2 (c1 (c1 x1 y1) (c1 x2 y2))
\<rbrakk> \<Longrightarrow>
ALL t2 hs1a hs2a hs1b hs2b .
regSkelOuter2 t1 = Some (hs1a,hs2a) \<longrightarrow>
regSkelOuter2 t2 = Some (hs1b,hs2b) \<longrightarrow>
hs1a = hs1b \<longrightarrow>
w1 (tFold a3 c3 (tMap (tFold a2 c2) (vConc t1 t2))) =
w2 (c1 (tFold a1 c1 (tMap (tFold a2 c2) t1))
(tFold a1 c1 (tMap (tFold a2 c2) t2)))"
apply (induct_tac t1 rule: T_cons_induct)
apply (rule T_cons_inductA)
txt {* Case 1.1: @{text "t1=addH, t2=addH"} *}
apply (intro strip)
apply (simp add: regSkelOuter1_def regSkelOuter2_def)
apply (erule conjE, erule conjE)
apply (subgoal_tac "singleton h = singleton ha", drule singleton_inj, simp)
apply fastsimp
txt {* Case 1.2: @{text "t1=addH, t2=hCons"} *}
apply (intro strip)
apply (drule regSkelOuter2_hCons_eq_Some)
apply (erule exE, erule exE, erule exE, erule conjE, erule conjE, erule conjE)
apply (simp add: regSkelOuter2_def)
txt {* Case 2: @{text "t1=hCons"} *}
apply (rule T_cons_inductA)
txt {* Case 2.1: @{text "t1=hCons, t2=addH"} *}
apply (intro strip)
apply (drule regSkelOuter2_hCons_eq_Some)
apply (erule exE, erule exE, erule exE, erule conjE, erule conjE, erule conjE)
apply (drule regSkelOuter2_addH_eq_Some, erule conjE)
apply simp
txt {* Case 2.2: @{text "t1=hCons, t2=hCons"} *}
apply (intro strip)
apply (drule regSkelOuter2_hCons_eq_Some)
apply (erule exE, erule exE, erule exE, erule conjE, erule conjE, erule conjE)
apply (drule regSkelOuter2_hCons_eq_Some)
apply (erule exE, erule exE, erule exE, erule conjE, erule conjE, erule conjE)
apply simp
apply (drule cons1_inj, erule conjE, simp)
done
lemma tFold_tFold_vConc_wrapped:
"\<lbrakk> assoc c1; assoc c2; assoc c3;
\<And> h x y . w1 (a3 h (c2 x y)) = w2 (c1 (a1 h x) (a1 h y));
\<And> x y . w1 (c3 x y) = c4 (w1 x) (w1 y);
\<And> x1 x2 y1 y2 . c4 (w2 (c1 x1 x2)) (w2 (c1 y1 y2)) =
w2 (c1 (c1 x1 y1) (c1 x2 y2));
regSkelOuter2 t1 = Some (hs1,hs2a);
regSkelOuter2 t2 = Some (hs1,hs2b)
\<rbrakk> \<Longrightarrow>
w1 (tFold a3 c3 (tMap (tFold a2 c2) (vConc t1 t2))) =
w2 (c1 (tFold a1 c1 (tMap (tFold a2 c2) t1))
(tFold a1 c1 (tMap (tFold a2 c2) t2)))"
by (insert tFold_tFold_vConc_wrapped_0 [of c1 c2 c3 w1 a3 w2 a1 c4 t1], auto)
lemma tTranspose_tFold2_gen_0:
"\<lbrakk> assoc c1; assoc c2; assoc c3; assoc c4; assoc c5;
\<And> x y z . w1 (a1 x (a2 y z)) = w2 (a3 y (a4 x z));
\<And> x y . w1 (c1 x y) = c5 (w1 x) (w1 y);
\<And> x y . w2 (c3 x y) = c5 (w2 x) (w2 y);
\<And> x y z . w1 (a1 x (c2 y z)) = c5 (w1 (a1 x y)) (w1 (a1 x z));
\<And> h x y . w2 (a3 h (c4 x y)) = c5 (w2 (a3 h x)) (w2 (a3 h y));
\<And> x1 x2 y1 y2 . c5 (c5 x1 x2) (c5 y1 y2) = c5 (c5 x1 y1) (c5 x2 y2)
(*
\<And> x y z . a2 x (c1 y z) = c1 (a2 x y) (a2 x z);
*)
\<rbrakk> \<Longrightarrow>
ALL hs1 hs2 . regSkelOuter2 t = Some (hs1,hs2) \<longrightarrow>
w2 (tFold a3 c3 (tMap (tFold a4 c4) (tTranspose t))) =
w1 (tFold a1 c1 (tMap (tFold a2 c2) t))"
apply (induct_tac t rule: T_induct)
apply (induct_tac t0 rule: T_induct)
apply (intro strip, simp)
apply (intro strip, simp add: regSkelOuter1_def regSkelOuter2_def)
apply (intro strip)
apply (drule regSkelOuter2_hConc_eq_Some)
apply (erule exE, erule exE, erule conjE, erule conjE)
apply (simp del: tFold_tMap)
apply (subst tFold_tFold_vConc_wrapped [of c3 c4 c3 w2 a3 w2 a3 c5])
apply (assumption, assumption, assumption)
apply simp
apply simp
apply simp
apply (erule regSkelOuter2_tTranspose)
apply (erule regSkelOuter2_tTranspose)
apply simp
done
lemma tTranspose_tFold2_gen:
"\<lbrakk> assoc c1; assoc c2; assoc c3; assoc c4; assoc c5;
\<And> x y z . w1 (a1 x (a2 y z)) = w2 (a3 y (a4 x z));
\<And> x y . w1 (c1 x y) = c5 (w1 x) (w1 y);
\<And> x y . w2 (c3 x y) = c5 (w2 x) (w2 y);
\<And> x y z . w1 (a1 x (c2 y z)) = c5 (w1 (a1 x y)) (w1 (a1 x z));
\<And> h x y . w2 (a3 h (c4 x y)) = c5 (w2 (a3 h x)) (w2 (a3 h y));
\<And> x1 x2 y1 y2 . c5 (c5 x1 x2) (c5 y1 y2) = c5 (c5 x1 y1) (c5 x2 y2);
regSkelOuter2 t = Some (hs1,hs2)
\<rbrakk> \<Longrightarrow>
w2 (tFold a3 c3 (tMap (tFold a4 c4) (tTranspose t))) =
w1 (tFold a1 c1 (tMap (tFold a2 c2) t))"
by (insert tTranspose_tFold2_gen_0 [of c1 c2 c3 c4 c5 w1 a1 a2 w2 a3 a4 t], auto)
end
lemma addH2_addH:
addH2 h2 (addH h1 t) = addH h1 (addH h2 t)
lemma addH2_hConc:
addH2 h2 (hConc t1 t2) = hConc (addH2 h2 t1) (addH2 h2 t2)
lemma addH2_hCons:
addH2 h2 (hCons p t) = hCons (fst p, addH h2 (snd p)) (addH2 h2 t)
lemma hHead_addH2:
hHead (addH2 h t) = (fst (hHead t), addH h (snd (hHead t)))
lemma addH2_tMap:
addH2 h = tMap (addH h)
lemma tFold_addH2:
assoc c ==> tFold a c (addH2 h t) = tFold (%ha t0. a ha (addH h t0)) c t
lemma tFold_tFold_addH2:
assoc c2
==> tFold a2 c2 (tMap (tFold a1 c1) (addH2 h t)) =
tFold (%h0 t0. a2 h0 (a1 h t0)) c2 t
lemma tMap_tFold_addH2:
assoc c1 ==> tMap (tFold a1 c1) (addH2 h t) = tFold (%h0 t0. addH h0 (a1 h t0)) hConc t
lemma vConc0:
vConc0 (h1, t1) (h2, t2) = (h1, hConc t1 t2)
lemma fst_vConc0:
fst (vConc0 p1 p2) = fst p1
lemma snd_vConc0:
snd (vConc0 p1 p2) = hConc (snd p1) (snd p2)
lemma vConc0_assoc:
vConc0 (vConc0 p1 p2) p3 = vConc0 p1 (vConc0 p2 p3)
lemma assoc_vConc0:
assoc vConc0
lemma assoc_vConc:
assoc vConc
lemma vConc_addH:
vConc (addH h t1) t2 = uncurry addH (vConc0 (h, t1) (hHead t2))
lemma hHead_vConc_hCons:
hHead (vConc (hCons p1 t1) t2) = vConc0 p1 (hHead t2)
lemma vConc__addH:
vConc t1 (addH h t2) = uncurry addH (vConc0 (hHead t1) (h, t2))
lemma hHead_vConc__hCons:
hHead (vConc t1 (hCons p2 t2)) = vConc0 (hHead t1) p2
lemma vConc_hCons_hCons:
vConc (hCons p1 t1) (hCons p2 t2) = hCons (vConc0 p1 p2) (vConc t1 t2)
lemma vCons:
vCons (h, t0) t = vConc (addH2 h t0) t
lemma vCons_addH:
vCons p (addH h t) = addH (fst (hHead (uncurry addH2 p))) (hConc (snd (hHead (uncurry addH2 p))) t)
lemma hHead_vCons_hCons:
hHead (vCons p1 (hCons p2 t2)) = vConc0 (hHead (uncurry addH2 p1)) p2
lemma vCons_hCons_hCons:
vCons (h, hCons p1 t1) (hCons p2 t2) = hCons (vConc0 (fst p1, addH h (snd p1)) p2) (vCons (h, t1) t2)
lemma headers_addH2:
headers (addH2 h t) = headers t
lemma headers_vCons_0:
ALL t p. headers (snd p) = headers t --> headers (vCons p t) = headers t
lemma headers_vCons:
headers (snd p) = headers t ==> headers (vCons p t) = headers t
lemma tMap_h_vConc_0:
[| !!t. headers (h t) = headers t; !!t. h (h t) = h t;
!!t1 t2. h (hConc t1 t2) = hConc (h t1) (h t2) |]
==> ALL t2 hs1 hs2a hs2b.
regSkelOuter2 t1 = Some (hs1, hs2a) -->
regSkelOuter2 t2 = Some (hs1, hs2b) -->
tMap h (vConc t1 t2) = vConc (tMap h t1) (tMap h t2)
lemma tMap_h_vConc:
[| !!t. headers (h t) = headers t; !!t. h (h t) = h t;
!!t1 t2. h (hConc t1 t2) = hConc (h t1) (h t2);
regSkelOuter2 t1 = Some (hs1, hs2a); regSkelOuter2 t2 = Some (hs1, hs2b) |]
==> tMap h (vConc t1 t2) = vConc (tMap h t1) (tMap h t2)
lemma tMap_const_vConc_0:
ALL t2 hs1a hs1b hs2a hs2b.
regSkelOuter2 t1 = Some (hs1a, hs2a) -->
regSkelOuter2 t2 = Some (hs1b, hs2b) -->
hs1a = hs1b --> tMap (const t) (vConc t1 t2) = tMap (const t) t1
lemma tMap_const_vConc:
[| regSkelOuter2 t1 = Some (hs1a, hs2a); regSkelOuter2 t2 = Some (hs1b, hs2b);
hs1a = hs1b |]
==> tMap (const t) (vConc t1 t2) = tMap (const t) t1
lemma tMap_const_hConc:
tMap (const (hConc t1 t2)) t = vConc (tMap (const t1) t) (tMap (const t2) t)
lemma regSkelOuter1_addH2:
regSkelOuter1 (addH2 h t) = Some (headers t)
lemma regSkelStep_addH2:
regSkelStep rs (addH2 h t) = option_map (Pair (headers t)) (tFold (%h. rs) optEq (addH2 h t))
lemma regSkelStep_Some_0:
ALL hs. regSkelStep rs t = Some (hs, r) --> headers t = hs
lemma regSkelStep_Some:
regSkelStep rs t = Some (hs, r) ==> headers t = hs
lemma regSkelOuter2_addH2:
regSkelOuter2 (addH2 h t) = Some (headers t, singleton h)
lemma regSkelOuter2_eq_Some:
regSkelOuter2 t = Some (hs1, hs2) ==> headers t = hs1
lemma regSkelOuter2_vCons_0:
ALL t p.
headers (snd p) = headers t -->
regSkelOuter2 (vCons p t) =
optThen (tFold (%h t. Some (headers t)) optEq (uncurry addH2 p))
(%hs1. optThen (regSkelOuter2 t)
(%p2. Some (headers t, append hs1 (snd p2))))
lemma regSkelOuter2_vCons:
headers (snd p) = headers t
==> regSkelOuter2 (vCons p t) =
optThen (tFold (%h t. Some (headers t)) optEq (uncurry addH2 p))
(%hs1. optThen (regSkelOuter2 t)
(%p2. Some (headers t, append hs1 (snd p2))))
lemma regSkelOuter2_Some_vCons:
[| regSkelOuter2 t = Some (hs1, hs2); headers (snd p) = headers t |] ==> regSkelOuter2 (vCons p t) = Some (hs1, cons1 (fst p) hs2)
lemma regSkelOuter2_vConc_0:
ALL t1 t2 hs1a hs2a hs1b hs2b.
headers t1 = headers t2 -->
regSkelOuter2 t1 = Some (hs1a, hs2a) -->
regSkelOuter2 t2 = Some (hs1b, hs2b) -->
hs1a = hs1b --> regSkelOuter2 (vConc t1 t2) = Some (hs1a, append hs2a hs2b)
lemma regSkelOuter2_vConc:
[| regSkelOuter2 t1 = Some (hs1a, hs2a); regSkelOuter2 t2 = Some (hs1b, hs2b);
hs1a = hs1b |]
==> regSkelOuter2 (vConc t1 t2) = Some (hs1a, append hs2a hs2b)
lemma headers_vConc:
[| regSkelOuter2 t1 = Some (hs1, hs2a); regSkelOuter2 t2 = Some (hs1, hs2b) |] ==> headers (vConc t1 t2) = headers t1
lemma vConc_hConc_0:
ALL t3 h1 v1 v2 t2 t4 h2.
regSkelOuter2 t1 = Some (h1, v1) -->
regSkelOuter2 t2 = Some (h2, v1) -->
regSkelOuter2 t3 = Some (h1, v2) -->
regSkelOuter2 t4 = Some (h2, v2) -->
vConc (hConc t1 t2) (hConc t3 t4) = hConc (vConc t1 t3) (vConc t2 t4)
lemma vConc_hConc:
[| regSkelOuter2 t1 = Some (h1, v1); regSkelOuter2 t2 = Some (h2, v1);
regSkelOuter2 t3 = Some (h1, v2); regSkelOuter2 t4 = Some (h2, v2) |]
==> vConc (hConc t1 t2) (hConc t3 t4) = hConc (vConc t1 t3) (vConc t2 t4)
lemma tTranspose_addH:
tTranspose (addH h t) = addH2 h t
lemma tTranspose_hConc:
tTranspose (hConc t1 t2) = vConc (tTranspose t1) (tTranspose t2)
lemma tTranspose_hCons:
tTranspose (hCons p t) = vCons p (tTranspose t)
lemma regSkelOuter2_tTranspose_via_T_cons_induct:
ALL hs1 hs2.
regSkelOuter2 t = Some (hs1, hs2) -->
regSkelOuter2 (tTranspose t) = Some (hs2, hs1)
lemma regSkelOuter2_tTranspose_via_T_induct:
ALL hs1 hs2.
regSkelOuter2 t = Some (hs1, hs2) -->
regSkelOuter2 (tTranspose t) = Some (hs2, hs1)
theorem regSkelOuter2_tTranspose:
regSkelOuter2 t = Some (hs1, hs2) ==> regSkelOuter2 (tTranspose t) = Some (hs2, hs1)
lemma tFold_tFold_vConc_0:
[| assoc c1; assoc c2; !!x y z. a2 x (c1 y z) = c1 (a2 x y) (a2 x z);
!!x1 x2 y1 y2. c2 (c1 x1 y1) (c1 x2 y2) = c1 (c2 x1 x2) (c2 y1 y2) |]
==> ALL t2 hs1a hs2a hs1b hs2b.
regSkelOuter2 t1 = Some (hs1a, hs2a) -->
regSkelOuter2 t2 = Some (hs1b, hs2b) -->
hs1a = hs1b -->
tFold a2 c2 (tMap (tFold a1 c1) (vConc t1 t2)) =
c1 (tFold a2 c2 (tMap (tFold a1 c1) t1))
(tFold a2 c2 (tMap (tFold a1 c1) t2))
lemma tFold_tFold_vConc:
[| assoc c1; assoc c2; !!x y z. a2 x (c1 y z) = c1 (a2 x y) (a2 x z);
!!x1 x2 y1 y2. c2 (c1 x1 y1) (c1 x2 y2) = c1 (c2 x1 x2) (c2 y1 y2);
regSkelOuter2 t1 = Some (hs1a, hs2a); regSkelOuter2 t2 = Some (hs1b, hs2b);
hs1a = hs1b |]
==> tFold a2 c2 (tMap (tFold a1 c1) (vConc t1 t2)) =
c1 (tFold a2 c2 (tMap (tFold a1 c1) t1))
(tFold a2 c2 (tMap (tFold a1 c1) t2))
lemma tTranspose_tFold2_0:
[| assoc c1; assoc c2; !!x y z. a1 x (a2 y z) = a2 y (a1 x z);
!!x y z. a1 x (c2 y z) = c2 (a1 x y) (a1 x z);
!!x y z. a2 x (c1 y z) = c1 (a2 x y) (a2 x z);
!!x1 x2 y1 y2. c2 (c1 x1 y1) (c1 x2 y2) = c1 (c2 x1 x2) (c2 y1 y2) |]
==> ALL hs1 hs2.
regSkelOuter2 t = Some (hs1, hs2) -->
tFold a2 c2 (tMap (tFold a1 c1) (tTranspose t)) =
tFold a1 c1 (tMap (tFold a2 c2) t)
theorem tTranspose_tFold2:
[| assoc c1; assoc c2; !!x y z. a1 x (a2 y z) = a2 y (a1 x z);
!!x y z. a1 x (c2 y z) = c2 (a1 x y) (a1 x z);
!!x y z. a2 x (c1 y z) = c1 (a2 x y) (a2 x z);
!!x1 x2 y1 y2. c2 (c1 x1 y1) (c1 x2 y2) = c1 (c2 x1 x2) (c2 y1 y2);
regSkelOuter2 t = Some (hs1, hs2) |]
==> tFold a2 c2 (tMap (tFold a1 c1) (tTranspose t)) =
tFold a1 c1 (tMap (tFold a2 c2) t)
lemma tFold_tFold_vConc_gen_0:
[| assoc c1; assoc c2; assoc c3; !!x y z. a3 x (c2 y z) = c1 (a1 x y) (a1 x z);
!!x1 x2 y1 y2. c3 (c1 x1 y1) (c1 x2 y2) = c1 (c1 x1 x2) (c1 y1 y2) |]
==> ALL t2 hs1a hs2a hs1b hs2b.
regSkelOuter2 t1 = Some (hs1a, hs2a) -->
regSkelOuter2 t2 = Some (hs1b, hs2b) -->
hs1a = hs1b -->
tFold a3 c3 (tMap (tFold a2 c2) (vConc t1 t2)) =
c1 (tFold a1 c1 (tMap (tFold a2 c2) t1))
(tFold a1 c1 (tMap (tFold a2 c2) t2))
lemma tFold_tFold_vConc_gen:
[| assoc c1; assoc c2; assoc c3; !!x y z. a3 x (c2 y z) = c1 (a1 x y) (a1 x z);
!!x1 x2 y1 y2. c3 (c1 x1 y1) (c1 x2 y2) = c1 (c1 x1 x2) (c1 y1 y2);
regSkelOuter2 t1 = Some (hs1a, hs2a); regSkelOuter2 t2 = Some (hs1b, hs2b);
hs1a = hs1b |]
==> tFold a3 c3 (tMap (tFold a2 c2) (vConc t1 t2)) =
c1 (tFold a1 c1 (tMap (tFold a2 c2) t1))
(tFold a1 c1 (tMap (tFold a2 c2) t2))
lemma tFold_tFold_vConc_wrapped_0:
[| assoc c1; assoc c2; assoc c3;
!!h x y. w1 (a3 h (c2 x y)) = w2 (c1 (a1 h x) (a1 h y));
!!x y. w1 (c3 x y) = c4 (w1 x) (w1 y);
!!x1 x2 y1 y2.
c4 (w2 (c1 x1 x2)) (w2 (c1 y1 y2)) = w2 (c1 (c1 x1 y1) (c1 x2 y2)) |]
==> ALL t2 hs1a hs2a hs1b hs2b.
regSkelOuter2 t1 = Some (hs1a, hs2a) -->
regSkelOuter2 t2 = Some (hs1b, hs2b) -->
hs1a = hs1b -->
w1 (tFold a3 c3 (tMap (tFold a2 c2) (vConc t1 t2))) =
w2 (c1 (tFold a1 c1 (tMap (tFold a2 c2) t1))
(tFold a1 c1 (tMap (tFold a2 c2) t2)))
lemma tFold_tFold_vConc_wrapped:
[| assoc c1; assoc c2; assoc c3;
!!h x y. w1 (a3 h (c2 x y)) = w2 (c1 (a1 h x) (a1 h y));
!!x y. w1 (c3 x y) = c4 (w1 x) (w1 y);
!!x1 x2 y1 y2.
c4 (w2 (c1 x1 x2)) (w2 (c1 y1 y2)) = w2 (c1 (c1 x1 y1) (c1 x2 y2));
regSkelOuter2 t1 = Some (hs1, hs2a); regSkelOuter2 t2 = Some (hs1, hs2b) |]
==> w1 (tFold a3 c3 (tMap (tFold a2 c2) (vConc t1 t2))) =
w2 (c1 (tFold a1 c1 (tMap (tFold a2 c2) t1))
(tFold a1 c1 (tMap (tFold a2 c2) t2)))
lemma tTranspose_tFold2_gen_0:
[| assoc c1; assoc c2; assoc c3; assoc c4; assoc c5;
!!x y z. w1 (a1 x (a2 y z)) = w2 (a3 y (a4 x z));
!!x y. w1 (c1 x y) = c5 (w1 x) (w1 y); !!x y. w2 (c3 x y) = c5 (w2 x) (w2 y);
!!x y z. w1 (a1 x (c2 y z)) = c5 (w1 (a1 x y)) (w1 (a1 x z));
!!h x y. w2 (a3 h (c4 x y)) = c5 (w2 (a3 h x)) (w2 (a3 h y));
!!x1 x2 y1 y2. c5 (c5 x1 x2) (c5 y1 y2) = c5 (c5 x1 y1) (c5 x2 y2) |]
==> ALL hs1 hs2.
regSkelOuter2 t = Some (hs1, hs2) -->
w2 (tFold a3 c3 (tMap (tFold a4 c4) (tTranspose t))) =
w1 (tFold a1 c1 (tMap (tFold a2 c2) t))
lemma tTranspose_tFold2_gen:
[| assoc c1; assoc c2; assoc c3; assoc c4; assoc c5;
!!x y z. w1 (a1 x (a2 y z)) = w2 (a3 y (a4 x z));
!!x y. w1 (c1 x y) = c5 (w1 x) (w1 y); !!x y. w2 (c3 x y) = c5 (w2 x) (w2 y);
!!x y z. w1 (a1 x (c2 y z)) = c5 (w1 (a1 x y)) (w1 (a1 x z));
!!h x y. w2 (a3 h (c4 x y)) = c5 (w2 (a3 h x)) (w2 (a3 h y));
!!x1 x2 y1 y2. c5 (c5 x1 x2) (c5 y1 y2) = c5 (c5 x1 y1) (c5 x2 y2);
regSkelOuter2 t = Some (hs1, hs2) |]
==> w2 (tFold a3 c3 (tMap (tFold a4 c4) (tTranspose t))) =
w1 (tFold a1 c1 (tMap (tFold a2 c2) t))