# HG changeset patch # User wenzelm # Date 963773563 -7200 # Node ID a4b990838074ff2907c8bd2853636fd776454b7c # Parent 97367249541473cf2e7b2bf3e9e149df72ebfd45 improved unit theory: unit_all_eq1, unit_all_eq2, split_all_tac; tuned; diff -r 973672495414 -r a4b990838074 src/HOL/Prod.ML --- a/src/HOL/Prod.ML Sun Jul 16 20:51:19 2000 +0200 +++ b/src/HOL/Prod.ML Sun Jul 16 20:52:43 2000 +0200 @@ -6,14 +6,58 @@ Ordered Pairs, the Cartesian product type, the unit type *) -(*This counts as a non-emptiness result for admitting 'a * 'b as a type*) +(** unit **) + +Goalw [Unity_def] + "u = ()"; +by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1); +by (rtac (Rep_unit_inverse RS sym) 1); +qed "unit_eq"; + +(*simplification procedure for unit_eq. + Cannot use this rule directly -- it loops!*) +local + val unit_pat = Thm.cterm_of (Theory.sign_of (the_context ())) (Free ("x", HOLogic.unitT)); + val unit_meta_eq = standard (mk_meta_eq unit_eq); + fun proc _ _ t = + if HOLogic.is_unit t then None + else Some unit_meta_eq; +in + val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc; +end; + +Addsimprocs [unit_eq_proc]; + +Goal "(!!x::unit. PROP P x) == PROP P ()"; +by (Simp_tac 1); +qed "unit_all_eq1"; + +Goal "(!!x::unit. PROP P) == PROP P"; +by (rtac triv_forall_equality 1); +qed "unit_all_eq2"; + +Goal "P () ==> P x"; +by (Simp_tac 1); +qed "unit_induct"; + +(*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u), + replacing it by f rather than by %u.f(). *) +Goal "(%u::unit. f()) = f"; +by (rtac ext 1); +by (Simp_tac 1); +qed "unit_abs_eta_conv"; +Addsimps [unit_abs_eta_conv]; + + +(** prod **) + Goalw [Prod_def] "Pair_Rep a b : Prod"; by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]); qed "ProdI"; -val [major] = goalw Prod.thy [Pair_Rep_def] +val [major] = goalw (the_context ()) [Pair_Rep_def] "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'"; -by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst), +by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst), rtac conjI, rtac refl, rtac refl]); qed "Pair_Rep_inject"; @@ -60,7 +104,7 @@ qed "PairE"; fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac, - K prune_params_tac]; + K prune_params_tac]; (* Do not add as rewrite rule: invalidates some proofs in IMP *) Goal "p = (fst(p),snd(p))"; @@ -79,26 +123,30 @@ bind_thm ("split_paired_all", SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection))); +bind_thms ("split_tupled_all", [split_paired_all, unit_all_eq2]); + (* -Addsimps [split_paired_all] does not work with simplifier -because it also affects premises in congrence rules, +Addsimps [split_paired_all] does not work with simplifier +because it also affects premises in congrence rules, where is can lead to premises of the form !!a b. ... = ?P(a,b) which cannot be solved by reflexivity. *) (* replace parameters of product type by individual component parameters *) local - fun is_pair (_,Type("*",_)) = true - | is_pair _ = false; - fun exists_paired_all prem = exists is_pair (Logic.strip_params prem); - val split_tac = full_simp_tac (HOL_basic_ss addsimps [split_paired_all]); + fun exists_paired_all prem = (* FIXME check deeper nesting of params!?! *) + Library.exists (can HOLogic.dest_prodT o #2) (Logic.strip_params prem); + val ss = HOL_basic_ss + addsimps [split_paired_all, unit_all_eq2, unit_abs_eta_conv] + addsimprocs [unit_eq_proc]; + val split_tac = full_simp_tac ss; in -val split_all_tac = SUBGOAL (fn (prem,i) => - if exists_paired_all prem then split_tac i else no_tac); + val split_all_tac = SUBGOAL (fn (prem,i) => + if exists_paired_all prem then split_tac i else no_tac); end; -claset_ref() := claset() addSWrapper ("split_all_tac", - fn tac2 => split_all_tac ORELSE' tac2); +claset_ref() := claset() + addSWrapper ("split_all_tac", fn tac2 => split_all_tac ORELSE' tac2); Goal "(!x. P x) = (!a b. P(a,b))"; by (Fast_tac 1); @@ -137,7 +185,7 @@ qed "Pair_fst_snd_eq"; (*Prevents simplification of c: much faster*) -val [prem] = goal Prod.thy +val [prem] = goal (the_context ()) "p=q ==> split c p = split c q"; by (rtac (prem RS arg_cong) 1); qed "split_weak_cong"; @@ -152,14 +200,14 @@ by (asm_simp_tac (simpset() addsimps prems@[split_eta]) 1); qed "cond_split_eta"; -(*simplification procedure for cond_split_eta. - using split_eta a rewrite rule is not general enough, and using +(*simplification procedure for cond_split_eta. + using split_eta a rewrite rule is not general enough, and using cond_split_eta directly would render some existing proofs very inefficient. similarly for split_beta. *) local fun Pair_pat k 0 (Bound m) = (m = k) | Pair_pat k i (Const ("Pair", _) $ Bound m $ t) = i > 0 andalso - m = k+i andalso Pair_pat k (i-1) t + m = k+i andalso Pair_pat k (i-1) t | Pair_pat _ _ _ = false; fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t | no_args k i (t $ u) = no_args k i t andalso no_args k i u @@ -168,33 +216,34 @@ fun split_pat tp i (Abs (_,_,t)) = if tp 0 i t then Some (i,t) else None | split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t | split_pat tp i _ = None; - fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm [] - (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))) - (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1])); - fun simproc name patstr = Simplifier.mk_simproc name - [Thm.read_cterm (sign_of Prod.thy) (patstr, HOLogic.termT)]; + fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm [] + (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))) + (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1])); + val sign = sign_of (the_context ()); + fun simproc name patstr = Simplifier.mk_simproc name + [Thm.read_cterm sign (patstr, HOLogic.termT)]; val beta_patstr = "split f z"; val eta_patstr = "split f"; fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t | beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse - (beta_term_pat k i t andalso beta_term_pat k i u) + (beta_term_pat k i t andalso beta_term_pat k i u) | beta_term_pat k i t = no_args k i t; fun eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg | eta_term_pat _ _ _ = false; fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t) | subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg - else (subst arg k i t $ subst arg k i u) + else (subst arg k i t $ subst arg k i u) | subst arg k i t = t; - fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) = - (case split_pat beta_term_pat 1 t of - Some (i,f) => Some (metaeq sg s (subst arg 0 i f)) - | None => None) + fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) = + (case split_pat beta_term_pat 1 t of + Some (i,f) => Some (metaeq sg s (subst arg 0 i f)) + | None => None) | beta_proc _ _ _ = None; - fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) = - (case split_pat eta_term_pat 1 t of - Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end)) - | None => None) + fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) = + (case split_pat eta_term_pat 1 t of + Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end)) + | None => None) | eta_proc _ _ _ = None; in val split_beta_proc = simproc "split_beta" beta_patstr beta_proc; @@ -254,7 +303,7 @@ by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); qed "splitE'"; -val major::prems = goal Prod.thy +val major::prems = goal (the_context ()) "[| Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R \ \ |] ==> R"; by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); @@ -282,13 +331,13 @@ AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2]; AddSEs [splitE, splitE', mem_splitE]; -Goal "(%u. ? x y. u = (x, y) & P (x, y)) = P"; +Goal "(%u. ? x y. u = (x, y) & P (x, y)) = P"; by (rtac ext 1); by (Fast_tac 1); qed "split_eta_SetCompr"; Addsimps [split_eta_SetCompr]; -Goal "(%u. ? x y. u = (x, y) & P x y) = split P"; +Goal "(%u. ? x y. u = (x, y) & P x y) = split P"; br ext 1; by (Fast_tac 1); qed "split_eta_SetCompr2"; @@ -306,7 +355,7 @@ qed "Eps_split_eq"; Addsimps [Eps_split_eq]; (* -the following would be slightly more general, +the following would be slightly more general, but cannot be used as rewrite rule: ### Cannot add premise as rewrite rule because it contains (type) unknowns: ### ?y = .x @@ -387,7 +436,7 @@ by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ; qed "SigmaD2"; -val [major,minor]= goal Prod.thy +val [major,minor]= goal (the_context ()) "[| (a,b) : Sigma A B; \ \ [| a:A; b:B(a) |] ==> P \ \ |] ==> P"; @@ -416,23 +465,23 @@ Goal "UNIV <*> UNIV = UNIV"; by Auto_tac; -qed "UNIV_Times_UNIV"; +qed "UNIV_Times_UNIV"; Addsimps [UNIV_Times_UNIV]; Goal "- (UNIV <*> A) = UNIV <*> (-A)"; by Auto_tac; -qed "Compl_Times_UNIV1"; +qed "Compl_Times_UNIV1"; Goal "- (A <*> UNIV) = (-A) <*> UNIV"; by Auto_tac; -qed "Compl_Times_UNIV2"; +qed "Compl_Times_UNIV2"; -Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; +Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; Goal "((a,b): Sigma A B) = (a:A & b:B(a))"; by (Blast_tac 1); qed "mem_Sigma_iff"; -AddIffs [mem_Sigma_iff]; +AddIffs [mem_Sigma_iff]; Goal "x:C ==> (A <*> C <= B <*> C) = (A <= B)"; by (Blast_tac 1); @@ -501,55 +550,19 @@ matching, especially when the rules are re-oriented*) Goal "(A Un B) <*> C = (A <*> C) Un (B <*> C)"; by (Blast_tac 1); -qed "Times_Un_distrib1"; +qed "Times_Un_distrib1"; Goal "(A Int B) <*> C = (A <*> C) Int (B <*> C)"; by (Blast_tac 1); -qed "Times_Int_distrib1"; +qed "Times_Int_distrib1"; Goal "(A - B) <*> C = (A <*> C) - (B <*> C)"; by (Blast_tac 1); -qed "Times_Diff_distrib1"; - -(** Exhaustion rule for unit -- a degenerate form of induction **) - -Goalw [Unity_def] - "u = ()"; -by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1); -by (rtac (Rep_unit_inverse RS sym) 1); -qed "unit_eq"; - -(*simplification procedure for unit_eq. - Cannot use this rule directly -- it loops!*) -local - val unit_pat = Thm.cterm_of (Theory.sign_of thy) (Free ("x", HOLogic.unitT)); - val unit_meta_eq = standard (mk_meta_eq unit_eq); - fun proc _ _ t = - if HOLogic.is_unit t then None - else Some unit_meta_eq; -in - val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc; -end; - -Addsimprocs [unit_eq_proc]; - - -Goal "P () ==> P x"; -by (Simp_tac 1); -qed "unit_induct"; - - -(*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u), - replacing it by f rather than by %u.f(). *) -Goal "(%u::unit. f()) = f"; -by (rtac ext 1); -by (Simp_tac 1); -qed "unit_abs_eta_conv"; -Addsimps [unit_abs_eta_conv]; +qed "Times_Diff_distrib1"; (*Attempts to remove occurrences of split, and pair-valued parameters*) -val remove_split = rewrite_rule [split RS eq_reflection] o +val remove_split = rewrite_rule [split RS eq_reflection] o rule_by_tactic (TRYALL split_all_tac); local @@ -557,11 +570,11 @@ (*In ap_split S T u, term u expects separate arguments for the factors of S, with result type T. The call creates a new term expecting one argument of type S.*) -fun ap_split (Type ("*", [T1, T2])) T3 u = - HOLogic.split_const (T1, T2, T3) $ - Abs("v", T1, +fun ap_split (Type ("*", [T1, T2])) T3 u = + HOLogic.split_const (T1, T2, T3) $ + Abs("v", T1, ap_split T2 T3 - ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $ + ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $ Bound 0)) | ap_split T T3 u = u; @@ -584,5 +597,3 @@ |> standard; end; - -