First steps towards termination of simply typed terms.

--- a/src/HOL/Lambda/Eta.ML	Thu Aug 06 10:28:44 1998 +0200
+++ b/src/HOL/Lambda/Eta.ML	Thu Aug 06 10:33:54 1998 +0200
@@ -9,18 +9,12 @@
 confluence of beta+eta
 *)
 
-open Eta;
-
 Addsimps eta.intrs;
+AddIs eta.intrs;
 
 val eta_cases = map (eta.mk_cases dB.simps)
     ["Abs s -e> z","s $ t -e> u","Var i -e> t"];
-
-val beta_cases = map (beta.mk_cases dB.simps)
-    ["s $ t -> u","Var i -> t"];
-
-AddIs eta.intrs;
-AddSEs (beta_cases@eta_cases);
+AddSEs eta_cases;
 
 section "eta, subst and free";
 
@@ -177,11 +171,11 @@
   by (rtac notE 1);
    by (assume_tac 2);
   by (etac thin_rl 1);
-  by (res_inst_tac [("dB","t")] dB_case_distinction 1);
-    by (Simp_tac 1);
+  by (exhaust_tac "t" 1);
+    by (Asm_simp_tac 1);
     by (blast_tac (HOL_cs addDs [less_not_refl2]) 1);
-   by (Simp_tac 1);
-  by (Simp_tac 1);
+   by (Asm_simp_tac 1);
+  by (Asm_simp_tac 1);
  by (Asm_simp_tac 1);
  by (etac thin_rl 1);
  by (etac thin_rl 1);
@@ -193,11 +187,11 @@
   by (Asm_simp_tac 1);
  by (etac exE 1);
  by (etac rev_mp 1);
- by (res_inst_tac [("dB","t")] dB_case_distinction 1);
-   by (Simp_tac 1);
-  by (Simp_tac 1);
+ by (exhaust_tac "t" 1);
+   by (Asm_simp_tac 1);
+  by (Asm_simp_tac 1);
   by (Blast_tac 1);
- by (Simp_tac 1);
+ by (Asm_simp_tac 1);
 by (Asm_simp_tac 1);
 by (etac thin_rl 1);
 by (rtac allI 1);
@@ -207,10 +201,10 @@
  by (Asm_simp_tac 1);
 by (etac exE 1);
 by (etac rev_mp 1);
-by (res_inst_tac [("dB","t")] dB_case_distinction 1);
-  by (Simp_tac 1);
- by (Simp_tac 1);
-by (Simp_tac 1);
+by (exhaust_tac "t" 1);
+  by (Asm_simp_tac 1);
+ by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "not_free_iff_lifted";
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/InductTermi.ML	Thu Aug 06 10:33:54 1998 +0200
@@ -0,0 +1,130 @@
+(*** 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;
+be thin_rl 1;
+br allI 1;
+br impI 1;
+be acc_induct 1;
+by(Clarify_tac 1);
+br accI 1;
+by(safe_tac (claset() addSEs [apps_betasE]));
+   ba 1;
+  by(blast_tac (claset() addIs [subst_preserves_beta,apps_preserves_beta]) 1);
+ by(blast_tac (claset()
+    addIs [apps_preserves_beta2,subst_preserves_beta2,rtrancl_converseI]
+    addDs [acc_downwards]) 1);
+(* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
+by(blast_tac (claset() addDs [apps_preserves_betas]) 1);
+qed_spec_mp "double_induction_lemma";
+
+Goal "t : IT ==> t : termi(beta)";
+be IT.induct 1;
+  bd rev_subsetD 1;
+   br lists_mono 1;
+   br Int_lower2 1;
+  by(Asm_full_simp_tac 1);
+  bd lists_accD 1;
+  be acc_induct 1;
+  br accI 1;
+  by(blast_tac (claset() addSDs [head_Var_reduction]) 1);
+ be acc_induct 1;
+ br accI 1;
+ by(Blast_tac 1);
+by(blast_tac (claset() addIs [double_induction_lemma]) 1);
+qed "IT_implies_termi";
+
+(*** Every terminating term is in IT ***)
+
+val IT_cases = map (IT.mk_cases
+ ([Var_apps_eq_Var_apps_conv, Abs_eq_apps_conv, apps_eq_Abs_conv,
+   Abs_apps_eq_Abs_apps_conv,
+   Var_apps_neq_Abs_apps, Var_apps_neq_Abs_apps RS not_sym,
+   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;
+
+(* FIXME
+"Arith.trans_less_add1",   "?i < ?j ==> ?i < ?j + ?m"
+"Arith.less_imp_add_less", "?m < ?n ==> ?m < ?n + ?k"
+"Arith.trans_le_add1", "?i <= ?j ==> ?i <= ?j + ?m"
+"Arith.le_imp_add_le", "?m <= ?n ==> ?m <= ?n + ?k"
+*)
+
+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);
+val lemma = result();
+
+Goal "r$$rs : termi beta ==> r : termi beta & rs : termi(step1 beta)";
+bd lemma 1;
+by(Blast_tac 1);
+qed "apps_in_termi_betaD";
+
+Goal "t : termi beta ==> !r. t = Abs r --> r : termi beta";
+be acc_induct 1;
+by(force_tac (claset() addIs [accI],simpset()) 1);
+val lemma = result();
+
+Goal "Abs r : termi beta ==> r : termi beta";
+bd lemma 1;
+by(Blast_tac 1);
+qed "Abs_in_termi_betaD";
+
+Goal "t : termi beta ==> !r s. t = r$s --> r : termi beta & s : termi beta";
+be acc_induct 1;
+by(force_tac (claset() addIs [accI],simpset()) 1);
+val lemma = result();
+
+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 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]);
+  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(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]);
+ 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";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/InductTermi.thy	Thu Aug 06 10:33:54 1998 +0200
@@ -0,0 +1,22 @@
+(*  Title:      HOL/Lambda/InductTermi.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TU Muenchen
+
+Inductive characterization of terminating lambda terms.
+Goes back to
+Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995.
+Also rediscovered by Matthes and Joachimski.
+*)
+
+InductTermi = Acc + ListBeta +
+
+consts IT :: dB set
+inductive IT
+intrs
+VarI "rs : lists IT ==> (Var n)$$rs : IT"
+LambdaI "r : IT ==> Abs r : IT"
+BetaI "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT"
+monos "[lists_mono]"
+
+end

--- a/src/HOL/Lambda/Lambda.ML	Thu Aug 06 10:28:44 1998 +0200
+++ b/src/HOL/Lambda/Lambda.ML	Thu Aug 06 10:33:54 1998 +0200
@@ -8,7 +8,9 @@
 
 (*** Lambda ***)
 
-open Lambda;
+val beta_cases = map (beta.mk_cases dB.simps)
+    ["Var i -> t", "Abs r -> s", "s $ t -> u"];
+AddSEs beta_cases;
 
 Delsimps [subst_Var];
 Addsimps ([if_not_P, not_less_eq] @ beta.intrs);
@@ -16,9 +18,6 @@
 (* don't add r_into_rtrancl! *)
 AddSIs beta.intrs;
 
-val dB_case_distinction =
-  rule_by_tactic(EVERY[etac thin_rl 2,etac thin_rl 2,etac thin_rl 3])dB.induct;
-
 (*** Congruence rules for ->> ***)
 
 Goal "s ->> s' ==> Abs s ->> Abs s'";
@@ -135,3 +134,26 @@
 Goal "substn t s 0 = t[s/0]";
 by (Simp_tac 1);
 qed "substn_subst_0";
+
+(*** Preservation thms ***)
+(* Not used in CR-proof but in SN-proof *)
+
+Goal "r -> s ==> !t i. r[t/i] -> s[t/i]";
+be beta.induct 1;
+by(ALLGOALS (asm_simp_tac (simpset() addsimps [subst_subst RS sym])));
+qed_spec_mp "subst_preserves_beta";
+Addsimps [subst_preserves_beta];
+
+Goal "r -> s ==> !i. lift r i -> lift s i";
+be beta.induct 1;
+by(Auto_tac);
+qed_spec_mp "lift_preserves_beta";
+Addsimps [lift_preserves_beta];
+
+Goal "!r s i. r -> s --> t[r/i] ->> t[s/i]";
+by(induct_tac "t" 1);
+by(asm_simp_tac (addsplit(simpset() addsimps [r_into_rtrancl])) 1);
+by(asm_simp_tac (simpset() addsimps [rtrancl_beta_App]) 1);
+by(asm_simp_tac (simpset() addsimps [rtrancl_beta_Abs]) 1);
+qed_spec_mp "subst_preserves_beta2";
+Addsimps [subst_preserves_beta2];

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/ListApplication.ML	Thu Aug 06 10:33:54 1998 +0200
@@ -0,0 +1,142 @@
+(*  Title:      HOL/Lambda/ListApplication.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TU Muenchen
+*)
+
+Goal "(r$$ts = s$$ts) = (r = s)";
+by(rev_induct_tac "ts" 1);
+by(Auto_tac);
+qed "apps_eq_tail_conv";
+AddIffs [apps_eq_tail_conv];
+
+Goal "!s. (Var m = s$$ss) = (Var m = s & ss = [])";
+by(induct_tac "ss" 1);
+by(Auto_tac);
+qed_spec_mp "Var_eq_apps_conv";
+AddIffs [Var_eq_apps_conv];
+
+Goal "!ss. ((Var m)$$rs = (Var n)$$ss) = (m=n & rs=ss)";
+by(rev_induct_tac "rs" 1);
+ by(Simp_tac 1);
+ by(Blast_tac 1);
+br allI 1;
+by(rev_induct_tac "ss" 1);
+by(Auto_tac);
+qed_spec_mp "Var_apps_eq_Var_apps_conv";
+AddIffs [Var_apps_eq_Var_apps_conv];
+
+Goal "(r$s = t$$ts) = \
+\     (if ts = [] then r$s = t \
+\      else (? ss. ts = ss@[s] & r = t$$ss))";
+by(res_inst_tac [("xs","ts")] rev_exhaust 1);
+by(Auto_tac);
+qed "App_eq_foldl_conv";
+
+Goal "(Abs r = s$$ss) = (Abs r = s & ss=[])";
+by(rev_induct_tac "ss" 1);
+by(Auto_tac);
+qed "Abs_eq_apps_conv";
+AddIffs [Abs_eq_apps_conv];
+
+Goal "(s$$ss = Abs r) = (s = Abs r & ss=[])";
+by(rev_induct_tac "ss" 1);
+by(Auto_tac);
+qed "apps_eq_Abs_conv";
+AddIffs [apps_eq_Abs_conv];
+
+Goal "!ss. ((Abs r)$$rs = (Abs s)$$ss) = (r=s & rs=ss)";
+by(rev_induct_tac "rs" 1);
+ by(Simp_tac 1);
+ by(Blast_tac 1);
+br allI 1;
+by(rev_induct_tac "ss" 1);
+by(Auto_tac);
+qed_spec_mp "Abs_apps_eq_Abs_apps_conv";
+AddIffs [Abs_apps_eq_Abs_apps_conv];
+
+Goal "!s t. Abs s $ t ~= (Var n)$$ss";
+by(rev_induct_tac "ss" 1);
+by(Auto_tac);
+qed_spec_mp "Abs_App_neq_Var_apps";
+AddIffs [Abs_App_neq_Var_apps];
+
+Goal "!ts. Var n $$ ts ~= (Abs r)$$ss";
+by(rev_induct_tac "ss" 1);
+ by(Simp_tac 1);
+br allI 1;
+by(rev_induct_tac "ts" 1);
+by(Auto_tac);
+qed_spec_mp "Var_apps_neq_Abs_apps";
+AddIffs [Var_apps_neq_Abs_apps];
+
+Goal "? ts h. t = h$$ts & ((? n. h = Var n) | (? u. h = Abs u))";
+by(induct_tac "t" 1);
+  by(res_inst_tac[("x","[]")] exI 1);
+  by(Simp_tac 1);
+ by(Clarify_tac 1);
+ by(rename_tac "ts1 ts2 h1 h2" 1);
+ by(res_inst_tac[("x","ts1@[h2$$ts2]")] exI 1);
+ by(Simp_tac 1);
+by(Simp_tac 1);
+qed "ex_head_tail";
+
+Goal "size(r$$rs) = size r + foldl (op +) 0 (map size rs) + length rs";
+by(rev_induct_tac "rs" 1);
+by(Auto_tac);
+qed "size_apps";
+Addsimps [size_apps];
+
+Goal "[| 0 < k; m <= n |] ==> m < n+k";
+by(exhaust_tac "k" 1);
+ by(Asm_full_simp_tac 1);
+by(Asm_full_simp_tac 1);
+br le_imp_less_Suc 1;
+by(exhaust_tac "n" 1);
+ by(Asm_full_simp_tac 1);
+by(hyp_subst_tac 1);
+be trans_le_add1 1;
+val lemma = result();
+
+(* a customized induction schema for $$ *)
+
+val prems = Goal
+"[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
+\   !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
+\|] ==> !t. size t = n --> P t";
+by(res_inst_tac [("n","n")] less_induct 1);
+br allI 1;
+by(cut_inst_tac [("t","t")] ex_head_tail 1);
+by(Clarify_tac 1);
+be disjE 1;
+ by(Clarify_tac 1);
+ brs prems 1;
+ by(Clarify_tac 1);
+ by(EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
+ by(Simp_tac 1);
+ br lemma 1;
+  by(Force_tac 1);
+ br elem_le_sum 1;
+ by(Force_tac 1);
+by(Clarify_tac 1);
+brs prems 1;
+by(EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
+by(Simp_tac 1);
+by(Clarify_tac 1);
+by(EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
+by(Simp_tac 1);
+br le_imp_less_Suc 1;
+br trans_le_add1 1;
+br trans_le_add2 1;
+br elem_le_sum 1;
+by(Force_tac 1);
+val lemma = result() RS spec RS mp;
+
+val prems = Goal
+"[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
+\   !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
+\|] ==> P t";
+by(res_inst_tac [("x1","t")] lemma 1);
+br refl 3;
+by(REPEAT(ares_tac prems 1));
+qed "Apps_dB_induct";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/ListApplication.thy	Thu Aug 06 10:33:54 1998 +0200
@@ -0,0 +1,14 @@
+(*  Title:      HOL/Lambda/ListApplication.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TU Muenchen
+
+Application of a term to a list of terms
+*)
+
+ListApplication = Lambda + List +
+
+syntax "$$" :: dB => dB list => dB (infixl 150)
+translations "t $$ ts" == "foldl op$ t ts"
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/ListBeta.ML	Thu Aug 06 10:33:54 1998 +0200
@@ -0,0 +1,97 @@
+(*  Title:      HOL/Lambda/ListBeta.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TU Muenchen
+*)
+
+Goal
+ "v -> v' ==> !rs. v = (Var n)$$rs --> (? ss. rs => ss & v' = (Var n)$$ss)";
+be beta.induct 1;
+by(Asm_full_simp_tac 1);
+br allI 1;
+by(res_inst_tac [("xs","rs")] rev_exhaust 1);
+by(Asm_full_simp_tac 1);
+by(force_tac (claset() addIs [append_step1I],simpset()) 1);
+br allI 1;
+by(res_inst_tac [("xs","rs")] rev_exhaust 1);
+by(Asm_full_simp_tac 1);
+by(force_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 1);
+by(Asm_full_simp_tac 1);
+val lemma = result();
+
+Goal "(Var n)$$rs -> v ==> (? ss. rs => ss & v = (Var n)$$ss)";
+bd lemma 1;
+by(Blast_tac 1);
+qed "head_Var_reduction";
+
+Goal "u -> u' ==> !r rs. u = r$$rs --> \
+\     ( (? r'. r -> r' & u' = r'$$rs) | \
+\       (? rs'. rs => rs' & u' = r$$rs') | \
+\       (? s t ts. r = Abs s & rs = t#ts & u' = s[t/0]$$ts))";
+be beta.induct 1;
+   by(clarify_tac (claset() delrules [disjCI]) 1);
+   by(exhaust_tac "r" 1);
+     by(Asm_full_simp_tac 1);
+    by(asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
+    by(split_asm_tac [split_if_asm] 1);
+     by(Asm_full_simp_tac 1);
+     by(Blast_tac 1);
+    by(Asm_full_simp_tac 1);
+   by(asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
+   by(split_asm_tac [split_if_asm] 1);
+    by(Asm_full_simp_tac 1);
+   by(Asm_full_simp_tac 1);
+  by(clarify_tac (claset() delrules [disjCI]) 1);
+  bd (App_eq_foldl_conv RS iffD1) 1;
+  by(split_asm_tac [split_if_asm] 1);
+   by(Asm_full_simp_tac 1);
+   by(Blast_tac 1);
+  by(force_tac (claset() addIs [disjI1 RS append_step1I],simpset()) 1);
+ by(clarify_tac (claset() delrules [disjCI]) 1);
+ bd (App_eq_foldl_conv RS iffD1) 1;
+ by(split_asm_tac [split_if_asm] 1);
+  by(Asm_full_simp_tac 1);
+  by(Blast_tac 1);
+ by(force_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 1);
+by(Asm_full_simp_tac 1);
+val lemma = result();
+
+Goal "[| r$$rs -> s; \
+\        !r'. r -> r' --> s = r'$$rs --> R; \
+\        !rs'. rs => rs' --> s = r$$rs' --> R; \
+\        !t u us. r = Abs t --> rs = u#us --> s = t[u/0]$$us --> R \
+\     |] ==> R";
+bd lemma 1;
+by(blast_tac HOL_cs 1);
+val lemma = result();
+bind_thm("apps_betasE",
+          impI RSN (4,impI RSN (4,impI RSN (4,allI RSN (4,allI RSN (4,allI RSN (4,
+          impI RSN (3,impI RSN (3,allI RSN (3,
+          impI RSN (2,impI RSN (2,allI RSN (2,lemma)))))))))))));
+AddSEs [apps_betasE];
+
+Goal "r -> s ==> r$$ss -> s$$ss";
+by(res_inst_tac [("xs","ss")] rev_induct 1);
+by(Auto_tac);
+qed "apps_preserves_beta";
+Addsimps [apps_preserves_beta];
+
+Goal "r ->> s ==> r$$ss ->> s$$ss";
+by(etac rtrancl_induct 1);
+ by(Blast_tac 1);
+by(blast_tac (claset() addIs [apps_preserves_beta,rtrancl_into_rtrancl]) 1);
+qed "apps_preserves_beta2";
+Addsimps [apps_preserves_beta2];
+
+Goal "!ss. rs => ss --> r$$rs -> r$$ss";
+by(res_inst_tac [("xs","rs")] rev_induct 1);
+ by(Asm_full_simp_tac 1);
+by(Asm_full_simp_tac 1);
+by(Clarify_tac 1);
+by(res_inst_tac [("xs","ss")] rev_exhaust 1);
+ by(Asm_full_simp_tac 1);
+by(Asm_full_simp_tac 1);
+bd Snoc_step1_SnocD 1;
+by(Blast_tac 1);
+qed_spec_mp "apps_preserves_betas";
+Addsimps [apps_preserves_betas];

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/ListBeta.thy	Thu Aug 06 10:33:54 1998 +0200
@@ -0,0 +1,14 @@
+(*  Title:      HOL/Lambda/ListBeta.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TU Muenchen
+
+Lifting beta-reduction to lists of terms, reducing exactly one element
+*)
+
+ListBeta = ListApplication + ListOrder +
+
+syntax "=>" :: dB => dB => bool (infixl 50)
+translations "rs => ss" == "(rs,ss) : step1 beta"
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/ListOrder.ML	Thu Aug 06 10:33:54 1998 +0200
@@ -0,0 +1,105 @@
+(*  Title:      HOL/Lambda/ListOrder.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TU Muenchen
+*)
+
+Goalw [step1_def] "step1(r^-1) = (step1 r)^-1";
+by(Blast_tac 1);
+qed "step1_converse";
+Addsimps [step1_converse];
+
+Goal "(p : step1(r^-1)) = (p : (step1 r)^-1)";
+by(Auto_tac);
+qed "in_step1_converse";
+AddIffs [in_step1_converse];
+
+Goalw [step1_def] "([],xs) ~: step1 r";
+by(Blast_tac 1);
+qed "not_Nil_step1";
+AddIffs [not_Nil_step1];
+
+Goalw [step1_def] "(xs,[]) ~: step1 r";
+by(Blast_tac 1);
+qed "not_step1_Nil";
+AddIffs [not_step1_Nil];
+
+Goalw [step1_def]
+  "((y#ys,x#xs) : step1 r) = ((y,x):r & xs=ys | x=y & (ys,xs) : step1 r)";
+by(Asm_full_simp_tac 1);
+br iffI 1;
+ be exE 1;
+ by(rename_tac "ts" 1);
+ by(exhaust_tac "ts" 1);
+  by(Force_tac 1);
+ by(Force_tac 1);
+be disjE 1;
+ by(Blast_tac 1);
+by(blast_tac (claset() addIs [Cons_eq_appendI]) 1);
+qed "Cons_step1_Cons";
+AddIffs [Cons_step1_Cons];
+
+Goalw [step1_def]
+ "(ys,xs) : step1 r & vs=us | ys=xs & (vs,us) : step1 r \
+\ ==> (ys@vs,xs@us) : step1 r";
+by(Auto_tac);
+by(Force_tac 1);
+by(blast_tac (claset() addIs [append_eq_appendI]) 1);
+qed "append_step1I";
+
+Goal "[| (ys,x#xs) : step1 r; \
+\        !y. ys = y#xs --> (y,x) : r --> R; \
+\        !zs. ys = x#zs --> (zs,xs) : step1 r --> R \
+\     |] ==> R";
+by(exhaust_tac "ys" 1);
+ by(asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
+by(Blast_tac 1);
+val lemma = result();
+bind_thm("Cons_step1E",
+          impI RSN (3,impI RSN (3,allI RSN (3,impI RSN (2,
+          impI RSN (2,allI RSN (2,lemma)))))));
+AddSEs [Cons_step1E];
+
+Goalw [step1_def]
+ "(ys@[y],xs@[x]) : step1 r ==> ((ys,xs) : step1 r & y=x | ys=xs & (y,x) : r)";
+by(Asm_full_simp_tac 1);
+by(clarify_tac (claset() delrules [disjCI]) 1);
+by(rename_tac "vs" 1);
+by(res_inst_tac [("xs","vs")]rev_exhaust 1);
+ by(Force_tac 1);
+by(Asm_full_simp_tac 1);
+by(Blast_tac 1);
+qed "Snoc_step1_SnocD";
+
+Goal "x : acc r ==> !xs. xs : acc(step1 r) --> x#xs : acc(step1 r)";
+be acc_induct 1;
+be thin_rl 1;
+by(Clarify_tac 1);
+be acc_induct 1;
+br accI 1;
+by(Blast_tac 1);
+val lemma = result();
+qed_spec_mp "Cons_acc_step1I";
+AddSIs [Cons_acc_step1I];
+
+Goal "xs : lists(acc r) ==> xs : acc(step1 r)";
+be lists.induct 1;
+ br accI 1;
+ by(asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
+br accI 1;
+by(fast_tac (claset() addDs [acc_downward]) 1);
+qed "lists_accD";
+
+Goalw [step1_def]
+ "[| x : set xs; (y,x) : r |] ==> ? ys. (ys,xs) : step1 r & y : set ys";
+bd (in_set_conv_decomp RS iffD1) 1;
+by(Force_tac 1);
+qed "ex_step1I";
+
+Goal "xs : acc(step1 r) ==> xs : lists(acc r)";
+be acc_induct 1;
+by(Clarify_tac 1);
+br accI 1;
+by(EVERY1[dtac ex_step1I, atac]);
+by(Blast_tac 1);
+qed "lists_accI";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/ListOrder.thy	Thu Aug 06 10:33:54 1998 +0200
@@ -0,0 +1,16 @@
+(*  Title:      HOL/Lambda/ListOrder.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TU Muenchen
+
+Lifting an order to lists of elements, relating exactly one element
+*)
+
+ListOrder = List + Acc +
+
+constdefs
+ step1 :: "('a * 'a)set => ('a list * 'a list)set"
+"step1 r ==
+   {(ys,xs). ? us z z' vs. xs = us@z#vs & (z',z) : r & ys = us@z'#vs}"
+
+end

--- a/src/HOL/Lambda/ROOT.ML	Thu Aug 06 10:28:44 1998 +0200
+++ b/src/HOL/Lambda/ROOT.ML	Thu Aug 06 10:33:54 1998 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Lambda/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1995 TUM
+    Copyright   1998 TUM
 *)
 
 HOL_build_completed;    (*Make examples fail if HOL did*)
@@ -9,3 +9,5 @@
 writeln"Root file for HOL/Lambda";
 
 time_use_thy "Eta";
+loadpath := [".","../Induct"];
+time_use_thy "InductTermi";