1165 apply (metis) |
1165 apply (metis) |
1166 done |
1166 done |
1167 |
1167 |
1168 ML {* val thm = @{thm list_induct_r} OF [li] *} |
1168 ML {* val thm = @{thm list_induct_r} OF [li] *} |
1169 ML {* val trm = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1169 ML {* val trm = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1170 thm APPLY_RSP |
|
1171 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"] |
1170 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"] |
1172 lemmas APPLY_RSP_I2 = APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"] |
|
1173 |
|
1174 thm REP_ABS_RSP(2) |
|
1175 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"] |
1171 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"] |
1176 |
1172 |
1177 prove trm |
1173 prove trm |
1178 thm UNION_def |
|
1179 apply (atomize(full)) |
1174 apply (atomize(full)) |
1180 apply (simp only: id_def[symmetric]) |
1175 apply (simp only: id_def[symmetric]) |
1181 |
1176 |
1182 (* APPLY_RSP_TAC *) |
1177 (* APPLY_RSP_TAC *) |
1183 ML_prf {* |
1178 ML_prf {* |
1184 val (_, gc') = Thm.dest_comb (Subgoal.focus @{context} 1 (Isar.goal ()) |> fst |> #concl) |
1179 val (_, gc') = Thm.dest_comb (Subgoal.focus @{context} 1 (Isar.goal ()) |> fst |> #concl) |
1185 val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "APPLY_RSP_I" })) |
1180 val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "APPLY_RSP_I" })) |
1186 val m = Thm.match (tc', gc') |
1181 val m = Thm.match (tc', gc') |
1187 val t2 = Drule.instantiate m @{thm "APPLY_RSP_I" } |
1182 val t2 = Drule.instantiate m @{thm "APPLY_RSP_I" } |
1188 *} |
1183 *} |
|
1184 thm APPLY_RSP_I |
1189 apply (tactic {* rtac t2 1 *}) |
1185 apply (tactic {* rtac t2 1 *}) |
1190 prefer 4 |
1186 prefer 2 |
|
1187 apply (rule IDENTITY_QUOTIENT) |
|
1188 prefer 3 |
1191 (* ABS_REP_RSP_TAC *) |
1189 (* ABS_REP_RSP_TAC *) |
1192 ML_prf {* |
1190 ML_prf {* |
1193 val (_, gc') = Thm.dest_comb (Subgoal.focus @{context} 1 (Isar.goal ()) |> fst |> #concl) |
1191 val (_, gc') = Thm.dest_comb (Subgoal.focus @{context} 1 (Isar.goal ()) |> fst |> #concl) |
1194 val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "REP_ABS_RSP_I" })) |
1192 val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "REP_ABS_RSP_I" })) |
1195 val m = Thm.match (tc', gc') |
1193 val m = Thm.match (tc', gc') |
1215 (* MK_COMB_TAC *) |
1213 (* MK_COMB_TAC *) |
1216 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1214 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1217 (* REFL_TAC *) |
1215 (* REFL_TAC *) |
1218 apply (simp) |
1216 apply (simp) |
1219 (* APPLY_RSP_TAC *) |
1217 (* APPLY_RSP_TAC *) |
1220 thm APPLY_RSP |
|
1221 apply (rule_tac APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
1218 apply (rule_tac APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
1222 (* MINE *) |
|
1223 apply (rule QUOTIENT_fset) |
1219 apply (rule QUOTIENT_fset) |
1224 prefer 3 |
1220 apply (rule IDENTITY_QUOTIENT) |
|
1221 prefer 2 |
1225 (* ABS_REP_RSP *) |
1222 (* ABS_REP_RSP *) |
1226 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1223 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1227 (* MINE *) |
|
1228 apply (rule QUOTIENT_fset) |
1224 apply (rule QUOTIENT_fset) |
1229 (* MINE *) |
1225 (* MINE *) |
1230 apply (rule list_eq_refl ) |
1226 apply (rule list_eq_refl ) |
1231 prefer 2 |
|
1232 (* ABS_REP_RSP *) |
1227 (* ABS_REP_RSP *) |
1233 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
1228 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
1234 prefer 2 |
1229 prefer 2 |
1235 (* MINE *) |
1230 (* MINE *) |
1236 apply (simp only: FUN_REL.simps) |
1231 apply (simp only: FUN_REL.simps) |
1237 prefer 3 |
1232 prefer 2 |
1238 (* APPLY_RSP *) |
1233 (* APPLY_RSP *) |
1239 apply (rule_tac APPLY_RSP[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id" "op =" "id" "id" "Ball (Respects op \<approx>)" "Ball (Respects op \<approx>)"]) |
1234 apply (rule_tac APPLY_RSP[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id" "op =" "id" "id" "Ball (Respects op \<approx>)" "Ball (Respects op \<approx>)"]) |
1240 (* 3: ho_respects *) |
1235 prefer 2 |
1241 prefer 4 |
1236 apply (rule IDENTITY_QUOTIENT) |
|
1237 (* 2: ho_respects *) |
|
1238 prefer 3 |
1242 (* ABS_REP_RSP *) |
1239 (* ABS_REP_RSP *) |
1243 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
1240 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
1244 prefer 2 |
1241 prefer 2 |
1245 (* LAMBDA_RSP *) |
1242 (* LAMBDA_RSP *) |
1246 apply (simp only: FUN_REL.simps) |
1243 apply (simp only: FUN_REL.simps) |
1253 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1250 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1254 (* REFL_TAC *) |
1251 (* REFL_TAC *) |
1255 apply (simp) |
1252 apply (simp) |
1256 (* APPLY_RSP *) |
1253 (* APPLY_RSP *) |
1257 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
1254 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
1258 prefer 3 |
1255 apply (rule QUOTIENT_fset) |
|
1256 apply (rule IDENTITY_QUOTIENT) |
1259 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
1257 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
1260 prefer 2 |
1258 prefer 2 |
1261 (* MINE *) |
1259 (* MINE *) |
1262 apply (simp only: FUN_REL.simps) |
1260 apply (simp only: FUN_REL.simps) |
1263 prefer 4 |
1261 prefer 2 |
1264 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1262 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1265 prefer 2 |
1263 apply (rule QUOTIENT_fset) |
1266 (* FIRST_ASSUM MATCH_ACCEPT_TAC *) |
1264 (* FIRST_ASSUM MATCH_ACCEPT_TAC *) |
1267 apply (assumption) |
1265 apply (assumption) |
1268 prefer 5 |
1266 prefer 2 |
1269 (* MK_COMB_TAC *) |
1267 (* MK_COMB_TAC *) |
1270 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1268 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1271 (* REFL_TAC *) |
1269 (* REFL_TAC *) |
1272 apply (simp) |
1270 apply (simp) |
1273 (* W(C (curry op THEN) (G... *) |
1271 (* W(C (curry op THEN) (G... *) |
1274 apply (rule ext) |
1272 apply (rule ext) |
1275 (* APPLY_RSP *) |
1273 (* APPLY_RSP *) |
1276 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
1274 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
1277 prefer 3 |
1275 apply (rule QUOTIENT_fset) |
|
1276 apply (rule IDENTITY_QUOTIENT) |
1278 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
1277 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
1279 prefer 2 |
1278 prefer 2 |
1280 apply (simp only: FUN_REL.simps) |
1279 apply (simp only: FUN_REL.simps) |
1281 prefer 4 |
1280 prefer 2 |
1282 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1281 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1283 prefer 2 |
1282 apply (rule QUOTIENT_fset) |
1284 (* APPLY_RSP *) |
1283 (* APPLY_RSP *) |
1285 apply (rule_tac ?f="\<lambda>x. h # x" and ?g="\<lambda>x. h # x" in APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] ) |
1284 apply (rule_tac ?f="\<lambda>x. h # x" and ?g="\<lambda>x. h # x" in APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] ) |
1286 prefer 3 |
1285 apply (rule QUOTIENT_fset) |
|
1286 apply (rule QUOTIENT_fset) |
1287 apply (rule_tac ?f="op #" and ?g="op #" in APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"]) |
1287 apply (rule_tac ?f="op #" and ?g="op #" in APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"]) |
1288 (* 3: CONS respects *) |
1288 apply (rule IDENTITY_QUOTIENT) |
1289 prefer 3 |
1289 (* CONS respects *) |
1290 apply (simp only: FUN_REL.simps) |
1290 prefer 2 |
|
1291 apply (simp add: FUN_REL.simps) |
|
1292 apply (rule allI) |
1291 apply (rule allI) |
1293 apply (rule allI) |
1292 apply (rule allI) |
1294 apply (rule allI) |
1293 apply (rule impI) |
1295 apply (rule impI) |
1294 apply (rule allI) |
|
1295 apply (rule allI) |
|
1296 apply (rule impI) |
|
1297 apply (simp) |
|
1298 thm cons_preserves |
|
1299 apply (rule cons_preserves) |
1296 apply (rule cons_preserves) |
1300 apply (assumption) |
1297 apply (assumption) |
1301 prefer 3 |
1298 prefer 2 |
1302 apply (simp) |
1299 apply (simp) |
1303 (* Mine *) |
|
1304 apply (simp only: id_def) |
|
1305 apply (rule IDENTITY_QUOTIENT) |
|
1306 prefer 2 |
|
1307 apply (rule QUOTIENT_fset) |
|
1308 prefer 2 |
|
1309 apply (rule QUOTIENT_fset) |
|
1310 prefer 3 |
|
1311 apply (rule QUOTIENT_fset) |
|
1312 sorry |
1300 sorry |
1313 |
1301 |
1314 thm list.recs(2) |
1302 thm list.recs(2) |
1315 |
1303 |
1316 |
1304 |