--- a/src/HOL/Finite_Set.thy Sun Jun 17 20:38:12 2012 +0200
+++ b/src/HOL/Finite_Set.thy Thu Jun 21 12:33:27 2012 +0200
@@ -7,6 +7,7 @@
theory Finite_Set
imports Option Power
+uses ("Tools/set_comprehension_pointfree.ML")
begin
subsection {* Predicate for finite sets *}
@@ -16,6 +17,12 @@
emptyI [simp, intro!]: "finite {}"
| insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
+use "Tools/set_comprehension_pointfree.ML"
+
+simproc_setup finite_Collect ("finite (Collect P)") =
+ {* Set_Comprehension_Pointfree.simproc *}
+
+
lemma finite_induct [case_names empty insert, induct set: finite]:
-- {* Discharging @{text "x \<notin> F"} entails extra work. *}
assumes "finite F"
--- a/src/HOL/IsaMakefile Sun Jun 17 20:38:12 2012 +0200
+++ b/src/HOL/IsaMakefile Thu Jun 21 12:33:27 2012 +0200
@@ -259,6 +259,7 @@
Tools/rewrite_hol_proof.ML \
Tools/sat_funcs.ML \
Tools/sat_solver.ML \
+ Tools/set_comprehension_pointfree.ML \
Tools/split_rule.ML \
Tools/try0.ML \
Tools/typedef.ML \
@@ -1042,8 +1043,7 @@
ex/Transfer_Int_Nat.thy \
ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy \
ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML \
- ex/svc_test.thy ../Tools/interpretation_with_defs.ML \
- ex/set_comprehension_pointfree.ML
+ ex/svc_test.thy ../Tools/interpretation_with_defs.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Thu Jun 21 12:33:27 2012 +0200
@@ -0,0 +1,155 @@
+(* Title: HOL/ex/set_comprehension_pointfree.ML
+ Author: Felix Kuperjans, Lukas Bulwahn, TU Muenchen
+ Rafal Kolanski, NICTA
+
+Simproc for rewriting set comprehensions to pointfree expressions.
+*)
+
+signature SET_COMPREHENSION_POINTFREE =
+sig
+ val simproc : morphism -> simpset -> cterm -> thm option
+ val rewrite_term : term -> term option
+ val conv : Proof.context -> term -> thm option
+end
+
+structure Set_Comprehension_Pointfree : SET_COMPREHENSION_POINTFREE =
+struct
+
+(* syntactic operations *)
+
+fun mk_inf (t1, t2) =
+ let
+ val T = fastype_of t1
+ in
+ Const (@{const_name Lattices.inf_class.inf}, T --> T --> T) $ t1 $ t2
+ end
+
+fun mk_image t1 t2 =
+ let
+ val T as Type (@{type_name fun}, [_ , R]) = fastype_of t1
+ in
+ Const (@{const_name image},
+ T --> fastype_of t2 --> HOLogic.mk_setT R) $ t1 $ t2
+ end;
+
+fun mk_sigma (t1, t2) =
+ let
+ val T1 = fastype_of t1
+ val T2 = fastype_of t2
+ val setT = HOLogic.dest_setT T1
+ val resT = HOLogic.mk_setT (HOLogic.mk_prodT (setT, HOLogic.dest_setT T2))
+ in
+ Const (@{const_name Sigma},
+ T1 --> (setT --> T2) --> resT) $ t1 $ absdummy setT t2
+ end;
+
+fun dest_Bound (Bound x) = x
+ | dest_Bound t = raise TERM("dest_Bound", [t]);
+
+fun dest_Collect (Const (@{const_name Collect}, _) $ Abs (_, _, t)) = t
+ | dest_Collect t = raise TERM ("dest_Collect", [t])
+
+(* Copied from predicate_compile_aux.ML *)
+fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
+ let
+ val (xTs, t') = strip_ex t
+ in
+ ((x, T) :: xTs, t')
+ end
+ | strip_ex t = ([], t)
+
+fun list_tupled_abs [] f = f
+ | list_tupled_abs [(n, T)] f = (Abs (n, T, f))
+ | list_tupled_abs ((n, T)::v::vs) f =
+ HOLogic.mk_split (Abs (n, T, list_tupled_abs (v::vs) f))
+
+fun mk_pointfree_expr t =
+ let
+ val (vs, t'') = strip_ex (dest_Collect t)
+ val (eq::conjs) = HOLogic.dest_conj t''
+ val f = if fst (HOLogic.dest_eq eq) = Bound (length vs)
+ then snd (HOLogic.dest_eq eq)
+ else raise TERM("mk_pointfree_expr", [t]);
+ val mems = map (apfst dest_Bound o HOLogic.dest_mem) conjs
+ val grouped_mems = AList.group (op =) mems
+ fun mk_grouped_unions (i, T) =
+ case AList.lookup (op =) grouped_mems i of
+ SOME ts => foldr1 mk_inf ts
+ | NONE => HOLogic.mk_UNIV T
+ val complete_sets = map mk_grouped_unions ((length vs - 1) downto 0 ~~ map snd vs)
+ in
+ mk_image (list_tupled_abs vs f) (foldr1 mk_sigma complete_sets)
+ end;
+
+val rewrite_term = try mk_pointfree_expr
+
+(* proof tactic *)
+
+(* Tactic works for arbitrary number of m : S conjuncts *)
+
+val dest_Collect_tac = dtac @{thm iffD1[OF mem_Collect_eq]}
+ THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE conjE}))
+ THEN' hyp_subst_tac;
+
+val intro_image_Sigma_tac = rtac @{thm image_eqI}
+ THEN' (REPEAT_DETERM1 o
+ (rtac @{thm refl}
+ ORELSE' rtac
+ @{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]}));
+
+val dest_image_Sigma_tac = etac @{thm imageE}
+ THEN' (TRY o REPEAT_DETERM1 o Splitter.split_asm_tac @{thms prod.split_asm})
+ THEN' hyp_subst_tac
+ THEN' (TRY o REPEAT_DETERM1 o
+ (etac @{thm conjE} ORELSE' dtac @{thm iffD1[OF mem_Sigma_iff]}));
+
+val intro_Collect_tac = rtac @{thm iffD2[OF mem_Collect_eq]}
+ THEN' REPEAT_DETERM1 o resolve_tac @{thms exI}
+ THEN' (TRY o (rtac @{thm conjI}))
+ THEN' (TRY o hyp_subst_tac)
+ THEN' rtac @{thm refl};
+
+val tac =
+ let
+ val subset_tac1 = rtac @{thm subsetI}
+ THEN' dest_Collect_tac
+ THEN' intro_image_Sigma_tac
+ THEN' (REPEAT_DETERM1 o
+ (rtac @{thm SigmaI}
+ ORELSE' rtac @{thm UNIV_I}
+ ORELSE' rtac @{thm IntI}
+ ORELSE' atac));
+
+ val subset_tac2 = rtac @{thm subsetI}
+ THEN' dest_image_Sigma_tac
+ THEN' intro_Collect_tac
+ THEN' REPEAT_DETERM o
+ (rtac @{thm conjI}
+ ORELSE' eresolve_tac @{thms IntD1 IntD2}
+ ORELSE' atac);
+ in
+ rtac @{thm subset_antisym} THEN' subset_tac1 THEN' subset_tac2
+ end;
+
+fun conv ctxt t =
+ let
+ fun mk_thm t' = Goal.prove ctxt [] []
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) (K (tac 1));
+ in
+ Option.map mk_thm (rewrite_term t)
+ end;
+
+(* simproc *)
+
+fun simproc _ ss redex =
+ let
+ val ctxt = Simplifier.the_context ss
+ val _ $ set_compr = term_of redex
+ in
+ conv ctxt set_compr
+ |> Option.map (fn thm =>
+ thm RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection})
+ end;
+
+end;
+
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Sun Jun 17 20:38:12 2012 +0200
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Thu Jun 21 12:33:27 2012 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/ex/Set_Comprehension_Pointfree_Tests.thy
- Author: Lukas Bulwahn
+ Author: Lukas Bulwahn, Rafal Kolanski
Copyright 2012 TU Muenchen
*)
@@ -7,39 +7,61 @@
theory Set_Comprehension_Pointfree_Tests
imports Main
-uses "set_comprehension_pointfree.ML"
begin
-simproc_setup finite_Collect ("finite (Collect P)") = {* Set_Comprehension_Pointfree.simproc *}
+lemma
+ "finite {p. EX x. p = (x, x)}"
+ apply simp
+ oops
lemma
"finite {f a b| a b. a : A \<and> b : B}"
-apply simp (* works :) *)
-oops
+ apply simp
+ oops
lemma
"finite {f a b| a b. a : A \<and> a : A' \<and> b : B}"
-(* apply simp -- does not terminate *)
-oops
+ apply simp
+ oops
lemma
"finite {f a b| a b. a : A \<and> b : B \<and> b : B'}"
-(* apply simp -- does not terminate *)
-oops
+ apply simp
+ oops
lemma
"finite {f a b c| a b c. a : A \<and> b : B \<and> c : C}"
-(* apply simp -- failed *)
-oops
+ apply simp
+ oops
lemma
"finite {f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D}"
-(* apply simp -- failed *)
-oops
+ apply simp
+ oops
lemma
"finite {f a b c d e | a b c d e. a : A \<and> b : B \<and> c : C \<and> d : D \<and> e : E}"
-(* apply simp -- failed *)
-oops
+ apply simp
+ oops
+
+lemma (* check arbitrary ordering *)
+ "finite {f a d c b e | e b c d a. b : B \<and> a : A \<and> e : E' \<and> c : C \<and> d : D \<and> e : E \<and> b : B'}"
+ apply simp
+ oops
+
+lemma
+ "\<lbrakk> finite A ; finite B ; finite C ; finite D \<rbrakk>
+ \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
+ by simp
+
+lemma
+ "finite ((\<lambda>(a,b,c,d). f a b c d) ` (A \<times> B \<times> C \<times> D))
+ \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
+ by simp
+
+schematic_lemma (* check interaction with schematics *)
+ "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
+ = finite ((\<lambda>(a:: ?'A, b :: ?'B). Pair_Rep a b) ` (UNIV \<times> UNIV))"
+ by simp
end
--- a/src/HOL/ex/set_comprehension_pointfree.ML Sun Jun 17 20:38:12 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,120 +0,0 @@
-(* Title: HOL/ex/set_comprehension_pointfree.ML
- Author: Felix Kuperjans, Lukas Bulwahn, TU Muenchen
-
-Simproc for rewriting set comprehensions to pointfree expressions.
-*)
-
-signature SET_COMPREHENSION_POINTFREE =
-sig
- val simproc : morphism -> simpset -> cterm -> thm option
-end
-
-structure Set_Comprehension_Pointfree : SET_COMPREHENSION_POINTFREE =
-struct
-
-(* syntactic operations *)
-
-fun mk_inf (t1, t2) =
- let
- val T = fastype_of t1
- in
- Const (@{const_name Lattices.inf_class.inf}, T --> T --> T) $ t1 $ t2
- end
-
-fun mk_image t1 t2 =
- let
- val T as Type (@{type_name fun}, [_ , R]) = fastype_of t1
- in
- Const (@{const_name image}, T --> fastype_of t2 --> HOLogic.mk_setT R) $ t1 $ t2
- end;
-
-fun mk_sigma (t1, t2) =
- let
- val T1 = fastype_of t1
- val T2 = fastype_of t2
- val setT = HOLogic.dest_setT T1
- val resultT = HOLogic.mk_setT (HOLogic.mk_prodT (setT, HOLogic.dest_setT T2))
- in
- Const (@{const_name Sigma}, T1 --> (setT --> T2) --> resultT) $ t1 $ absdummy setT t2
- end;
-
-fun dest_Bound (Bound x) = x
- | dest_Bound t = raise TERM("dest_Bound", [t]);
-
-fun dest_Collect (Const (@{const_name Collect}, _) $ Abs (_, _, t)) = t
- | dest_Collect t = raise TERM ("dest_Collect", [t])
-
-(* Copied from predicate_compile_aux.ML *)
-fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
- let
- val (xTs, t') = strip_ex t
- in
- ((x, T) :: xTs, t')
- end
- | strip_ex t = ([], t)
-
-fun list_tupled_abs [] f = f
- | list_tupled_abs [(n, T)] f = (Abs (n, T, f))
- | list_tupled_abs ((n, T)::v::vs) f = HOLogic.mk_split (Abs (n, T, list_tupled_abs (v::vs) f))
-
-fun mk_pointfree_expr t =
- let
- val (vs, t'') = strip_ex (dest_Collect t)
- val (eq::conjs) = HOLogic.dest_conj t''
- val f = if fst (HOLogic.dest_eq eq) = Bound (length vs)
- then snd (HOLogic.dest_eq eq)
- else raise TERM("mk_pointfree_expr", [t]);
- val mems = map (apfst dest_Bound o HOLogic.dest_mem) conjs
- val grouped_mems = AList.group (op =) mems
- fun mk_grouped_unions (i, T) =
- case AList.lookup (op =) grouped_mems i of
- SOME ts => foldr1 mk_inf ts
- | NONE => HOLogic.mk_UNIV T
- val complete_sets = map mk_grouped_unions ((length vs - 1) downto 0 ~~ map snd vs)
- in
- mk_image (list_tupled_abs vs f) (foldr1 mk_sigma complete_sets)
- end;
-
-(* proof tactic *)
-
-(* This tactic is terribly incomplete *)
-
-val goal1_tac_part2 = REPEAT_ALL_NEW (CHANGED o (atac ORELSE' rtac @{thm SigmaI}))
-
-val goal1_tac = etac @{thm CollectE}
- THEN' REPEAT1 o CHANGED o etac @{thm exE}
- THEN' REPEAT1 o CHANGED o etac @{thm conjE}
- THEN' rtac @{thm image_eqI}
- THEN' RANGE [(REPEAT o CHANGED o stac @{thm split}) THEN' goal1_tac_part2, goal1_tac_part2]
-
-val goal2_tac = etac @{thm imageE}
- THEN' rtac @{thm CollectI}
- THEN' REPEAT o CHANGED o etac @{thm SigmaE}
- THEN' REPEAT o CHANGED o rtac @{thm exI}
- THEN' REPEAT_ALL_NEW (rtac @{thm conjI})
- THEN_ALL_NEW
- (atac ORELSE'
- (asm_full_simp_tac HOL_basic_ss THEN' stac @{thm split} THEN' rtac @{thm refl}))
-
-val tac =
- rtac @{thm set_eqI} 1
- THEN rtac @{thm iffI} 1
- THEN goal1_tac 1
- THEN goal2_tac 1
-
-(* simproc *)
-
-fun simproc _ ss redex =
- let
- val ctxt = Simplifier.the_context ss
- val _ $ set_compr = term_of redex
- in
- case try mk_pointfree_expr set_compr of
- NONE => NONE
- | SOME pointfree_expr =>
- SOME (Goal.prove ctxt [] []
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (set_compr, pointfree_expr))) (K tac)
- RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection})
- end
-
-end;
--- a/src/Provers/hypsubst.ML Sun Jun 17 20:38:12 2012 +0200
+++ b/src/Provers/hypsubst.ML Thu Jun 21 12:33:27 2012 +0200
@@ -2,7 +2,7 @@
Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson
Copyright 1995 University of Cambridge
-Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "subst".
+Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "simplesubst".
Tactic to substitute using (at least) the assumption x=t in the rest
of the subgoal, and to delete (at least) that assumption. Original