equal
deleted
inserted
replaced
1160 prefer 2 |
1160 prefer 2 |
1161 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1161 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1162 apply (rule FUN_QUOTIENT) |
1162 apply (rule FUN_QUOTIENT) |
1163 apply (rule QUOTIENT_fset) |
1163 apply (rule QUOTIENT_fset) |
1164 apply (rule IDENTITY_QUOTIENT) |
1164 apply (rule IDENTITY_QUOTIENT) |
|
1165 apply (simp only: FUN_REL.simps) |
|
1166 apply (rule allI) |
|
1167 apply (rule allI) |
|
1168 apply (rule impI) |
|
1169 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
|
1170 apply (rule QUOTIENT_fset) |
|
1171 apply (rule IDENTITY_QUOTIENT) |
|
1172 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
|
1173 apply (rule FUN_QUOTIENT) |
|
1174 apply (rule QUOTIENT_fset) |
|
1175 apply (rule IDENTITY_QUOTIENT) |
|
1176 apply (simp add: FUN_REL.simps) |
|
1177 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
|
1178 apply (rule QUOTIENT_fset) |
|
1179 apply (assumption) |
1165 sorry |
1180 sorry |
1166 |
1181 |
1167 prove list_induct_t: trm |
1182 prove list_induct_t: trm |
1168 apply (simp only: list_induct_tr[symmetric]) |
1183 apply (simp only: list_induct_tr[symmetric]) |
1169 apply (tactic {* rtac thm 1 *}) |
1184 apply (tactic {* rtac thm 1 *}) |