1380 (cterm_instantiate_pos (nones @ [SOME cxIn]) |
1380 (cterm_instantiate_pos (nones @ [SOME cxIn]) |
1381 (if fp = Least_FP then fp_map_thm |
1381 (if fp = Least_FP then fp_map_thm |
1382 else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans)))) |
1382 else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans)))) |
1383 |> singleton (Proof_Context.export names_lthy no_defs_lthy); |
1383 |> singleton (Proof_Context.export names_lthy no_defs_lthy); |
1384 |
1384 |
1385 fun mk_set_thm fp_set_thm ctr_def' cxIn = |
1385 |
|
1386 fun mk_set0_thm fp_set_thm ctr_def' cxIn = |
1386 fold_thms lthy [ctr_def'] |
1387 fold_thms lthy [ctr_def'] |
1387 (unfold_thms lthy (pre_set_defs @ fp_nesting_set_maps @ live_nesting_set_maps @ |
1388 (unfold_thms lthy (pre_set_defs @ fp_nesting_set_maps @ live_nesting_set_maps @ |
1388 (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_set @ |
1389 (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_set @ |
1389 abs_inverses) |
1390 @{thms UN_Un sup_assoc[THEN sym]} @ abs_inverses) |
1390 (cterm_instantiate_pos [SOME cxIn] fp_set_thm)) |
1391 (cterm_instantiate_pos [SOME cxIn] fp_set_thm)) |
1391 |> singleton (Proof_Context.export names_lthy no_defs_lthy); |
1392 |> singleton (Proof_Context.export names_lthy no_defs_lthy); |
1392 |
1393 |
1393 fun mk_set_thms fp_set_thm = map2 (mk_set_thm fp_set_thm) ctr_defs' cxIns; |
1394 fun mk_set0_thms fp_set_thm = map2 (mk_set0_thm fp_set_thm) ctr_defs' cxIns; |
1394 |
1395 |
1395 val map_thms = map2 mk_map_thm ctr_defs' cxIns; |
1396 val map_thms = map2 mk_map_thm ctr_defs' cxIns; |
1396 val set_thmss = map mk_set_thms fp_set_thms; |
1397 val set0_thmss = map mk_set0_thms fp_set_thms; |
1397 val set_thms = flat set_thmss; |
1398 val set0_thms = flat set0_thmss; |
|
1399 val set_thms = set0_thms |
|
1400 |> map (unfold_thms lthy @{thms insert_is_Un[THEN sym] Un_empty_left |
|
1401 Un_insert_left}); |
1398 |
1402 |
1399 val sets = map (mk_set (snd (Term.dest_Type fpT))) (sets_of_bnf fp_bnf); |
1403 val sets = map (mk_set (snd (Term.dest_Type fpT))) (sets_of_bnf fp_bnf); |
1400 |
1404 |
1401 val set_empty_thms = |
1405 val set_empty_thms = |
1402 let |
1406 let |
1424 if null goals then |
1428 if null goals then |
1425 [] |
1429 [] |
1426 else |
1430 else |
1427 Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) |
1431 Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) |
1428 (fn {context = ctxt, prems = _} => |
1432 (fn {context = ctxt, prems = _} => |
1429 mk_set_empty_tac ctxt (certify ctxt u) exhaust set_thms (flat disc_thmss)) |
1433 mk_set_empty_tac ctxt (certify ctxt u) exhaust set0_thms (flat disc_thmss)) |
1430 |> Conjunction.elim_balanced (length goals) |
1434 |> Conjunction.elim_balanced (length goals) |
1431 |> Proof_Context.export names_lthy lthy |
1435 |> Proof_Context.export names_lthy lthy |
1432 |> map Thm.close_derivation |
1436 |> map Thm.close_derivation |
1433 end; |
1437 end; |
1434 |
1438 |
1693 [] |
1697 [] |
1694 else |
1698 else |
1695 Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) |
1699 Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) |
1696 (fn {context = ctxt, prems = _} => |
1700 (fn {context = ctxt, prems = _} => |
1697 mk_sel_set_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) |
1701 mk_sel_set_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) |
1698 (flat sel_thmss) set_thms) |
1702 (flat sel_thmss) set0_thms) |
1699 |> Conjunction.elim_balanced (length goals) |
1703 |> Conjunction.elim_balanced (length goals) |
1700 |> Proof_Context.export names_lthy lthy |
1704 |> Proof_Context.export names_lthy lthy |
1701 end; |
1705 end; |
1702 in |
1706 in |
1703 (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, |
1707 (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, |
1726 val (noted, lthy') = |
1730 val (noted, lthy') = |
1727 lthy |
1731 lthy |
1728 |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms) |
1732 |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms) |
1729 |> fp = Least_FP |
1733 |> fp = Least_FP |
1730 ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms) |
1734 ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms) |
1731 |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set_thms) |
1735 |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set0_thms) |
1732 |> Local_Theory.notes (anonymous_notes @ notes); |
1736 |> Local_Theory.notes (anonymous_notes @ notes); |
1733 |
1737 |
1734 val subst = Morphism.thm (substitute_noted_thm noted); |
1738 val subst = Morphism.thm (substitute_noted_thm noted); |
1735 in |
1739 in |
1736 (((map subst map_thms, map subst rel_inject_thms, map subst rel_distinct_thms, |
1740 (((map subst map_thms, map subst rel_inject_thms, map subst rel_distinct_thms, |
1737 map (map subst) set_thmss), ctr_sugar), lthy') |
1741 map (map subst) set0_thmss), ctr_sugar), lthy') |
1738 end; |
1742 end; |
1739 |
1743 |
1740 fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b); |
1744 fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b); |
1741 |
1745 |
1742 fun massage_res (((maps_sets_rels, ctr_sugar), co_rec_res), lthy) = |
1746 fun massage_res (((maps_sets_rels, ctr_sugar), co_rec_res), lthy) = |