# HG changeset patch # User wenzelm # Date 1428354845 -7200 # Node ID 087d81f5213ea0664e519b2e4f87b39547478d9b # Parent 7d46aa03696e6b8ad8aec0acc08f24da743fa920 local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts; diff -r 7d46aa03696e -r 087d81f5213e src/FOL/FOL.thy --- a/src/FOL/FOL.thy Mon Apr 06 22:11:01 2015 +0200 +++ b/src/FOL/FOL.thy Mon Apr 06 23:14:05 2015 +0200 @@ -384,10 +384,13 @@ text {* Proper handling of non-atomic rule statements. *} -definition "induct_forall(P) == \x. P(x)" -definition "induct_implies(A, B) == A \ B" -definition "induct_equal(x, y) == x = y" -definition "induct_conj(A, B) == A \ B" +context +begin + +restricted definition "induct_forall(P) == \x. P(x)" +restricted definition "induct_implies(A, B) == A \ B" +restricted definition "induct_equal(x, y) == x = y" +restricted definition "induct_conj(A, B) == A \ B" lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\x. P(x)))" unfolding atomize_all induct_forall_def . @@ -406,9 +409,6 @@ lemmas induct_rulify_fallback = induct_forall_def induct_implies_def induct_equal_def induct_conj_def -hide_const induct_forall induct_implies induct_equal induct_conj - - text {* Method setup. *} ML_file "~~/src/Tools/induct.ML" @@ -427,6 +427,8 @@ declare case_split [cases type: o] +end + ML_file "~~/src/Tools/case_product.ML" diff -r 7d46aa03696e -r 087d81f5213e src/HOL/Extraction.thy --- a/src/HOL/Extraction.thy Mon Apr 06 22:11:01 2015 +0200 +++ b/src/HOL/Extraction.thy Mon Apr 06 23:14:05 2015 +0200 @@ -34,8 +34,8 @@ True_implies_equals TrueE lemmas [extraction_expand_def] = - induct_forall_def induct_implies_def induct_equal_def induct_conj_def - induct_true_def induct_false_def + HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def + HOL.induct_true_def HOL.induct_false_def datatype (plugins only: code extraction) sumbool = Left | Right diff -r 7d46aa03696e -r 087d81f5213e src/HOL/HOL.thy --- a/src/HOL/HOL.thy Mon Apr 06 22:11:01 2015 +0200 +++ b/src/HOL/HOL.thy Mon Apr 06 23:14:05 2015 +0200 @@ -1374,12 +1374,15 @@ ); *} -definition "induct_forall P \ \x. P x" -definition "induct_implies A B \ A \ B" -definition "induct_equal x y \ x = y" -definition "induct_conj A B \ A \ B" -definition "induct_true \ True" -definition "induct_false \ False" +context +begin + +restricted definition "induct_forall P \ \x. P x" +restricted definition "induct_implies A B \ A \ B" +restricted definition "induct_equal x y \ x = y" +restricted definition "induct_conj A B \ A \ B" +restricted definition "induct_true \ True" +restricted definition "induct_false \ False" lemma induct_forall_eq: "(\x. P x) \ Trueprop (induct_forall (\x. P x))" by (unfold atomize_all induct_forall_def) @@ -1444,8 +1447,8 @@ ML_file "~~/src/Tools/induction.ML" -setup {* - Context.theory_map (Induct.map_simpset (fn ss => ss +declaration {* + fn _ => Induct.map_simpset (fn ss => ss addsimprocs [Simplifier.simproc_global @{theory} "swap_induct_false" ["induct_false ==> PROP P ==> PROP Q"] @@ -1468,7 +1471,7 @@ | _ => NONE))] |> Simplifier.set_mksimps (fn ctxt => Simpdata.mksimps Simpdata.mksimps_pairs ctxt #> - map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))) + map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))) *} text {* Pre-simplification of induction and cases rules *} @@ -1523,7 +1526,7 @@ lemma [induct_simp]: "x = x \ True" by (rule simp_thms) -hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false +end ML_file "~~/src/Tools/induct_tacs.ML" diff -r 7d46aa03696e -r 087d81f5213e src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Apr 06 22:11:01 2015 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Apr 06 23:14:05 2015 +0200 @@ -247,10 +247,10 @@ end val forbidden_mutant_constnames = - ["HOL.induct_equal", - "HOL.induct_implies", - "HOL.induct_conj", - "HOL.induct_forall", +[@{const_name HOL.induct_equal}, + @{const_name HOL.induct_implies}, + @{const_name HOL.induct_conj}, + @{const_name HOL.induct_forall}, @{const_name undefined}, @{const_name default}, @{const_name Pure.dummy_pattern}, diff -r 7d46aa03696e -r 087d81f5213e src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Mon Apr 06 22:11:01 2015 +0200 +++ b/src/HOL/Nominal/Nominal.thy Mon Apr 06 23:14:05 2015 +0200 @@ -3563,7 +3563,7 @@ (* connectives *) if_eqvt imp_eqvt disj_eqvt conj_eqvt neg_eqvt true_eqvt false_eqvt - imp_eqvt [folded induct_implies_def] + imp_eqvt [folded HOL.induct_implies_def] (* datatypes *) perm_unit.simps diff -r 7d46aa03696e -r 087d81f5213e src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Mon Apr 06 22:11:01 2015 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Mon Apr 06 23:14:05 2015 +0200 @@ -28,7 +28,7 @@ val finite_emptyI = @{thm "finite.emptyI"}; val Collect_const = @{thm "Collect_const"}; -val inductive_forall_def = @{thm "induct_forall_def"}; +val inductive_forall_def = @{thm HOL.induct_forall_def}; (* theory data *) diff -r 7d46aa03696e -r 087d81f5213e src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Mon Apr 06 22:11:01 2015 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Mon Apr 06 23:14:05 2015 +0200 @@ -14,7 +14,7 @@ structure NominalInductive : NOMINAL_INDUCTIVE = struct -val inductive_forall_def = @{thm induct_forall_def}; +val inductive_forall_def = @{thm HOL.induct_forall_def}; val inductive_atomize = @{thms induct_atomize}; val inductive_rulify = @{thms induct_rulify}; diff -r 7d46aa03696e -r 087d81f5213e src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Mon Apr 06 22:11:01 2015 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Apr 06 23:14:05 2015 +0200 @@ -15,7 +15,7 @@ structure NominalInductive2 : NOMINAL_INDUCTIVE2 = struct -val inductive_forall_def = @{thm induct_forall_def}; +val inductive_forall_def = @{thm HOL.induct_forall_def}; val inductive_atomize = @{thms induct_atomize}; val inductive_rulify = @{thms induct_rulify}; diff -r 7d46aa03696e -r 087d81f5213e src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Mon Apr 06 22:11:01 2015 +0200 +++ b/src/HOL/Tools/inductive.ML Mon Apr 06 23:14:05 2015 +0200 @@ -97,9 +97,8 @@ (** theory context references **) -val inductive_forall_def = @{thm induct_forall_def}; -val inductive_conj_name = "HOL.induct_conj"; -val inductive_conj_def = @{thm induct_conj_def}; +val inductive_forall_def = @{thm HOL.induct_forall_def}; +val inductive_conj_def = @{thm HOL.induct_conj_def}; val inductive_conj = @{thms induct_conj}; val inductive_atomize = @{thms induct_atomize}; val inductive_rulify = @{thms induct_rulify}; @@ -689,7 +688,7 @@ val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs); val Q = fold_rev Term.abs (mk_names "x" k ~~ Ts) - (HOLogic.mk_binop inductive_conj_name + (HOLogic.mk_binop @{const_name HOL.induct_conj} (list_comb (incr_boundvars k s, bs), P)); in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end | NONE => diff -r 7d46aa03696e -r 087d81f5213e src/Tools/induct.ML --- a/src/Tools/induct.ML Mon Apr 06 22:11:01 2015 +0200 +++ b/src/Tools/induct.ML Mon Apr 06 23:14:05 2015 +0200 @@ -88,7 +88,7 @@ (Proof.context -> bool -> (binding option * (term * bool)) option list list -> (string * typ) list list -> term option list -> thm list option -> thm list -> int -> cases_tactic) -> - theory -> theory + local_theory -> local_theory end; functor Induct(Induct_Args: INDUCT_ARGS): INDUCT = @@ -363,14 +363,14 @@ in val _ = - Theory.setup - (Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del) + Theory.local_setup + (Attrib.local_setup @{binding cases} (attrib cases_type cases_pred cases_del) "declaration of cases rule" #> - Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del) + Attrib.local_setup @{binding induct} (attrib induct_type induct_pred induct_del) "declaration of induction rule" #> - Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del) + Attrib.local_setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del) "declaration of coinduction rule" #> - Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del) + Attrib.local_setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del) "declaration of rules for simplifying induction or cases rules"); end; @@ -737,10 +737,10 @@ SUBGOAL_CASES (fn (_, i, st) => let val thy = Proof_Context.theory_of ctxt; - + val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list; val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs; - + fun inst_rule (concls, r) = (if null insts then `Rule_Cases.get r else (align_left "Rule has fewer conclusions than arguments given" @@ -749,7 +749,7 @@ |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r)) |> mod_cases thy |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th)); - + val ruleq = (case opt_rule of SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs)) @@ -759,7 +759,7 @@ |> map_filter (Rule_Cases.mutual_rule ctxt) |> tap (trace_rules ctxt inductN o map #2) |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); - + fun rule_cases ctxt rule cases = let val rule' = Rule_Cases.internalize_params rule; @@ -910,18 +910,8 @@ in -val _ = - Theory.setup - (Method.setup @{binding cases} - (Scan.lift (Args.mode no_simpN) -- - (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >> - (fn (no_simp, (insts, opt_rule)) => fn ctxt => - METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL - (cases_tac ctxt (not no_simp) insts opt_rule facts))))) - "case analysis on types or predicates/sets"); - fun gen_induct_setup binding tac = - Method.setup binding + Method.local_setup binding (Scan.lift (Args.mode no_simpN) -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) -- (arbitrary -- taking -- Scan.option induct_rule)) >> @@ -929,11 +919,17 @@ Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))) "induction on types or predicates/sets"; -val _ = Theory.setup (gen_induct_setup @{binding induct} induct_tac); - val _ = - Theory.setup - (Method.setup @{binding coinduct} + Theory.local_setup + (Method.local_setup @{binding cases} + (Scan.lift (Args.mode no_simpN) -- + (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >> + (fn (no_simp, (insts, opt_rule)) => fn ctxt => + METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL + (cases_tac ctxt (not no_simp) insts opt_rule facts))))) + "case analysis on types or predicates/sets" #> + gen_induct_setup @{binding induct} induct_tac #> + Method.local_setup @{binding coinduct} (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >> (fn ((insts, taking), opt_rule) => fn ctxt => fn facts => Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts)))) diff -r 7d46aa03696e -r 087d81f5213e src/Tools/induction.ML --- a/src/Tools/induction.ML Mon Apr 06 22:11:01 2015 +0200 +++ b/src/Tools/induction.ML Mon Apr 06 23:14:05 2015 +0200 @@ -45,6 +45,6 @@ val induction_tac = Induct.gen_induct_tac (K name_hyps); -val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac); +val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac); end