src/HOL/Lambda/ParRed.thy
author berghofe
Wed Feb 07 17:44:07 2007 +0100 (2007-02-07)
changeset 22271 51a80e238b29
parent 21404 eb85850d3eb7
child 23750 a1db5f819d00
permissions -rw-r--r--
Adapted to new inductive definition package.
nipkow@1120
     1
(*  Title:      HOL/Lambda/ParRed.thy
nipkow@1120
     2
    ID:         $Id$
nipkow@1120
     3
    Author:     Tobias Nipkow
nipkow@1120
     4
    Copyright   1995 TU Muenchen
nipkow@1120
     5
wenzelm@9811
     6
Properties of => and "cd", in particular the diamond property of => and
wenzelm@9811
     7
confluence of beta.
nipkow@1120
     8
*)
nipkow@1120
     9
wenzelm@9811
    10
header {* Parallel reduction and a complete developments *}
nipkow@1120
    11
haftmann@16417
    12
theory ParRed imports Lambda Commutation begin
wenzelm@9811
    13
wenzelm@9811
    14
wenzelm@9811
    15
subsection {* Parallel reduction *}
nipkow@1120
    16
berghofe@22271
    17
inductive2 par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
berghofe@22271
    18
  where
berghofe@22271
    19
    var [simp, intro!]: "Var n => Var n"
berghofe@22271
    20
  | abs [simp, intro!]: "s => t ==> Abs s => Abs t"
berghofe@22271
    21
  | app [simp, intro!]: "[| s => s'; t => t' |] ==> s \<degree> t => s' \<degree> t'"
berghofe@22271
    22
  | beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) \<degree> t => s'[t'/0]"
nipkow@1120
    23
berghofe@22271
    24
inductive_cases2 par_beta_cases [elim!]:
wenzelm@9811
    25
  "Var n => t"
wenzelm@9811
    26
  "Abs s => Abs t"
wenzelm@12011
    27
  "(Abs s) \<degree> t => u"
wenzelm@12011
    28
  "s \<degree> t => u"
wenzelm@9811
    29
  "Abs s => t"
wenzelm@9811
    30
wenzelm@9811
    31
wenzelm@9811
    32
subsection {* Inclusions *}
wenzelm@9811
    33
wenzelm@9811
    34
text {* @{text "beta \<subseteq> par_beta \<subseteq> beta^*"} \medskip *}
wenzelm@9811
    35
wenzelm@9811
    36
lemma par_beta_varL [simp]:
wenzelm@9811
    37
    "(Var n => t) = (t = Var n)"
wenzelm@18241
    38
  by blast
wenzelm@9811
    39
wenzelm@9811
    40
lemma par_beta_refl [simp]: "t => t"  (* par_beta_refl [intro!] causes search to blow up *)
wenzelm@18241
    41
  by (induct t) simp_all
wenzelm@9811
    42
wenzelm@9811
    43
lemma beta_subset_par_beta: "beta <= par_beta"
berghofe@22271
    44
  apply (rule predicate2I)
wenzelm@9811
    45
  apply (erule beta.induct)
wenzelm@9811
    46
     apply (blast intro!: par_beta_refl)+
wenzelm@9811
    47
  done
wenzelm@9811
    48
berghofe@22271
    49
lemma par_beta_subset_beta: "par_beta <= beta^**"
berghofe@22271
    50
  apply (rule predicate2I)
wenzelm@9811
    51
  apply (erule par_beta.induct)
wenzelm@9811
    52
     apply blast
berghofe@22271
    53
    apply (blast del: rtrancl.rtrancl_refl intro: rtrancl.rtrancl_into_rtrancl)+
wenzelm@9811
    54
      -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *}
wenzelm@9811
    55
  done
wenzelm@9811
    56
wenzelm@9811
    57
wenzelm@9811
    58
subsection {* Misc properties of par-beta *}
wenzelm@9811
    59
wenzelm@18241
    60
lemma par_beta_lift [simp]:
wenzelm@18241
    61
    "t => t' \<Longrightarrow> lift t n => lift t' n"
wenzelm@20503
    62
  by (induct t arbitrary: t' n) fastsimp+
wenzelm@9811
    63
wenzelm@18241
    64
lemma par_beta_subst:
wenzelm@18241
    65
    "s => s' \<Longrightarrow> t => t' \<Longrightarrow> t[s/n] => t'[s'/n]"
wenzelm@20503
    66
  apply (induct t arbitrary: s s' t' n)
wenzelm@9811
    67
    apply (simp add: subst_Var)
wenzelm@9811
    68
   apply (erule par_beta_cases)
wenzelm@9811
    69
    apply simp
wenzelm@9811
    70
   apply (simp add: subst_subst [symmetric])
wenzelm@9811
    71
   apply (fastsimp intro!: par_beta_lift)
wenzelm@9811
    72
  apply fastsimp
wenzelm@9811
    73
  done
wenzelm@9811
    74
wenzelm@9811
    75
wenzelm@9811
    76
subsection {* Confluence (directly) *}
wenzelm@9811
    77
wenzelm@9811
    78
lemma diamond_par_beta: "diamond par_beta"
wenzelm@9811
    79
  apply (unfold diamond_def commute_def square_def)
wenzelm@9811
    80
  apply (rule impI [THEN allI [THEN allI]])
wenzelm@9811
    81
  apply (erule par_beta.induct)
wenzelm@9811
    82
     apply (blast intro!: par_beta_subst)+
wenzelm@9811
    83
  done
wenzelm@9811
    84
wenzelm@9811
    85
wenzelm@9811
    86
subsection {* Complete developments *}
nipkow@1120
    87
nipkow@1120
    88
consts
wenzelm@9811
    89
  "cd" :: "dB => dB"
wenzelm@9811
    90
recdef "cd" "measure size"
wenzelm@9811
    91
  "cd (Var n) = Var n"
wenzelm@12011
    92
  "cd (Var n \<degree> t) = Var n \<degree> cd t"
wenzelm@12011
    93
  "cd ((s1 \<degree> s2) \<degree> t) = cd (s1 \<degree> s2) \<degree> cd t"
wenzelm@12011
    94
  "cd (Abs u \<degree> t) = (cd u)[cd t/0]"
wenzelm@9811
    95
  "cd (Abs s) = Abs (cd s)"
wenzelm@9811
    96
wenzelm@18241
    97
lemma par_beta_cd: "s => t \<Longrightarrow> t => cd s"
wenzelm@20503
    98
  apply (induct s arbitrary: t rule: cd.induct)
wenzelm@9811
    99
      apply auto
wenzelm@9811
   100
  apply (fast intro!: par_beta_subst)
wenzelm@9811
   101
  done
nipkow@1120
   102
wenzelm@9811
   103
wenzelm@9811
   104
subsection {* Confluence (via complete developments) *}
wenzelm@9811
   105
wenzelm@9811
   106
lemma diamond_par_beta2: "diamond par_beta"
wenzelm@9811
   107
  apply (unfold diamond_def commute_def square_def)
wenzelm@9811
   108
  apply (blast intro: par_beta_cd)
wenzelm@9811
   109
  done
wenzelm@9811
   110
wenzelm@9811
   111
theorem beta_confluent: "confluent beta"
wenzelm@9811
   112
  apply (rule diamond_par_beta2 diamond_to_confluence
wenzelm@9811
   113
    par_beta_subset_beta beta_subset_par_beta)+
wenzelm@9811
   114
  done
wenzelm@9811
   115
wenzelm@11638
   116
end