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