First steps towards termination of simply typed terms.
authornipkow
Thu Aug 06 10:33:54 1998 +0200 (1998-08-06)
changeset 5261ce3c25c8a694
parent 5260 1835a591d3a7
child 5262 212d203d6cd3
First steps towards termination of simply typed terms.
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/InductTermi.ML
src/HOL/Lambda/InductTermi.thy
src/HOL/Lambda/Lambda.ML
src/HOL/Lambda/ListApplication.ML
src/HOL/Lambda/ListApplication.thy
src/HOL/Lambda/ListBeta.ML
src/HOL/Lambda/ListBeta.thy
src/HOL/Lambda/ListOrder.ML
src/HOL/Lambda/ListOrder.thy
src/HOL/Lambda/ROOT.ML
     1.1 --- a/src/HOL/Lambda/Eta.ML	Thu Aug 06 10:28:44 1998 +0200
     1.2 +++ b/src/HOL/Lambda/Eta.ML	Thu Aug 06 10:33:54 1998 +0200
     1.3 @@ -9,18 +9,12 @@
     1.4  confluence of beta+eta
     1.5  *)
     1.6  
     1.7 -open Eta;
     1.8 -
     1.9  Addsimps eta.intrs;
    1.10 +AddIs eta.intrs;
    1.11  
    1.12  val eta_cases = map (eta.mk_cases dB.simps)
    1.13      ["Abs s -e> z","s $ t -e> u","Var i -e> t"];
    1.14 -
    1.15 -val beta_cases = map (beta.mk_cases dB.simps)
    1.16 -    ["s $ t -> u","Var i -> t"];
    1.17 -
    1.18 -AddIs eta.intrs;
    1.19 -AddSEs (beta_cases@eta_cases);
    1.20 +AddSEs eta_cases;
    1.21  
    1.22  section "eta, subst and free";
    1.23  
    1.24 @@ -177,11 +171,11 @@
    1.25    by (rtac notE 1);
    1.26     by (assume_tac 2);
    1.27    by (etac thin_rl 1);
    1.28 -  by (res_inst_tac [("dB","t")] dB_case_distinction 1);
    1.29 -    by (Simp_tac 1);
    1.30 +  by (exhaust_tac "t" 1);
    1.31 +    by (Asm_simp_tac 1);
    1.32      by (blast_tac (HOL_cs addDs [less_not_refl2]) 1);
    1.33 -   by (Simp_tac 1);
    1.34 -  by (Simp_tac 1);
    1.35 +   by (Asm_simp_tac 1);
    1.36 +  by (Asm_simp_tac 1);
    1.37   by (Asm_simp_tac 1);
    1.38   by (etac thin_rl 1);
    1.39   by (etac thin_rl 1);
    1.40 @@ -193,11 +187,11 @@
    1.41    by (Asm_simp_tac 1);
    1.42   by (etac exE 1);
    1.43   by (etac rev_mp 1);
    1.44 - by (res_inst_tac [("dB","t")] dB_case_distinction 1);
    1.45 -   by (Simp_tac 1);
    1.46 -  by (Simp_tac 1);
    1.47 + by (exhaust_tac "t" 1);
    1.48 +   by (Asm_simp_tac 1);
    1.49 +  by (Asm_simp_tac 1);
    1.50    by (Blast_tac 1);
    1.51 - by (Simp_tac 1);
    1.52 + by (Asm_simp_tac 1);
    1.53  by (Asm_simp_tac 1);
    1.54  by (etac thin_rl 1);
    1.55  by (rtac allI 1);
    1.56 @@ -207,10 +201,10 @@
    1.57   by (Asm_simp_tac 1);
    1.58  by (etac exE 1);
    1.59  by (etac rev_mp 1);
    1.60 -by (res_inst_tac [("dB","t")] dB_case_distinction 1);
    1.61 -  by (Simp_tac 1);
    1.62 - by (Simp_tac 1);
    1.63 -by (Simp_tac 1);
    1.64 +by (exhaust_tac "t" 1);
    1.65 +  by (Asm_simp_tac 1);
    1.66 + by (Asm_simp_tac 1);
    1.67 +by (Asm_simp_tac 1);
    1.68  by (Blast_tac 1);
    1.69  qed_spec_mp "not_free_iff_lifted";
    1.70  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Lambda/InductTermi.ML	Thu Aug 06 10:33:54 1998 +0200
     2.3 @@ -0,0 +1,130 @@
     2.4 +(*** Every term in IT terminates ***)
     2.5 +
     2.6 +Goal "s : termi beta ==> !t. t : termi beta --> \
     2.7 +\     (!r ss. t = r[s/0]$$ss --> Abs r $ s $$ ss : termi beta)";
     2.8 +be acc_induct 1;
     2.9 +be thin_rl 1;
    2.10 +br allI 1;
    2.11 +br impI 1;
    2.12 +be acc_induct 1;
    2.13 +by(Clarify_tac 1);
    2.14 +br accI 1;
    2.15 +by(safe_tac (claset() addSEs [apps_betasE]));
    2.16 +   ba 1;
    2.17 +  by(blast_tac (claset() addIs [subst_preserves_beta,apps_preserves_beta]) 1);
    2.18 + by(blast_tac (claset()
    2.19 +    addIs [apps_preserves_beta2,subst_preserves_beta2,rtrancl_converseI]
    2.20 +    addDs [acc_downwards]) 1);
    2.21 +(* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
    2.22 +by(blast_tac (claset() addDs [apps_preserves_betas]) 1);
    2.23 +qed_spec_mp "double_induction_lemma";
    2.24 +
    2.25 +Goal "t : IT ==> t : termi(beta)";
    2.26 +be IT.induct 1;
    2.27 +  bd rev_subsetD 1;
    2.28 +   br lists_mono 1;
    2.29 +   br Int_lower2 1;
    2.30 +  by(Asm_full_simp_tac 1);
    2.31 +  bd lists_accD 1;
    2.32 +  be acc_induct 1;
    2.33 +  br accI 1;
    2.34 +  by(blast_tac (claset() addSDs [head_Var_reduction]) 1);
    2.35 + be acc_induct 1;
    2.36 + br accI 1;
    2.37 + by(Blast_tac 1);
    2.38 +by(blast_tac (claset() addIs [double_induction_lemma]) 1);
    2.39 +qed "IT_implies_termi";
    2.40 +
    2.41 +(*** Every terminating term is in IT ***)
    2.42 +
    2.43 +val IT_cases = map (IT.mk_cases
    2.44 + ([Var_apps_eq_Var_apps_conv, Abs_eq_apps_conv, apps_eq_Abs_conv,
    2.45 +   Abs_apps_eq_Abs_apps_conv,
    2.46 +   Var_apps_neq_Abs_apps, Var_apps_neq_Abs_apps RS not_sym,
    2.47 +   hd(tl(get_thms List.thy "foldl.simps")) RS sym ]
    2.48 +  @ dB.simps @ list.simps))
    2.49 +    ["Var n $$ ss : IT", "Abs t : IT", "Abs r $ s $$ ts : IT"];
    2.50 +AddSEs IT_cases;
    2.51 +
    2.52 +(* FIXME
    2.53 +"Arith.trans_less_add1",   "?i < ?j ==> ?i < ?j + ?m"
    2.54 +"Arith.less_imp_add_less", "?m < ?n ==> ?m < ?n + ?k"
    2.55 +"Arith.trans_le_add1", "?i <= ?j ==> ?i <= ?j + ?m"
    2.56 +"Arith.le_imp_add_le", "?m <= ?n ==> ?m <= ?n + ?k"
    2.57 +*)
    2.58 +
    2.59 +Goal "t : termi beta ==> \
    2.60 +\     !r rs. t = r$$rs --> r : termi beta & rs : termi(step1 beta)";
    2.61 +be acc_induct 1;
    2.62 +by(force_tac (claset()
    2.63 +     addIs [apps_preserves_beta,apps_preserves_betas,accI],simpset()) 1);
    2.64 +val lemma = result();
    2.65 +
    2.66 +Goal "r$$rs : termi beta ==> r : termi beta & rs : termi(step1 beta)";
    2.67 +bd lemma 1;
    2.68 +by(Blast_tac 1);
    2.69 +qed "apps_in_termi_betaD";
    2.70 +
    2.71 +Goal "t : termi beta ==> !r. t = Abs r --> r : termi beta";
    2.72 +be acc_induct 1;
    2.73 +by(force_tac (claset() addIs [accI],simpset()) 1);
    2.74 +val lemma = result();
    2.75 +
    2.76 +Goal "Abs r : termi beta ==> r : termi beta";
    2.77 +bd lemma 1;
    2.78 +by(Blast_tac 1);
    2.79 +qed "Abs_in_termi_betaD";
    2.80 +
    2.81 +Goal "t : termi beta ==> !r s. t = r$s --> r : termi beta & s : termi beta";
    2.82 +be acc_induct 1;
    2.83 +by(force_tac (claset() addIs [accI],simpset()) 1);
    2.84 +val lemma = result();
    2.85 +
    2.86 +Goal "r$s : termi beta ==> r : termi beta & s : termi beta";
    2.87 +bd lemma 1;
    2.88 +by(Blast_tac 1);
    2.89 +qed "App_in_termi_betaD";
    2.90 +
    2.91 +
    2.92 +Goal "r : termi beta ==> r : IT";
    2.93 +be acc_induct 1;
    2.94 +by(rename_tac "r" 1);
    2.95 +be rev_mp 1;
    2.96 +be rev_mp 1;
    2.97 +by(Simp_tac 1);
    2.98 +by(res_inst_tac [("t","r")] Apps_dB_induct 1);
    2.99 + by(rename_tac "n ts" 1);
   2.100 + by(Clarify_tac 1);
   2.101 + brs IT.intrs 1;
   2.102 + by(Clarify_tac 1);
   2.103 + by(EVERY1[dtac bspec, atac]);
   2.104 + by(EVERY[etac impE 1, etac mp 2]);
   2.105 +  by(Clarify_tac 1);
   2.106 +  bd converseI 1;
   2.107 +  by(EVERY1[dtac ex_step1I, atac]);
   2.108 +  by(Clarify_tac 1);
   2.109 +  by(rename_tac "us" 1);
   2.110 +  by(eres_inst_tac [("x","Var n $$ us")] allE 1);
   2.111 +  by(Force_tac 1);
   2.112 + bd apps_in_termi_betaD 1;
   2.113 + by(asm_full_simp_tac (simpset() delsimps [step1_converse]
   2.114 +                                 addsimps [step1_converse RS sym]) 1);
   2.115 + by(blast_tac (claset() addDs [lists_accI]) 1);
   2.116 +by(rename_tac "u ts" 1);
   2.117 +by(exhaust_tac "ts" 1);
   2.118 + by(Asm_full_simp_tac 1);
   2.119 + by(Clarify_tac 1);
   2.120 + brs IT.intrs 1;
   2.121 + by(blast_tac (claset() addDs [Abs_in_termi_betaD]) 1);
   2.122 +by(rename_tac "s ss" 1);
   2.123 +by(Asm_full_simp_tac 1);
   2.124 +by(Clarify_tac 1);
   2.125 +brs IT.intrs 1;
   2.126 + by(blast_tac (claset() addIs [apps_preserves_beta]) 1);
   2.127 +by(EVERY[etac impE 1, etac mp 2]);
   2.128 + by(Clarify_tac 1);
   2.129 + by(rename_tac "t" 1);
   2.130 + by(eres_inst_tac [("x","Abs u $ t $$ ss")] allE 1);
   2.131 + by(Force_tac 1);
   2.132 +by(blast_tac (claset() addSDs [apps_in_termi_betaD, App_in_termi_betaD]) 1);
   2.133 +qed "termi_implies_IT";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Lambda/InductTermi.thy	Thu Aug 06 10:33:54 1998 +0200
     3.3 @@ -0,0 +1,22 @@
     3.4 +(*  Title:      HOL/Lambda/InductTermi.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Tobias Nipkow
     3.7 +    Copyright   1998 TU Muenchen
     3.8 +
     3.9 +Inductive characterization of terminating lambda terms.
    3.10 +Goes back to
    3.11 +Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995.
    3.12 +Also rediscovered by Matthes and Joachimski.
    3.13 +*)
    3.14 +
    3.15 +InductTermi = Acc + ListBeta +
    3.16 +
    3.17 +consts IT :: dB set
    3.18 +inductive IT
    3.19 +intrs
    3.20 +VarI "rs : lists IT ==> (Var n)$$rs : IT"
    3.21 +LambdaI "r : IT ==> Abs r : IT"
    3.22 +BetaI "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT"
    3.23 +monos "[lists_mono]"
    3.24 +
    3.25 +end
     4.1 --- a/src/HOL/Lambda/Lambda.ML	Thu Aug 06 10:28:44 1998 +0200
     4.2 +++ b/src/HOL/Lambda/Lambda.ML	Thu Aug 06 10:33:54 1998 +0200
     4.3 @@ -8,7 +8,9 @@
     4.4  
     4.5  (*** Lambda ***)
     4.6  
     4.7 -open Lambda;
     4.8 +val beta_cases = map (beta.mk_cases dB.simps)
     4.9 +    ["Var i -> t", "Abs r -> s", "s $ t -> u"];
    4.10 +AddSEs beta_cases;
    4.11  
    4.12  Delsimps [subst_Var];
    4.13  Addsimps ([if_not_P, not_less_eq] @ beta.intrs);
    4.14 @@ -16,9 +18,6 @@
    4.15  (* don't add r_into_rtrancl! *)
    4.16  AddSIs beta.intrs;
    4.17  
    4.18 -val dB_case_distinction =
    4.19 -  rule_by_tactic(EVERY[etac thin_rl 2,etac thin_rl 2,etac thin_rl 3])dB.induct;
    4.20 -
    4.21  (*** Congruence rules for ->> ***)
    4.22  
    4.23  Goal "s ->> s' ==> Abs s ->> Abs s'";
    4.24 @@ -135,3 +134,26 @@
    4.25  Goal "substn t s 0 = t[s/0]";
    4.26  by (Simp_tac 1);
    4.27  qed "substn_subst_0";
    4.28 +
    4.29 +(*** Preservation thms ***)
    4.30 +(* Not used in CR-proof but in SN-proof *)
    4.31 +
    4.32 +Goal "r -> s ==> !t i. r[t/i] -> s[t/i]";
    4.33 +be beta.induct 1;
    4.34 +by(ALLGOALS (asm_simp_tac (simpset() addsimps [subst_subst RS sym])));
    4.35 +qed_spec_mp "subst_preserves_beta";
    4.36 +Addsimps [subst_preserves_beta];
    4.37 +
    4.38 +Goal "r -> s ==> !i. lift r i -> lift s i";
    4.39 +be beta.induct 1;
    4.40 +by(Auto_tac);
    4.41 +qed_spec_mp "lift_preserves_beta";
    4.42 +Addsimps [lift_preserves_beta];
    4.43 +
    4.44 +Goal "!r s i. r -> s --> t[r/i] ->> t[s/i]";
    4.45 +by(induct_tac "t" 1);
    4.46 +by(asm_simp_tac (addsplit(simpset() addsimps [r_into_rtrancl])) 1);
    4.47 +by(asm_simp_tac (simpset() addsimps [rtrancl_beta_App]) 1);
    4.48 +by(asm_simp_tac (simpset() addsimps [rtrancl_beta_Abs]) 1);
    4.49 +qed_spec_mp "subst_preserves_beta2";
    4.50 +Addsimps [subst_preserves_beta2];
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Lambda/ListApplication.ML	Thu Aug 06 10:33:54 1998 +0200
     5.3 @@ -0,0 +1,142 @@
     5.4 +(*  Title:      HOL/Lambda/ListApplication.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Tobias Nipkow
     5.7 +    Copyright   1998 TU Muenchen
     5.8 +*)
     5.9 +
    5.10 +Goal "(r$$ts = s$$ts) = (r = s)";
    5.11 +by(rev_induct_tac "ts" 1);
    5.12 +by(Auto_tac);
    5.13 +qed "apps_eq_tail_conv";
    5.14 +AddIffs [apps_eq_tail_conv];
    5.15 +
    5.16 +Goal "!s. (Var m = s$$ss) = (Var m = s & ss = [])";
    5.17 +by(induct_tac "ss" 1);
    5.18 +by(Auto_tac);
    5.19 +qed_spec_mp "Var_eq_apps_conv";
    5.20 +AddIffs [Var_eq_apps_conv];
    5.21 +
    5.22 +Goal "!ss. ((Var m)$$rs = (Var n)$$ss) = (m=n & rs=ss)";
    5.23 +by(rev_induct_tac "rs" 1);
    5.24 + by(Simp_tac 1);
    5.25 + by(Blast_tac 1);
    5.26 +br allI 1;
    5.27 +by(rev_induct_tac "ss" 1);
    5.28 +by(Auto_tac);
    5.29 +qed_spec_mp "Var_apps_eq_Var_apps_conv";
    5.30 +AddIffs [Var_apps_eq_Var_apps_conv];
    5.31 +
    5.32 +Goal "(r$s = t$$ts) = \
    5.33 +\     (if ts = [] then r$s = t \
    5.34 +\      else (? ss. ts = ss@[s] & r = t$$ss))";
    5.35 +by(res_inst_tac [("xs","ts")] rev_exhaust 1);
    5.36 +by(Auto_tac);
    5.37 +qed "App_eq_foldl_conv";
    5.38 +
    5.39 +Goal "(Abs r = s$$ss) = (Abs r = s & ss=[])";
    5.40 +by(rev_induct_tac "ss" 1);
    5.41 +by(Auto_tac);
    5.42 +qed "Abs_eq_apps_conv";
    5.43 +AddIffs [Abs_eq_apps_conv];
    5.44 +
    5.45 +Goal "(s$$ss = Abs r) = (s = Abs r & ss=[])";
    5.46 +by(rev_induct_tac "ss" 1);
    5.47 +by(Auto_tac);
    5.48 +qed "apps_eq_Abs_conv";
    5.49 +AddIffs [apps_eq_Abs_conv];
    5.50 +
    5.51 +Goal "!ss. ((Abs r)$$rs = (Abs s)$$ss) = (r=s & rs=ss)";
    5.52 +by(rev_induct_tac "rs" 1);
    5.53 + by(Simp_tac 1);
    5.54 + by(Blast_tac 1);
    5.55 +br allI 1;
    5.56 +by(rev_induct_tac "ss" 1);
    5.57 +by(Auto_tac);
    5.58 +qed_spec_mp "Abs_apps_eq_Abs_apps_conv";
    5.59 +AddIffs [Abs_apps_eq_Abs_apps_conv];
    5.60 +
    5.61 +Goal "!s t. Abs s $ t ~= (Var n)$$ss";
    5.62 +by(rev_induct_tac "ss" 1);
    5.63 +by(Auto_tac);
    5.64 +qed_spec_mp "Abs_App_neq_Var_apps";
    5.65 +AddIffs [Abs_App_neq_Var_apps];
    5.66 +
    5.67 +Goal "!ts. Var n $$ ts ~= (Abs r)$$ss";
    5.68 +by(rev_induct_tac "ss" 1);
    5.69 + by(Simp_tac 1);
    5.70 +br allI 1;
    5.71 +by(rev_induct_tac "ts" 1);
    5.72 +by(Auto_tac);
    5.73 +qed_spec_mp "Var_apps_neq_Abs_apps";
    5.74 +AddIffs [Var_apps_neq_Abs_apps];
    5.75 +
    5.76 +Goal "? ts h. t = h$$ts & ((? n. h = Var n) | (? u. h = Abs u))";
    5.77 +by(induct_tac "t" 1);
    5.78 +  by(res_inst_tac[("x","[]")] exI 1);
    5.79 +  by(Simp_tac 1);
    5.80 + by(Clarify_tac 1);
    5.81 + by(rename_tac "ts1 ts2 h1 h2" 1);
    5.82 + by(res_inst_tac[("x","ts1@[h2$$ts2]")] exI 1);
    5.83 + by(Simp_tac 1);
    5.84 +by(Simp_tac 1);
    5.85 +qed "ex_head_tail";
    5.86 +
    5.87 +Goal "size(r$$rs) = size r + foldl (op +) 0 (map size rs) + length rs";
    5.88 +by(rev_induct_tac "rs" 1);
    5.89 +by(Auto_tac);
    5.90 +qed "size_apps";
    5.91 +Addsimps [size_apps];
    5.92 +
    5.93 +Goal "[| 0 < k; m <= n |] ==> m < n+k";
    5.94 +by(exhaust_tac "k" 1);
    5.95 + by(Asm_full_simp_tac 1);
    5.96 +by(Asm_full_simp_tac 1);
    5.97 +br le_imp_less_Suc 1;
    5.98 +by(exhaust_tac "n" 1);
    5.99 + by(Asm_full_simp_tac 1);
   5.100 +by(hyp_subst_tac 1);
   5.101 +be trans_le_add1 1;
   5.102 +val lemma = result();
   5.103 +
   5.104 +(* a customized induction schema for $$ *)
   5.105 +
   5.106 +val prems = Goal
   5.107 +"[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
   5.108 +\   !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
   5.109 +\|] ==> !t. size t = n --> P t";
   5.110 +by(res_inst_tac [("n","n")] less_induct 1);
   5.111 +br allI 1;
   5.112 +by(cut_inst_tac [("t","t")] ex_head_tail 1);
   5.113 +by(Clarify_tac 1);
   5.114 +be disjE 1;
   5.115 + by(Clarify_tac 1);
   5.116 + brs prems 1;
   5.117 + by(Clarify_tac 1);
   5.118 + by(EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
   5.119 + by(Simp_tac 1);
   5.120 + br lemma 1;
   5.121 +  by(Force_tac 1);
   5.122 + br elem_le_sum 1;
   5.123 + by(Force_tac 1);
   5.124 +by(Clarify_tac 1);
   5.125 +brs prems 1;
   5.126 +by(EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
   5.127 +by(Simp_tac 1);
   5.128 +by(Clarify_tac 1);
   5.129 +by(EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
   5.130 +by(Simp_tac 1);
   5.131 +br le_imp_less_Suc 1;
   5.132 +br trans_le_add1 1;
   5.133 +br trans_le_add2 1;
   5.134 +br elem_le_sum 1;
   5.135 +by(Force_tac 1);
   5.136 +val lemma = result() RS spec RS mp;
   5.137 +
   5.138 +val prems = Goal
   5.139 +"[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
   5.140 +\   !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
   5.141 +\|] ==> P t";
   5.142 +by(res_inst_tac [("x1","t")] lemma 1);
   5.143 +br refl 3;
   5.144 +by(REPEAT(ares_tac prems 1));
   5.145 +qed "Apps_dB_induct";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Lambda/ListApplication.thy	Thu Aug 06 10:33:54 1998 +0200
     6.3 @@ -0,0 +1,14 @@
     6.4 +(*  Title:      HOL/Lambda/ListApplication.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Tobias Nipkow
     6.7 +    Copyright   1998 TU Muenchen
     6.8 +
     6.9 +Application of a term to a list of terms
    6.10 +*)
    6.11 +
    6.12 +ListApplication = Lambda + List +
    6.13 +
    6.14 +syntax "$$" :: dB => dB list => dB (infixl 150)
    6.15 +translations "t $$ ts" == "foldl op$ t ts"
    6.16 +
    6.17 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Lambda/ListBeta.ML	Thu Aug 06 10:33:54 1998 +0200
     7.3 @@ -0,0 +1,97 @@
     7.4 +(*  Title:      HOL/Lambda/ListBeta.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Tobias Nipkow
     7.7 +    Copyright   1998 TU Muenchen
     7.8 +*)
     7.9 +
    7.10 +Goal
    7.11 + "v -> v' ==> !rs. v = (Var n)$$rs --> (? ss. rs => ss & v' = (Var n)$$ss)";
    7.12 +be beta.induct 1;
    7.13 +by(Asm_full_simp_tac 1);
    7.14 +br allI 1;
    7.15 +by(res_inst_tac [("xs","rs")] rev_exhaust 1);
    7.16 +by(Asm_full_simp_tac 1);
    7.17 +by(force_tac (claset() addIs [append_step1I],simpset()) 1);
    7.18 +br allI 1;
    7.19 +by(res_inst_tac [("xs","rs")] rev_exhaust 1);
    7.20 +by(Asm_full_simp_tac 1);
    7.21 +by(force_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 1);
    7.22 +by(Asm_full_simp_tac 1);
    7.23 +val lemma = result();
    7.24 +
    7.25 +Goal "(Var n)$$rs -> v ==> (? ss. rs => ss & v = (Var n)$$ss)";
    7.26 +bd lemma 1;
    7.27 +by(Blast_tac 1);
    7.28 +qed "head_Var_reduction";
    7.29 +
    7.30 +Goal "u -> u' ==> !r rs. u = r$$rs --> \
    7.31 +\     ( (? r'. r -> r' & u' = r'$$rs) | \
    7.32 +\       (? rs'. rs => rs' & u' = r$$rs') | \
    7.33 +\       (? s t ts. r = Abs s & rs = t#ts & u' = s[t/0]$$ts))";
    7.34 +be beta.induct 1;
    7.35 +   by(clarify_tac (claset() delrules [disjCI]) 1);
    7.36 +   by(exhaust_tac "r" 1);
    7.37 +     by(Asm_full_simp_tac 1);
    7.38 +    by(asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
    7.39 +    by(split_asm_tac [split_if_asm] 1);
    7.40 +     by(Asm_full_simp_tac 1);
    7.41 +     by(Blast_tac 1);
    7.42 +    by(Asm_full_simp_tac 1);
    7.43 +   by(asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
    7.44 +   by(split_asm_tac [split_if_asm] 1);
    7.45 +    by(Asm_full_simp_tac 1);
    7.46 +   by(Asm_full_simp_tac 1);
    7.47 +  by(clarify_tac (claset() delrules [disjCI]) 1);
    7.48 +  bd (App_eq_foldl_conv RS iffD1) 1;
    7.49 +  by(split_asm_tac [split_if_asm] 1);
    7.50 +   by(Asm_full_simp_tac 1);
    7.51 +   by(Blast_tac 1);
    7.52 +  by(force_tac (claset() addIs [disjI1 RS append_step1I],simpset()) 1);
    7.53 + by(clarify_tac (claset() delrules [disjCI]) 1);
    7.54 + bd (App_eq_foldl_conv RS iffD1) 1;
    7.55 + by(split_asm_tac [split_if_asm] 1);
    7.56 +  by(Asm_full_simp_tac 1);
    7.57 +  by(Blast_tac 1);
    7.58 + by(force_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 1);
    7.59 +by(Asm_full_simp_tac 1);
    7.60 +val lemma = result();
    7.61 +
    7.62 +Goal "[| r$$rs -> s; \
    7.63 +\        !r'. r -> r' --> s = r'$$rs --> R; \
    7.64 +\        !rs'. rs => rs' --> s = r$$rs' --> R; \
    7.65 +\        !t u us. r = Abs t --> rs = u#us --> s = t[u/0]$$us --> R \
    7.66 +\     |] ==> R";
    7.67 +bd lemma 1;
    7.68 +by(blast_tac HOL_cs 1);
    7.69 +val lemma = result();
    7.70 +bind_thm("apps_betasE",
    7.71 +          impI RSN (4,impI RSN (4,impI RSN (4,allI RSN (4,allI RSN (4,allI RSN (4,
    7.72 +          impI RSN (3,impI RSN (3,allI RSN (3,
    7.73 +          impI RSN (2,impI RSN (2,allI RSN (2,lemma)))))))))))));
    7.74 +AddSEs [apps_betasE];
    7.75 +
    7.76 +Goal "r -> s ==> r$$ss -> s$$ss";
    7.77 +by(res_inst_tac [("xs","ss")] rev_induct 1);
    7.78 +by(Auto_tac);
    7.79 +qed "apps_preserves_beta";
    7.80 +Addsimps [apps_preserves_beta];
    7.81 +
    7.82 +Goal "r ->> s ==> r$$ss ->> s$$ss";
    7.83 +by(etac rtrancl_induct 1);
    7.84 + by(Blast_tac 1);
    7.85 +by(blast_tac (claset() addIs [apps_preserves_beta,rtrancl_into_rtrancl]) 1);
    7.86 +qed "apps_preserves_beta2";
    7.87 +Addsimps [apps_preserves_beta2];
    7.88 +
    7.89 +Goal "!ss. rs => ss --> r$$rs -> r$$ss";
    7.90 +by(res_inst_tac [("xs","rs")] rev_induct 1);
    7.91 + by(Asm_full_simp_tac 1);
    7.92 +by(Asm_full_simp_tac 1);
    7.93 +by(Clarify_tac 1);
    7.94 +by(res_inst_tac [("xs","ss")] rev_exhaust 1);
    7.95 + by(Asm_full_simp_tac 1);
    7.96 +by(Asm_full_simp_tac 1);
    7.97 +bd Snoc_step1_SnocD 1;
    7.98 +by(Blast_tac 1);
    7.99 +qed_spec_mp "apps_preserves_betas";
   7.100 +Addsimps [apps_preserves_betas];
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Lambda/ListBeta.thy	Thu Aug 06 10:33:54 1998 +0200
     8.3 @@ -0,0 +1,14 @@
     8.4 +(*  Title:      HOL/Lambda/ListBeta.thy
     8.5 +    ID:         $Id$
     8.6 +    Author:     Tobias Nipkow
     8.7 +    Copyright   1998 TU Muenchen
     8.8 +
     8.9 +Lifting beta-reduction to lists of terms, reducing exactly one element
    8.10 +*)
    8.11 +
    8.12 +ListBeta = ListApplication + ListOrder +
    8.13 +
    8.14 +syntax "=>" :: dB => dB => bool (infixl 50)
    8.15 +translations "rs => ss" == "(rs,ss) : step1 beta"
    8.16 +
    8.17 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Lambda/ListOrder.ML	Thu Aug 06 10:33:54 1998 +0200
     9.3 @@ -0,0 +1,105 @@
     9.4 +(*  Title:      HOL/Lambda/ListOrder.ML
     9.5 +    ID:         $Id$
     9.6 +    Author:     Tobias Nipkow
     9.7 +    Copyright   1998 TU Muenchen
     9.8 +*)
     9.9 +
    9.10 +Goalw [step1_def] "step1(r^-1) = (step1 r)^-1";
    9.11 +by(Blast_tac 1);
    9.12 +qed "step1_converse";
    9.13 +Addsimps [step1_converse];
    9.14 +
    9.15 +Goal "(p : step1(r^-1)) = (p : (step1 r)^-1)";
    9.16 +by(Auto_tac);
    9.17 +qed "in_step1_converse";
    9.18 +AddIffs [in_step1_converse];
    9.19 +
    9.20 +Goalw [step1_def] "([],xs) ~: step1 r";
    9.21 +by(Blast_tac 1);
    9.22 +qed "not_Nil_step1";
    9.23 +AddIffs [not_Nil_step1];
    9.24 +
    9.25 +Goalw [step1_def] "(xs,[]) ~: step1 r";
    9.26 +by(Blast_tac 1);
    9.27 +qed "not_step1_Nil";
    9.28 +AddIffs [not_step1_Nil];
    9.29 +
    9.30 +Goalw [step1_def]
    9.31 +  "((y#ys,x#xs) : step1 r) = ((y,x):r & xs=ys | x=y & (ys,xs) : step1 r)";
    9.32 +by(Asm_full_simp_tac 1);
    9.33 +br iffI 1;
    9.34 + be exE 1;
    9.35 + by(rename_tac "ts" 1);
    9.36 + by(exhaust_tac "ts" 1);
    9.37 +  by(Force_tac 1);
    9.38 + by(Force_tac 1);
    9.39 +be disjE 1;
    9.40 + by(Blast_tac 1);
    9.41 +by(blast_tac (claset() addIs [Cons_eq_appendI]) 1);
    9.42 +qed "Cons_step1_Cons";
    9.43 +AddIffs [Cons_step1_Cons];
    9.44 +
    9.45 +Goalw [step1_def]
    9.46 + "(ys,xs) : step1 r & vs=us | ys=xs & (vs,us) : step1 r \
    9.47 +\ ==> (ys@vs,xs@us) : step1 r";
    9.48 +by(Auto_tac);
    9.49 +by(Force_tac 1);
    9.50 +by(blast_tac (claset() addIs [append_eq_appendI]) 1);
    9.51 +qed "append_step1I";
    9.52 +
    9.53 +Goal "[| (ys,x#xs) : step1 r; \
    9.54 +\        !y. ys = y#xs --> (y,x) : r --> R; \
    9.55 +\        !zs. ys = x#zs --> (zs,xs) : step1 r --> R \
    9.56 +\     |] ==> R";
    9.57 +by(exhaust_tac "ys" 1);
    9.58 + by(asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
    9.59 +by(Blast_tac 1);
    9.60 +val lemma = result();
    9.61 +bind_thm("Cons_step1E",
    9.62 +          impI RSN (3,impI RSN (3,allI RSN (3,impI RSN (2,
    9.63 +          impI RSN (2,allI RSN (2,lemma)))))));
    9.64 +AddSEs [Cons_step1E];
    9.65 +
    9.66 +Goalw [step1_def]
    9.67 + "(ys@[y],xs@[x]) : step1 r ==> ((ys,xs) : step1 r & y=x | ys=xs & (y,x) : r)";
    9.68 +by(Asm_full_simp_tac 1);
    9.69 +by(clarify_tac (claset() delrules [disjCI]) 1);
    9.70 +by(rename_tac "vs" 1);
    9.71 +by(res_inst_tac [("xs","vs")]rev_exhaust 1);
    9.72 + by(Force_tac 1);
    9.73 +by(Asm_full_simp_tac 1);
    9.74 +by(Blast_tac 1);
    9.75 +qed "Snoc_step1_SnocD";
    9.76 +
    9.77 +Goal "x : acc r ==> !xs. xs : acc(step1 r) --> x#xs : acc(step1 r)";
    9.78 +be acc_induct 1;
    9.79 +be thin_rl 1;
    9.80 +by(Clarify_tac 1);
    9.81 +be acc_induct 1;
    9.82 +br accI 1;
    9.83 +by(Blast_tac 1);
    9.84 +val lemma = result();
    9.85 +qed_spec_mp "Cons_acc_step1I";
    9.86 +AddSIs [Cons_acc_step1I];
    9.87 +
    9.88 +Goal "xs : lists(acc r) ==> xs : acc(step1 r)";
    9.89 +be lists.induct 1;
    9.90 + br accI 1;
    9.91 + by(asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
    9.92 +br accI 1;
    9.93 +by(fast_tac (claset() addDs [acc_downward]) 1);
    9.94 +qed "lists_accD";
    9.95 +
    9.96 +Goalw [step1_def]
    9.97 + "[| x : set xs; (y,x) : r |] ==> ? ys. (ys,xs) : step1 r & y : set ys";
    9.98 +bd (in_set_conv_decomp RS iffD1) 1;
    9.99 +by(Force_tac 1);
   9.100 +qed "ex_step1I";
   9.101 +
   9.102 +Goal "xs : acc(step1 r) ==> xs : lists(acc r)";
   9.103 +be acc_induct 1;
   9.104 +by(Clarify_tac 1);
   9.105 +br accI 1;
   9.106 +by(EVERY1[dtac ex_step1I, atac]);
   9.107 +by(Blast_tac 1);
   9.108 +qed "lists_accI";
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Lambda/ListOrder.thy	Thu Aug 06 10:33:54 1998 +0200
    10.3 @@ -0,0 +1,16 @@
    10.4 +(*  Title:      HOL/Lambda/ListOrder.thy
    10.5 +    ID:         $Id$
    10.6 +    Author:     Tobias Nipkow
    10.7 +    Copyright   1998 TU Muenchen
    10.8 +
    10.9 +Lifting an order to lists of elements, relating exactly one element
   10.10 +*)
   10.11 +
   10.12 +ListOrder = List + Acc +
   10.13 +
   10.14 +constdefs
   10.15 + step1 :: "('a * 'a)set => ('a list * 'a list)set"
   10.16 +"step1 r ==
   10.17 +   {(ys,xs). ? us z z' vs. xs = us@z#vs & (z',z) : r & ys = us@z'#vs}"
   10.18 +
   10.19 +end
    11.1 --- a/src/HOL/Lambda/ROOT.ML	Thu Aug 06 10:28:44 1998 +0200
    11.2 +++ b/src/HOL/Lambda/ROOT.ML	Thu Aug 06 10:33:54 1998 +0200
    11.3 @@ -1,7 +1,7 @@
    11.4  (*  Title:      HOL/Lambda/ROOT.ML
    11.5      ID:         $Id$
    11.6      Author:     Tobias Nipkow
    11.7 -    Copyright   1995 TUM
    11.8 +    Copyright   1998 TUM
    11.9  *)
   11.10  
   11.11  HOL_build_completed;    (*Make examples fail if HOL did*)
   11.12 @@ -9,3 +9,5 @@
   11.13  writeln"Root file for HOL/Lambda";
   11.14  
   11.15  time_use_thy "Eta";
   11.16 +loadpath := [".","../Induct"];
   11.17 +time_use_thy "InductTermi";