src/HOL/Proofs/Lambda/ListBeta.thy
 author wenzelm Thu May 24 17:25:53 2012 +0200 (2012-05-24) changeset 47988 e4b69e10b990 parent 39157 b98909faaea8 child 58889 5b7a9633cfa8 permissions -rw-r--r--
tuned proofs;
```     1 (*  Title:      HOL/Proofs/Lambda/ListBeta.thy
```
```     2     Author:     Tobias Nipkow
```
```     3     Copyright   1998 TU Muenchen
```
```     4 *)
```
```     5
```
```     6 header {* Lifting beta-reduction to lists *}
```
```     7
```
```     8 theory ListBeta imports ListApplication ListOrder begin
```
```     9
```
```    10 text {*
```
```    11   Lifting beta-reduction to lists of terms, reducing exactly one element.
```
```    12 *}
```
```    13
```
```    14 abbreviation
```
```    15   list_beta :: "dB list => dB list => bool"  (infixl "=>" 50) where
```
```    16   "rs => ss == step1 beta rs ss"
```
```    17
```
```    18 lemma 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
```
```    30 lemma 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
```
```    36 proof -
```
```    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 split_if_asm)
```
```    46          apply simp
```
```    47          apply blast
```
```    48         apply simp
```
```    49        apply (simp add: App_eq_foldl_conv)
```
```    50        apply (split split_if_asm)
```
```    51         apply simp
```
```    52        apply simp
```
```    53       apply (drule App_eq_foldl_conv [THEN iffD1])
```
```    54       apply (split split_if_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 split_if_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
```
```    65 qed
```
```    66
```
```    67 lemma 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
```
```    71 lemma apps_preserves_beta2 [simp]:
```
```    72     "r ->> s ==> r \<degree>\<degree> ss ->> 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
```
```    78 lemma 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
```
```    90 end
```