--- 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
--- 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
--- 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];
--- 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' ==> \<forall>rs. v = Var n $$ rs --> (\<exists>ss. rs => ss \<and> 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 ==> (\<exists>ss. rs => ss \<and> 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' ==> \<forall>r rs. u = r $$ rs -->
+ ((\<exists>r'. r -> r' \<and> u' = r'$$rs) \<or>
+ (\<exists>rs'. rs => rs' \<and> u' = r$$rs') \<or>
+ (\<exists>s t ts. r = Abs s \<and> rs = t#ts \<and> 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]:
+ "\<forall>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