# HG changeset patch
# User nipkow
# Date 902405089 -7200
# Node ID dd99b958b3064039125e5b045d7dc29ebbaf9f0c
# Parent  de5d5e5eb69251631e3ec710d5b57bdb072cca1d
Simplified proof!!

diff -r de5d5e5eb692 -r dd99b958b306 src/HOL/Lambda/InductTermi.ML
--- a/src/HOL/Lambda/InductTermi.ML	Thu Aug 06 12:52:03 1998 +0200
+++ b/src/HOL/Lambda/InductTermi.ML	Thu Aug 06 14:04:49 1998 +0200
@@ -1,3 +1,9 @@
+(*  Title:      HOL/Lambda/InductTermi.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TU Muenchen
+*)
+
 (*** Every term in IT terminates ***)
 
 Goal "s : termi beta ==> !t. t : termi beta --> \
@@ -46,6 +52,7 @@
     ["Var n $$ ss : IT", "Abs t : IT", "Abs r $ s $$ ts : IT"];
 AddSEs IT_cases;
 
+(* Turned out to be redundant:
 Goal "t : termi beta ==> \
 \     !r rs. t = r$$rs --> r : termi beta & rs : termi(step1 beta)";
 be acc_induct 1;
@@ -77,12 +84,12 @@
 bd lemma 1;
 by(Blast_tac 1);
 qed "App_in_termi_betaD";
-
+*)
 
 Goal "r : termi beta ==> r : IT";
 be acc_induct 1;
 by(rename_tac "r" 1);
-be rev_mp 1;
+be thin_rl 1;
 be rev_mp 1;
 by(Simp_tac 1);
 by(res_inst_tac [("t","r")] Apps_dB_induct 1);
@@ -91,7 +98,7 @@
  brs IT.intrs 1;
  by(Clarify_tac 1);
  by(EVERY1[dtac bspec, atac]);
- by(EVERY[etac impE 1, etac mp 2]);
+ be mp 1;
   by(Clarify_tac 1);
   bd converseI 1;
   by(EVERY1[dtac ex_step1I, atac]);
@@ -99,25 +106,18 @@
   by(rename_tac "us" 1);
   by(eres_inst_tac [("x","Var n $$ us")] allE 1);
   by(Force_tac 1);
- bd apps_in_termi_betaD 1;
- by(asm_full_simp_tac (simpset() delsimps [step1_converse]
-                                 addsimps [step1_converse RS sym]) 1);
- by(blast_tac (claset() addDs [lists_accI]) 1);
 by(rename_tac "u ts" 1);
 by(exhaust_tac "ts" 1);
  by(Asm_full_simp_tac 1);
- by(Clarify_tac 1);
- brs IT.intrs 1;
- by(blast_tac (claset() addDs [Abs_in_termi_betaD]) 1);
+ by(blast_tac (claset() addIs IT.intrs) 1);
 by(rename_tac "s ss" 1);
 by(Asm_full_simp_tac 1);
 by(Clarify_tac 1);
 brs IT.intrs 1;
  by(blast_tac (claset() addIs [apps_preserves_beta]) 1);
-by(EVERY[etac impE 1, etac mp 2]);
+be mp 1;
  by(Clarify_tac 1);
  by(rename_tac "t" 1);
  by(eres_inst_tac [("x","Abs u $ t $$ ss")] allE 1);
  by(Force_tac 1);
-by(blast_tac (claset() addSDs [apps_in_termi_betaD, App_in_termi_betaD]) 1);
 qed "termi_implies_IT";