author | wenzelm |
Wed, 01 Feb 2006 22:20:40 +0100 | |
changeset 18888 | 3b643f81b378 |
parent 18513 | 791b53bf4073 |
child 19086 | 1b3780be6cc2 |
permissions | -rw-r--r-- |
5261 | 1 |
(* Title: HOL/Lambda/ListBeta.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1998 TU Muenchen |
|
5 |
*) |
|
6 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
7 |
header {* Lifting beta-reduction to lists *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
8 |
|
16417 | 9 |
theory ListBeta imports ListApplication ListOrder begin |
9762 | 10 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
11 |
text {* |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
12 |
Lifting beta-reduction to lists of terms, reducing exactly one element. |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
13 |
*} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
14 |
|
9762 | 15 |
syntax |
16 |
"_list_beta" :: "dB => dB => bool" (infixl "=>" 50) |
|
17 |
translations |
|
9827 | 18 |
"rs => ss" == "(rs, ss) : step1 beta" |
9762 | 19 |
|
18513 | 20 |
lemma head_Var_reduction: |
21 |
"Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss" |
|
22 |
apply (induct u == "Var n \<degree>\<degree> rs" v fixing: rs set: beta) |
|
9762 | 23 |
apply simp |
24 |
apply (rule_tac xs = rs in rev_exhaust) |
|
25 |
apply simp |
|
18513 | 26 |
apply (atomize, force intro: append_step1I) |
9762 | 27 |
apply (rule_tac xs = rs in rev_exhaust) |
28 |
apply simp |
|
9771 | 29 |
apply (auto 0 3 intro: disjI2 [THEN append_step1I]) |
9762 | 30 |
done |
31 |
||
18513 | 32 |
lemma apps_betasE [elim!]: |
33 |
assumes major: "r \<degree>\<degree> rs -> s" |
|
34 |
and cases: "!!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R" |
|
35 |
"!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R" |
|
36 |
"!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R" |
|
37 |
shows R |
|
38 |
proof - |
|
39 |
from major have |
|
40 |
"(\<exists>r'. r -> r' \<and> s = r' \<degree>\<degree> rs) \<or> |
|
41 |
(\<exists>rs'. rs => rs' \<and> s = r \<degree>\<degree> rs') \<or> |
|
42 |
(\<exists>t u us. r = Abs t \<and> rs = u # us \<and> s = t[u/0] \<degree>\<degree> us)" |
|
43 |
apply (induct u == "r \<degree>\<degree> rs" s fixing: r rs set: beta) |
|
44 |
apply (case_tac r) |
|
45 |
apply simp |
|
46 |
apply (simp add: App_eq_foldl_conv) |
|
47 |
apply (split split_if_asm) |
|
48 |
apply simp |
|
49 |
apply blast |
|
50 |
apply simp |
|
51 |
apply (simp add: App_eq_foldl_conv) |
|
52 |
apply (split split_if_asm) |
|
53 |
apply simp |
|
9762 | 54 |
apply simp |
18513 | 55 |
apply (drule App_eq_foldl_conv [THEN iffD1]) |
10653 | 56 |
apply (split split_if_asm) |
9762 | 57 |
apply simp |
58 |
apply blast |
|
18513 | 59 |
apply (force intro!: disjI1 [THEN append_step1I]) |
60 |
apply (drule App_eq_foldl_conv [THEN iffD1]) |
|
10653 | 61 |
apply (split split_if_asm) |
9762 | 62 |
apply simp |
18513 | 63 |
apply blast |
64 |
apply (clarify, auto 0 3 intro!: exI intro: append_step1I) |
|
65 |
done |
|
66 |
with cases show ?thesis by blast |
|
67 |
qed |
|
9762 | 68 |
|
69 |
lemma apps_preserves_beta [simp]: |
|
12011 | 70 |
"r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss" |
18241 | 71 |
by (induct ss rule: rev_induct) auto |
9762 | 72 |
|
73 |
lemma apps_preserves_beta2 [simp]: |
|
12011 | 74 |
"r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss" |
18241 | 75 |
apply (induct set: rtrancl) |
9762 | 76 |
apply blast |
77 |
apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl) |
|
78 |
done |
|
79 |
||
18241 | 80 |
lemma apps_preserves_betas [simp]: |
81 |
"rs => ss \<Longrightarrow> r \<degree>\<degree> rs -> r \<degree>\<degree> ss" |
|
82 |
apply (induct rs fixing: ss rule: rev_induct) |
|
9762 | 83 |
apply simp |
84 |
apply simp |
|
85 |
apply (rule_tac xs = ss in rev_exhaust) |
|
86 |
apply simp |
|
87 |
apply simp |
|
88 |
apply (drule Snoc_step1_SnocD) |
|
89 |
apply blast |
|
90 |
done |
|
5261 | 91 |
|
11639 | 92 |
end |