# HG changeset patch
# User clasohm
# Date 830514810 -7200
# Node ID e0ff33a33fa53660334c70ed5ebd005708898a0e
# Parent  c38d953caedb918e0a5201183424dcc05938b55b
added changes by Konrad to prove_nchotomy

diff -r c38d953caedb -r e0ff33a33fa5 src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Thu Apr 25 18:44:13 1996 +0200
+++ b/src/HOL/datatype.ML	Fri Apr 26 12:33:30 1996 +0200
@@ -498,7 +498,7 @@
   val build_nchotomy: Sign.sg -> thm list -> cterm
 
   val prove_case_cong: thm -> thm list -> cterm -> thm
-  val prove_nchotomy: (string -> int -> tactic) -> thm list -> cterm -> thm
+  val prove_nchotomy: (string -> int -> tactic) -> cterm -> thm
 
   val case_thms : Sign.sg -> thm list -> (string -> int -> tactic)
                    -> {nchotomy:thm, case_cong:thm}
@@ -758,19 +758,28 @@
 
 (*---------------------------------------------------------------------------
  * Takes the induction tactic for the datatype, and the result from 
- * "build_nchotomy" and proves the theorem.
+ * "build_nchotomy" 
+ *
+ *    !v. (EX y1..yi. v = C1 y1..yi) | ... | (EX y1..yj. v = Cn y1..yj)
+ *
+ * and proves the theorem. The proof works along a diagonal: the nth 
+ * disjunct in the nth subgoal is easy to solve. Thus this routine depends 
+ * on the order of goals arising out of the application of the induction 
+ * tactic. A more general solution would have to use injectiveness and 
+ * distinctness rewrite rules.
  *---------------------------------------------------------------------------*)
-
-fun prove_nchotomy induct_tac case_rewrites ctm =
- let val {sign,t,...} = rep_cterm ctm
-     val (Const ("Trueprop",_) $ g) = t
+fun prove_nchotomy induct_tac ctm =
+ let val (Const ("Trueprop",_) $ g) = #t(rep_cterm ctm)
      val (Const ("All",_) $ Abs (v,_,_)) = g
+     (* For goal i, select the correct disjunct to attack, then prove it *)
+     fun tac i 0 = (rtac disjI1 i ORELSE all_tac) THEN
+                   REPEAT (rtac exI i) THEN (rtac refl i)
+       | tac i n = rtac disjI2 i THEN tac i (n-1)
  in 
  prove_goalw_cterm[] ctm
      (fn _ => [rtac allI 1,
                induct_tac v 1,
-               ALLGOALS (simp_tac (HOL_ss addsimps case_rewrites)),
-               ALLGOALS (fast_tac HOL_cs)])
+               ALLGOALS (fn i => tac i (i-1))])
  end
  handle _ => raise DTYPE_ERR {func="prove_nchotomy", mesg="failed"};
 
@@ -779,13 +788,14 @@
  * Brings the preceeding functions together.
  *---------------------------------------------------------------------------*)
 fun case_thms sign case_rewrites induct_tac =
-  let val nchotomy = prove_nchotomy induct_tac case_rewrites
-                            (build_nchotomy sign case_rewrites)
+  let val nchotomy = prove_nchotomy induct_tac
+                                    (build_nchotomy sign case_rewrites)
       val cong = prove_case_cong nchotomy case_rewrites
                                  (build_case_cong sign case_rewrites)
   in {nchotomy=nchotomy, case_cong=cong}
   end;
 
+
 (*---------------------------------------------------------------------------
  * Tests
  *