293 register_coinduct_dynamic_base fpT_name |
293 register_coinduct_dynamic_base fpT_name |
294 #> ensure_codatatype_extra fpT_name; |
294 #> ensure_codatatype_extra fpT_name; |
295 |
295 |
296 fun is_set ctxt (const_name, T) = |
296 fun is_set ctxt (const_name, T) = |
297 (case T of |
297 (case T of |
298 Type (@{type_name fun}, [Type (fpT_name, _), Type (@{type_name set}, [_])]) => |
298 Type (\<^type_name>\<open>fun\<close>, [Type (fpT_name, _), Type (\<^type_name>\<open>set\<close>, [_])]) => |
299 (case bnf_of ctxt fpT_name of |
299 (case bnf_of ctxt fpT_name of |
300 SOME bnf => exists (fn Const (s, _) => s = const_name | _ => false) (sets_of_bnf bnf) |
300 SOME bnf => exists (fn Const (s, _) => s = const_name | _ => false) (sets_of_bnf bnf) |
301 | NONE => false) |
301 | NONE => false) |
302 | _ => false); |
302 | _ => false); |
303 |
303 |
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 HOL.eq}, _) $ lhs $ rhs) = code_goal; |
388 val @{const Trueprop} $ (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 HOL.eq}, _) $ _ |
450 fun is_nullary_disc_def (@{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ |
451 $ (Const (@{const_name HOL.eq}, _) $ _ $ _))) = true |
451 $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _))) = true |
452 | is_nullary_disc_def (Const (@{const_name Pure.eq}, _) $ _ |
452 | is_nullary_disc_def (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ |
453 $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true |
453 $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _)) = true |
454 | is_nullary_disc_def _ = false; |
454 | is_nullary_disc_def _ = false; |
455 |
455 |
456 val dtor_ctor = nth (#dtor_ctors fp_res) fp_res_index; |
456 val dtor_ctor = nth (#dtor_ctors fp_res) fp_res_index; |
457 val ctor_iff_dtor = #ctor_iff_dtor fp_ctr_sugar; |
457 val ctor_iff_dtor = #ctor_iff_dtor fp_ctr_sugar; |
458 val ctr_sugar = #ctr_sugar fp_ctr_sugar; |
458 val ctr_sugar = #ctr_sugar fp_ctr_sugar; |
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 HOL.eq}, _) $ _ $ rhs)) = |
624 fun has_algrho (@{const Trueprop} $ (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 HOL.eq}, _) $ friend0 $ _) = Thm.prop_of eq_algrho; |
630 val @{const Trueprop} $ (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 [] |
666 fp_sugar_of ctxt fpT_name; |
666 fp_sugar_of ctxt fpT_name; |
667 |
667 |
668 val n = length ctrXs_Tss; |
668 val n = length ctrXs_Tss; |
669 val ms = map length ctrXs_Tss; |
669 val ms = map length ctrXs_Tss; |
670 |
670 |
671 val X' = TVar ((X_s, maxidx_of_typ fpT + 1), @{sort type}); |
671 val X' = TVar ((X_s, maxidx_of_typ fpT + 1), \<^sort>\<open>type\<close>); |
672 val As_rho = tvar_subst thy T0_args fpT_args; |
672 val As_rho = tvar_subst thy T0_args fpT_args; |
673 val substXAT = Term.typ_subst_TVars As_rho o Tsubst X X'; |
673 val substXAT = Term.typ_subst_TVars As_rho o Tsubst X X'; |
674 val substXA = Term.subst_TVars As_rho o substT X X'; |
674 val substXA = Term.subst_TVars As_rho o substT X X'; |
675 val phi = Morphism.typ_morphism "BNF" substXAT $> Morphism.term_morphism "BNF" substXA; |
675 val phi = Morphism.typ_morphism "BNF" substXAT $> Morphism.term_morphism "BNF" substXA; |
676 |
676 |
697 |
697 |
698 fun explore_nested lthy explore {bound_Us, bound_Ts, U, T} t = |
698 fun explore_nested lthy explore {bound_Us, bound_Ts, U, T} t = |
699 let |
699 let |
700 fun build_simple (T, U) = |
700 fun build_simple (T, U) = |
701 if T = U then |
701 if T = U then |
702 @{term "%y. y"} |
702 \<^term>\<open>%y. y\<close> |
703 else |
703 else |
704 Bound 0 |
704 Bound 0 |
705 |> explore {bound_Us = T :: bound_Us, bound_Ts = T :: bound_Ts, U = U, T = T} |
705 |> explore {bound_Us = T :: bound_Us, bound_Ts = T :: bound_Ts, U = U, T = T} |
706 |> (fn t => Abs (Name.uu, T, t)); |
706 |> (fn t => Abs (Name.uu, T, t)); |
707 in |
707 in |
734 massage_any massages |
734 massage_any massages |
735 end; |
735 end; |
736 |
736 |
737 fun massage_let explore params t = |
737 fun massage_let explore params t = |
738 (case strip_comb t of |
738 (case strip_comb t of |
739 (Const (@{const_name Let}, _), [_, _]) => unfold_lets_splits t |
739 (Const (\<^const_name>\<open>Let\<close>, _), [_, _]) => unfold_lets_splits t |
740 | _ => t) |
740 | _ => t) |
741 |> explore params; |
741 |> explore params; |
742 |
742 |
743 fun check_corec_equation ctxt fun_frees (lhs, rhs) = |
743 fun check_corec_equation ctxt fun_frees (lhs, rhs) = |
744 let |
744 let |
914 val sel_positionss = map mk_sel_positions ordered_sels; |
914 val sel_positionss = map mk_sel_positions ordered_sels; |
915 val sel_rhss = map2 mk_sel_rhs sel_positionss ordered_sels; |
915 val sel_rhss = map2 mk_sel_rhs sel_positionss ordered_sels; |
916 val sel_lhss = map (rapp lhs o mk_disc_or_sel Ts) ordered_sels; |
916 val sel_lhss = map (rapp lhs o mk_disc_or_sel Ts) ordered_sels; |
917 val sel_condss = map collect_sel_condss sel_positionss; |
917 val sel_condss = map collect_sel_condss sel_positionss; |
918 |
918 |
919 fun is_undefined (Const (@{const_name undefined}, _)) = true |
919 fun is_undefined (Const (\<^const_name>\<open>undefined\<close>, _)) = true |
920 | is_undefined _ = false; |
920 | is_undefined _ = false; |
921 in |
921 in |
922 sel_condss ~~ (sel_lhss ~~ sel_rhss) |
922 sel_condss ~~ (sel_lhss ~~ sel_rhss) |
923 |> filter_out (is_undefined o snd o snd) |
923 |> filter_out (is_undefined o snd o snd) |
924 |> map (apsnd HOLogic.mk_eq) |
924 |> map (apsnd HOLogic.mk_eq) |
999 val parametric_consts = Unsynchronized.ref []; |
999 val parametric_consts = Unsynchronized.ref []; |
1000 |
1000 |
1001 (* We are assuming that set functions are marked with "[transfer_rule]" (cf. the "transfer" |
1001 (* We are assuming that set functions are marked with "[transfer_rule]" (cf. the "transfer" |
1002 plugin). Otherwise, the "eq_algrho" tactic might fail. *) |
1002 plugin). Otherwise, the "eq_algrho" tactic might fail. *) |
1003 fun is_special_parametric_const (x as (s, _)) = |
1003 fun is_special_parametric_const (x as (s, _)) = |
1004 s = @{const_name id} orelse is_set lthy x; |
1004 s = \<^const_name>\<open>id\<close> orelse is_set lthy x; |
1005 |
1005 |
1006 fun add_parametric_const s general_T T U = |
1006 fun add_parametric_const s general_T T U = |
1007 let |
1007 let |
1008 fun tupleT_of_funT T = |
1008 fun tupleT_of_funT T = |
1009 let val (Ts, T) = strip_type T in |
1009 let val (Ts, T) = strip_type T in |
1101 U :: [] => U |
1101 U :: [] => U |
1102 | _ => fpT_to ssig_T default_T); |
1102 | _ => fpT_to ssig_T default_T); |
1103 |
1103 |
1104 fun massage_if explore_cond explore (params as {bound_Us, bound_Ts, ...}) t = |
1104 fun massage_if explore_cond explore (params as {bound_Us, bound_Ts, ...}) t = |
1105 (case strip_comb t of |
1105 (case strip_comb t of |
1106 (const as Const (@{const_name If}, _), obj :: (branches as [_, _])) => |
1106 (const as Const (\<^const_name>\<open>If\<close>, _), obj :: (branches as [_, _])) => |
1107 (case List.partition Term.is_dummy_pattern (map (explore params) branches) of |
1107 (case List.partition Term.is_dummy_pattern (map (explore params) branches) of |
1108 (dummy_branch' :: _, []) => dummy_branch' |
1108 (dummy_branch' :: _, []) => dummy_branch' |
1109 | (_, [branch']) => branch' |
1109 | (_, [branch']) => branch' |
1110 | (_, branches') => |
1110 | (_, branches') => |
1111 let |
1111 let |
1112 val brancheUs = map (curry fastype_of1 bound_Us) branches'; |
1112 val brancheUs = map (curry fastype_of1 bound_Us) branches'; |
1113 val U = deduce_according_type (fastype_of1 (bound_Ts, hd branches)) brancheUs; |
1113 val U = deduce_according_type (fastype_of1 (bound_Ts, hd branches)) brancheUs; |
1114 val const_obj' = (If_const U, obj) |
1114 val const_obj' = (If_const U, obj) |
1115 ||> explore_cond (update_UT params @{typ bool} @{typ bool}) |
1115 ||> explore_cond (update_UT params \<^typ>\<open>bool\<close> \<^typ>\<open>bool\<close>) |
1116 |> op $; |
1116 |> op $; |
1117 in |
1117 in |
1118 build_function_after_encapsulation (const $ obj) const_obj' params branches branches' |
1118 build_function_after_encapsulation (const $ obj) const_obj' params branches branches' |
1119 end) |
1119 end) |
1120 | _ => explore params t); |
1120 | _ => explore params t); |
1164 | NONE => explore params t) |
1164 | NONE => explore params t) |
1165 | massage_map explore params t = explore params t; |
1165 | massage_map explore params t = explore params t; |
1166 |
1166 |
1167 fun massage_comp explore (params as {bound_Us, ...}) t = |
1167 fun massage_comp explore (params as {bound_Us, ...}) t = |
1168 (case strip_comb t of |
1168 (case strip_comb t of |
1169 (Const (@{const_name comp}, _), f1 :: f2 :: args) => |
1169 (Const (\<^const_name>\<open>comp\<close>, _), f1 :: f2 :: args) => |
1170 let |
1170 let |
1171 val args' = map (typ_before explore params) args; |
1171 val args' = map (typ_before explore params) args; |
1172 val f2' = typ_before (explore_fun (map (curry fastype_of1 bound_Us) args') explore) params |
1172 val f2' = typ_before (explore_fun (map (curry fastype_of1 bound_Us) args') explore) params |
1173 f2; |
1173 f2; |
1174 val f1' = typ_before (explore_fun [range_type (fastype_of1 (bound_Us, f2'))] explore) |
1174 val f1' = typ_before (explore_fun [range_type (fastype_of1 (bound_Us, f2'))] explore) |
1204 | const_of ((sel as Const (s1, _)) :: r) (const as Const (s2, _)) = |
1204 | const_of ((sel as Const (s1, _)) :: r) (const as Const (s2, _)) = |
1205 if s1 = s2 then SOME sel else const_of r const |
1205 if s1 = s2 then SOME sel else const_of r const |
1206 | const_of _ _ = NONE; |
1206 | const_of _ _ = NONE; |
1207 |
1207 |
1208 fun massage_disc explore (params as {T, bound_Us, bound_Ts, ...}) t = |
1208 fun massage_disc explore (params as {T, bound_Us, bound_Ts, ...}) t = |
1209 (case (strip_comb t, T = @{typ bool}) of |
1209 (case (strip_comb t, T = \<^typ>\<open>bool\<close>) of |
1210 ((fun_t, arg :: []), true) => |
1210 ((fun_t, arg :: []), true) => |
1211 let val arg_T = fastype_of1 (bound_Ts, arg) in |
1211 let val arg_T = fastype_of1 (bound_Ts, arg) in |
1212 if arg_T <> res_T then |
1212 if arg_T <> res_T then |
1213 (case arg_T |> try (fst o dest_Type) |> Option.mapPartial (ctr_sugar_of lthy) of |
1213 (case arg_T |> try (fst o dest_Type) |> Option.mapPartial (ctr_sugar_of lthy) of |
1214 SOME {discs, T = Type (_, Ts), ...} => |
1214 SOME {discs, T = Type (_, Ts), ...} => |
1249 | _ => explore params t) |
1249 | _ => explore params t) |
1250 end |
1250 end |
1251 end; |
1251 end; |
1252 |
1252 |
1253 fun massage_equality explore (params as {bound_Us, bound_Ts, ...}) |
1253 fun massage_equality explore (params as {bound_Us, bound_Ts, ...}) |
1254 (t as Const (@{const_name HOL.eq}, _) $ t1 $ t2) = |
1254 (t as Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) = |
1255 let |
1255 let |
1256 val check_is_VLeaf = |
1256 val check_is_VLeaf = |
1257 not o (Term.exists_subterm (fn t => t aconv CLeaf orelse t aconv Oper)); |
1257 not o (Term.exists_subterm (fn t => t aconv CLeaf orelse t aconv Oper)); |
1258 |
1258 |
1259 fun try_pattern_matching (fun_t, arg_ts) t = |
1259 fun try_pattern_matching (fun_t, arg_ts) t = |
1679 massage_nested_corec_call ctxt has_self_call explore' explore' bound_Ts U T t |
1679 massage_nested_corec_call ctxt has_self_call explore' explore' bound_Ts U T t |
1680 end; |
1680 end; |
1681 |
1681 |
1682 fun massage_comp explore params t = |
1682 fun massage_comp explore params t = |
1683 (case strip_comb t of |
1683 (case strip_comb t of |
1684 (Const (@{const_name comp}, _), f1 :: f2 :: args) => |
1684 (Const (\<^const_name>\<open>comp\<close>, _), f1 :: f2 :: args) => |
1685 explore params (betapply (f1, (betapplys (f2, args)))) |
1685 explore params (betapply (f1, (betapplys (f2, args)))) |
1686 | _ => explore params t); |
1686 | _ => explore params t); |
1687 |
1687 |
1688 fun massage_fun explore (params as {bound_Us, bound_Ts, U, T}) t = |
1688 fun massage_fun explore (params as {bound_Us, bound_Ts, U, T}) t = |
1689 if can dest_funT T then |
1689 if can dest_funT T then |
2188 val ((def_fun, (_, (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals))), |
2188 val ((def_fun, (_, (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals))), |
2189 lthy) = |
2189 lthy) = |
2190 prepare_corec_ursive_cmd int false opts (raw_fixes, raw_eq) lthy; |
2190 prepare_corec_ursive_cmd int false opts (raw_fixes, raw_eq) lthy; |
2191 in |
2191 in |
2192 if not (null termin_goals) then |
2192 if not (null termin_goals) then |
2193 error ("Termination prover failed (try " ^ quote (#1 @{command_keyword corecursive}) ^ |
2193 error ("Termination prover failed (try " ^ quote (#1 \<^command_keyword>\<open>corecursive\<close>) ^ |
2194 " instead of " ^ quote (#1 @{command_keyword corec}) ^ ")") |
2194 " instead of " ^ quote (#1 \<^command_keyword>\<open>corec\<close>) ^ ")") |
2195 else if not (null const_transfer_goals) then |
2195 else if not (null const_transfer_goals) then |
2196 error ("Transfer prover failed (try " ^ quote (#1 @{command_keyword corecursive}) ^ |
2196 error ("Transfer prover failed (try " ^ quote (#1 \<^command_keyword>\<open>corecursive\<close>) ^ |
2197 " instead of " ^ quote (#1 @{command_keyword corec}) ^ ")") |
2197 " instead of " ^ quote (#1 \<^command_keyword>\<open>corec\<close>) ^ ")") |
2198 else |
2198 else |
2199 def_fun inner_fp_triple const_transfers [] lthy |
2199 def_fun inner_fp_triple const_transfers [] lthy |
2200 end; |
2200 end; |
2201 |
2201 |
2202 fun corecursive_cmd int opts (raw_fixes, raw_eq) lthy = |
2202 fun corecursive_cmd int opts (raw_fixes, raw_eq) lthy = |
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 HOL.eq}, _) $ t $ _) => fastype_of (head_of t) |
2244 @{const Trueprop} $ (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 |
2363 |
2363 |
2364 fun consolidate_global thy = |
2364 fun consolidate_global thy = |
2365 SOME (Named_Target.theory_map consolidate thy) |
2365 SOME (Named_Target.theory_map consolidate thy) |
2366 handle Same.SAME => NONE; |
2366 handle Same.SAME => NONE; |
2367 |
2367 |
2368 val _ = Outer_Syntax.local_theory @{command_keyword corec} |
2368 val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>corec\<close> |
2369 "define nonprimitive corecursive functions" |
2369 "define nonprimitive corecursive functions" |
2370 ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser) |
2370 ((Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.list1 corec_option_parser) |
2371 --| @{keyword ")"}) []) -- (Parse.vars --| Parse.where_ -- Parse.prop) |
2371 --| \<^keyword>\<open>)\<close>) []) -- (Parse.vars --| Parse.where_ -- Parse.prop) |
2372 >> uncurry (corec_cmd true)); |
2372 >> uncurry (corec_cmd true)); |
2373 |
2373 |
2374 val _ = Outer_Syntax.local_theory_to_proof @{command_keyword corecursive} |
2374 val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>corecursive\<close> |
2375 "define nonprimitive corecursive functions" |
2375 "define nonprimitive corecursive functions" |
2376 ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser) |
2376 ((Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.list1 corec_option_parser) |
2377 --| @{keyword ")"}) []) -- (Parse.vars --| Parse.where_ -- Parse.prop) |
2377 --| \<^keyword>\<open>)\<close>) []) -- (Parse.vars --| Parse.where_ -- Parse.prop) |
2378 >> uncurry (corecursive_cmd true)); |
2378 >> uncurry (corecursive_cmd true)); |
2379 |
2379 |
2380 val _ = Outer_Syntax.local_theory_to_proof @{command_keyword friend_of_corec} |
2380 val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>friend_of_corec\<close> |
2381 "register a function as a legal context for nonprimitive corecursion" |
2381 "register a function as a legal context for nonprimitive corecursion" |
2382 (Parse.const -- Scan.option (Parse.$$$ "::" |-- Parse.typ) --| Parse.where_ -- Parse.prop |
2382 (Parse.const -- Scan.option (Parse.$$$ "::" |-- Parse.typ) --| Parse.where_ -- Parse.prop |
2383 >> friend_of_corec_cmd); |
2383 >> friend_of_corec_cmd); |
2384 |
2384 |
2385 val _ = Outer_Syntax.local_theory @{command_keyword coinduction_upto} |
2385 val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>coinduction_upto\<close> |
2386 "derive a coinduction up-to principle and a corresponding congruence closure" |
2386 "derive a coinduction up-to principle and a corresponding congruence closure" |
2387 (Parse.name --| Parse.$$$ ":" -- Parse.typ >> coinduction_upto_cmd); |
2387 (Parse.name --| Parse.$$$ ":" -- Parse.typ >> coinduction_upto_cmd); |
2388 |
2388 |
2389 val _ = Theory.setup (Theory.at_begin consolidate_global); |
2389 val _ = Theory.setup (Theory.at_begin consolidate_global); |
2390 |
2390 |