# HG changeset patch # User nipkow # Date 902392434 -7200 # Node ID ce3c25c8a694a862ba57cb6b1b00e8e63d003c08 # Parent 1835a591d3a7eea7fc081ebc5bc4be365e617e02 First steps towards termination of simply typed terms. diff -r 1835a591d3a7 -r ce3c25c8a694 src/HOL/Lambda/Eta.ML --- 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"; diff -r 1835a591d3a7 -r ce3c25c8a694 src/HOL/Lambda/InductTermi.ML --- /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"; diff -r 1835a591d3a7 -r ce3c25c8a694 src/HOL/Lambda/InductTermi.thy --- /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 diff -r 1835a591d3a7 -r ce3c25c8a694 src/HOL/Lambda/Lambda.ML --- 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]; diff -r 1835a591d3a7 -r ce3c25c8a694 src/HOL/Lambda/ListApplication.ML --- /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"; diff -r 1835a591d3a7 -r ce3c25c8a694 src/HOL/Lambda/ListApplication.thy --- /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 diff -r 1835a591d3a7 -r ce3c25c8a694 src/HOL/Lambda/ListBeta.ML --- /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]; diff -r 1835a591d3a7 -r ce3c25c8a694 src/HOL/Lambda/ListBeta.thy --- /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 diff -r 1835a591d3a7 -r ce3c25c8a694 src/HOL/Lambda/ListOrder.ML --- /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"; diff -r 1835a591d3a7 -r ce3c25c8a694 src/HOL/Lambda/ListOrder.thy --- /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 diff -r 1835a591d3a7 -r ce3c25c8a694 src/HOL/Lambda/ROOT.ML --- 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";