383 val fpsig_nesting_map_thms = maps #map_thms fpsig_nesting_fp_bnf_sugars; |
383 val fpsig_nesting_map_thms = maps #map_thms fpsig_nesting_fp_bnf_sugars; |
384 val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; |
384 val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; |
385 val ssig_map_thms = #map_thms ssig_fp_bnf_sugar; |
385 val ssig_map_thms = #map_thms ssig_fp_bnf_sugar; |
386 val all_algLam_alg_pointfuls = map (mk_pointful ctxt) all_algLam_algs; |
386 val all_algLam_alg_pointfuls = map (mk_pointful ctxt) all_algLam_algs; |
387 |
387 |
388 val @{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) = code_goal; |
388 val \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) = code_goal; |
389 val (fun_t, args) = strip_comb lhs; |
389 val (fun_t, args) = strip_comb lhs; |
390 val closed_rhs = fold_rev lambda args rhs; |
390 val closed_rhs = fold_rev lambda args rhs; |
391 |
391 |
392 val fun_T = fastype_of fun_t; |
392 val fun_T = fastype_of fun_t; |
393 val num_args = num_binder_types fun_T; |
393 val num_args = num_binder_types fun_T; |
445 fp_sugar_of ctxt fpT_name; |
445 fp_sugar_of ctxt fpT_name; |
446 val SOME {case_dtor, ...} = codatatype_extra_of ctxt fpT_name; |
446 val SOME {case_dtor, ...} = codatatype_extra_of ctxt fpT_name; |
447 |
447 |
448 val fp_nesting_Ts = map T_of_bnf fp_nesting_bnfs; |
448 val fp_nesting_Ts = map T_of_bnf fp_nesting_bnfs; |
449 |
449 |
450 fun is_nullary_disc_def (@{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ |
450 fun is_nullary_disc_def (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ |
451 $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _))) = true |
451 $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _))) = true |
452 | is_nullary_disc_def (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ |
452 | is_nullary_disc_def (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ |
453 $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _)) = true |
453 $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _)) = true |
454 | is_nullary_disc_def _ = false; |
454 | is_nullary_disc_def _ = false; |
455 |
455 |
510 val algrho = mk_ctr Ts algrho0; |
510 val algrho = mk_ctr Ts algrho0; |
511 |
511 |
512 val goal = mk_Trueprop_eq (fun_t, abs_curried_balanced arg_Ts algrho); |
512 val goal = mk_Trueprop_eq (fun_t, abs_curried_balanced arg_Ts algrho); |
513 |
513 |
514 fun const_of_transfer thm = |
514 fun const_of_transfer thm = |
515 (case Thm.prop_of thm of @{const Trueprop} $ (_ $ cst $ _) => cst); |
515 (case Thm.prop_of thm of \<^const>\<open>Trueprop\<close> $ (_ $ cst $ _) => cst); |
516 |
516 |
517 val eq_algrho = |
517 val eq_algrho = |
518 Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} => |
518 Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} => |
519 mk_eq_algrho_tac ctxt fpsig_nesting_maps abs rep ctor ssig_map eval pre_map_def abs_inverse |
519 mk_eq_algrho_tac ctxt fpsig_nesting_maps abs rep ctor ssig_map eval pre_map_def abs_inverse |
520 fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms |
520 fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms |
588 Logic.list_implies (map HOLogic.mk_Trueprop prems, HOLogic.mk_Trueprop concl) |
588 Logic.list_implies (map HOLogic.mk_Trueprop prems, HOLogic.mk_Trueprop concl) |
589 end; |
589 end; |
590 |
590 |
591 fun derive_cong_ctr_intros ctxt cong_ctor_intro = |
591 fun derive_cong_ctr_intros ctxt cong_ctor_intro = |
592 let |
592 let |
593 val @{const Pure.imp} $ _ $ (@{const Trueprop} $ ((Rcong as _ $ _) $ _ $ (ctor $ _))) = |
593 val \<^const>\<open>Pure.imp\<close> $ _ $ (\<^const>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _ $ (ctor $ _))) = |
594 Thm.prop_of cong_ctor_intro; |
594 Thm.prop_of cong_ctor_intro; |
595 |
595 |
596 val fpT as Type (fpT_name, fp_argTs) = range_type (fastype_of ctor); |
596 val fpT as Type (fpT_name, fp_argTs) = range_type (fastype_of ctor); |
597 |
597 |
598 val SOME {pre_bnf, absT_info = {abs_inverse, ...}, |
598 val SOME {pre_bnf, absT_info = {abs_inverse, ...}, |
613 map2 prove ctr_defs goals |
613 map2 prove ctr_defs goals |
614 end; |
614 end; |
615 |
615 |
616 fun derive_cong_friend_intro ctxt cong_algrho_intro = |
616 fun derive_cong_friend_intro ctxt cong_algrho_intro = |
617 let |
617 let |
618 val @{const Pure.imp} $ _ $ (@{const Trueprop} $ ((Rcong as _ $ _) $ _ |
618 val \<^const>\<open>Pure.imp\<close> $ _ $ (\<^const>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _ |
619 $ ((algrho as Const (algrho_name, _)) $ _))) = |
619 $ ((algrho as Const (algrho_name, _)) $ _))) = |
620 Thm.prop_of cong_algrho_intro; |
620 Thm.prop_of cong_algrho_intro; |
621 |
621 |
622 val fpT as Type (_, fp_argTs) = range_type (fastype_of algrho); |
622 val fpT as Type (_, fp_argTs) = range_type (fastype_of algrho); |
623 |
623 |
624 fun has_algrho (@{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ rhs)) = |
624 fun has_algrho (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ rhs)) = |
625 fst (dest_Const (head_of (strip_abs_body rhs))) = algrho_name; |
625 fst (dest_Const (head_of (strip_abs_body rhs))) = algrho_name; |
626 |
626 |
627 val eq_algrho :: _ = |
627 val eq_algrho :: _ = |
628 maps (filter (has_algrho o Thm.prop_of) o #eq_algrhos o snd) (all_friend_extras_of ctxt); |
628 maps (filter (has_algrho o Thm.prop_of) o #eq_algrhos o snd) (all_friend_extras_of ctxt); |
629 |
629 |
630 val @{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ friend0 $ _) = Thm.prop_of eq_algrho; |
630 val \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ friend0 $ _) = Thm.prop_of eq_algrho; |
631 val friend = mk_ctr fp_argTs friend0; |
631 val friend = mk_ctr fp_argTs friend0; |
632 |
632 |
633 val goal = mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong friend; |
633 val goal = mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong friend; |
634 in |
634 in |
635 Variable.add_free_names ctxt goal [] |
635 Variable.add_free_names ctxt goal [] |
652 |
652 |
653 fun derive_coinduct ctxt (fpT as Type (fpT_name, fpT_args)) dtor_coinduct = |
653 fun derive_coinduct ctxt (fpT as Type (fpT_name, fpT_args)) dtor_coinduct = |
654 let |
654 let |
655 val thy = Proof_Context.theory_of ctxt; |
655 val thy = Proof_Context.theory_of ctxt; |
656 |
656 |
657 val @{const Pure.imp} $ (@{const Trueprop} $ (_ $ Abs (_, _, _ $ |
657 val \<^const>\<open>Pure.imp\<close> $ (\<^const>\<open>Trueprop\<close> $ (_ $ Abs (_, _, _ $ |
658 Abs (_, _, @{const implies} $ _ $ (_ $ (cong0 $ _) $ _ $ _))))) $ _ = |
658 Abs (_, _, \<^const>\<open>implies\<close> $ _ $ (_ $ (cong0 $ _) $ _ $ _))))) $ _ = |
659 Thm.prop_of dtor_coinduct; |
659 Thm.prop_of dtor_coinduct; |
660 |
660 |
661 val SOME {X as TVar ((X_s, _), _), fp_res = {dtor_ctors, ...}, pre_bnf, |
661 val SOME {X as TVar ((X_s, _), _), fp_res = {dtor_ctors, ...}, pre_bnf, |
662 absT_info = {abs_inverse, ...}, live_nesting_bnfs, |
662 absT_info = {abs_inverse, ...}, live_nesting_bnfs, |
663 fp_ctr_sugar = {ctrXs_Tss, ctr_defs, |
663 fp_ctr_sugar = {ctrXs_Tss, ctr_defs, |
818 val grouped_disc_views = discs |
818 val grouped_disc_views = discs |
819 |> map (collect_condss_disc [] raw_views) |
819 |> map (collect_condss_disc [] raw_views) |
820 |> curry (op ~~) (map (fn disc => disc $ lhs) discs); |
820 |> curry (op ~~) (map (fn disc => disc $ lhs) discs); |
821 |
821 |
822 fun mk_disc_iff_props props [] = props |
822 fun mk_disc_iff_props props [] = props |
823 | mk_disc_iff_props _ ((lhs, @{const HOL.True}) :: _) = [lhs] |
823 | mk_disc_iff_props _ ((lhs, \<^const>\<open>HOL.True\<close>) :: _) = [lhs] |
824 | mk_disc_iff_props props ((lhs, rhs) :: views) = |
824 | mk_disc_iff_props props ((lhs, rhs) :: views) = |
825 mk_disc_iff_props ((HOLogic.mk_eq (lhs, rhs)) :: props) views; |
825 mk_disc_iff_props ((HOLogic.mk_eq (lhs, rhs)) :: props) views; |
826 in |
826 in |
827 (grouped_disc_views |
827 (grouped_disc_views |
828 |> map swap, |
828 |> map swap, |
2239 val fun_b = Binding.name (Long_Name.base_name fun_name); |
2239 val fun_b = Binding.name (Long_Name.base_name fun_name); |
2240 val code_goal = Syntax.read_prop fake_lthy raw_eq; |
2240 val code_goal = Syntax.read_prop fake_lthy raw_eq; |
2241 |
2241 |
2242 val fun_T = |
2242 val fun_T = |
2243 (case code_goal of |
2243 (case code_goal of |
2244 @{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _) => fastype_of (head_of t) |
2244 \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _) => fastype_of (head_of t) |
2245 | _ => ill_formed_equation_lhs_rhs lthy [code_goal]); |
2245 | _ => ill_formed_equation_lhs_rhs lthy [code_goal]); |
2246 val fun_t = Const (fun_name, fun_T); |
2246 val fun_t = Const (fun_name, fun_T); |
2247 |
2247 |
2248 val (arg_Ts, res_T as Type (fpT_name, _)) = strip_type fun_T; |
2248 val (arg_Ts, res_T as Type (fpT_name, _)) = strip_type fun_T; |
2249 |
2249 |