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