equal
deleted
inserted
replaced
130 |
130 |
131 (* TODO: induct_tac doesn't accept 'arbitrary'. |
131 (* TODO: induct_tac doesn't accept 'arbitrary'. |
132 induct doesn't accept 'rule'. |
132 induct doesn't accept 'rule'. |
133 that's why the proof uses manual generalisation and needs assumptions |
133 that's why the proof uses manual generalisation and needs assumptions |
134 both in conclusion for induction and in assumptions. *) |
134 both in conclusion for induction and in assumptions. *) |
135 lemma foldl_rsp[quotient_rsp]: |
135 lemma foldl_rsp: |
136 assumes q1: "Quotient R1 Abs1 Rep1" |
136 assumes q1: "Quotient R1 Abs1 Rep1" |
137 and q2: "Quotient R2 Abs2 Rep2" |
137 and q2: "Quotient R2 Abs2 Rep2" |
138 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" |
138 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" |
139 apply auto |
139 apply auto |
140 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)") |
140 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)") |