69 end; |
69 end; |
70 |
70 |
71 signature INDUCTIVE = |
71 signature INDUCTIVE = |
72 sig |
72 sig |
73 include BASIC_INDUCTIVE |
73 include BASIC_INDUCTIVE |
74 val inductive_defs: bool Config.T |
74 val inductive_internals: bool Config.T |
75 val select_disj_tac: Proof.context -> int -> int -> int -> tactic |
75 val select_disj_tac: Proof.context -> int -> int -> int -> tactic |
76 type add_ind_def = |
76 type add_ind_def = |
77 inductive_flags -> |
77 inductive_flags -> |
78 term list -> (Attrib.binding * term) list -> thm list -> |
78 term list -> (Attrib.binding * term) list -> thm list -> |
79 term list -> (binding * mixfix) list -> |
79 term list -> (binding * mixfix) list -> |
120 |
120 |
121 |
121 |
122 |
122 |
123 (** misc utilities **) |
123 (** misc utilities **) |
124 |
124 |
125 val inductive_defs = Attrib.setup_config_bool @{binding inductive_defs} (K false); |
125 val inductive_internals = Attrib.setup_config_bool @{binding inductive_internals} (K false); |
126 |
126 |
127 fun message quiet_mode s = if quiet_mode then () else writeln s; |
127 fun message quiet_mode s = if quiet_mode then () else writeln s; |
128 |
128 |
129 fun clean_message ctxt quiet_mode s = |
129 fun clean_message ctxt quiet_mode s = |
130 if Config.get ctxt quick_and_dirty then () else message quiet_mode s; |
130 if Config.get ctxt quick_and_dirty then () else message quiet_mode s; |
847 [(b, _)] => b |
847 [(b, _)] => b |
848 | _ => Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))) |
848 | _ => Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))) |
849 else alt_name; |
849 else alt_name; |
850 val rec_name = Binding.name_of rec_binding; |
850 val rec_name = Binding.name_of rec_binding; |
851 |
851 |
852 val inductive_defs = Config.get lthy inductive_defs; |
852 val internals = Config.get lthy inductive_internals; |
853 fun cond_def_binding b = |
|
854 if inductive_defs then Binding.reset_pos (Thm.def_binding b) |
|
855 else Binding.empty; |
|
856 |
853 |
857 val ((rec_const, (_, fp_def)), lthy') = lthy |
854 val ((rec_const, (_, fp_def)), lthy') = lthy |
858 |> is_auxiliary ? Proof_Context.concealed |
855 |> is_auxiliary ? Proof_Context.concealed |
859 |> Local_Theory.define |
856 |> Local_Theory.define |
860 ((rec_binding, case cnames_syn of [(_, mx)] => mx | _ => NoSyn), |
857 ((rec_binding, case cnames_syn of [(_, mx)] => mx | _ => NoSyn), |
861 ((cond_def_binding rec_binding, @{attributes [nitpick_unfold]}), |
858 ((Thm.make_def_binding internals rec_binding, @{attributes [nitpick_unfold]}), |
862 fold_rev lambda params |
859 fold_rev lambda params |
863 (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) |
860 (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) |
864 ||> Proof_Context.restore_naming lthy; |
861 ||> Proof_Context.restore_naming lthy; |
865 val fp_def' = |
862 val fp_def' = |
866 Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def]) |
863 Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def]) |
872 val Ts = arg_types_of (length params) c; |
869 val Ts = arg_types_of (length params) c; |
873 val xs = |
870 val xs = |
874 map Free (Variable.variant_frees lthy' intr_ts (mk_names "x" (length Ts) ~~ Ts)); |
871 map Free (Variable.variant_frees lthy' intr_ts (mk_names "x" (length Ts) ~~ Ts)); |
875 in |
872 in |
876 ((b, mx), |
873 ((b, mx), |
877 ((cond_def_binding b, []), fold_rev lambda (params @ xs) |
874 ((Thm.make_def_binding internals b, []), fold_rev lambda (params @ xs) |
878 (list_comb (rec_const, params @ make_bool_args' bs i @ |
875 (list_comb (rec_const, params @ make_bool_args' bs i @ |
879 make_args argTs (xs ~~ Ts))))) |
876 make_args argTs (xs ~~ Ts))))) |
880 end) (cnames_syn ~~ cs) |
877 end) (cnames_syn ~~ cs) |
881 else []; |
878 else []; |
882 val (consts_defs, lthy'') = lthy' |
879 val (consts_defs, lthy'') = lthy' |
885 |
882 |
886 val (_, ctxt'') = Variable.add_fixes (map (fst o dest_Free) params) lthy''; |
883 val (_, ctxt'') = Variable.add_fixes (map (fst o dest_Free) params) lthy''; |
887 val mono = prove_mono quiet_mode skip_mono predT fp_fun monos ctxt''; |
884 val mono = prove_mono quiet_mode skip_mono predT fp_fun monos ctxt''; |
888 val (_, lthy''') = lthy'' |
885 val (_, lthy''') = lthy'' |
889 |> Local_Theory.note |
886 |> Local_Theory.note |
890 ((if inductive_defs |
887 ((if internals |
891 then Binding.qualify true rec_name (Binding.name "mono") |
888 then Binding.qualify true rec_name (Binding.name "mono") |
892 else Binding.empty, []), |
889 else Binding.empty, []), |
893 Proof_Context.export ctxt'' lthy'' [mono]); |
890 Proof_Context.export ctxt'' lthy'' [mono]); |
894 in |
891 in |
895 (lthy''', Proof_Context.transfer (Proof_Context.theory_of lthy''') ctxt'', |
892 (lthy''', Proof_Context.transfer (Proof_Context.theory_of lthy''') ctxt'', |