src/HOL/Lambda/InductTermi.ML

+(*  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 --> \
 \     (!r ss. t = r[s/0]$$ss --> Abs r $ s $$ ss : termi beta)";
 be acc_induct 1;

    hd(tl(get_thms List.thy "foldl.simps")) RS sym ]
   @ dB.simps @ list.simps))
     ["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;
 by(force_tac (claset()
      addIs [apps_preserves_beta,apps_preserves_betas,accI],simpset()) 1);

 
 Goal "r$s : termi beta ==> r : termi beta & s : termi beta";
 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);
  by(rename_tac "n ts" 1);
  by(Clarify_tac 1);
  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]);
   by(Clarify_tac 1);
   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";