1.1 --- a/NEWS Mon Apr 23 21:46:52 2012 +0200
1.2 +++ b/NEWS Mon Apr 23 22:22:57 2012 +0200
1.3 @@ -187,6 +187,10 @@
1.4
1.5 * New type synonym 'a rel = ('a * 'a) set
1.6
1.7 +* Typedef with implicit set definition is considered legacy. Use
1.8 +"typedef (open)" form instead, which will eventually become the
1.9 +default.
1.10 +
1.11 * More default pred/set conversions on a couple of relation operations
1.12 and predicates. Added powers of predicate relations. Consolidation
1.13 of some relation theorems:
2.1 --- a/src/HOL/Algebra/Ring.thy Mon Apr 23 21:46:52 2012 +0200
2.2 +++ b/src/HOL/Algebra/Ring.thy Mon Apr 23 22:22:57 2012 +0200
2.3 @@ -391,7 +391,11 @@
2.4
2.5 use "ringsimp.ML"
2.6
2.7 -setup Algebra.setup
2.8 +setup Algebra.attrib_setup
2.9 +
2.10 +method_setup algebra = {*
2.11 + Scan.succeed (SIMPLE_METHOD' o Algebra.algebra_tac)
2.12 +*} "normalisation of algebraic structure"
2.13
2.14 lemmas (in ring) ring_simprules
2.15 [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
3.1 --- a/src/HOL/Algebra/ringsimp.ML Mon Apr 23 21:46:52 2012 +0200
3.2 +++ b/src/HOL/Algebra/ringsimp.ML Mon Apr 23 22:22:57 2012 +0200
3.3 @@ -6,7 +6,8 @@
3.4 signature ALGEBRA =
3.5 sig
3.6 val print_structures: Proof.context -> unit
3.7 - val setup: theory -> theory
3.8 + val attrib_setup: theory -> theory
3.9 + val algebra_tac: Proof.context -> int -> tactic
3.10 end;
3.11
3.12 structure Algebra: ALGEBRA =
3.13 @@ -58,6 +59,7 @@
3.14 fun add_struct_thm s =
3.15 Thm.declaration_attribute
3.16 (fn thm => Data.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
3.17 +
3.18 fun del_struct s =
3.19 Thm.declaration_attribute
3.20 (fn _ => Data.map (AList.delete struct_eq s));
3.21 @@ -69,13 +71,4 @@
3.22 >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)))
3.23 "theorems controlling algebra method";
3.24
3.25 -
3.26 -
3.27 -(** Setup **)
3.28 -
3.29 -val setup =
3.30 - Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
3.31 - "normalisation of algebraic structure" #>
3.32 - attrib_setup;
3.33 -
3.34 end;
4.1 --- a/src/HOL/FunDef.thy Mon Apr 23 21:46:52 2012 +0200
4.2 +++ b/src/HOL/FunDef.thy Mon Apr 23 22:22:57 2012 +0200
4.3 @@ -108,6 +108,11 @@
4.4 use "Tools/Function/mutual.ML"
4.5 use "Tools/Function/pattern_split.ML"
4.6 use "Tools/Function/relation.ML"
4.7 +
4.8 +method_setup relation = {*
4.9 + Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
4.10 +*} "prove termination using a user-specified wellfounded relation"
4.11 +
4.12 use "Tools/Function/function.ML"
4.13 use "Tools/Function/pat_completeness.ML"
4.14
4.15 @@ -122,7 +127,7 @@
4.16 Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
4.17 *} "prove an induction principle"
4.18
4.19 -setup {*
4.20 +setup {*
4.21 Function.setup
4.22 #> Function_Fun.setup
4.23 *}
4.24 @@ -150,7 +155,7 @@
4.25 (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
4.26 *} "termination prover for lexicographic orderings"
4.27
4.28 -setup Lexicographic_Order.setup
4.29 +setup Lexicographic_Order.setup
4.30
4.31
4.32 subsection {* Congruence Rules *}
4.33 @@ -175,7 +180,7 @@
4.34 subsection {* Simp rules for termination proofs *}
4.35
4.36 lemma termination_basic_simps[termination_simp]:
4.37 - "x < (y::nat) \<Longrightarrow> x < y + z"
4.38 + "x < (y::nat) \<Longrightarrow> x < y + z"
4.39 "x < z \<Longrightarrow> x < y + z"
4.40 "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
4.41 "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
4.42 @@ -190,13 +195,13 @@
4.43
4.44 subsection {* Decomposition *}
4.45
4.46 -lemma less_by_empty:
4.47 +lemma less_by_empty:
4.48 "A = {} \<Longrightarrow> A \<subseteq> B"
4.49 and union_comp_emptyL:
4.50 "\<lbrakk> A O C = {}; B O C = {} \<rbrakk> \<Longrightarrow> (A \<union> B) O C = {}"
4.51 and union_comp_emptyR:
4.52 "\<lbrakk> A O B = {}; A O C = {} \<rbrakk> \<Longrightarrow> A O (B \<union> C) = {}"
4.53 -and wf_no_loop:
4.54 +and wf_no_loop:
4.55 "R O R = {} \<Longrightarrow> wf R"
4.56 by (auto simp add: wf_comp_self[of R])
4.57
4.58 @@ -218,10 +223,10 @@
4.59 proof -
4.60 from rp `S \<subseteq> snd P` have "wf (fst P)" "fst P O S \<subseteq> fst P"
4.61 unfolding reduction_pair_def by auto
4.62 - with `wf S` have "wf (fst P \<union> S)"
4.63 + with `wf S` have "wf (fst P \<union> S)"
4.64 by (auto intro: wf_union_compatible)
4.65 moreover from `R \<subseteq> fst P` have "R \<union> S \<subseteq> fst P \<union> S" by auto
4.66 - ultimately show ?thesis by (rule wf_subset)
4.67 + ultimately show ?thesis by (rule wf_subset)
4.68 qed
4.69
4.70 definition
4.71 @@ -253,33 +258,33 @@
4.72 unfolding pair_leq_def pair_less_def by auto
4.73
4.74 text {* Introduction rules for max *}
4.75 -lemma smax_emptyI:
4.76 - "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict"
4.77 - and smax_insertI:
4.78 +lemma smax_emptyI:
4.79 + "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict"
4.80 + and smax_insertI:
4.81 "\<lbrakk>y \<in> Y; (x, y) \<in> pair_less; (X, Y) \<in> max_strict\<rbrakk> \<Longrightarrow> (insert x X, Y) \<in> max_strict"
4.82 - and wmax_emptyI:
4.83 - "finite X \<Longrightarrow> ({}, X) \<in> max_weak"
4.84 + and wmax_emptyI:
4.85 + "finite X \<Longrightarrow> ({}, X) \<in> max_weak"
4.86 and wmax_insertI:
4.87 - "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak"
4.88 + "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak"
4.89 unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases)
4.90
4.91 text {* Introduction rules for min *}
4.92 -lemma smin_emptyI:
4.93 - "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict"
4.94 - and smin_insertI:
4.95 +lemma smin_emptyI:
4.96 + "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict"
4.97 + and smin_insertI:
4.98 "\<lbrakk>x \<in> XS; (x, y) \<in> pair_less; (XS, YS) \<in> min_strict\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_strict"
4.99 - and wmin_emptyI:
4.100 - "(X, {}) \<in> min_weak"
4.101 - and wmin_insertI:
4.102 - "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak"
4.103 + and wmin_emptyI:
4.104 + "(X, {}) \<in> min_weak"
4.105 + and wmin_insertI:
4.106 + "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak"
4.107 by (auto simp: min_strict_def min_weak_def min_ext_def)
4.108
4.109 text {* Reduction Pairs *}
4.110
4.111 -lemma max_ext_compat:
4.112 +lemma max_ext_compat:
4.113 assumes "R O S \<subseteq> R"
4.114 shows "max_ext R O (max_ext S \<union> {({},{})}) \<subseteq> max_ext R"
4.115 -using assms
4.116 +using assms
4.117 apply auto
4.118 apply (elim max_ext.cases)
4.119 apply rule
4.120 @@ -291,16 +296,16 @@
4.121 by auto
4.122
4.123 lemma max_rpair_set: "reduction_pair (max_strict, max_weak)"
4.124 - unfolding max_strict_def max_weak_def
4.125 + unfolding max_strict_def max_weak_def
4.126 apply (intro reduction_pairI max_ext_wf)
4.127 apply simp
4.128 apply (rule max_ext_compat)
4.129 by (auto simp: pair_less_def pair_leq_def)
4.130
4.131 -lemma min_ext_compat:
4.132 +lemma min_ext_compat:
4.133 assumes "R O S \<subseteq> R"
4.134 shows "min_ext R O (min_ext S \<union> {({},{})}) \<subseteq> min_ext R"
4.135 -using assms
4.136 +using assms
4.137 apply (auto simp: min_ext_def)
4.138 apply (drule_tac x=ya in bspec, assumption)
4.139 apply (erule bexE)
4.140 @@ -309,7 +314,7 @@
4.141 by auto
4.142
4.143 lemma min_rpair_set: "reduction_pair (min_strict, min_weak)"
4.144 - unfolding min_strict_def min_weak_def
4.145 + unfolding min_strict_def min_weak_def
4.146 apply (intro reduction_pairI min_ext_wf)
4.147 apply simp
4.148 apply (rule min_ext_compat)
5.1 --- a/src/HOL/SMT.thy Mon Apr 23 21:46:52 2012 +0200
5.2 +++ b/src/HOL/SMT.thy Mon Apr 23 22:22:57 2012 +0200
5.3 @@ -153,13 +153,17 @@
5.4 setup {*
5.5 SMT_Config.setup #>
5.6 SMT_Normalize.setup #>
5.7 - SMT_Solver.setup #>
5.8 SMTLIB_Interface.setup #>
5.9 Z3_Interface.setup #>
5.10 Z3_Proof_Reconstruction.setup #>
5.11 SMT_Setup_Solvers.setup
5.12 *}
5.13
5.14 +method_setup smt = {*
5.15 + Scan.optional Attrib.thms [] >>
5.16 + (fn thms => fn ctxt =>
5.17 + METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts))))
5.18 +*} "apply an SMT solver to the current goal"
5.19
5.20
5.21 subsection {* Configuration *}
6.1 --- a/src/HOL/Tools/Function/function.ML Mon Apr 23 21:46:52 2012 +0200
6.2 +++ b/src/HOL/Tools/Function/function.ML Mon Apr 23 22:22:57 2012 +0200
6.3 @@ -265,7 +265,6 @@
6.4 (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
6.5 "declaration of congruence rule for function definitions"
6.6 #> setup_case_cong
6.7 - #> Function_Relation.setup
6.8 #> Function_Common.Termination_Simps.setup
6.9
6.10 val get_congs = Function_Ctx_Tree.get_function_congs
7.1 --- a/src/HOL/Tools/Function/relation.ML Mon Apr 23 21:46:52 2012 +0200
7.2 +++ b/src/HOL/Tools/Function/relation.ML Mon Apr 23 22:22:57 2012 +0200
7.3 @@ -1,13 +1,13 @@
7.4 (* Title: HOL/Tools/Function/relation.ML
7.5 Author: Alexander Krauss, TU Muenchen
7.6
7.7 -Method "relation" to start a termination proof using a user-specified relation.
7.8 +Tactics to start a termination proof using a user-specified relation.
7.9 *)
7.10
7.11 signature FUNCTION_RELATION =
7.12 sig
7.13 val relation_tac: Proof.context -> (typ -> term) -> int -> tactic
7.14 - val setup: theory -> theory
7.15 + val relation_infer_tac: Proof.context -> term -> int -> tactic
7.16 end
7.17
7.18 structure Function_Relation : FUNCTION_RELATION =
7.19 @@ -27,7 +27,7 @@
7.20 THEN inst_state_tac rel;
7.21
7.22
7.23 -(* method version (with type inference) *)
7.24 +(* version with type inference *)
7.25
7.26 fun inst_state_infer_tac ctxt rel st =
7.27 case Term.add_vars (prop_of st) [] of
7.28 @@ -44,12 +44,8 @@
7.29 end
7.30 | _ => Seq.empty;
7.31
7.32 -fun relation_meth rel ctxt = SIMPLE_METHOD' (fn i =>
7.33 +fun relation_infer_tac ctxt rel i =
7.34 TRY (Function_Common.apply_termination_rule ctxt i)
7.35 - THEN inst_state_infer_tac ctxt rel);
7.36 -
7.37 -val setup =
7.38 - Method.setup @{binding relation} (Args.term >> relation_meth)
7.39 - "proves termination using a user-specified wellfounded relation";
7.40 + THEN inst_state_infer_tac ctxt rel;
7.41
7.42 end
8.1 --- a/src/HOL/Tools/SMT/smt_solver.ML Mon Apr 23 21:46:52 2012 +0200
8.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Apr 23 22:22:57 2012 +0200
8.3 @@ -41,9 +41,6 @@
8.4 (*tactic*)
8.5 val smt_tac: Proof.context -> thm list -> int -> tactic
8.6 val smt_tac': Proof.context -> thm list -> int -> tactic
8.7 -
8.8 - (*setup*)
8.9 - val setup: theory -> theory
8.10 end
8.11
8.12 structure SMT_Solver: SMT_SOLVER =
8.13 @@ -373,17 +370,4 @@
8.14
8.15 end
8.16
8.17 -
8.18 -val smt_method =
8.19 - Scan.optional Attrib.thms [] >>
8.20 - (fn thms => fn ctxt => METHOD (fn facts =>
8.21 - HEADGOAL (smt_tac ctxt (thms @ facts))))
8.22 -
8.23 -
8.24 -(* setup *)
8.25 -
8.26 -val setup =
8.27 - Method.setup @{binding smt} smt_method
8.28 - "Applies an SMT solver to the current goal."
8.29 -
8.30 end
9.1 --- a/src/HOL/Tools/typedef.ML Mon Apr 23 21:46:52 2012 +0200
9.2 +++ b/src/HOL/Tools/typedef.ML Mon Apr 23 22:22:57 2012 +0200
9.3 @@ -308,8 +308,11 @@
9.4 (Parse.type_args_constrained -- Parse.binding) --
9.5 Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
9.6 Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
9.7 - >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) =>
9.8 - typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)));
9.9 + >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) => fn lthy =>
9.10 + (if def then
9.11 + legacy_feature "typedef with implicit set definition -- use \"typedef (open)\" instead"
9.12 + else ();
9.13 + typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs) lthy)));
9.14
9.15 end;
9.16