author | berghofe |
Sun, 10 Jan 2010 18:09:11 +0100 | |
changeset 34910 | b23bd3ee4813 |
parent 23750 | a1db5f819d00 |
child 36862 | 952b2b102a0a |
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 |
|
19363 | 15 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20503
diff
changeset
|
16 |
list_beta :: "dB list => dB list => bool" (infixl "=>" 50) where |
22271 | 17 |
"rs => ss == step1 beta rs ss" |
9762 | 18 |
|
18513 | 19 |
lemma head_Var_reduction: |
22271 | 20 |
"Var n \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss" |
20503 | 21 |
apply (induct u == "Var n \<degree>\<degree> rs" v arbitrary: rs set: beta) |
9762 | 22 |
apply simp |
23 |
apply (rule_tac xs = rs in rev_exhaust) |
|
24 |
apply simp |
|
18513 | 25 |
apply (atomize, force intro: append_step1I) |
9762 | 26 |
apply (rule_tac xs = rs in rev_exhaust) |
27 |
apply simp |
|
9771 | 28 |
apply (auto 0 3 intro: disjI2 [THEN append_step1I]) |
9762 | 29 |
done |
30 |
||
18513 | 31 |
lemma apps_betasE [elim!]: |
22271 | 32 |
assumes major: "r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> s" |
33 |
and cases: "!!r'. [| r \<rightarrow>\<^sub>\<beta> r'; s = r' \<degree>\<degree> rs |] ==> R" |
|
18513 | 34 |
"!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R" |
35 |
"!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R" |
|
36 |
shows R |
|
37 |
proof - |
|
38 |
from major have |
|
22271 | 39 |
"(\<exists>r'. r \<rightarrow>\<^sub>\<beta> r' \<and> s = r' \<degree>\<degree> rs) \<or> |
18513 | 40 |
(\<exists>rs'. rs => rs' \<and> s = r \<degree>\<degree> rs') \<or> |
41 |
(\<exists>t u us. r = Abs t \<and> rs = u # us \<and> s = t[u/0] \<degree>\<degree> us)" |
|
20503 | 42 |
apply (induct u == "r \<degree>\<degree> rs" s arbitrary: r rs set: beta) |
18513 | 43 |
apply (case_tac r) |
44 |
apply simp |
|
45 |
apply (simp add: App_eq_foldl_conv) |
|
46 |
apply (split split_if_asm) |
|
47 |
apply simp |
|
48 |
apply blast |
|
49 |
apply simp |
|
50 |
apply (simp add: App_eq_foldl_conv) |
|
51 |
apply (split split_if_asm) |
|
52 |
apply simp |
|
9762 | 53 |
apply simp |
18513 | 54 |
apply (drule App_eq_foldl_conv [THEN iffD1]) |
10653 | 55 |
apply (split split_if_asm) |
9762 | 56 |
apply simp |
57 |
apply blast |
|
18513 | 58 |
apply (force intro!: disjI1 [THEN append_step1I]) |
59 |
apply (drule App_eq_foldl_conv [THEN iffD1]) |
|
10653 | 60 |
apply (split split_if_asm) |
9762 | 61 |
apply simp |
18513 | 62 |
apply blast |
63 |
apply (clarify, auto 0 3 intro!: exI intro: append_step1I) |
|
64 |
done |
|
65 |
with cases show ?thesis by blast |
|
66 |
qed |
|
9762 | 67 |
|
68 |
lemma apps_preserves_beta [simp]: |
|
22271 | 69 |
"r \<rightarrow>\<^sub>\<beta> s ==> r \<degree>\<degree> ss \<rightarrow>\<^sub>\<beta> s \<degree>\<degree> ss" |
18241 | 70 |
by (induct ss rule: rev_induct) auto |
9762 | 71 |
|
72 |
lemma apps_preserves_beta2 [simp]: |
|
12011 | 73 |
"r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss" |
23750 | 74 |
apply (induct set: rtranclp) |
9762 | 75 |
apply blast |
23750 | 76 |
apply (blast intro: apps_preserves_beta rtranclp.rtrancl_into_rtrancl) |
9762 | 77 |
done |
78 |
||
18241 | 79 |
lemma apps_preserves_betas [simp]: |
22271 | 80 |
"rs => ss \<Longrightarrow> r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> r \<degree>\<degree> ss" |
20503 | 81 |
apply (induct rs arbitrary: ss rule: rev_induct) |
9762 | 82 |
apply simp |
83 |
apply simp |
|
84 |
apply (rule_tac xs = ss in rev_exhaust) |
|
85 |
apply simp |
|
86 |
apply simp |
|
87 |
apply (drule Snoc_step1_SnocD) |
|
88 |
apply blast |
|
89 |
done |
|
5261 | 90 |
|
11639 | 91 |
end |