author | haftmann |
Fri, 17 Jun 2005 16:12:49 +0200 | |
changeset 16417 | 9bc16273c2d4 |
parent 12011 | 1a3a7b3cd9bb |
child 18241 | afdba6b3e383 |
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 |
|
20 |
lemma head_Var_reduction_aux: |
|
12011 | 21 |
"v -> v' ==> \<forall>rs. v = Var n \<degree>\<degree> rs --> (\<exists>ss. rs => ss \<and> v' = Var n \<degree>\<degree> ss)" |
9762 | 22 |
apply (erule beta.induct) |
23 |
apply simp |
|
24 |
apply (rule allI) |
|
25 |
apply (rule_tac xs = rs in rev_exhaust) |
|
26 |
apply simp |
|
27 |
apply (force intro: append_step1I) |
|
28 |
apply (rule allI) |
|
29 |
apply (rule_tac xs = rs in rev_exhaust) |
|
30 |
apply simp |
|
9771 | 31 |
apply (auto 0 3 intro: disjI2 [THEN append_step1I]) |
9762 | 32 |
done |
33 |
||
34 |
lemma head_Var_reduction: |
|
12011 | 35 |
"Var n \<degree>\<degree> rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss)" |
9762 | 36 |
apply (drule head_Var_reduction_aux) |
37 |
apply blast |
|
38 |
done |
|
5261 | 39 |
|
9762 | 40 |
lemma apps_betasE_aux: |
12011 | 41 |
"u -> u' ==> \<forall>r rs. u = r \<degree>\<degree> rs --> |
42 |
((\<exists>r'. r -> r' \<and> u' = r' \<degree>\<degree> rs) \<or> |
|
43 |
(\<exists>rs'. rs => rs' \<and> u' = r \<degree>\<degree> rs') \<or> |
|
44 |
(\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] \<degree>\<degree> ts))" |
|
9762 | 45 |
apply (erule beta.induct) |
46 |
apply (clarify del: disjCI) |
|
47 |
apply (case_tac r) |
|
48 |
apply simp |
|
49 |
apply (simp add: App_eq_foldl_conv) |
|
10653 | 50 |
apply (split split_if_asm) |
9762 | 51 |
apply simp |
52 |
apply blast |
|
53 |
apply simp |
|
54 |
apply (simp add: App_eq_foldl_conv) |
|
10653 | 55 |
apply (split split_if_asm) |
9762 | 56 |
apply simp |
57 |
apply simp |
|
58 |
apply (clarify del: disjCI) |
|
59 |
apply (drule App_eq_foldl_conv [THEN iffD1]) |
|
10653 | 60 |
apply (split split_if_asm) |
9762 | 61 |
apply simp |
62 |
apply blast |
|
11183 | 63 |
apply (force intro!: disjI1 [THEN append_step1I]) |
9762 | 64 |
apply (clarify del: disjCI) |
65 |
apply (drule App_eq_foldl_conv [THEN iffD1]) |
|
10653 | 66 |
apply (split split_if_asm) |
9762 | 67 |
apply simp |
68 |
apply blast |
|
11183 | 69 |
apply (clarify, auto 0 3 intro!: exI intro: append_step1I) |
9762 | 70 |
done |
71 |
||
72 |
lemma apps_betasE [elim!]: |
|
12011 | 73 |
"[| r \<degree>\<degree> rs -> s; !!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R; |
74 |
!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R; |
|
75 |
!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R |] |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
76 |
==> R" |
9762 | 77 |
proof - |
12011 | 78 |
assume major: "r \<degree>\<degree> rs -> s" |
11549 | 79 |
case rule_context |
9762 | 80 |
show ?thesis |
81 |
apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec]) |
|
82 |
apply (assumption | rule refl | erule prems exE conjE impE disjE)+ |
|
83 |
done |
|
84 |
qed |
|
85 |
||
86 |
lemma apps_preserves_beta [simp]: |
|
12011 | 87 |
"r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss" |
9762 | 88 |
apply (induct_tac ss rule: rev_induct) |
89 |
apply auto |
|
90 |
done |
|
91 |
||
92 |
lemma apps_preserves_beta2 [simp]: |
|
12011 | 93 |
"r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss" |
9762 | 94 |
apply (erule rtrancl_induct) |
95 |
apply blast |
|
96 |
apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl) |
|
97 |
done |
|
98 |
||
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
99 |
lemma apps_preserves_betas [rule_format, simp]: |
12011 | 100 |
"\<forall>ss. rs => ss --> r \<degree>\<degree> rs -> r \<degree>\<degree> ss" |
9762 | 101 |
apply (induct_tac rs rule: rev_induct) |
102 |
apply simp |
|
103 |
apply simp |
|
104 |
apply clarify |
|
105 |
apply (rule_tac xs = ss in rev_exhaust) |
|
106 |
apply simp |
|
107 |
apply simp |
|
108 |
apply (drule Snoc_step1_SnocD) |
|
109 |
apply blast |
|
110 |
done |
|
5261 | 111 |
|
11639 | 112 |
end |