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