(** redecorationTYPES.thy Version 1.0 December 2007 *)

(** This is companion material to the article "Verification of the Redecoration 
    Algorithm for Triangular Matrices" by Ralph Matthes and Martin Strecker in 
    the post-proceedings of TYPES 2007. *) 

(* runs with Isabelle 2007 of November 2007 but also under Isabelle 2005 
   of October 2005 *)

(** Copyright 2007 by Ralph Matthes and Martin Strecker, IRIT Toulouse *)


theory redec imports Main

begin

(* nested datatypes are not implemented in Isabelle:

datatype ('a, 'e) tri 
  = sg 'a
  | constr 'a "('e * 'a, 'e) tri"

The 'e * decoration of the first argument to tri is the problem.
*)

(* We follow an axiomatic approach. *)


(* the triangles *)
typedecl ('a, 'e) tri

(* the trapeziums *)
types ('a, 'e) trap = "('e * 'a, 'e) tri"


(* tri becomes a nested datatype - a heterogeneous family of datatypes *)
consts
  sg :: "'a \<Rightarrow> ('a,'e) tri"
  constr :: "'a \<Rightarrow> ('a, 'e) trap \<Rightarrow> ('a, 'e) tri"

(* without the abbreviation trap:
  constr :: "['a, ('e * 'a, 'e) tri] \<Rightarrow> ('a, 'e) tri"
*)

(* display the type *)
term constr


(* the generic pattern for the induction principle for triangles *)

consts 
  P :: "('a, 'e) tri \<Rightarrow> bool"

axioms Tri_ind: "(\<forall> a. P (sg a)) \<longrightarrow> (\<forall> a r. P r \<longrightarrow> P (constr a r))
\<longrightarrow> (\<forall> t. P t)"

(* we could have written lemma \<dots> and sorry as a proof *)


(* Fake primitive recursion: only axiomatic approach *)
consts
  top :: "('a, 'e) tri \<Rightarrow> 'a"

axioms top_sg [simp]:
  "top (sg a) = a"
  top_constr [simp]:
  "top (constr a r) = a"

(* cutting off the top row of a triangle *)
consts
  cut :: "('a, 'e) trap \<Rightarrow> ('a, 'e) tri"

axioms cut_sg [simp]:
  "cut (sg (e,a)) = sg a"
  cut_constr [simp]: 
  "cut (constr (e,a) r) = constr a (cut r)"

constdefs
  "lift \<equiv> \<lambda> f t. (fst (top t), f(cut t))"


consts
  redec :: "(('a, 'e)tri \<Rightarrow> 'b) \<Rightarrow> ('a, 'e) tri  \<Rightarrow> ('b, 'e) tri"

axioms redec_sg [simp]:
  "redec f (sg a) = sg (f(sg a))"
 redec_constr [simp]:
  "redec f (constr a r) = constr (f(constr a r)) (redec (lift f) r)"



(* some testing *)
consts sum' :: "('a \<Rightarrow> nat) \<Rightarrow> ('a, nat) tri \<Rightarrow> nat"

axioms sum'_sg [simp]:
  "sum' f (sg a) = f a"
 sum'_constr [simp]:
  "sum' f (constr a r) = f a + sum' (\<lambda> p . fst p + f(snd p)) r"


constdefs
  "sum \<equiv> \<lambda>r. sum' (\<lambda> x .x) r"

constdefs
  t0 :: "(nat, nat) tri"
  "t0 \<equiv> sg 0"

  t1 :: "(nat, nat) tri"
  "t1 \<equiv> constr 0 (sg (1,2))"

  t2 :: "(nat, nat) tri"
  "t2 \<equiv> constr 0 (constr (1,2) (sg (3,(4,5))))"

  t3r :: "(nat * nat, nat) tri"
  "t3r \<equiv> constr (1,2) (constr (3,(4,5)) (sg (6,(7,(8,9)))))"

  t3 :: "(nat, nat) tri"
  "t3 \<equiv> constr 0 t3r"

  "t01 \<equiv> redec sum t0"

  "t11 \<equiv> redec sum t1"

  "t21 \<equiv> redec sum t2"

  "t31 \<equiv> redec sum t3"

lemma t21_calc: "t21 = x"
apply (simp add: t21_def sum_def t2_def lift_def)
oops

lemma t21_ok: "t21 = 
constr 15 (constr (1, 11) (sg (3, (4, 5))))"
by (simp add: t21_def sum_def t2_def lift_def)

lemma cut_t3r: "cut t3r = constr 2 (constr (4, 5) (sg (7, (8, 9))))"
by (simp add: t3r_def)


(* the list-based model *)

(* the respective overapproximations by lists *)
types ('a, 'e) tril = "('e list * 'a) list"



constdefs
  shiftToE :: "'e list \<times> 'e \<times> 'a \<Rightarrow> 'e list \<times> 'a"
  "shiftToE \<equiv> \<lambda>(es,(e,a)). (es@[e],a)"

  shiftToEs :: "('e * 'a, 'e) tril \<Rightarrow> ('a, 'e) tril"
  "shiftToEs \<equiv> map shiftToE"


(* list representation of triangles *)
consts 
  toListRep :: "('a, 'e) tri \<Rightarrow> ('a, 'e) tril"

axioms toListRep_sg [simp]: 
  "toListRep (sg a) = [([], a)]"
  toListRep_constr [simp]: 
  "toListRep (constr a r) = ([], a) # map shiftToE (toListRep r)"


(* a little test *)
lemma t3_ok: "toListRep t3 = ([], 0)
       # (1 # [], 2)
          # (3 # 4 # [], 5) # (6 # 7 # 8 # [], 9) # []"
by (simp add: t3_def t3r_def shiftToE_def)


constdefs
  "removeTopE \<equiv> \<lambda>(es, a). (tl es, a)"

(* output just the top E if it exists *)
consts singletonTopE::"'e list * 'a \<Rightarrow> 'e list"
recdef singletonTopE "{}"
  "singletonTopE ([],a) = []"
  "singletonTopE (e#es,a) = [e]"

(* the means to append Es to a column *)
constdefs 
  "appendEs \<equiv> \<lambda> es (es',a). (es@es',a)"

lemma appendEsLemma:
   "appendEs(singletonTopE p)(removeTopE p)=p"
apply (case_tac p)
apply (case_tac a)
 apply simp
 apply (clarsimp simp add: appendEs_def singletonTopE_def removeTopE_def)
 apply simp
 apply (clarsimp simp add: appendEs_def singletonTopE_def removeTopE_def)
done

consts zipWith::"'a list * 'b list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'c list"
recdef zipWith "measure (\<lambda> (l1, l2). length l1)"
  "zipWith (a # l1, b # l2) =  (\<lambda> f. ((f a b) # (zipWith (l1, l2) f)))"
  "zipWith ([], l2) =  (\<lambda> f. [])"
  "zipWith (l1, []) =  (\<lambda> f. [])"
thm zipWith.induct

constdefs removeTopEs::"('e, 'a) tril \<Rightarrow> ('e, 'a) tril"
  "removeTopEs \<equiv> map removeTopE"
  singletonTopEs::"('a, 'e) tril \<Rightarrow> 'e list list"
  "singletonTopEs \<equiv> map singletonTopE"
  "zipAppendEs \<equiv> \<lambda> l1 l2. zipWith (l1, l2) appendEs"


consts redecL::"('a, 'e) tril \<Rightarrow> (('a, 'e) tril \<Rightarrow> 'b)  \<Rightarrow> ('b, 'e) tril"
recdef redecL "measure length"
  "redecL [] = (\<lambda> f. [])"
  "redecL ((es,a)#rest) = (\<lambda> f. 
        ((es,f((es,a)#rest))#zipAppendEs (singletonTopEs rest) (redecL (removeTopEs rest) f)))"
(hints recdef_simp: removeTopEs_def)


(* Verification *)

types ('a, 'e) trapl = "('e * 'a, 'e) tril"

constdefs
  "remsh \<equiv> removeTopE \<circ> shiftToE"


(* the equivalent to cut on the list level *)
constdefs
  cutL :: "('a, 'e) trapl \<Rightarrow> ('a, 'e) tril"
  "cutL \<equiv> map remsh"


(* preparations for lemma cutL_ok *)

lemma remshEsComm: "remsh (e # es, p) = shiftToE(removeTopE(e # es,p))"
by (case_tac p, simp add: remsh_def removeTopE_def shiftToE_def)


lemma shiftToEremshComm: "shiftToE (remsh r) = remsh (shiftToE r)" 
apply (simp add: remsh_def removeTopE_def shiftToE_def split_beta)
apply (case_tac r)
apply (rename_tac es p)
apply (case_tac es)
 apply simp+
done

lemma cutLShiftToEsComm: 
  "shiftToEs (cutL t) = cutL (shiftToEs t)"
by (simp add: shiftToEs_def cutL_def map_compose [THEN sym] shiftToEremshComm)

(* a variant we feel to need *)
lemma cutLShiftToEsComm_altern: 
  "map shiftToE (cutL t) = cutL (map shiftToE t)"
by (simp add: cutL_def map_compose [THEN sym] shiftToEremshComm)

(* now a specific instance of induction on triangles *)
constdefs 
  P_cutL_ok :: "('a, 'e) trap \<Rightarrow> bool"
  "P_cutL_ok \<equiv> \<lambda>t. toListRep (cut t) = cutL (toListRep t)"

axioms Trap_ind_cutL_ok: 
  "(\<forall> a. P_cutL_ok (sg a)) \<longrightarrow> 
  (\<forall> a r. P_cutL_ok r \<longrightarrow> P_cutL_ok (constr a r))
\<longrightarrow> (\<forall> t. P_cutL_ok t)"
(* remark: it is not visible from the formulation that it is now trap induction *)

(* here, we have to unfold the target *)
lemma Trap_ind_cutL_ok_appl [rule_format]:
  "(\<forall> a. P_cutL_ok (sg a)) \<longrightarrow> 
  (\<forall> a r. P_cutL_ok r \<longrightarrow> P_cutL_ok (constr a r))
\<longrightarrow> (\<forall> t. toListRep (cut t) = cutL (toListRep t))"
apply (insert Trap_ind_cutL_ok)
apply (unfold P_cutL_ok_def)
apply fast
done

(* some help for the simplifier *)
lemma cutL_cons [simp]: "cutL (x # xs) = (remsh x) # cutL xs"
by (simp add: cutL_def)
lemma shiftToE_empty [simp]:  "shiftToE ([], e, a) = ([e],a)"
by (simp add: shiftToE_def)

(** The following is Lemma 1 in the paper. *)
(* Updated with Stefan Berghofer's advice *)
lemma cutL_ok: "toListRep (cut t) = cutL (toListRep t)"
apply (rule Trap_ind_cutL_ok_appl 
  [where ?'a='a and ?'b='b and ?'c='c and ?'d='d])
 apply (clarsimp 
   simp add: P_cutL_ok_def cutL_def remsh_def removeTopE_def shiftToE_def)
apply (clarsimp simp add: P_cutL_ok_def remsh_def
  removeTopE_def cutLShiftToEsComm_altern)
done



consts liftL::"'e \<Rightarrow> (('a, 'e) tril \<Rightarrow> 'b) \<Rightarrow> ('a, 'e) trapl \<Rightarrow> 'e * 'b"
primrec "liftL e0 f [] = (arbitrary, f(cutL []))"
        "liftL e0 f (x#l) = (fst(snd x),f(cutL (x#l)))"

(* For Lemma 2 of the paper, we need more preparations: some inversion *)

(* now another specific instance of induction on triangles *)
constdefs 
  P1 :: "('a, 'e) tri \<Rightarrow> bool"
  "P1 \<equiv> \<lambda>t. (\<forall> a list. toListRep t = a # list \<longrightarrow>  top t = snd a)"

axioms Tri_ind_P1: 
  "(\<forall> a. P1 (sg a)) \<longrightarrow> (\<forall> a r. P1 r \<longrightarrow> P1 (constr a r)) \<longrightarrow> (\<forall> t. P1 t)"

(* here, we have to unfold the target *)
lemma Tri_ind_P1_appl [rule_format]:
  "(\<forall> a. P1 (sg a)) \<longrightarrow> 
  (\<forall> a r. P1 r \<longrightarrow> P1 (constr a r))
\<longrightarrow> (\<forall> t. toListRep t = a # list \<longrightarrow>  top t = snd a)"
apply (insert Tri_ind_P1)
apply (unfold P1_def)
apply fast
done

lemma toListRep_cons_inv: "toListRep t = a # list \<Longrightarrow> top t = snd a"
apply (rule Tri_ind_P1_appl)
 apply (simp add: P1_def)+
done


(* another specific instance of induction on triangles *)
constdefs 
  P2 :: "('a, 'e) tri \<Rightarrow> bool"
  "P2 \<equiv> \<lambda> t. \<not> (toListRep t = [])"

axioms Tri_ind_P2: 
  "(\<forall> a. P2 (sg a)) \<longrightarrow> 
  (\<forall> a r. P2 r \<longrightarrow> P2 (constr a r))
\<longrightarrow> (\<forall> t. P2 t)"

(* here, we have to unfold the target *)
lemma Tri_ind_P2_appl [rule_format]:
  "(\<forall> a. P2 (sg a)) \<longrightarrow> 
  (\<forall> a r. P2 r \<longrightarrow> P2 (constr a r))
\<longrightarrow> (\<forall> t. \<not> (toListRep t = []))"
apply (insert Tri_ind_P2)
apply (unfold P2_def)
apply fast
done

lemma toListRep_sg_inv: "\<not> (toListRep t = [])"
apply (rule Tri_ind_P2_appl)
 apply (simp add: P2_def)+
done

(* The following corresponds to Lemma 2 in the paper. *)
lemma liftL_ok: "lift (f \<circ> toListRep) r = liftL e0 f (toListRep r)"
apply (case_tac "toListRep r")
 apply (simp add: toListRep_sg_inv)
apply (simp add: lift_def cutL_ok)
apply (rule arg_cong [where f="fst"])
apply (simp add: toListRep_cons_inv)
done

(* a variant of the lemma *)
lemma liftL_ok_altern: "lift (\<lambda> x. f(toListRep x)) t = liftL e0 f (toListRep t)"
apply (rule trans)
 defer
 apply (rule liftL_ok)
apply (simp add: comp_def)
done


(* now several preparatory lemmas for the proof of the Main Lemma *)

lemma shiftToEappendEsComp: "shiftToE (appendEs a b) = appendEs a (shiftToE b)"
apply (case_tac b)
apply (case_tac ba)
apply (simp add: shiftToE_def appendEs_def)
done


lemma zipAppendEsShiftToEsComm:
  "shiftToEs (zipAppendEs l1 l2) = zipAppendEs l1 (shiftToEs l2)"
apply (simp add: zipAppendEs_def shiftToEs_def)
apply (induct_tac l1 l2 rule: zipWith.induct)
 apply (simp add:shiftToEappendEsComp)
 apply simp+
done


(* instead, we will need the following variant in redecLMainLemma *) 
lemma zipAppendEsShiftToEsComm_altern:
  "map shiftToE (zipAppendEs l1 l2) = zipAppendEs l1 (map shiftToE l2)"
apply (simp add: zipAppendEs_def)
apply (induct_tac l1 l2 rule: zipWith.induct)
 apply (simp add:shiftToEappendEsComp)
 apply simp+
done

(* a little preparation for the next lemma below *)
lemma appendEsComp: "appendEs es1 (appendEs es2 p) = appendEs (es1@es2) p"
by (case_tac p, simp add: appendEs_def)

lemma zipAppendEsComp: "\<forall> u. zipAppendEs (map f t) (zipAppendEs (map g t) u) = 
      zipAppendEs (map (\<lambda> l. f l @ g l) t) u"
apply (induct_tac t)
 apply (simp add: zipAppendEs_def)
apply clarsimp
apply (simp add: zipAppendEs_def)
apply (case_tac u)
 apply simp
apply (simp add: appendEsComp)
done

(* another simple observation *) 
lemma singletonTopELemma:
(* (l::'e list * 'e * 'a) *)
  "singletonTopE l @ singletonTopE (shiftToE (removeTopE l)) = 
        singletonTopE (shiftToE l) @ singletonTopE (removeTopE (shiftToE l))"
apply (case_tac l)
apply (case_tac b)
apply (case_tac a)
 apply (simp add: removeTopE_def shiftToE_def)+
done


lemma redecLMainLemma:
"shiftToEs (redecL r (liftL e0 f)) =
            zipAppendEs (singletonTopEs (shiftToEs r))
                       (redecL (removeTopEs (shiftToEs r)) f)"
apply (induct_tac r rule: redecL.induct)
 apply (simp add: zipAppendEs_def singletonTopEs_def shiftToEs_def)
apply clarsimp
apply (subgoal_tac "
zipAppendEs (singletonTopEs (shiftToEs ((es, a, b) # rest)))
        (redecL (removeTopEs (shiftToEs ((es, a, b) # rest))) f) =
(es @ [a],
  f (remsh (es, (a, b)) # removeTopEs (shiftToEs rest)))
  # zipAppendEs (singletonTopEs (shiftToEs rest))
     (zipAppendEs
        (singletonTopEs (removeTopEs (shiftToEs rest)))
        (redecL (removeTopEs (removeTopEs (shiftToEs rest)))f))")
 defer
 apply (case_tac es)
  apply (simp add: shiftToEs_def removeTopEs_def zipAppendEs_def singletonTopEs_def  removeTopE_def remsh_def appendEs_def)
 apply (simp add: shiftToEs_def shiftToE_def removeTopEs_def singletonTopEs_def  removeTopE_def zipAppendEs_def appendEs_def remsh_def)
apply (simp add: shiftToEs_def)
apply (rule conjI)
 apply (simp add: shiftToE_def cutL_def remsh_def removeTopEs_def map_compose)
(* w.r.t. the last "back" remark in the respective Coq proof, we see the unfolded
   version of shiftToEs and removeTopEs (map shiftToE rest) instead of cutL rest *)
apply (simp add:zipAppendEsShiftToEsComm_altern)
(* this also applied the IH that is one of the premises *)
apply (simp add: singletonTopEs_def removeTopEs_def map_compose [THEN sym] zipAppendEsComp)
apply (subgoal_tac "map (removeTopE \<circ> (shiftToE \<circ> removeTopE)) rest =
                    map (removeTopE \<circ> (removeTopE \<circ> shiftToE)) rest")
 defer
 apply (induct_tac rest)
  apply simp
  apply (clarsimp simp add: removeTopE_def shiftToE_def)
  apply (case_tac aa, simp)
 apply simp
apply (simp (no_asm_simp))
apply (subgoal_tac "map (\<lambda>l. singletonTopE l @ singletonTopE (shiftToE (removeTopE l))) rest
    = map (\<lambda>l. singletonTopE (shiftToE l) @ singletonTopE (removeTopE (shiftToE l))) rest")
 apply (simp (no_asm_simp))
apply (induct_tac rest)
 apply simp
 apply simp
 apply (rule singletonTopELemma)
done

(* just a simple reformulation *)
lemma redecLMainLemmaCorr:
"map shiftToE (redecL r (liftL e0 f)) =
            zipAppendEs (singletonTopEs (map shiftToE r))
                       (redecL (removeTopEs (map shiftToE r)) f)"
apply (rule trans)
apply (fold shiftToEs_def)
apply (simp add: redecLMainLemma)
apply (rule refl)
done

(* now, we cannot just formulate the instance of the induction axiom by
   using a specific definition of the predicate but have to write this out
   in the whole induction principle *)
axioms Tri_ind_MAIN_appl2:
  "(\<forall> a.\<forall> f . toListRep (redec (\<lambda> x. f (toListRep x)) (sg a)) = redecL (toListRep (sg a)) f) 
\<longrightarrow> 
  (\<forall> a r. (\<forall> f' . toListRep (redec (\<lambda> x. f' (toListRep x)) r) = redecL (toListRep r) f') \<longrightarrow> 
          (\<forall> f' . toListRep (redec (\<lambda> x. f' (toListRep x)) (constr a r)) = redecL (toListRep (constr a r)) f'))
\<longrightarrow> (\<forall> t. \<forall> f . toListRep (redec (\<lambda> x. f (toListRep x)) t) = redecL (toListRep t) f)"


(* now a formulation that better suits the needs *)
lemma Tri_ind_MAIN_appl:
"\<lbrakk>\<And>a f.  (toListRep (redec (\<lambda>x. f (toListRep x)) (sg a)) = redecL (toListRep (sg a)) f);
 \<And>a r f'.
    (\<forall> f'. toListRep (redec (\<lambda>x. f' (toListRep x)) r) = redecL (toListRep r) f') \<Longrightarrow>
    toListRep (redec (\<lambda>x. f' (toListRep x)) (constr a r)) = redecL (toListRep (constr a r)) f'\<rbrakk>
\<Longrightarrow> toListRep (redec (\<lambda>x. f (toListRep x)) t) = redecL (toListRep t) f"
by (rule Tri_ind_MAIN_appl2 [rule_format]) fast+

lemma redec_ext: "(\<forall> t. f t = f' t) \<longrightarrow> redec f t' = redec f' t'" 
apply clarsimp
apply (subgoal_tac "f = f'")
 apply simp
apply (simp add: expand_fun_eq)
done


(* Simulation *)

typedecl E

consts e0::E

lemma redecL_ok:
    "toListRep (redec (\<lambda> x. f (toListRep x)) t::('a,E) tri) = redecL (toListRep t) f"
apply (rule Tri_ind_MAIN_appl [where ?'a='a and ?'b='b and ?'c='c and ?'d='d and ?'e=E])
 apply (simp add: removeTopEs_def singletonTopEs_def zipAppendEs_def)
apply clarsimp
apply (rule trans)
 defer
 apply (rule redecLMainLemmaCorr [where ?e0.0="e0"])
apply (rule arg_cong [where f="map shiftToE"])
apply (rule trans)
 defer
 apply (drule spec)
 apply assumption
apply (rule arg_cong [where f="toListRep"])
apply (rule redec_ext [rule_format])
apply (fastsimp simp add: liftL_ok_altern)
done

(* This result is not yet in the form that allows to calculate redec through redecL. *)

(* Towards a left inverse of toListRep *)


constdefs
  shiftFromE :: "[E list * 'a] \<Rightarrow> E list * (E * 'a)"
  "shiftFromE == \<lambda> (es, a). (butlast es, (last es, a))"

lemma shiftToFromEInv: "shiftFromE (shiftToE p) = p"
by (clarsimp simp add: shiftFromE_def shiftToE_def split_beta)

constdefs
  shiftFromEs :: "('a, E) tril \<Rightarrow> (E \<times> 'a, E) tril"
 "shiftFromEs == map shiftFromE"

lemma shiftToFromEsInv :
  "shiftFromEs (shiftToEs r) = r"
apply (simp add: shiftFromEs_def
  shiftToEs_def map_compose [THEN sym] del: map_compose)
apply (simp add: comp_def shiftToFromEInv)
done

consts fromListRep :: "('a, E) tril \<Rightarrow> ('a, E) tri"

axioms
  fromListRep_single [simp]: 
  "fromListRep [(es,a)] = sg a"
  fromListRep_cons [simp]: 
  "fromListRep ((es,a)#p#rest) = constr a (fromListRep (shiftFromEs (p#rest)))"


constdefs 
  tLRp :: "('a, E) tri \<Rightarrow> bool"
  "tLRp \<equiv> (\<lambda>t. \<exists> p rest. toListRep t = p # rest)"

axioms Tri_ind_tLRp: 
  "(\<forall> a. tLRp (sg a)) \<longrightarrow> (\<forall> a r. tLRp r \<longrightarrow> tLRp (constr a r)) \<longrightarrow> (\<forall> t. tLRp t)"

lemma Tri_ind_tLRp_appl [rule_format]:
  "(\<forall> (a:: 'a). tLRp (sg a)) \<longrightarrow> 
  (\<forall> a r. tLRp r \<longrightarrow> tLRp (constr a r))
\<longrightarrow> (\<forall> t. \<exists> (p::((E list) * 'a)) rest. toListRep t = p # rest)"
apply (insert Tri_ind_tLRp)
apply (simp add: tLRp_def)
done

lemma toListRepPair: "\<exists> (p::((E list) * 'a)) rest. toListRep t = p # rest"
apply (rule Tri_ind_tLRp_appl)
apply (simp add: tLRp_def)+
done

constdefs 
  ftLR :: "('a, E) tri \<Rightarrow> bool"
  "ftLR \<equiv> (\<lambda>t. fromListRep (toListRep t) = t)"

axioms Tri_ind_ftLR: 
  "(\<forall> a. ftLR (sg a)) \<longrightarrow> (\<forall> a r. ftLR r \<longrightarrow> ftLR (constr a r)) \<longrightarrow> (\<forall> t. ftLR t)"

lemma Tri_ind_ftLR_appl [rule_format]:
  "(\<forall> a. ftLR (sg a)) \<longrightarrow> 
  (\<forall> a r. ftLR r \<longrightarrow> ftLR (constr a r))
\<longrightarrow> (\<forall> t. fromListRep (toListRep t) = t)"
apply (insert Tri_ind_ftLR)
apply (unfold ftLR_def)
apply fast
done

lemma toFromListRepInv_aux: "fromListRep (toListRep r) = r \<Longrightarrow>
          fromListRep (([], a) # map shiftToE (toListRep r)) = constr a r"
apply (insert toListRepPair [where ?t=r])
apply (clarsimp)
apply (simp add: shiftFromEs_def shiftToFromEInv)
apply (simp add: map_compose [THEN sym] comp_def shiftToFromEInv del: map_compose)
done

lemma toFromListRepInv: "fromListRep (toListRep t) = t"
apply (rule Tri_ind_ftLR_appl)
apply (simp add: ftLR_def shiftFromEs_def)
apply (simp add: ftLR_def shiftFromEs_def)
apply (erule toFromListRepInv_aux)
done

lemma MainTheorem: "redec f t = fromListRep (redecL (toListRep t) (f \<circ> fromListRep))"
apply (simp add: redecL_ok [THEN sym])
apply (simp add: toFromListRepInv)
done


(* the comonad laws *)

(* another specific instance of induction on triangles *)
constdefs 
  P3 :: "('a, 'e) tri \<Rightarrow> bool"
  "P3 \<equiv> \<lambda> t. (\<exists> a r. t = constr a r) \<or> (\<exists> a. t = sg a)"

axioms Tri_ind_P3: 
  "(\<forall> a. P3 (sg a)) \<longrightarrow> 
  (\<forall> a r. P3 r \<longrightarrow> P3 (constr a r))
\<longrightarrow> (\<forall> t. P3 t)"

(* here, we have to unfold the target *)
lemma Tri_ind_P3_appl [rule_format]:
  "(\<forall> a. P3 (sg a)) \<longrightarrow> 
  (\<forall> a r. P3 r \<longrightarrow> P3 (constr a r))
\<longrightarrow> (\<forall> t. (\<exists> a r. t = constr a r) \<or> (\<exists> a. t = sg a))"
apply (insert Tri_ind_P3)
apply (unfold P3_def)
apply fast
done


lemma tridiscr: "(\<exists> a r. t = constr a r) \<or> (\<exists> a. t = sg a)"
apply (rule Tri_ind_P3_appl)
 apply (simp add: P3_def)+
  apply fastsimp
 apply (simp add: P3_def)+
 apply fastsimp
done


lemma comonad1: "top (redec f t) = f t" 
apply (insert tridiscr [where ?t="t"])
apply (erule disjE)
 apply (erule exE)+
 apply simp
apply (erule exE)
apply simp
done

lemma auxcomonad2: "lift top r = top r"
apply (insert tridiscr [where ?t="r"])
apply (erule disjE)
 apply (erule exE)+
 apply (case_tac a)
 apply (simp add: lift_def)
apply (erule exE)
apply (case_tac a)
apply (simp add: lift_def)
done

lemma auxcomonad2_altern: "lift top = top"
apply (simp add: expand_fun_eq auxcomonad2)
done

(* another specific instance of induction on triangles *)
constdefs 
  P4 :: "('a, 'e) tri \<Rightarrow> bool"
  "P4 \<equiv> \<lambda> t. redec top t = t"

axioms Tri_ind_P4: 
  "(\<forall> a. P4 (sg a)) \<longrightarrow> 
  (\<forall> a r. P4 r \<longrightarrow> P4 (constr a r))
\<longrightarrow> (\<forall> t. P4 t)"

(* here, we have to unfold the target *)
lemma Tri_ind_P4_appl [rule_format]:
  "(\<forall> a. P4 (sg a)) \<longrightarrow> 
  (\<forall> a r. P4 r \<longrightarrow> P4 (constr a r))
\<longrightarrow> (\<forall> t. redec top t = t)"
apply (insert Tri_ind_P4)
apply (unfold P4_def)
apply fast
done

lemma constrcong: "r = r' \<Longrightarrow> constr a r = constr a r'"
by simp

lemma comonad2: "redec top t = t"
apply (rule Tri_ind_P4_appl)
 apply (simp add: P4_def)+
apply (simp add: auxcomonad2_altern)
apply (rule constrcong)
apply assumption
done


(* another specific instance of induction on trapeziums *)
axioms Trap_ind_A1C3_appl2:
  "(\<forall> a. \<forall> f. redec f (cut (sg a)) = cut (redec (lift f) (sg a))) \<longrightarrow> 
  (\<forall> a r. (\<forall> f. redec f (cut r) = cut (redec (lift f) r)) \<longrightarrow> 
  (\<forall> f. redec f (cut (constr a r)) = cut (redec (lift f) (constr a r))))
\<longrightarrow> (\<forall> r. \<forall> f. redec f (cut r) = cut (redec (lift f) r))"

lemma Trap_ind_A1C3_appl:
"\<lbrakk>\<And>a f. redec f (redec.cut (sg a)) = redec.cut (redec (lift f) (sg a));
 \<And>a r f.
    (\<forall> f. redec f (redec.cut r) = redec.cut (redec (lift f) r)) \<Longrightarrow>
    redec f (redec.cut (constr a r)) =
    redec.cut (redec (lift f) (constr a r))\<rbrakk>
\<Longrightarrow> redec f (redec.cut r) = redec.cut (redec (lift f) r)"
by (rule  Trap_ind_A1C3_appl2 [rule_format]) fast+


lemma aux1comonad3: "redec f (cut r) = cut (redec (lift f) r)"
apply (rule Trap_ind_A1C3_appl)
 apply clarsimp
 apply (simp add: lift_def)
apply clarsimp
apply (simp add: lift_def)
apply (rule constrcong)
apply fastsimp
done


lemma aux2comonad3:
  "lift (g \<circ> redec f) r = (lift g \<circ> redec (lift f)) r"
apply (insert tridiscr [where ?t="r"])
apply (erule disjE)
 apply (erule exE)+
 apply clarsimp
 apply (simp add: comp_def lift_def aux1comonad3)
apply (erule exE)
apply clarsimp
apply (simp add: comp_def lift_def)
done

lemma aux2comonad3_altern:
  "lift (g \<circ> redec f) = (lift g \<circ> redec (lift f))"
by (simp add: expand_fun_eq aux2comonad3)

(* another specific instance of induction on triangles *)
axioms Tri_ind_C3_appl2:
  "(\<forall> a. \<forall> f g.  redec g (redec f (sg a)) = redec (g \<circ> redec f) (sg a)) \<longrightarrow> 
  (\<forall> a r. (\<forall> f g. redec g (redec f r) = redec (g \<circ> redec f) r) \<longrightarrow> 
  (\<forall> f g. redec g (redec f (constr a r)) = redec (g \<circ> redec f) (constr a r)))
\<longrightarrow> (\<forall> t. \<forall> f g. redec g (redec f t) = redec (g \<circ> redec f) t)"


lemma Tri_ind_C3_appl:
"\<lbrakk>\<And>a f g. redec g (redec f (sg a)) = redec (g \<circ> redec f) (sg a);
 \<And>a r f g.
    (\<forall> f g. redec g (redec f r) = redec (g \<circ> redec f) r) \<Longrightarrow>
    redec g (redec f (constr a r)) = redec (g \<circ> redec f) (constr a r)\<rbrakk>
\<Longrightarrow> redec g (redec f t) = redec (g \<circ> redec f) t"
by (rule  Tri_ind_C3_appl2 [rule_format]) fast+


lemma comonad3: "redec (g \<circ> redec f) t = redec g (redec f t)"
apply (rule sym)
apply (rule Tri_ind_C3_appl)
 apply clarsimp
apply clarsimp
apply (rule constrcong)
apply (simp add:aux2comonad3_altern)
apply fastsimp
done

end
