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;
nipkow@5261
     1
(*  Title:      HOL/Lambda/ListBeta.thy
nipkow@5261
     2
    ID:         $Id$
nipkow@5261
     3
    Author:     Tobias Nipkow
nipkow@5261
     4
    Copyright   1998 TU Muenchen
nipkow@5261
     5
*)
nipkow@5261
     6
wenzelm@9811
     7
header {* Lifting beta-reduction to lists *}
wenzelm@9811
     8
wenzelm@9762
     9
theory ListBeta = ListApplication + ListOrder:
wenzelm@9762
    10
wenzelm@9811
    11
text {*
wenzelm@9811
    12
  Lifting beta-reduction to lists of terms, reducing exactly one element.
wenzelm@9811
    13
*}
wenzelm@9811
    14
wenzelm@9762
    15
syntax
wenzelm@9762
    16
  "_list_beta" :: "dB => dB => bool"   (infixl "=>" 50)
wenzelm@9762
    17
translations
wenzelm@9827
    18
  "rs => ss" == "(rs, ss) : step1 beta"
wenzelm@9762
    19
wenzelm@9762
    20
lemma head_Var_reduction_aux:
wenzelm@9762
    21
  "v -> v' ==> \<forall>rs. v = Var n $$ rs --> (\<exists>ss. rs => ss \<and> v' = Var n $$ ss)"
wenzelm@9762
    22
  apply (erule beta.induct)
wenzelm@9762
    23
     apply simp
wenzelm@9762
    24
    apply (rule allI)
wenzelm@9762
    25
    apply (rule_tac xs = rs in rev_exhaust)
wenzelm@9762
    26
     apply simp
wenzelm@9762
    27
    apply (force intro: append_step1I)
wenzelm@9762
    28
   apply (rule allI)
wenzelm@9762
    29
   apply (rule_tac xs = rs in rev_exhaust)
wenzelm@9762
    30
    apply simp
wenzelm@9771
    31
    apply (auto 0 3 intro: disjI2 [THEN append_step1I])
wenzelm@9762
    32
  done
wenzelm@9762
    33
wenzelm@9762
    34
lemma head_Var_reduction:
wenzelm@9762
    35
  "Var n $$ rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n $$ ss)"
wenzelm@9762
    36
  apply (drule head_Var_reduction_aux)
wenzelm@9762
    37
  apply blast
wenzelm@9762
    38
  done
nipkow@5261
    39
wenzelm@9762
    40
lemma apps_betasE_aux:
wenzelm@9762
    41
  "u -> u' ==> \<forall>r rs. u = r $$ rs -->
wenzelm@9771
    42
    ((\<exists>r'. r -> r' \<and> u' = r' $$ rs) \<or>
wenzelm@9771
    43
     (\<exists>rs'. rs => rs' \<and> u' = r $$ rs') \<or>
wenzelm@9771
    44
     (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] $$ ts))"
wenzelm@9762
    45
  apply (erule beta.induct)
wenzelm@9762
    46
     apply (clarify del: disjCI)
wenzelm@9762
    47
     apply (case_tac r)
wenzelm@9762
    48
       apply simp
wenzelm@9762
    49
      apply (simp add: App_eq_foldl_conv)
wenzelm@9811
    50
      apply (split (asm) split_if_asm)
wenzelm@9762
    51
       apply simp
wenzelm@9762
    52
       apply blast
wenzelm@9762
    53
      apply simp
wenzelm@9762
    54
     apply (simp add: App_eq_foldl_conv)
wenzelm@9811
    55
     apply (split (asm) split_if_asm)
wenzelm@9762
    56
      apply simp
wenzelm@9762
    57
     apply simp
wenzelm@9762
    58
    apply (clarify del: disjCI)
wenzelm@9762
    59
    apply (drule App_eq_foldl_conv [THEN iffD1])
wenzelm@9811
    60
    apply (split (asm) split_if_asm)
wenzelm@9762
    61
     apply simp
wenzelm@9762
    62
     apply blast
wenzelm@9762
    63
    apply (force intro: disjI1 [THEN append_step1I])
wenzelm@9762
    64
   apply (clarify del: disjCI)
wenzelm@9762
    65
   apply (drule App_eq_foldl_conv [THEN iffD1])
wenzelm@9811
    66
   apply (split (asm) split_if_asm)
wenzelm@9762
    67
    apply simp
wenzelm@9762
    68
    apply blast
wenzelm@9771
    69
   apply (auto 0 3 intro: disjI2 [THEN append_step1I])
wenzelm@9762
    70
  done
wenzelm@9762
    71
wenzelm@9762
    72
lemma apps_betasE [elim!]:
wenzelm@9811
    73
  "[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R;
wenzelm@9811
    74
    !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R;
wenzelm@9811
    75
    !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |]
wenzelm@9811
    76
  ==> R"
wenzelm@9762
    77
proof -
wenzelm@9762
    78
  assume major: "r $$ rs -> s"
wenzelm@9762
    79
  case antecedent
wenzelm@9762
    80
  show ?thesis
wenzelm@9762
    81
    apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
wenzelm@9762
    82
    apply (assumption | rule refl | erule prems exE conjE impE disjE)+
wenzelm@9762
    83
    done
wenzelm@9762
    84
qed
wenzelm@9762
    85
wenzelm@9762
    86
lemma apps_preserves_beta [simp]:
wenzelm@9762
    87
    "r -> s ==> r $$ ss -> s $$ ss"
wenzelm@9762
    88
  apply (induct_tac ss rule: rev_induct)
wenzelm@9762
    89
  apply auto
wenzelm@9762
    90
  done
wenzelm@9762
    91
wenzelm@9762
    92
lemma apps_preserves_beta2 [simp]:
wenzelm@9762
    93
    "r ->> s ==> r $$ ss ->> s $$ ss"
wenzelm@9762
    94
  apply (erule rtrancl_induct)
wenzelm@9762
    95
   apply blast
wenzelm@9762
    96
  apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
wenzelm@9762
    97
  done
wenzelm@9762
    98
wenzelm@9941
    99
lemma apps_preserves_betas [rule_format, simp]:
wenzelm@9811
   100
    "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
wenzelm@9762
   101
  apply (induct_tac rs rule: rev_induct)
wenzelm@9762
   102
   apply simp
wenzelm@9762
   103
  apply simp
wenzelm@9762
   104
  apply clarify
wenzelm@9762
   105
  apply (rule_tac xs = ss in rev_exhaust)
wenzelm@9762
   106
   apply simp
wenzelm@9762
   107
  apply simp
wenzelm@9762
   108
  apply (drule Snoc_step1_SnocD)
wenzelm@9762
   109
  apply blast
wenzelm@9762
   110
  done
nipkow@5261
   111
wenzelm@9811
   112
end