1182 apply (metis) |
1182 apply (metis) |
1183 done |
1183 done |
1184 |
1184 |
1185 ML {* val thm = @{thm list_induct_r} OF [li] *} |
1185 ML {* val thm = @{thm list_induct_r} OF [li] *} |
1186 ML {* val trm = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1186 ML {* val trm = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
|
1187 thm APPLY_RSP |
|
1188 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"] |
|
1189 |
|
1190 thm REP_ABS_RSP |
|
1191 lemmas REP_ABS_RSP_I = REP_ABS_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"] |
|
1192 |
1187 prove trm |
1193 prove trm |
|
1194 apply (atomize(full)) |
|
1195 |
|
1196 ML_prf {* |
|
1197 val gc = Subgoal.focus @{context} 1 (Isar.goal ()) |
|
1198 |> fst |
|
1199 |> #concl |
|
1200 val tc = cterm_of @{theory} (concl_of ( @{thm "APPLY_RSP_I" })) |
|
1201 val (_, tc') = Thm.dest_comb tc |
|
1202 val (_, gc') = Thm.dest_comb gc |
|
1203 *} |
|
1204 ML_prf {* val m = Thm.match (tc', gc') *} |
|
1205 ML_prf {* val t2 = Drule.instantiate m @{thm "APPLY_RSP_I" } *} |
|
1206 (* APPLY_RSP_TAC *) |
|
1207 apply (tactic {* rtac t2 1 *}) |
|
1208 prefer 4 |
|
1209 (* ABS_REP_RSP_TAC *) |
|
1210 ML_prf {* |
|
1211 val gc = Subgoal.focus @{context} 1 (Isar.goal ()) |
|
1212 |> fst |
|
1213 |> #concl |
|
1214 val tc = cterm_of @{theory} (concl_of @{thm "REP_ABS_RSP_I" }) |
|
1215 val (_, tc') = Thm.dest_comb tc |
|
1216 val (_, gc') = Thm.dest_comb gc |
|
1217 *} |
|
1218 |
|
1219 ML_prf {* val m = Thm.match (tc', gc') *} |
|
1220 ML_prf {* val t2 = Drule.instantiate m @{thm "REP_ABS_RSP_I" } *} |
|
1221 apply (tactic {* rtac t2 1 *}) |
|
1222 |
|
1223 thm QUOT_TYPE.REP_ABS_rsp(2) |
|
1224 |
|
1225 (* LAMBDA_RES_TAC *) |
|
1226 |
|
1227 |
|
1228 apply (simp) |
|
1229 apply (simp only: FUN_REL.simps) |
|
1230 |
|
1231 apply (unfold FUN_REL_def) |
|
1232 |
1188 sorry |
1233 sorry |
|
1234 |
|
1235 thm list.recs(2) |
|
1236 |
1189 |
1237 |
1190 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
1238 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
1191 |
1239 |
1192 prove card1_suc_r: {* |
1240 prove card1_suc_r: {* |
1193 Logic.mk_implies |
1241 Logic.mk_implies |
1297 (REP_fset (ABS_fset l))))))))) |
1345 (REP_fset (ABS_fset l))))))))) |
1298 |
1346 |
1299 = Ball (Respects ((op \<approx>) ===> (op =))) |
1347 = Ball (Respects ((op \<approx>) ===> (op =))) |
1300 (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow> |
1348 (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow> |
1301 (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))" |
1349 (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))" |
|
1350 |
|
1351 thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"] |
|
1352 proof - |
|
1353 note APPLY_RSP_I = APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"] |
|
1354 show ?thesis apply - |
|
1355 |
|
1356 |
|
1357 ML_prf {* |
|
1358 val gc = Subgoal.focus @{context} 1 (Isar.goal ()) |
|
1359 |> fst |
|
1360 |> #concl |
|
1361 val tc = cterm_of @{theory} (concl_of ( @{thm "APPLY_RSP" })) |
|
1362 val (_, tc') = Thm.dest_comb tc |
|
1363 val (_, gc') = Thm.dest_comb gc |
|
1364 *} |
|
1365 |
|
1366 |
|
1367 |
|
1368 |
|
1369 ML_prf {* |
|
1370 (gc', tc') |
|
1371 *} |
|
1372 ML_prf {* Pattern.first_order_match *} |
|
1373 ML_prf {* Thm.match (@{cpat "?P::?'a"}, @{cterm "1::nat"}) *} |
|
1374 ML_prf {* Pattern.match @{theory} (term_of @{cpat "?P::nat"}, term_of @{cterm "1::nat"}) (Vartab.empty, Vartab.empty) *} |
|
1375 |
|
1376 ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *} |
|
1377 ML_prf {* val (op2, (l2, r2)) = dest_cbinop gc' *} |
|
1378 |
|
1379 ML_prf {* val mo = Thm.match (op1, op2) *} |
|
1380 ML_prf {* val t1 = Drule.instantiate mo @{thm "APPLY_RSP" } *} |
|
1381 ML_prf {* val tc = cterm_of @{theory} (concl_of t1) *} |
|
1382 ML_prf {* val (_, tc') = Thm.dest_comb tc *} |
|
1383 ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *} |
|
1384 ML_prf {* val (mlty, mlt) = Thm.match (l1, l2) *} |
|
1385 ML_prf {* val t2 = Drule.instantiate (mlty, []) t1 *} |
|
1386 ML_prf {* val tc = cterm_of @{theory} (concl_of t2) *} |
|
1387 ML_prf {* val (_, tc') = Thm.dest_comb tc *} |
|
1388 ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *} |
|
1389 ML_prf {* val mr = Thm.match (r1, r2) *} |
|
1390 |
|
1391 ML_prf {* val t3 = Drule.instantiate ml t2 *} |
|
1392 ML_prf {* val tc = cterm_of @{theory} (concl_of t3) *} |
|
1393 ML_prf {* val (_, tc') = Thm.dest_comb tc *} |
|
1394 |
|
1395 |
|
1396 |
|
1397 ML_prf {* mtyl; mtyr *} |
|
1398 |
|
1399 ML_prf {* val ol1 = Thm.capply op1 l1 *} |
|
1400 ML_prf {* val ol2 = Thm.capply op2 l2 *} |
|
1401 ML_prf {* (ol1, ol2); Thm.match (ol1, ol2) *} |
|
1402 ML_prf {* val w1 = Thm.capply ol1 r1 *} |
|
1403 ML_prf {* val w2 = Thm.capply ol2 r2 *} |
|
1404 |
|
1405 |
|
1406 . |
|
1407 (*ML_prf {* (w1, w2); Thm.match (w1, w2) *}*) |
|
1408 |
|
1409 |
|
1410 |
|
1411 ML_prf {* |
|
1412 (tc', gc') |
|
1413 *} |
|
1414 |
1302 thm APPLY_RSP |
1415 thm APPLY_RSP |
1303 thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"] |
1416 thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)"] |
|
1417 term "(op \<approx> ===> op =) ===> op =" |
|
1418 proof - |
|
1419 note APPLY_RSP_I2 = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id" "Ball (Respects op \<approx> ===> op =)" "Ball (Respects op \<approx> ===> op =)"] |
|
1420 show ?thesis apply - |
|
1421 |
|
1422 thm APPLY_RSP_I2[of _ "\<lambda>P. (P [] \<and> (\<forall>t\<Colon>'b list\<in>Respects op \<approx>. P t \<longrightarrow> (\<forall>h\<Colon>'b. P (h # t))) \<longrightarrow> |
|
1423 (\<forall>l\<Colon>'b list\<in>Respects op \<approx>. P l))"] |
|
1424 proof - |
|
1425 note APPLY_RSP_I3=APPLY_RSP_I2[of _ "\<lambda>P. (P [] \<and> (\<forall>t\<Colon>'b list\<in>Respects op \<approx>. P t \<longrightarrow> (\<forall>h\<Colon>'b. P (h # t))) \<longrightarrow> |
|
1426 (\<forall>l\<Colon>'b list\<in>Respects op \<approx>. P l))"] |
|
1427 show ?thesis apply - |
|
1428 term "(REP_fset ---> id ---> id |
|
1429 (ABS_fset ---> id ---> id |
|
1430 (\<lambda>P\<Colon>'a list \<Rightarrow> bool. |
|
1431 ABS_fset ---> id (REP_fset ---> id P) |
|
1432 (REP_fset (ABS_fset [])) \<and> |
|
1433 Ball (Respects op \<approx>) |
|
1434 (ABS_fset ---> id |
|
1435 (REP_fset ---> id |
|
1436 (\<lambda>t\<Colon>'a list. |
|
1437 ABS_fset ---> id (REP_fset ---> id P) |
|
1438 (REP_fset (ABS_fset t)) \<longrightarrow> |
|
1439 (\<forall>h\<Colon>'a. |
|
1440 ABS_fset ---> id (REP_fset ---> id P) |
|
1441 (REP_fset |
|
1442 (ABS_fset |
|
1443 (h # REP_fset (ABS_fset t)))))))) \<longrightarrow> |
|
1444 Ball (Respects op \<approx>) |
|
1445 (ABS_fset ---> id |
|
1446 (REP_fset ---> id |
|
1447 (\<lambda>l\<Colon>'a list. |
|
1448 ABS_fset ---> id (REP_fset ---> id P) |
|
1449 (REP_fset (ABS_fset l))))))))" |
|
1450 |
|
1451 apply (rule APPLY_RSP_I3) |
|
1452 term "Ball (Respects op \<approx> ===> op =)" |
|
1453 thm APPLY_RSP_I [of _ "Ball (Respects op \<approx> ===> op =)"] |
|
1454 |
|
1455 thm APPLY_RSP |
|
1456 |
|
1457 . |
|
1458 |
|
1459 apply (tactic {* Cong_Tac.cong_tac @{thm APPLY_RSP_I} 1 *} ) |
|
1460 |
|
1461 apply (tactic {* match_tac @{thms APPLY_RSP_I} 1 *}) |
|
1462 . |
|
1463 |
1304 apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"]) |
1464 apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"]) |
1305 apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op ="]) |
1465 apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op ="]) |
1306 term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))" |
1466 term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))" |
1307 thm LAMBDA_PRS1[symmetric] |
1467 thm LAMBDA_PRS1[symmetric] |
1308 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*) |
1468 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*) |