src/HOL/Lambda/ListBeta.thy
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 19363 667b5ea637dd
child 20503 503ac4c5ef91
permissions -rw-r--r--
simplified code generator setup
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
haftmann@16417
     9
theory ListBeta imports ListApplication ListOrder begin
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@19363
    15
abbreviation
wenzelm@19086
    16
  list_beta :: "dB list => dB list => bool"   (infixl "=>" 50)
wenzelm@19363
    17
  "rs => ss == (rs, ss) : step1 beta"
wenzelm@9762
    18
wenzelm@18513
    19
lemma head_Var_reduction:
wenzelm@18513
    20
  "Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
wenzelm@18513
    21
  apply (induct u == "Var n \<degree>\<degree> rs" v fixing: rs set: beta)
wenzelm@9762
    22
     apply simp
wenzelm@9762
    23
    apply (rule_tac xs = rs in rev_exhaust)
wenzelm@9762
    24
     apply simp
wenzelm@18513
    25
    apply (atomize, force intro: append_step1I)
wenzelm@9762
    26
   apply (rule_tac xs = rs in rev_exhaust)
wenzelm@9762
    27
    apply simp
wenzelm@9771
    28
    apply (auto 0 3 intro: disjI2 [THEN append_step1I])
wenzelm@9762
    29
  done
wenzelm@9762
    30
wenzelm@18513
    31
lemma apps_betasE [elim!]:
wenzelm@18513
    32
  assumes major: "r \<degree>\<degree> rs -> s"
wenzelm@18513
    33
    and cases: "!!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R"
wenzelm@18513
    34
      "!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R"
wenzelm@18513
    35
      "!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R"
wenzelm@18513
    36
  shows R
wenzelm@18513
    37
proof -
wenzelm@18513
    38
  from major have
wenzelm@18513
    39
   "(\<exists>r'. r -> r' \<and> s = r' \<degree>\<degree> rs) \<or>
wenzelm@18513
    40
    (\<exists>rs'. rs => rs' \<and> s = r \<degree>\<degree> rs') \<or>
wenzelm@18513
    41
    (\<exists>t u us. r = Abs t \<and> rs = u # us \<and> s = t[u/0] \<degree>\<degree> us)"
wenzelm@18513
    42
    apply (induct u == "r \<degree>\<degree> rs" s fixing: r rs set: beta)
wenzelm@18513
    43
       apply (case_tac r)
wenzelm@18513
    44
         apply simp
wenzelm@18513
    45
        apply (simp add: App_eq_foldl_conv)
wenzelm@18513
    46
        apply (split split_if_asm)
wenzelm@18513
    47
         apply simp
wenzelm@18513
    48
         apply blast
wenzelm@18513
    49
        apply simp
wenzelm@18513
    50
       apply (simp add: App_eq_foldl_conv)
wenzelm@18513
    51
       apply (split split_if_asm)
wenzelm@18513
    52
        apply simp
wenzelm@9762
    53
       apply simp
wenzelm@18513
    54
      apply (drule App_eq_foldl_conv [THEN iffD1])
nipkow@10653
    55
      apply (split split_if_asm)
wenzelm@9762
    56
       apply simp
wenzelm@9762
    57
       apply blast
wenzelm@18513
    58
      apply (force intro!: disjI1 [THEN append_step1I])
wenzelm@18513
    59
     apply (drule App_eq_foldl_conv [THEN iffD1])
nipkow@10653
    60
     apply (split split_if_asm)
wenzelm@9762
    61
      apply simp
wenzelm@18513
    62
      apply blast
wenzelm@18513
    63
     apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
wenzelm@18513
    64
    done
wenzelm@18513
    65
  with cases show ?thesis by blast
wenzelm@18513
    66
qed
wenzelm@9762
    67
wenzelm@9762
    68
lemma apps_preserves_beta [simp]:
wenzelm@12011
    69
    "r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss"
wenzelm@18241
    70
  by (induct ss rule: rev_induct) auto
wenzelm@9762
    71
wenzelm@9762
    72
lemma apps_preserves_beta2 [simp]:
wenzelm@12011
    73
    "r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
wenzelm@18241
    74
  apply (induct set: rtrancl)
wenzelm@9762
    75
   apply blast
wenzelm@9762
    76
  apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
wenzelm@9762
    77
  done
wenzelm@9762
    78
wenzelm@18241
    79
lemma apps_preserves_betas [simp]:
wenzelm@18241
    80
    "rs => ss \<Longrightarrow> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
wenzelm@18241
    81
  apply (induct rs fixing: ss rule: rev_induct)
wenzelm@9762
    82
   apply simp
wenzelm@9762
    83
  apply simp
wenzelm@9762
    84
  apply (rule_tac xs = ss in rev_exhaust)
wenzelm@9762
    85
   apply simp
wenzelm@9762
    86
  apply simp
wenzelm@9762
    87
  apply (drule Snoc_step1_SnocD)
wenzelm@9762
    88
  apply blast
wenzelm@9762
    89
  done
nipkow@5261
    90
wenzelm@11639
    91
end