src/HOL/Lambda/ListBeta.thy
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10653 55f33da63366
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
     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 = ListApplication + ListOrder:
    10 
    11 text {*
    12   Lifting beta-reduction to lists of terms, reducing exactly one element.
    13 *}
    14 
    15 syntax
    16   "_list_beta" :: "dB => dB => bool"   (infixl "=>" 50)
    17 translations
    18   "rs => ss" == "(rs, ss) : step1 beta"
    19 
    20 lemma head_Var_reduction_aux:
    21   "v -> v' ==> \<forall>rs. v = Var n $$ rs --> (\<exists>ss. rs => ss \<and> v' = Var n $$ ss)"
    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
    31     apply (auto 0 3 intro: disjI2 [THEN append_step1I])
    32   done
    33 
    34 lemma head_Var_reduction:
    35   "Var n $$ rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n $$ ss)"
    36   apply (drule head_Var_reduction_aux)
    37   apply blast
    38   done
    39 
    40 lemma apps_betasE_aux:
    41   "u -> u' ==> \<forall>r rs. u = r $$ rs -->
    42     ((\<exists>r'. r -> r' \<and> u' = r' $$ rs) \<or>
    43      (\<exists>rs'. rs => rs' \<and> u' = r $$ rs') \<or>
    44      (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] $$ ts))"
    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)
    50       apply (split (asm) split_if_asm)
    51        apply simp
    52        apply blast
    53       apply simp
    54      apply (simp add: App_eq_foldl_conv)
    55      apply (split (asm) split_if_asm)
    56       apply simp
    57      apply simp
    58     apply (clarify del: disjCI)
    59     apply (drule App_eq_foldl_conv [THEN iffD1])
    60     apply (split (asm) split_if_asm)
    61      apply simp
    62      apply blast
    63     apply (force intro: disjI1 [THEN append_step1I])
    64    apply (clarify del: disjCI)
    65    apply (drule App_eq_foldl_conv [THEN iffD1])
    66    apply (split (asm) split_if_asm)
    67     apply simp
    68     apply blast
    69    apply (auto 0 3 intro: disjI2 [THEN append_step1I])
    70   done
    71 
    72 lemma apps_betasE [elim!]:
    73   "[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R;
    74     !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R;
    75     !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |]
    76   ==> R"
    77 proof -
    78   assume major: "r $$ rs -> s"
    79   case antecedent
    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]:
    87     "r -> s ==> r $$ ss -> s $$ ss"
    88   apply (induct_tac ss rule: rev_induct)
    89   apply auto
    90   done
    91 
    92 lemma apps_preserves_beta2 [simp]:
    93     "r ->> s ==> r $$ ss ->> s $$ ss"
    94   apply (erule rtrancl_induct)
    95    apply blast
    96   apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
    97   done
    98 
    99 lemma apps_preserves_betas [rule_format, simp]:
   100     "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
   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
   111 
   112 end