# HG changeset patch # User Andreas Lochbihler # Date 1349867055 -7200 # Node ID b1493798d2532cb0e40881c8e2939e759b885b3c # Parent cf6a78acf4457757ab41fdcf97cb0d99abfe1024# Parent c7c2152322f2b9fcb20f820ae113b10873106291 merged diff -r cf6a78acf445 -r b1493798d253 src/HOL/Finite_Set.thy --- 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 \ 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 \ F"} entails extra work. *} diff -r cf6a78acf445 -r b1493798d253 src/HOL/IMP/Collecting_Examples.thy --- 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)" diff -r cf6a78acf445 -r b1493798d253 src/HOL/Lattices.thy --- 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 \ g = (\x. f x \ g x)" -lemma inf_apply [simp] (* CANDIDATE [code] *): +lemma inf_apply [simp, code]: "(f \ g) x = f x \ g x" by (simp add: inf_fun_def) definition "f \ g = (\x. f x \ g x)" -lemma sup_apply [simp] (* CANDIDATE [code] *): +lemma sup_apply [simp, code]: "(f \ g) x = f x \ g x" by (simp add: sup_fun_def) @@ -677,7 +677,7 @@ definition fun_Compl_def: "- A = (\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 = (\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) diff -r cf6a78acf445 -r b1493798d253 src/HOL/Orderings.thy --- 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 "\ = (\x. \)" -lemma bot_apply [simp] (* CANDIDATE [code] *): +lemma bot_apply [simp, code]: "\ x = \" by (simp add: bot_fun_def) @@ -1311,7 +1311,7 @@ definition [no_atp]: "\ = (\x. \)" -lemma top_apply [simp] (* CANDIDATE [code] *): +lemma top_apply [simp, code]: "\ x = \" by (simp add: top_fun_def) diff -r cf6a78acf445 -r b1493798d253 src/HOL/Product_Type.thy --- 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" diff -r cf6a78acf445 -r b1493798d253 src/HOL/Tools/set_comprehension_pointfree.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 = diff -r cf6a78acf445 -r b1493798d253 src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy --- 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 @@ \ finite ({f a b c d| a b c d. a : A \ b : B \ c : C \ 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 \ ?'B \ bool. \a b. x = Pair_Rep a b} = finite ((\(a:: ?'A, b :: ?'B). Pair_Rep a b) ` (UNIV \ UNIV))" diff -r cf6a78acf445 -r b1493798d253 src/Pure/Isar/code.ML --- 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))))