(** 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 \ ('a,'e) tri" constr :: "'a \ ('a, 'e) trap \ ('a, 'e) tri" (* without the abbreviation trap: constr :: "['a, ('e * 'a, 'e) tri] \ ('a, 'e) tri" *) (* display the type *) term constr (* the generic pattern for the induction principle for triangles *) consts P :: "('a, 'e) tri \ bool" axioms Tri_ind: "(\ a. P (sg a)) \ (\ a r. P r \ P (constr a r)) \ (\ t. P t)" (* we could have written lemma \ and sorry as a proof *) (* Fake primitive recursion: only axiomatic approach *) consts top :: "('a, 'e) tri \ '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 \ ('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 \ \ f t. (fst (top t), f(cut t))" consts redec :: "(('a, 'e)tri \ 'b) \ ('a, 'e) tri \ ('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 \ nat) \ ('a, nat) tri \ nat" axioms sum'_sg [simp]: "sum' f (sg a) = f a" sum'_constr [simp]: "sum' f (constr a r) = f a + sum' (\ p . fst p + f(snd p)) r" constdefs "sum \ \r. sum' (\ x .x) r" constdefs t0 :: "(nat, nat) tri" "t0 \ sg 0" t1 :: "(nat, nat) tri" "t1 \ constr 0 (sg (1,2))" t2 :: "(nat, nat) tri" "t2 \ constr 0 (constr (1,2) (sg (3,(4,5))))" t3r :: "(nat * nat, nat) tri" "t3r \ constr (1,2) (constr (3,(4,5)) (sg (6,(7,(8,9)))))" t3 :: "(nat, nat) tri" "t3 \ constr 0 t3r" "t01 \ redec sum t0" "t11 \ redec sum t1" "t21 \ redec sum t2" "t31 \ 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 \ 'e \ 'a \ 'e list \ 'a" "shiftToE \ \(es,(e,a)). (es@[e],a)" shiftToEs :: "('e * 'a, 'e) tril \ ('a, 'e) tril" "shiftToEs \ map shiftToE" (* list representation of triangles *) consts toListRep :: "('a, 'e) tri \ ('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 \ \(es, a). (tl es, a)" (* output just the top E if it exists *) consts singletonTopE::"'e list * 'a \ 'e list" recdef singletonTopE "{}" "singletonTopE ([],a) = []" "singletonTopE (e#es,a) = [e]" (* the means to append Es to a column *) constdefs "appendEs \ \ 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 \ ('a \ 'b \ 'c) \ 'c list" recdef zipWith "measure (\ (l1, l2). length l1)" "zipWith (a # l1, b # l2) = (\ f. ((f a b) # (zipWith (l1, l2) f)))" "zipWith ([], l2) = (\ f. [])" "zipWith (l1, []) = (\ f. [])" thm zipWith.induct constdefs removeTopEs::"('e, 'a) tril \ ('e, 'a) tril" "removeTopEs \ map removeTopE" singletonTopEs::"('a, 'e) tril \ 'e list list" "singletonTopEs \ map singletonTopE" "zipAppendEs \ \ l1 l2. zipWith (l1, l2) appendEs" consts redecL::"('a, 'e) tril \ (('a, 'e) tril \ 'b) \ ('b, 'e) tril" recdef redecL "measure length" "redecL [] = (\ f. [])" "redecL ((es,a)#rest) = (\ 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 \ removeTopE \ shiftToE" (* the equivalent to cut on the list level *) constdefs cutL :: "('a, 'e) trapl \ ('a, 'e) tril" "cutL \ 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 \ bool" "P_cutL_ok \ \t. toListRep (cut t) = cutL (toListRep t)" axioms Trap_ind_cutL_ok: "(\ a. P_cutL_ok (sg a)) \ (\ a r. P_cutL_ok r \ P_cutL_ok (constr a r)) \ (\ 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]: "(\ a. P_cutL_ok (sg a)) \ (\ a r. P_cutL_ok r \ P_cutL_ok (constr a r)) \ (\ 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 \ (('a, 'e) tril \ 'b) \ ('a, 'e) trapl \ '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 \ bool" "P1 \ \t. (\ a list. toListRep t = a # list \ top t = snd a)" axioms Tri_ind_P1: "(\ a. P1 (sg a)) \ (\ a r. P1 r \ P1 (constr a r)) \ (\ t. P1 t)" (* here, we have to unfold the target *) lemma Tri_ind_P1_appl [rule_format]: "(\ a. P1 (sg a)) \ (\ a r. P1 r \ P1 (constr a r)) \ (\ t. toListRep t = a # list \ top t = snd a)" apply (insert Tri_ind_P1) apply (unfold P1_def) apply fast done lemma toListRep_cons_inv: "toListRep t = a # list \ 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 \ bool" "P2 \ \ t. \ (toListRep t = [])" axioms Tri_ind_P2: "(\ a. P2 (sg a)) \ (\ a r. P2 r \ P2 (constr a r)) \ (\ t. P2 t)" (* here, we have to unfold the target *) lemma Tri_ind_P2_appl [rule_format]: "(\ a. P2 (sg a)) \ (\ a r. P2 r \ P2 (constr a r)) \ (\ t. \ (toListRep t = []))" apply (insert Tri_ind_P2) apply (unfold P2_def) apply fast done lemma toListRep_sg_inv: "\ (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 \ 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 (\ 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: "\ u. zipAppendEs (map f t) (zipAppendEs (map g t) u) = zipAppendEs (map (\ 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 \ (shiftToE \ removeTopE)) rest = map (removeTopE \ (removeTopE \ 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 (\l. singletonTopE l @ singletonTopE (shiftToE (removeTopE l))) rest = map (\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: "(\ a.\ f . toListRep (redec (\ x. f (toListRep x)) (sg a)) = redecL (toListRep (sg a)) f) \ (\ a r. (\ f' . toListRep (redec (\ x. f' (toListRep x)) r) = redecL (toListRep r) f') \ (\ f' . toListRep (redec (\ x. f' (toListRep x)) (constr a r)) = redecL (toListRep (constr a r)) f')) \ (\ t. \ f . toListRep (redec (\ x. f (toListRep x)) t) = redecL (toListRep t) f)" (* now a formulation that better suits the needs *) lemma Tri_ind_MAIN_appl: "\\a f. (toListRep (redec (\x. f (toListRep x)) (sg a)) = redecL (toListRep (sg a)) f); \a r f'. (\ f'. toListRep (redec (\x. f' (toListRep x)) r) = redecL (toListRep r) f') \ toListRep (redec (\x. f' (toListRep x)) (constr a r)) = redecL (toListRep (constr a r)) f'\ \ toListRep (redec (\x. f (toListRep x)) t) = redecL (toListRep t) f" by (rule Tri_ind_MAIN_appl2 [rule_format]) fast+ lemma redec_ext: "(\ t. f t = f' t) \ 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 (\ 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] \ E list * (E * 'a)" "shiftFromE == \ (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 \ (E \ '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 \ ('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 \ bool" "tLRp \ (\t. \ p rest. toListRep t = p # rest)" axioms Tri_ind_tLRp: "(\ a. tLRp (sg a)) \ (\ a r. tLRp r \ tLRp (constr a r)) \ (\ t. tLRp t)" lemma Tri_ind_tLRp_appl [rule_format]: "(\ (a:: 'a). tLRp (sg a)) \ (\ a r. tLRp r \ tLRp (constr a r)) \ (\ t. \ (p::((E list) * 'a)) rest. toListRep t = p # rest)" apply (insert Tri_ind_tLRp) apply (simp add: tLRp_def) done lemma toListRepPair: "\ (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 \ bool" "ftLR \ (\t. fromListRep (toListRep t) = t)" axioms Tri_ind_ftLR: "(\ a. ftLR (sg a)) \ (\ a r. ftLR r \ ftLR (constr a r)) \ (\ t. ftLR t)" lemma Tri_ind_ftLR_appl [rule_format]: "(\ a. ftLR (sg a)) \ (\ a r. ftLR r \ ftLR (constr a r)) \ (\ t. fromListRep (toListRep t) = t)" apply (insert Tri_ind_ftLR) apply (unfold ftLR_def) apply fast done lemma toFromListRepInv_aux: "fromListRep (toListRep r) = r \ 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 \ 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 \ bool" "P3 \ \ t. (\ a r. t = constr a r) \ (\ a. t = sg a)" axioms Tri_ind_P3: "(\ a. P3 (sg a)) \ (\ a r. P3 r \ P3 (constr a r)) \ (\ t. P3 t)" (* here, we have to unfold the target *) lemma Tri_ind_P3_appl [rule_format]: "(\ a. P3 (sg a)) \ (\ a r. P3 r \ P3 (constr a r)) \ (\ t. (\ a r. t = constr a r) \ (\ a. t = sg a))" apply (insert Tri_ind_P3) apply (unfold P3_def) apply fast done lemma tridiscr: "(\ a r. t = constr a r) \ (\ 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 \ bool" "P4 \ \ t. redec top t = t" axioms Tri_ind_P4: "(\ a. P4 (sg a)) \ (\ a r. P4 r \ P4 (constr a r)) \ (\ t. P4 t)" (* here, we have to unfold the target *) lemma Tri_ind_P4_appl [rule_format]: "(\ a. P4 (sg a)) \ (\ a r. P4 r \ P4 (constr a r)) \ (\ t. redec top t = t)" apply (insert Tri_ind_P4) apply (unfold P4_def) apply fast done lemma constrcong: "r = r' \ 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: "(\ a. \ f. redec f (cut (sg a)) = cut (redec (lift f) (sg a))) \ (\ a r. (\ f. redec f (cut r) = cut (redec (lift f) r)) \ (\ f. redec f (cut (constr a r)) = cut (redec (lift f) (constr a r)))) \ (\ r. \ f. redec f (cut r) = cut (redec (lift f) r))" lemma Trap_ind_A1C3_appl: "\\a f. redec f (redec.cut (sg a)) = redec.cut (redec (lift f) (sg a)); \a r f. (\ f. redec f (redec.cut r) = redec.cut (redec (lift f) r)) \ redec f (redec.cut (constr a r)) = redec.cut (redec (lift f) (constr a r))\ \ 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 \ redec f) r = (lift g \ 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 \ redec f) = (lift g \ redec (lift f))" by (simp add: expand_fun_eq aux2comonad3) (* another specific instance of induction on triangles *) axioms Tri_ind_C3_appl2: "(\ a. \ f g. redec g (redec f (sg a)) = redec (g \ redec f) (sg a)) \ (\ a r. (\ f g. redec g (redec f r) = redec (g \ redec f) r) \ (\ f g. redec g (redec f (constr a r)) = redec (g \ redec f) (constr a r))) \ (\ t. \ f g. redec g (redec f t) = redec (g \ redec f) t)" lemma Tri_ind_C3_appl: "\\a f g. redec g (redec f (sg a)) = redec (g \ redec f) (sg a); \a r f g. (\ f g. redec g (redec f r) = redec (g \ redec f) r) \ redec g (redec f (constr a r)) = redec (g \ redec f) (constr a r)\ \ redec g (redec f t) = redec (g \ redec f) t" by (rule Tri_ind_C3_appl2 [rule_format]) fast+ lemma comonad3: "redec (g \ 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