1(*  Title:      HOL/Proofs/Lambda/ListBeta.thy
2    Author:     Tobias Nipkow
3    Copyright   1998 TU Muenchen
4*)
5
6section \<open>Lifting beta-reduction to lists\<close>
7
8theory ListBeta imports ListApplication ListOrder begin
9
10text \<open>
11  Lifting beta-reduction to lists of terms, reducing exactly one element.
12\<close>
13
14abbreviation
15  list_beta :: "dB list => dB list => bool"  (infixl "=>" 50) where
16  "rs => ss == step1 beta rs ss"
17
18lemma head_Var_reduction:
19  "Var n \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
20  apply (induct u == "Var n \<degree>\<degree> rs" v arbitrary: rs set: beta)
21     apply simp
22    apply (rule_tac xs = rs in rev_exhaust)
23     apply simp
24    apply (atomize, force intro: append_step1I)
25   apply (rule_tac xs = rs in rev_exhaust)
26    apply simp
27    apply (auto 0 3 intro: disjI2 [THEN append_step1I])
28  done
29
30lemma apps_betasE [elim!]:
31  assumes major: "r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> s"
32    and cases: "!!r'. [| r \<rightarrow>\<^sub>\<beta> r'; s = r' \<degree>\<degree> rs |] ==> R"
33      "!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R"
34      "!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R"
35  shows R
36proof -
37  from major have
38   "(\<exists>r'. r \<rightarrow>\<^sub>\<beta> r' \<and> s = r' \<degree>\<degree> rs) \<or>
39    (\<exists>rs'. rs => rs' \<and> s = r \<degree>\<degree> rs') \<or>
40    (\<exists>t u us. r = Abs t \<and> rs = u # us \<and> s = t[u/0] \<degree>\<degree> us)"
41    apply (induct u == "r \<degree>\<degree> rs" s arbitrary: r rs set: beta)
42       apply (case_tac r)
43         apply simp
44        apply (simp add: App_eq_foldl_conv)
45        apply (split if_split_asm)
46         apply simp
47         apply blast
48        apply simp
49       apply (simp add: App_eq_foldl_conv)
50       apply (split if_split_asm)
51        apply simp
52       apply simp
53      apply (drule App_eq_foldl_conv [THEN iffD1])
54      apply (split if_split_asm)
55       apply simp
56       apply blast
57      apply (force intro!: disjI1 [THEN append_step1I])
58     apply (drule App_eq_foldl_conv [THEN iffD1])
59     apply (split if_split_asm)
60      apply simp
61      apply blast
62     apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
63    done
64  with cases show ?thesis by blast
65qed
66
67lemma apps_preserves_beta [simp]:
68    "r \<rightarrow>\<^sub>\<beta> s ==> r \<degree>\<degree> ss \<rightarrow>\<^sub>\<beta> s \<degree>\<degree> ss"
69  by (induct ss rule: rev_induct) auto
70
71lemma apps_preserves_beta2 [simp]:
72    "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r \<degree>\<degree> ss \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree>\<degree> ss"
73  apply (induct set: rtranclp)
74   apply blast
75  apply (blast intro: apps_preserves_beta rtranclp.rtrancl_into_rtrancl)
76  done
77
78lemma apps_preserves_betas [simp]:
79    "rs => ss \<Longrightarrow> r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> r \<degree>\<degree> ss"
80  apply (induct rs arbitrary: ss rule: rev_induct)
81   apply simp
82  apply simp
83  apply (rule_tac xs = ss in rev_exhaust)
84   apply simp
85  apply simp
86  apply (drule Snoc_step1_SnocD)
87  apply blast
88  done
89
90end
91