1 (* Title: HOL/Lambda/ListBeta.thy |
1 (* Title: HOL/Lambda/ListBeta.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1998 TU Muenchen |
4 Copyright 1998 TU Muenchen |
5 |
|
6 Lifting beta-reduction to lists of terms, reducing exactly one element |
|
7 *) |
5 *) |
8 |
6 |
|
7 header {* Lifting beta-reduction to lists *} |
|
8 |
9 theory ListBeta = ListApplication + ListOrder: |
9 theory ListBeta = ListApplication + ListOrder: |
|
10 |
|
11 text {* |
|
12 Lifting beta-reduction to lists of terms, reducing exactly one element. |
|
13 *} |
10 |
14 |
11 syntax |
15 syntax |
12 "_list_beta" :: "dB => dB => bool" (infixl "=>" 50) |
16 "_list_beta" :: "dB => dB => bool" (infixl "=>" 50) |
13 translations |
17 translations |
14 "rs => ss" == "(rs,ss) : step1 beta" |
18 "rs => ss" == "(rs,ss) : step1 beta" |
25 apply (rule_tac xs = rs in rev_exhaust) |
29 apply (rule_tac xs = rs in rev_exhaust) |
26 apply simp |
30 apply simp |
27 apply (auto 0 3 intro: disjI2 [THEN append_step1I]) |
31 apply (auto 0 3 intro: disjI2 [THEN append_step1I]) |
28 done |
32 done |
29 |
33 |
30 |
|
31 lemma head_Var_reduction: |
34 lemma head_Var_reduction: |
32 "Var n $$ rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n $$ ss)" |
35 "Var n $$ rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n $$ ss)" |
33 apply (drule head_Var_reduction_aux) |
36 apply (drule head_Var_reduction_aux) |
34 apply blast |
37 apply blast |
35 done |
38 done |
42 apply (erule beta.induct) |
45 apply (erule beta.induct) |
43 apply (clarify del: disjCI) |
46 apply (clarify del: disjCI) |
44 apply (case_tac r) |
47 apply (case_tac r) |
45 apply simp |
48 apply simp |
46 apply (simp add: App_eq_foldl_conv) |
49 apply (simp add: App_eq_foldl_conv) |
47 apply (simp only: split: split_if_asm) |
50 apply (split (asm) split_if_asm) |
48 apply simp |
51 apply simp |
49 apply blast |
52 apply blast |
50 apply simp |
53 apply simp |
51 apply (simp add: App_eq_foldl_conv) |
54 apply (simp add: App_eq_foldl_conv) |
52 apply (simp only: split: split_if_asm) |
55 apply (split (asm) split_if_asm) |
53 apply simp |
56 apply simp |
54 apply simp |
57 apply simp |
55 apply (clarify del: disjCI) |
58 apply (clarify del: disjCI) |
56 apply (drule App_eq_foldl_conv [THEN iffD1]) |
59 apply (drule App_eq_foldl_conv [THEN iffD1]) |
57 apply (simp only: split: split_if_asm) |
60 apply (split (asm) split_if_asm) |
58 apply simp |
61 apply simp |
59 apply blast |
62 apply blast |
60 apply (force intro: disjI1 [THEN append_step1I]) |
63 apply (force intro: disjI1 [THEN append_step1I]) |
61 apply (clarify del: disjCI) |
64 apply (clarify del: disjCI) |
62 apply (drule App_eq_foldl_conv [THEN iffD1]) |
65 apply (drule App_eq_foldl_conv [THEN iffD1]) |
63 apply (simp only: split: split_if_asm) |
66 apply (split (asm) split_if_asm) |
64 apply simp |
67 apply simp |
65 apply blast |
68 apply blast |
66 apply (auto 0 3 intro: disjI2 [THEN append_step1I]) |
69 apply (auto 0 3 intro: disjI2 [THEN append_step1I]) |
67 done |
70 done |
68 |
71 |
69 lemma apps_betasE [elim!]: |
72 lemma apps_betasE [elim!]: |
70 "[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R; |
73 "[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R; |
71 !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R; |
74 !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R; |
72 !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |] |
75 !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |] |
73 ==> R" |
76 ==> R" |
74 proof - |
77 proof - |
75 assume major: "r $$ rs -> s" |
78 assume major: "r $$ rs -> s" |
76 case antecedent |
79 case antecedent |
77 show ?thesis |
80 show ?thesis |
78 apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec]) |
81 apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec]) |
92 apply blast |
95 apply blast |
93 apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl) |
96 apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl) |
94 done |
97 done |
95 |
98 |
96 lemma apps_preserves_betas [rulify, simp]: |
99 lemma apps_preserves_betas [rulify, simp]: |
97 "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss" |
100 "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss" |
98 apply (induct_tac rs rule: rev_induct) |
101 apply (induct_tac rs rule: rev_induct) |
99 apply simp |
102 apply simp |
100 apply simp |
103 apply simp |
101 apply clarify |
104 apply clarify |
102 apply (rule_tac xs = ss in rev_exhaust) |
105 apply (rule_tac xs = ss in rev_exhaust) |