# HG changeset patch # User wenzelm # Date 967678943 -7200 # Node ID 66f7eefb396717ac771c9b4d3e9ec6ba01c5483b # Parent 21a11b9da31887b5e7dfa442bde41818c6012462 ported HOL/Lambda/ListBeta; diff -r 21a11b9da318 -r 66f7eefb3967 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Aug 31 00:16:32 2000 +0200 +++ b/src/HOL/IsaMakefile Thu Aug 31 01:42:23 2000 +0200 @@ -306,7 +306,7 @@ $(LOG)/HOL-Lambda.gz: $(OUT)/HOL Lambda/Commutation.ML \ Lambda/Commutation.thy Lambda/Eta.ML Lambda/Eta.thy \ Lambda/InductTermi.thy Lambda/Lambda.ML Lambda/Lambda.thy \ - Lambda/ListApplication.ML Lambda/ListApplication.thy Lambda/ListBeta.ML \ + Lambda/ListApplication.ML Lambda/ListApplication.thy \ Lambda/ListBeta.thy Lambda/ListOrder.ML Lambda/ListOrder.thy \ Lambda/ParRed.ML Lambda/ParRed.thy Lambda/Type.thy Lambda/ROOT.ML @$(ISATOOL) usedir $(OUT)/HOL Lambda diff -r 21a11b9da318 -r 66f7eefb3967 src/HOL/Lambda/InductTermi.thy --- a/src/HOL/Lambda/InductTermi.thy Thu Aug 31 00:16:32 2000 +0200 +++ b/src/HOL/Lambda/InductTermi.thy Thu Aug 31 01:42:23 2000 +0200 @@ -34,7 +34,7 @@ apply (erule acc_induct) apply clarify apply (rule accI) - apply (tactic {* safe_tac (claset () addSEs [apps_betasE]) *}) -- FIXME + apply (tactic {* safe_tac (claset () addSEs [thm "apps_betasE"]) *}) -- FIXME apply assumption apply (blast intro: subst_preserves_beta apps_preserves_beta) apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI diff -r 21a11b9da318 -r 66f7eefb3967 src/HOL/Lambda/ListBeta.ML --- a/src/HOL/Lambda/ListBeta.ML Thu Aug 31 00:16:32 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,92 +0,0 @@ -(* 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)"; -by (etac beta.induct 1); - by (Asm_full_simp_tac 1); - by (rtac 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); - by (rtac allI 1); - by (res_inst_tac [("xs","rs")] rev_exhaust 1); - by (Asm_full_simp_tac 1); - by (mk_auto_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 0 3); -val lemma = result(); - -Goal "(Var n)$$rs -> v ==> (? ss. rs => ss & v = (Var n)$$ss)"; -by (dtac 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))"; -by (etac beta.induct 1); - by (clarify_tac (claset() delrules [disjCI]) 1); - by (case_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); - by (dtac (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); - by (dtac (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 (mk_auto_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 0 3); -val lemma = result(); - -val major::prems = -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"; -by (cut_facts_tac [major RS lemma RS spec RS spec] 1); -by (REPEAT_FIRST (ares_tac [refl] ORELSE' - eresolve_tac (prems @ [exE, conjE, impE, disjE]))); -qed "apps_betasE"; -AddSEs [apps_betasE]; - -Goal "r -> s ==> r$$ss -> s$$ss"; -by (rev_induct_tac "ss" 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 (rev_induct_tac "rs" 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); -by (dtac Snoc_step1_SnocD 1); -by (Blast_tac 1); -qed_spec_mp "apps_preserves_betas"; -Addsimps [apps_preserves_betas]; diff -r 21a11b9da318 -r 66f7eefb3967 src/HOL/Lambda/ListBeta.thy --- a/src/HOL/Lambda/ListBeta.thy Thu Aug 31 00:16:32 2000 +0200 +++ b/src/HOL/Lambda/ListBeta.thy Thu Aug 31 01:42:23 2000 +0200 @@ -6,9 +6,106 @@ Lifting beta-reduction to lists of terms, reducing exactly one element *) -ListBeta = ListApplication + ListOrder + +theory ListBeta = ListApplication + ListOrder: + +syntax + "_list_beta" :: "dB => dB => bool" (infixl "=>" 50) +translations + "rs => ss" == "(rs,ss) : step1 beta" + +lemma head_Var_reduction_aux: + "v -> v' ==> \rs. v = Var n $$ rs --> (\ss. rs => ss \ v' = Var n $$ ss)" + apply (erule beta.induct) + apply simp + apply (rule allI) + apply (rule_tac xs = rs in rev_exhaust) + apply simp + apply (force intro: append_step1I) + apply (rule allI) + apply (rule_tac xs = rs in rev_exhaust) + apply simp + apply (tactic {* mk_auto_tac (claset() addIs [disjI2 RS append_step1I], simpset()) 0 3 *}) + -- FIXME + done + + +lemma head_Var_reduction: + "Var n $$ rs -> v ==> (\ss. rs => ss \ v = Var n $$ ss)" + apply (drule head_Var_reduction_aux) + apply blast + done -syntax "=>" :: dB => dB => bool (infixl 50) -translations "rs => ss" == "(rs,ss) : step1 beta" +lemma apps_betasE_aux: + "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))" + apply (erule beta.induct) + apply (clarify del: disjCI) + apply (case_tac r) + apply simp + apply (simp add: App_eq_foldl_conv) + apply (simp only: split: split_if_asm) + apply simp + apply blast + apply simp + apply (simp add: App_eq_foldl_conv) + apply (simp only: split: split_if_asm) + apply simp + apply simp + apply (clarify del: disjCI) + apply (drule App_eq_foldl_conv [THEN iffD1]) + apply (simp only: split: split_if_asm) + apply simp + apply blast + apply (force intro: disjI1 [THEN append_step1I]) + apply (clarify del: disjCI) + apply (drule App_eq_foldl_conv [THEN iffD1]) + apply (simp only: split: split_if_asm) + apply simp + apply blast + apply (tactic {* mk_auto_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 0 3 *}) + -- FIXME + done + +lemma apps_betasE [elim!]: +"[| 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" +proof - + assume major: "r $$ rs -> s" + case antecedent + show ?thesis + apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec]) + apply (assumption | rule refl | erule prems exE conjE impE disjE)+ + done +qed + +lemma apps_preserves_beta [simp]: + "r -> s ==> r $$ ss -> s $$ ss" + apply (induct_tac ss rule: rev_induct) + apply auto + done + +lemma apps_preserves_beta2 [simp]: + "r ->> s ==> r $$ ss ->> s $$ ss" + apply (erule rtrancl_induct) + apply blast + apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl) + done + +lemma apps_preserves_betas [rulify, simp]: + "\ss. rs => ss --> r $$ rs -> r $$ ss" + apply (induct_tac rs rule: rev_induct) + apply simp + apply simp + apply clarify + apply (rule_tac xs = ss in rev_exhaust) + apply simp + apply simp + apply (drule Snoc_step1_SnocD) + apply blast + done end