# 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;
-
-