# HG changeset patch
# User wenzelm
# Date 1335212577 -7200
# Node ID 3eef88e8496b159a20cf333f1728e29a0f6f26f9
# Parent  918e98008d6e0133b61469a53ca2136936d4c291# Parent  5f9ce06f281e1496730c795eca7ef050787c4be2
merged

diff -r 918e98008d6e -r 3eef88e8496b NEWS
--- a/NEWS	Mon Apr 23 21:46:52 2012 +0200
+++ b/NEWS	Mon Apr 23 22:22:57 2012 +0200
@@ -187,6 +187,10 @@
 
 * New type synonym 'a rel = ('a * 'a) set
 
+* Typedef with implicit set definition is considered legacy.  Use
+"typedef (open)" form instead, which will eventually become the
+default.
+
 * More default pred/set conversions on a couple of relation operations
 and predicates.  Added powers of predicate relations.  Consolidation
 of some relation theorems:
diff -r 918e98008d6e -r 3eef88e8496b src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Mon Apr 23 21:46:52 2012 +0200
+++ b/src/HOL/Algebra/Ring.thy	Mon Apr 23 22:22:57 2012 +0200
@@ -391,7 +391,11 @@
 
 use "ringsimp.ML"
 
-setup Algebra.setup
+setup Algebra.attrib_setup
+
+method_setup algebra = {*
+  Scan.succeed (SIMPLE_METHOD' o Algebra.algebra_tac)
+*} "normalisation of algebraic structure"
 
 lemmas (in ring) ring_simprules
   [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
diff -r 918e98008d6e -r 3eef88e8496b src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Mon Apr 23 21:46:52 2012 +0200
+++ b/src/HOL/Algebra/ringsimp.ML	Mon Apr 23 22:22:57 2012 +0200
@@ -6,7 +6,8 @@
 signature ALGEBRA =
 sig
   val print_structures: Proof.context -> unit
-  val setup: theory -> theory
+  val attrib_setup: theory -> theory
+  val algebra_tac: Proof.context -> int -> tactic
 end;
 
 structure Algebra: ALGEBRA =
@@ -58,6 +59,7 @@
 fun add_struct_thm s =
   Thm.declaration_attribute
     (fn thm => Data.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
+
 fun del_struct s =
   Thm.declaration_attribute
     (fn _ => Data.map (AList.delete struct_eq s));
@@ -69,13 +71,4 @@
       >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)))
     "theorems controlling algebra method";
 
-
-
-(** Setup **)
-
-val setup =
-  Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
-    "normalisation of algebraic structure" #>
-  attrib_setup;
-
 end;
diff -r 918e98008d6e -r 3eef88e8496b src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Mon Apr 23 21:46:52 2012 +0200
+++ b/src/HOL/FunDef.thy	Mon Apr 23 22:22:57 2012 +0200
@@ -108,6 +108,11 @@
 use "Tools/Function/mutual.ML"
 use "Tools/Function/pattern_split.ML"
 use "Tools/Function/relation.ML"
+
+method_setup relation = {*
+  Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
+*} "prove termination using a user-specified wellfounded relation"
+
 use "Tools/Function/function.ML"
 use "Tools/Function/pat_completeness.ML"
 
@@ -122,7 +127,7 @@
   Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
 *} "prove an induction principle"
 
-setup {* 
+setup {*
   Function.setup
   #> Function_Fun.setup
 *}
@@ -150,7 +155,7 @@
   (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
 *} "termination prover for lexicographic orderings"
 
-setup Lexicographic_Order.setup 
+setup Lexicographic_Order.setup
 
 
 subsection {* Congruence Rules *}
@@ -175,7 +180,7 @@
 subsection {* Simp rules for termination proofs *}
 
 lemma termination_basic_simps[termination_simp]:
-  "x < (y::nat) \<Longrightarrow> x < y + z" 
+  "x < (y::nat) \<Longrightarrow> x < y + z"
   "x < z \<Longrightarrow> x < y + z"
   "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
   "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
@@ -190,13 +195,13 @@
 
 subsection {* Decomposition *}
 
-lemma less_by_empty: 
+lemma less_by_empty:
   "A = {} \<Longrightarrow> A \<subseteq> B"
 and  union_comp_emptyL:
   "\<lbrakk> A O C = {}; B O C = {} \<rbrakk> \<Longrightarrow> (A \<union> B) O C = {}"
 and union_comp_emptyR:
   "\<lbrakk> A O B = {}; A O C = {} \<rbrakk> \<Longrightarrow> A O (B \<union> C) = {}"
-and wf_no_loop: 
+and wf_no_loop:
   "R O R = {} \<Longrightarrow> wf R"
 by (auto simp add: wf_comp_self[of R])
 
@@ -218,10 +223,10 @@
 proof -
   from rp `S \<subseteq> snd P` have "wf (fst P)" "fst P O S \<subseteq> fst P"
     unfolding reduction_pair_def by auto
-  with `wf S` have "wf (fst P \<union> S)" 
+  with `wf S` have "wf (fst P \<union> S)"
     by (auto intro: wf_union_compatible)
   moreover from `R \<subseteq> fst P` have "R \<union> S \<subseteq> fst P \<union> S" by auto
-  ultimately show ?thesis by (rule wf_subset) 
+  ultimately show ?thesis by (rule wf_subset)
 qed
 
 definition
@@ -253,33 +258,33 @@
   unfolding pair_leq_def pair_less_def by auto
 
 text {* Introduction rules for max *}
-lemma smax_emptyI: 
-  "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict" 
-  and smax_insertI: 
+lemma smax_emptyI:
+  "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict"
+  and smax_insertI:
   "\<lbrakk>y \<in> Y; (x, y) \<in> pair_less; (X, Y) \<in> max_strict\<rbrakk> \<Longrightarrow> (insert x X, Y) \<in> max_strict"
-  and wmax_emptyI: 
-  "finite X \<Longrightarrow> ({}, X) \<in> max_weak" 
+  and wmax_emptyI:
+  "finite X \<Longrightarrow> ({}, X) \<in> max_weak"
   and wmax_insertI:
-  "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak" 
+  "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak"
 unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases)
 
 text {* Introduction rules for min *}
-lemma smin_emptyI: 
-  "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict" 
-  and smin_insertI: 
+lemma smin_emptyI:
+  "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict"
+  and smin_insertI:
   "\<lbrakk>x \<in> XS; (x, y) \<in> pair_less; (XS, YS) \<in> min_strict\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_strict"
-  and wmin_emptyI: 
-  "(X, {}) \<in> min_weak" 
-  and wmin_insertI: 
-  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak" 
+  and wmin_emptyI:
+  "(X, {}) \<in> min_weak"
+  and wmin_insertI:
+  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak"
 by (auto simp: min_strict_def min_weak_def min_ext_def)
 
 text {* Reduction Pairs *}
 
-lemma max_ext_compat: 
+lemma max_ext_compat:
   assumes "R O S \<subseteq> R"
   shows "max_ext R O (max_ext S \<union> {({},{})}) \<subseteq> max_ext R"
-using assms 
+using assms
 apply auto
 apply (elim max_ext.cases)
 apply rule
@@ -291,16 +296,16 @@
 by auto
 
 lemma max_rpair_set: "reduction_pair (max_strict, max_weak)"
-  unfolding max_strict_def max_weak_def 
+  unfolding max_strict_def max_weak_def
 apply (intro reduction_pairI max_ext_wf)
 apply simp
 apply (rule max_ext_compat)
 by (auto simp: pair_less_def pair_leq_def)
 
-lemma min_ext_compat: 
+lemma min_ext_compat:
   assumes "R O S \<subseteq> R"
   shows "min_ext R O  (min_ext S \<union> {({},{})}) \<subseteq> min_ext R"
-using assms 
+using assms
 apply (auto simp: min_ext_def)
 apply (drule_tac x=ya in bspec, assumption)
 apply (erule bexE)
@@ -309,7 +314,7 @@
 by auto
 
 lemma min_rpair_set: "reduction_pair (min_strict, min_weak)"
-  unfolding min_strict_def min_weak_def 
+  unfolding min_strict_def min_weak_def
 apply (intro reduction_pairI min_ext_wf)
 apply simp
 apply (rule min_ext_compat)
diff -r 918e98008d6e -r 3eef88e8496b src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Mon Apr 23 21:46:52 2012 +0200
+++ b/src/HOL/SMT.thy	Mon Apr 23 22:22:57 2012 +0200
@@ -153,13 +153,17 @@
 setup {*
   SMT_Config.setup #>
   SMT_Normalize.setup #>
-  SMT_Solver.setup #>
   SMTLIB_Interface.setup #>
   Z3_Interface.setup #>
   Z3_Proof_Reconstruction.setup #>
   SMT_Setup_Solvers.setup
 *}
 
+method_setup smt = {*
+  Scan.optional Attrib.thms [] >>
+    (fn thms => fn ctxt =>
+      METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts))))
+*} "apply an SMT solver to the current goal"
 
 
 subsection {* Configuration *}
diff -r 918e98008d6e -r 3eef88e8496b src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Mon Apr 23 21:46:52 2012 +0200
+++ b/src/HOL/Tools/Function/function.ML	Mon Apr 23 22:22:57 2012 +0200
@@ -265,7 +265,6 @@
     (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
     "declaration of congruence rule for function definitions"
   #> setup_case_cong
-  #> Function_Relation.setup
   #> Function_Common.Termination_Simps.setup
 
 val get_congs = Function_Ctx_Tree.get_function_congs
diff -r 918e98008d6e -r 3eef88e8496b src/HOL/Tools/Function/relation.ML
--- a/src/HOL/Tools/Function/relation.ML	Mon Apr 23 21:46:52 2012 +0200
+++ b/src/HOL/Tools/Function/relation.ML	Mon Apr 23 22:22:57 2012 +0200
@@ -1,13 +1,13 @@
 (*  Title:      HOL/Tools/Function/relation.ML
     Author:     Alexander Krauss, TU Muenchen
 
-Method "relation" to start a termination proof using a user-specified relation.
+Tactics to start a termination proof using a user-specified relation.
 *)
 
 signature FUNCTION_RELATION =
 sig
   val relation_tac: Proof.context -> (typ -> term) -> int -> tactic
-  val setup: theory -> theory
+  val relation_infer_tac: Proof.context -> term -> int -> tactic
 end
 
 structure Function_Relation : FUNCTION_RELATION =
@@ -27,7 +27,7 @@
   THEN inst_state_tac rel;
 
 
-(* method version (with type inference) *)
+(* version with type inference *)
 
 fun inst_state_infer_tac ctxt rel st =
   case Term.add_vars (prop_of st) [] of
@@ -44,12 +44,8 @@
       end
   | _ => Seq.empty;
 
-fun relation_meth rel ctxt = SIMPLE_METHOD' (fn i =>
+fun relation_infer_tac ctxt rel i =
   TRY (Function_Common.apply_termination_rule ctxt i)
-  THEN inst_state_infer_tac ctxt rel);
-
-val setup =
-  Method.setup @{binding relation} (Args.term >> relation_meth)
-    "proves termination using a user-specified wellfounded relation";
+  THEN inst_state_infer_tac ctxt rel;
 
 end
diff -r 918e98008d6e -r 3eef88e8496b src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Mon Apr 23 21:46:52 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Apr 23 22:22:57 2012 +0200
@@ -41,9 +41,6 @@
   (*tactic*)
   val smt_tac: Proof.context -> thm list -> int -> tactic
   val smt_tac': Proof.context -> thm list -> int -> tactic
-
-  (*setup*)
-  val setup: theory -> theory
 end
 
 structure SMT_Solver: SMT_SOLVER =
@@ -373,17 +370,4 @@
 
 end
 
-
-val smt_method =
-  Scan.optional Attrib.thms [] >>
-  (fn thms => fn ctxt => METHOD (fn facts =>
-    HEADGOAL (smt_tac ctxt (thms @ facts))))
-
-
-(* setup *)
-
-val setup =
-  Method.setup @{binding smt} smt_method
-    "Applies an SMT solver to the current goal."
-
 end
diff -r 918e98008d6e -r 3eef88e8496b src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Mon Apr 23 21:46:52 2012 +0200
+++ b/src/HOL/Tools/typedef.ML	Mon Apr 23 22:22:57 2012 +0200
@@ -308,8 +308,11 @@
       (Parse.type_args_constrained -- Parse.binding) --
         Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
         Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
-    >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) =>
-        typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)));
+    >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) => fn lthy =>
+          (if def then
+            legacy_feature "typedef with implicit set definition -- use \"typedef (open)\" instead"
+           else ();
+           typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs) lthy)));
 
 end;