--- a/src/HOL/Finite_Set.thy Wed Oct 10 13:03:50 2012 +0200
+++ b/src/HOL/Finite_Set.thy Wed Oct 10 13:04:15 2012 +0200
@@ -16,18 +16,7 @@
emptyI [simp, intro!]: "finite {}"
| insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
-(* FIXME: move to Set theory *)
-ML_file "Tools/set_comprehension_pointfree.ML"
-
-simproc_setup finite_Collect ("finite (Collect P)") =
- {* K Set_Comprehension_Pointfree.simproc *}
-
-(* FIXME: move to Set theory*)
-setup {*
- Code_Preproc.map_pre (fn ss => ss addsimprocs
- [Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}],
- proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}])
-*}
+simproc_setup finite_Collect ("finite (Collect P)") = {* K Set_Comprehension_Pointfree.simproc *}
lemma finite_induct [case_names empty insert, induct set: finite]:
-- {* Discharging @{text "x \<notin> F"} entails extra work. *}
--- a/src/HOL/IMP/Collecting_Examples.thy Wed Oct 10 13:03:50 2012 +0200
+++ b/src/HOL/IMP/Collecting_Examples.thy Wed Oct 10 13:04:15 2012 +0200
@@ -7,12 +7,6 @@
lemma insert_code [code]: "insert x (set xs) = set (x#xs)"
by simp
-text{* Make assignment rule executable: *}
-declare step.simps(2)[code del]
-lemma [code]: "step S (x ::= e {P}) = (x ::= e {(%s. s(x := aval e s)) ` S})"
-by auto
-declare step.simps(1,3-)[code]
-
text{* The example: *}
definition "c = WHILE Less (V ''x'') (N 3)
DO ''x'' ::= Plus (V ''x'') (N 2)"
--- a/src/HOL/Lattices.thy Wed Oct 10 13:03:50 2012 +0200
+++ b/src/HOL/Lattices.thy Wed Oct 10 13:04:15 2012 +0200
@@ -650,14 +650,14 @@
definition
"f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
-lemma inf_apply [simp] (* CANDIDATE [code] *):
+lemma inf_apply [simp, code]:
"(f \<sqinter> g) x = f x \<sqinter> g x"
by (simp add: inf_fun_def)
definition
"f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
-lemma sup_apply [simp] (* CANDIDATE [code] *):
+lemma sup_apply [simp, code]:
"(f \<squnion> g) x = f x \<squnion> g x"
by (simp add: sup_fun_def)
@@ -677,7 +677,7 @@
definition
fun_Compl_def: "- A = (\<lambda>x. - A x)"
-lemma uminus_apply [simp] (* CANDIDATE [code] *):
+lemma uminus_apply [simp, code]:
"(- A) x = - (A x)"
by (simp add: fun_Compl_def)
@@ -691,7 +691,7 @@
definition
fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
-lemma minus_apply [simp] (* CANDIDATE [code] *):
+lemma minus_apply [simp, code]:
"(A - B) x = A x - B x"
by (simp add: fun_diff_def)
--- a/src/HOL/Orderings.thy Wed Oct 10 13:03:50 2012 +0200
+++ b/src/HOL/Orderings.thy Wed Oct 10 13:04:15 2012 +0200
@@ -1296,7 +1296,7 @@
definition
"\<bottom> = (\<lambda>x. \<bottom>)"
-lemma bot_apply [simp] (* CANDIDATE [code] *):
+lemma bot_apply [simp, code]:
"\<bottom> x = \<bottom>"
by (simp add: bot_fun_def)
@@ -1311,7 +1311,7 @@
definition
[no_atp]: "\<top> = (\<lambda>x. \<top>)"
-lemma top_apply [simp] (* CANDIDATE [code] *):
+lemma top_apply [simp, code]:
"\<top> x = \<top>"
by (simp add: top_fun_def)
--- a/src/HOL/Product_Type.thy Wed Oct 10 13:03:50 2012 +0200
+++ b/src/HOL/Product_Type.thy Wed Oct 10 13:04:15 2012 +0200
@@ -1117,6 +1117,17 @@
qed
+subsection {* Simproc for rewriting a set comprehension into a pointfree expression *}
+
+ML_file "Tools/set_comprehension_pointfree.ML"
+
+setup {*
+ Code_Preproc.map_pre (fn ss => ss addsimprocs
+ [Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}],
+ proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}])
+*}
+
+
subsection {* Inductively defined sets *}
ML_file "Tools/inductive_set.ML"
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Wed Oct 10 13:03:50 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Wed Oct 10 13:04:15 2012 +0200
@@ -26,6 +26,20 @@
Const (@{const_name Lattices.inf_class.inf}, T --> T --> T) $ t1 $ t2
end
+fun mk_sup (t1, t2) =
+ let
+ val T = fastype_of t1
+ in
+ Const (@{const_name Lattices.sup_class.sup}, T --> T --> T) $ t1 $ t2
+ end
+
+fun mk_Compl t =
+ let
+ val T = fastype_of t
+ in
+ Const (@{const_name "Groups.uminus_class.uminus"}, T --> T) $ t
+ end
+
fun mk_image t1 t2 =
let
val T as Type (@{type_name fun}, [_ , R]) = fastype_of t1
@@ -68,11 +82,13 @@
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 conjs = HOLogic.dest_conj t''
+ val is_the_eq =
+ the_default false o (try (fn eq => fst (HOLogic.dest_eq eq) = Bound (length vs)))
+ val SOME eq = find_first is_the_eq conjs
+ val f = snd (HOLogic.dest_eq eq)
+ val conjs' = filter_out (fn t => eq = t) conjs
+ 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
@@ -107,9 +123,8 @@
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};
+ THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI}))
+ THEN' (K (ALLGOALS (TRY o ((TRY o hyp_subst_tac) THEN' rtac @{thm refl}))))
val tac =
let
@@ -125,20 +140,22 @@
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);
+ THEN' REPEAT_DETERM o (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));
+ val ct = cterm_of (Proof_Context.theory_of ctxt) t
+ val Bex_def = mk_meta_eq @{thm Bex_def}
+ val unfold_eq = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv Bex_def))) ctxt ct
+ val t' = term_of (Thm.rhs_of unfold_eq)
+ fun mk_thm t'' = Goal.prove ctxt [] []
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq (t', t''))) (K (tac 1))
+ fun unfold th = th RS ((unfold_eq RS meta_eq_to_obj_eq) RS @{thm trans})
in
- Option.map mk_thm (rewrite_term t)
+ Option.map (unfold o mk_thm) (rewrite_term t')
end;
(* simproc *)
@@ -152,15 +169,23 @@
|> Option.map (fn thm => thm RS @{thm eq_reflection})
end;
-(* FIXME: turn into generic simproc for many predicates, i.e., remove hard-coded finite! *)
+fun instantiate_arg_cong ctxt pred =
+ let
+ val certify = cterm_of (Proof_Context.theory_of ctxt)
+ val arg_cong = @{thm arg_cong}
+ val f $ _ = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (concl_of arg_cong)))
+ in
+ cterm_instantiate [(certify f, certify pred)] arg_cong
+ end;
+
fun simproc ss redex =
let
val ctxt = Simplifier.the_context ss
- val _ $ set_compr = term_of redex
+ val pred $ set_compr = term_of redex
+ val arg_cong' = instantiate_arg_cong ctxt pred
in
conv ctxt set_compr
- |> Option.map (fn thm =>
- thm RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection})
+ |> Option.map (fn thm => thm RS arg_cong' RS @{thm eq_reflection})
end;
fun code_simproc ss redex =
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Wed Oct 10 13:03:50 2012 +0200
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Wed Oct 10 13:04:15 2012 +0200
@@ -59,6 +59,10 @@
\<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 S ==> finite {s'. EX s:S. s' = f a e s}"
+ 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))"
--- a/src/Pure/Isar/code.ML Wed Oct 10 13:03:50 2012 +0200
+++ b/src/Pure/Isar/code.ML Wed Oct 10 13:04:15 2012 +0200
@@ -437,9 +437,14 @@
exception BAD_THM of string;
fun bad_thm msg = raise BAD_THM msg;
-fun error_thm f thm = f thm handle BAD_THM msg => error msg;
-fun warning_thm f thm = SOME (f thm) handle BAD_THM msg => (warning msg; NONE)
-fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
+fun error_thm f thy (thm, proper) = f (thm, proper)
+ handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm);
+fun error_abs_thm f thy thm = f thm
+ handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm);
+fun warning_thm f thy (thm, proper) = SOME (f (thm, proper))
+ handle BAD_THM msg => (warning (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm); NONE)
+fun try_thm f thm_proper = SOME (f thm_proper)
+ handle BAD_THM _ => NONE;
fun is_linear thm =
let val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm
@@ -458,30 +463,29 @@
fun check_eqn thy { allow_nonlinear, allow_consts, allow_pats } thm (lhs, rhs) =
let
- fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
- | Free _ => bad "Illegal free variable in equation"
+ | Free _ => bad_thm "Illegal free variable"
| _ => I) t [];
fun tvars_of t = fold_term_types (fn _ =>
fold_atyps (fn TVar (v, _) => insert (op =) v
- | TFree _ => bad "Illegal free type variable in equation")) t [];
+ | TFree _ => bad_thm "Illegal free type variable")) t [];
val lhs_vs = vars_of lhs;
val rhs_vs = vars_of rhs;
val lhs_tvs = tvars_of lhs;
val rhs_tvs = tvars_of rhs;
val _ = if null (subtract (op =) lhs_vs rhs_vs)
then ()
- else bad "Free variables on right hand side of equation";
+ else bad_thm "Free variables on right hand side of equation";
val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
then ()
- else bad "Free type variables on right hand side of equation";
+ else bad_thm "Free type variables on right hand side of equation";
val (head, args) = strip_comb lhs;
val (c, ty) = case head
of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty)
- | _ => bad "Equation not headed by constant";
- fun check _ (Abs _) = bad "Abstraction on left hand side of equation"
+ | _ => bad_thm "Equation not headed by constant";
+ fun check _ (Abs _) = bad_thm "Abstraction on left hand side of equation"
| check 0 (Var _) = ()
- | check _ (Var _) = bad "Variable with application on left hand side of equation"
+ | check _ (Var _) = bad_thm "Variable with application on left hand side of equation"
| check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
| check n (Const (c_ty as (c, ty))) =
if allow_pats then let
@@ -489,70 +493,68 @@
in if n = (length o binder_types) ty
then if allow_consts orelse is_constr thy c'
then ()
- else bad (quote c ^ " is not a constructor, on left hand side of equation")
- else bad ("Partially applied constant " ^ quote c ^ " on left hand side of equation")
- end else bad ("Pattern not allowed here, but constant " ^ quote c ^ " encountered on left hand side")
+ else bad_thm (quote c ^ " is not a constructor, on left hand side of equation")
+ else bad_thm ("Partially applied constant " ^ quote c ^ " on left hand side of equation")
+ end else bad_thm ("Pattern not allowed here, but constant " ^ quote c ^ " encountered on left hand side of equation")
val _ = map (check 0) args;
val _ = if allow_nonlinear orelse is_linear thm then ()
- else bad "Duplicate variables on left hand side of equation";
+ else bad_thm "Duplicate variables on left hand side of equation";
val _ = if (is_none o AxClass.class_of_param thy) c then ()
- else bad "Overloaded constant as head in equation";
+ else bad_thm "Overloaded constant as head in equation";
val _ = if not (is_constr thy c) then ()
- else bad "Constructor as head in equation";
+ else bad_thm "Constructor as head in equation";
val _ = if not (is_abstr thy c) then ()
- else bad "Abstractor as head in equation";
+ else bad_thm "Abstractor as head in equation";
val _ = check_decl_ty thy (c, ty);
in () end;
fun gen_assert_eqn thy check_patterns (thm, proper) =
let
- fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
- handle TERM _ => bad "Not an equation"
- | THM _ => bad "Not a proper equation";
+ handle TERM _ => bad_thm "Not an equation"
+ | THM _ => bad_thm "Not a proper equation";
val _ = check_eqn thy { allow_nonlinear = not proper,
allow_consts = not (proper andalso check_patterns), allow_pats = true } thm (lhs, rhs);
in (thm, proper) end;
fun assert_abs_eqn thy some_tyco thm =
let
- fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
val (full_lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
- handle TERM _ => bad "Not an equation"
- | THM _ => bad "Not a proper equation";
+ handle TERM _ => bad_thm "Not an equation"
+ | THM _ => bad_thm "Not a proper equation";
val (rep, lhs) = dest_comb full_lhs
- handle TERM _ => bad "Not an abstract equation";
+ handle TERM _ => bad_thm "Not an abstract equation";
val (rep_const, ty) = dest_Const rep
- handle TERM _ => bad "Not an abstract equation";
+ handle TERM _ => bad_thm "Not an abstract equation";
val (tyco, Ts) = (dest_Type o domain_type) ty
- handle TERM _ => bad "Not an abstract equation"
- | TYPE _ => bad "Not an abstract equation";
+ handle TERM _ => bad_thm "Not an abstract equation"
+ | TYPE _ => bad_thm "Not an abstract equation";
val _ = case some_tyco of SOME tyco' => if tyco = tyco' then ()
- else bad ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco')
+ else bad_thm ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco')
| NONE => ();
val (vs', (_, (rep', _))) = get_abstype_spec thy tyco;
val _ = if rep_const = rep' then ()
- else bad ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep');
+ else bad_thm ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep');
val _ = check_eqn thy { allow_nonlinear = false,
allow_consts = false, allow_pats = false } thm (lhs, rhs);
val _ = if forall2 (fn T => fn (_, sort) => Sign.of_sort thy (T, sort)) Ts vs' then ()
else error ("Type arguments do not satisfy sort constraints of abstype certificate.");
in (thm, tyco) end;
-fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
+fun assert_eqn thy = error_thm (gen_assert_eqn thy true) thy;
fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy);
-fun mk_eqn thy = error_thm (gen_assert_eqn thy false) o
+fun mk_eqn thy = error_thm (gen_assert_eqn thy false) thy o
apfst (meta_rewrite thy);
fun mk_eqn_warning thy = Option.map (fn (thm, _) => (thm, is_linear thm))
- o warning_thm (gen_assert_eqn thy false) o rpair false o meta_rewrite thy;
+ o warning_thm (gen_assert_eqn thy false) thy o rpair false o meta_rewrite thy;
fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm))
o try_thm (gen_assert_eqn thy false) o rpair false o meta_rewrite thy;
-fun mk_abs_eqn thy = error_thm (assert_abs_eqn thy NONE) o meta_rewrite thy;
+fun mk_abs_eqn thy = error_abs_thm (assert_abs_eqn thy NONE) thy o meta_rewrite thy;
val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
@@ -632,23 +634,22 @@
fun check_abstype_cert thy proto_thm =
let
val thm = (AxClass.unoverload thy o meta_rewrite thy) proto_thm;
- fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm)
- handle TERM _ => bad "Not an equation"
- | THM _ => bad "Not a proper equation";
+ handle TERM _ => bad_thm "Not an equation"
+ | THM _ => bad_thm "Not a proper equation";
val ((abs, raw_ty), ((rep, rep_ty), param)) = (apsnd (apfst dest_Const o dest_comb)
o apfst dest_Const o dest_comb) lhs
- handle TERM _ => bad "Not an abstype certificate";
+ handle TERM _ => bad_thm "Not an abstype certificate";
val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
val _ = check_decl_ty thy (abs, raw_ty);
val _ = check_decl_ty thy (rep, rep_ty);
val _ = if length (binder_types raw_ty) = 1
then ()
- else bad "Bad type for abstract constructor";
+ else bad_thm "Bad type for abstract constructor";
val _ = (fst o dest_Var) param
- handle TERM _ => bad "Not an abstype certificate";
- val _ = if param = rhs then () else bad "Not an abstype certificate";
+ handle TERM _ => bad_thm "Not an abstype certificate";
+ val _ = if param = rhs then () else bad_thm "Not an abstype certificate";
val ((tyco, sorts), (abs, (vs, ty'))) =
analyze_constructor thy (abs, Logic.unvarifyT_global raw_ty);
val ty = domain_type ty';
@@ -1198,7 +1199,7 @@
fun add_abstype proto_thm thy =
let
val (tyco, (vs, (abs_ty as (abs, (_, ty)), (rep, cert)))) =
- error_thm (check_abstype_cert thy) proto_thm;
+ error_abs_thm (check_abstype_cert thy) thy proto_thm;
in
thy
|> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))