# HG changeset patch
# User nipkow
# Date 832328624 -7200
# Node ID f0c6aabc6c027efb6518419bcc4b1a550e052a35
# Parent  6040ec66e1e4a092dfb95706f06072ab89bab7e0
Moved split_rule et al from ind_syntax.ML to Prod.ML.
Used split_rule in Lfp.ML and Trancl.ML.

diff -r 6040ec66e1e4 -r f0c6aabc6c02 src/HOL/Lfp.ML
--- a/src/HOL/Lfp.ML	Wed May 15 13:51:15 1996 +0200
+++ b/src/HOL/Lfp.ML	Fri May 17 12:23:44 1996 +0200
@@ -51,16 +51,10 @@
             rtac (CollectI RS subsetI), rtac indhyp, atac]);
 qed "induct";
 
-val major::prems = goal Lfp.thy
-  "[| (a,b) : lfp f; mono f; \
-\     !!a b. (a,b) : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b";
-by (res_inst_tac [("c1","P")] (split RS subst) 1);
-by (rtac (major RS induct) 1);
-by (resolve_tac prems 1);
-by (res_inst_tac[("p","x")]PairE 1);
-by (hyp_subst_tac 1);
-by (asm_simp_tac (!simpset addsimps prems) 1);
-qed"induct2";
+bind_thm
+  ("induct2",
+   Prod_Syntax.split_rule
+     (read_instantiate [("a","(a,b)")] induct));
 
 (*** Fixpoint induction a la David Park ***)
 goal Lfp.thy "!!f. [| mono f; f A <= A |] ==> lfp(f) <= A";
diff -r 6040ec66e1e4 -r f0c6aabc6c02 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Wed May 15 13:51:15 1996 +0200
+++ b/src/HOL/Prod.ML	Fri May 17 12:23:44 1996 +0200
@@ -298,3 +298,60 @@
                      addSEs [SigmaE2, SigmaE, splitE, mem_splitE, 
                              fst_imageE, snd_imageE, prod_fun_imageE,
                              Pair_inject];
+
+structure Prod_Syntax =
+struct
+
+val unitT = Type("unit",[]);
+
+fun mk_prod (T1,T2) = Type("*", [T1,T2]);
+
+(*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
+fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
+  | factors T                    = [T];
+
+(*Make a correctly typed ordered pair*)
+fun mk_Pair (t1,t2) = 
+  let val T1 = fastype_of t1
+      and T2 = fastype_of t2
+  in  Const("Pair", [T1, T2] ---> mk_prod(T1,T2)) $ t1 $ t2  end;
+   
+fun split_const(Ta,Tb,Tc) = 
+    Const("split", [[Ta,Tb]--->Tc, mk_prod(Ta,Tb)] ---> Tc);
+
+(*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 = 
+      split_const(T1,T2,T3) $ 
+      Abs("v", T1, 
+	  ap_split T2 T3
+	     ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ 
+	      Bound 0))
+  | ap_split T T3 u = u;
+
+(*Makes a nested tuple from a list, following the product type structure*)
+fun mk_tuple (Type("*", [T1,T2])) tms = 
+        mk_Pair (mk_tuple T1 tms, 
+		 mk_tuple T2 (drop (length (factors T1), tms)))
+  | mk_tuple T (t::_) = t;
+
+(*Attempts to remove occurrences of split, and pair-valued parameters*)
+val remove_split = rewrite_rule [split RS eq_reflection]  o  
+	           rule_by_tactic (ALLGOALS split_all_tac);
+
+(*Uncurries any Var of function type in the rule*)
+fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) =
+      let val T' = factors T1 ---> T2
+	  val newt = ap_split T1 T2 (Var(v,T'))
+	  val cterm = Thm.cterm_of (#sign(rep_thm rl))
+      in
+	  remove_split (instantiate ([], [(cterm t, cterm newt)]) rl)
+      end
+  | split_rule_var (t,rl) = rl;
+
+(*Uncurries ALL function variables occurring in a rule's conclusion*)
+fun split_rule rl = foldr split_rule_var (term_vars (concl_of rl), rl)
+                    |> standard;
+
+end;
diff -r 6040ec66e1e4 -r f0c6aabc6c02 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Wed May 15 13:51:15 1996 +0200
+++ b/src/HOL/Trancl.ML	Fri May 17 12:23:44 1996 +0200
@@ -68,19 +68,10 @@
 by (fast_tac (rel_cs addIs prems) 1);
 qed "rtrancl_induct";
 
-val prems = goal Trancl.thy
- "[| ((a,b),(c,d)) : r^*; P a b; \
-\    !!x y z u.[| ((a,b),(x,y)) : r^*;  ((x,y),(z,u)) : r;  P x y |] ==> P z u\
-\ |] ==> P c d";
-by(res_inst_tac[("R","P")]splitD 1);
-by(res_inst_tac[("P","split P")]rtrancl_induct 1);
-brs prems 1;
-by(Simp_tac 1);
-brs prems 1;
-by(split_all_tac 1);
-by(Asm_full_simp_tac 1);
-by(REPEAT(ares_tac prems 1));
-qed "rtrancl_induct2";
+bind_thm
+  ("rtrancl_induct2",
+   Prod_Syntax.split_rule
+     (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] rtrancl_induct));
 
 (*transitivity of transitive closure!! -- by induction.*)
 goalw Trancl.thy [trans_def] "trans(r^*)";
diff -r 6040ec66e1e4 -r f0c6aabc6c02 src/HOL/ind_syntax.ML
--- a/src/HOL/ind_syntax.ML	Wed May 15 13:51:15 1996 +0200
+++ b/src/HOL/ind_syntax.ML	Fri May 17 12:23:44 1996 +0200
@@ -31,61 +31,6 @@
   in  all_const T $ Abs("v", T, imp $ (mk_mem (Bound 0, A)) $ (P $ Bound 0))
   end;
 
-(** Cartesian product type **)
-
-val unitT = Type("unit",[]);
-
-fun mk_prod (T1,T2) = Type("*", [T1,T2]);
-
-(*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
-fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
-  | factors T                    = [T];
-
-(*Make a correctly typed ordered pair*)
-fun mk_Pair (t1,t2) = 
-  let val T1 = fastype_of t1
-      and T2 = fastype_of t2
-  in  Const("Pair", [T1, T2] ---> mk_prod(T1,T2)) $ t1 $ t2  end;
-   
-fun split_const(Ta,Tb,Tc) = 
-    Const("split", [[Ta,Tb]--->Tc, mk_prod(Ta,Tb)] ---> Tc);
-
-(*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 = 
-      split_const(T1,T2,T3) $ 
-      Abs("v", T1, 
-	  ap_split T2 T3
-	     ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ 
-	      Bound 0))
-  | ap_split T T3 u = u;
-
-(*Makes a nested tuple from a list, following the product type structure*)
-fun mk_tuple (Type("*", [T1,T2])) tms = 
-        mk_Pair (mk_tuple T1 tms, 
-		 mk_tuple T2 (drop (length (factors T1), tms)))
-  | mk_tuple T (t::_) = t;
-
-(*Attempts to remove occurrences of split, and pair-valued parameters*)
-val remove_split = rewrite_rule [split RS eq_reflection]  o  
-	           rule_by_tactic (ALLGOALS split_all_tac);
-
-(*Uncurries any Var of function type in the rule*)
-fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) =
-      let val T' = factors T1 ---> T2
-	  val newt = ap_split T1 T2 (Var(v,T'))
-	  val cterm = Thm.cterm_of (#sign(rep_thm rl))
-      in
-	  remove_split (instantiate ([], [(cterm t, cterm newt)]) rl)
-      end
-  | split_rule_var (t,rl) = rl;
-
-(*Uncurries ALL function variables occurring in a rule's conclusion*)
-fun split_rule rl = foldr split_rule_var (term_vars (concl_of rl), rl)
-                    |> standard;
-
-
 (** Disjoint sum type **)
 
 fun mk_sum (T1,T2) = Type("+", [T1,T2]);
diff -r 6040ec66e1e4 -r f0c6aabc6c02 src/HOL/indrule.ML
--- a/src/HOL/indrule.ML	Wed May 15 13:51:15 1996 +0200
+++ b/src/HOL/indrule.ML	Fri May 17 12:23:44 1996 +0200
@@ -102,9 +102,9 @@
   Splits cartesian products in elem_type, however nested*)
 
 (*The components of the element type, several if it is a product*)
-val elem_factors = Ind_Syntax.factors elem_type;
+val elem_factors = Prod_Syntax.factors elem_type;
 val elem_frees = mk_frees "za" elem_factors;
-val elem_tuple = Ind_Syntax.mk_tuple elem_type elem_frees;
+val elem_tuple = Prod_Syntax.mk_tuple elem_type elem_frees;
 
 (*Given a recursive set, return the "split" predicate
   and a conclusion for the simultaneous induction rule*)
@@ -117,7 +117,7 @@
           (elem_frees, 
            Ind_Syntax.imp $ (Ind_Syntax.mk_mem (elem_tuple, rec_tm))
                 $ (list_comb (pfree, elem_frees)))
-  in  (Ind_Syntax.ap_split elem_type Ind_Syntax.boolT pfree, 
+  in  (Prod_Syntax.ap_split elem_type Ind_Syntax.boolT pfree, 
        qconcl)  
   end;
 
@@ -214,14 +214,14 @@
 in
   struct
   val induct = standard 
-                  (Ind_Syntax.split_rule_var
+                  (Prod_Syntax.split_rule_var
 		    (Var((pred_name,2), elem_type --> Ind_Syntax.boolT),
 		     induct0));
 
   (*Just "True" unless there's true mutual recursion.  This saves storage.*)
   val mutual_induct = 
       if length Intr_elim.rec_names > 1
-      then Ind_Syntax.remove_split mutual_induct_split
+      then Prod_Syntax.remove_split mutual_induct_split
       else TrueI;
   end
 end;