equal
deleted
inserted
replaced
1449 map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong0 => |
1449 map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong0 => |
1450 Goal.prove_sorry lthy [] [] goal (K (mk_map_tac m n foldx map_comp_id map_cong0)) |
1450 Goal.prove_sorry lthy [] [] goal (K (mk_map_tac m n foldx map_comp_id map_cong0)) |
1451 |> Thm.close_derivation) |
1451 |> Thm.close_derivation) |
1452 goals ctor_fold_thms map_comp_id_thms map_cong0s; |
1452 goals ctor_fold_thms map_comp_id_thms map_cong0s; |
1453 in |
1453 in |
1454 map (fn thm => thm RS @{thm pointfreeE}) maps |
1454 map (fn thm => thm RS @{thm comp_eq_dest}) maps |
1455 end; |
1455 end; |
1456 |
1456 |
1457 val (ctor_map_unique_thms, ctor_map_unique_thm) = |
1457 val (ctor_map_unique_thms, ctor_map_unique_thm) = |
1458 let |
1458 let |
1459 fun mk_prem u map ctor ctor' = |
1459 fun mk_prem u map ctor ctor' = |