--- a/src/HOL/Product_Type.thy Thu Apr 10 12:30:02 2014 +0200
+++ b/src/HOL/Product_Type.thy Thu Apr 10 12:48:01 2014 +0200
@@ -1219,8 +1219,37 @@
subsection {* Inductively defined sets *}
+(* simplify {(x1, ..., xn). (x1, ..., xn) : S} to S *)
+simproc_setup Collect_mem ("Collect t") = {*
+ fn _ => fn ctxt => fn ct =>
+ (case term_of ct of
+ S as Const (@{const_name Collect}, Type (@{type_name fun}, [_, T])) $ t =>
+ let val (u, _, ps) = HOLogic.strip_psplits t in
+ (case u of
+ (c as Const (@{const_name Set.member}, _)) $ q $ S' =>
+ (case try (HOLogic.strip_ptuple ps) q of
+ NONE => NONE
+ | SOME ts =>
+ if not (Term.is_open S') andalso
+ ts = map Bound (length ps downto 0)
+ then
+ let val simp =
+ full_simp_tac (put_simpset HOL_basic_ss ctxt
+ addsimps [@{thm split_paired_all}, @{thm split_conv}]) 1
+ in
+ SOME (Goal.prove ctxt [] []
+ (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S')
+ (K (EVERY
+ [rtac eq_reflection 1, rtac @{thm subset_antisym} 1,
+ rtac subsetI 1, dtac CollectD 1, simp,
+ rtac subsetI 1, rtac CollectI 1, simp])))
+ end
+ else NONE)
+ | _ => NONE)
+ end
+ | _ => NONE)
+*}
ML_file "Tools/inductive_set.ML"
-setup Inductive_Set.setup
subsection {* Legacy theorem bindings and duplicates *}
--- a/src/HOL/Tools/inductive_set.ML Thu Apr 10 12:30:02 2014 +0200
+++ b/src/HOL/Tools/inductive_set.ML Thu Apr 10 12:48:01 2014 +0200
@@ -25,42 +25,11 @@
val mono_add: attribute
val mono_del: attribute
val codegen_preproc: theory -> thm list -> thm list
- val setup: theory -> theory
end;
structure Inductive_Set: INDUCTIVE_SET =
struct
-(**** simplify {(x1, ..., xn). (x1, ..., xn) : S} to S ****)
-
-val collect_mem_simproc =
- Simplifier.simproc_global @{theory Set} "Collect_mem" ["Collect t"] (fn ctxt =>
- fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
- let val (u, _, ps) = HOLogic.strip_psplits t
- in case u of
- (c as Const (@{const_name Set.member}, _)) $ q $ S' =>
- (case try (HOLogic.strip_ptuple ps) q of
- NONE => NONE
- | SOME ts =>
- if not (Term.is_open S') andalso
- ts = map Bound (length ps downto 0)
- then
- let val simp =
- full_simp_tac (put_simpset HOL_basic_ss ctxt
- addsimps [@{thm split_paired_all}, @{thm split_conv}]) 1
- in
- SOME (Goal.prove ctxt [] []
- (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S')
- (K (EVERY
- [rtac eq_reflection 1, rtac @{thm subset_antisym} 1,
- rtac subsetI 1, dtac CollectD 1, simp,
- rtac subsetI 1, rtac CollectI 1, simp])))
- end
- else NONE)
- | _ => NONE
- end
- | _ => NONE);
-
(***********************************************************************************)
(* simplifies (%x y. (x, y) : S & P x y) to (%x y. (x, y) : S Int {(x, y). P x y}) *)
(* and (%x y. (x, y) : S | P x y) to (%x y. (x, y) : S Un {(x, y). P x y}) *)
@@ -206,7 +175,7 @@
(swap #> Pattern.matches thy) (f #> fst) (op aconv) rules;
fun infer_arities thy arities (optf, t) fs = case strip_comb t of
- (Abs (s, T, u), []) => infer_arities thy arities (NONE, u) fs
+ (Abs (_, _, u), []) => infer_arities thy arities (NONE, u) fs
| (Abs _, _) => infer_arities thy arities (NONE, Envir.beta_norm t) fs
| (u, ts) => (case Option.map (lookup_arity thy arities) (name_type_of u) of
SOME (SOME (_, (arity, _))) =>
@@ -266,7 +235,7 @@
end)
in
Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]
- addsimprocs [collect_mem_simproc]) thm'' |>
+ addsimprocs [@{simproc Collect_mem}]) thm'' |>
zero_var_indexes |> eta_contract_thm (equal p)
end;
@@ -397,7 +366,7 @@
thm |>
Thm.instantiate ([], insts) |>
Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps to_set_simps
- addsimprocs [strong_ind_simproc pred_arities, collect_mem_simproc]) |>
+ addsimprocs [strong_ind_simproc pred_arities, @{simproc Collect_mem}]) |>
Rule_Cases.save thm
end;
@@ -425,8 +394,6 @@
else thm
in map preproc end;
-fun code_ind_att optmod = to_pred_att [];
-
(**** definition of inductive sets ****)
@@ -569,21 +536,21 @@
(** package setup **)
-(* setup theory *)
+(* attributes *)
-val setup =
- Attrib.setup @{binding pred_set_conv} (Scan.succeed pred_set_conv_att)
- "declare rules for converting between predicate and set notation" #>
- Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att)
- "convert rule to set notation" #>
- Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att)
- "convert rule to predicate notation" #>
- Attrib.setup @{binding mono_set} (Attrib.add_del mono_add mono_del)
- "declaration of monotonicity rule for set operators" #>
- map_theory_simpset (fn ctxt => ctxt addsimprocs [collect_mem_simproc]);
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding pred_set_conv} (Scan.succeed pred_set_conv_att)
+ "declare rules for converting between predicate and set notation" #>
+ Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att)
+ "convert rule to set notation" #>
+ Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att)
+ "convert rule to predicate notation" #>
+ Attrib.setup @{binding mono_set} (Attrib.add_del mono_add mono_del)
+ "declare of monotonicity rule for set operators");
-(* outer syntax *)
+(* commands *)
val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;