src/HOL/Lambda/ParRed.thy
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 11638 2c3dee321b4b
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
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
wenzelm@9811
    12
theory ParRed = Lambda + Commutation:
wenzelm@9811
    13
wenzelm@9811
    14
wenzelm@9811
    15
subsection {* Parallel reduction *}
nipkow@1120
    16
wenzelm@9811
    17
consts
wenzelm@9811
    18
  par_beta :: "(dB \<times> dB) set"
nipkow@1120
    19
wenzelm@9811
    20
syntax
wenzelm@9811
    21
  par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
nipkow@1120
    22
translations
wenzelm@9811
    23
  "s => t" == "(s, t) \<in> par_beta"
nipkow@1120
    24
paulson@1789
    25
inductive par_beta
wenzelm@9811
    26
  intros [simp, intro!]
wenzelm@9811
    27
    var: "Var n => Var n"
wenzelm@9811
    28
    abs: "s => t ==> Abs s => Abs t"
wenzelm@9811
    29
    app: "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
wenzelm@9811
    30
    beta: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
wenzelm@9811
    31
wenzelm@9811
    32
inductive_cases par_beta_cases [elim!]:
wenzelm@9811
    33
  "Var n => t"
wenzelm@9811
    34
  "Abs s => Abs t"
wenzelm@9811
    35
  "(Abs s) $ t => u"
wenzelm@9811
    36
  "s $ t => u"
wenzelm@9811
    37
  "Abs s => t"
wenzelm@9811
    38
wenzelm@9811
    39
wenzelm@9811
    40
subsection {* Inclusions *}
wenzelm@9811
    41
wenzelm@9811
    42
text {* @{text "beta \<subseteq> par_beta \<subseteq> beta^*"} \medskip *}
wenzelm@9811
    43
wenzelm@9811
    44
lemma par_beta_varL [simp]:
wenzelm@9811
    45
    "(Var n => t) = (t = Var n)"
wenzelm@9811
    46
  apply blast
wenzelm@9811
    47
  done
wenzelm@9811
    48
wenzelm@9811
    49
lemma par_beta_refl [simp]: "t => t"  (* par_beta_refl [intro!] causes search to blow up *)
wenzelm@9811
    50
  apply (induct_tac t)
wenzelm@9811
    51
    apply simp_all
wenzelm@9811
    52
  done
wenzelm@9811
    53
wenzelm@9811
    54
lemma beta_subset_par_beta: "beta <= par_beta"
wenzelm@9811
    55
  apply (rule subsetI)
wenzelm@9811
    56
  apply clarify
wenzelm@9811
    57
  apply (erule beta.induct)
wenzelm@9811
    58
     apply (blast intro!: par_beta_refl)+
wenzelm@9811
    59
  done
wenzelm@9811
    60
wenzelm@9811
    61
lemma par_beta_subset_beta: "par_beta <= beta^*"
wenzelm@9811
    62
  apply (rule subsetI)
wenzelm@9811
    63
  apply clarify
wenzelm@9811
    64
  apply (erule par_beta.induct)
wenzelm@9811
    65
     apply blast
wenzelm@9811
    66
    apply (blast del: rtrancl_refl intro: rtrancl_into_rtrancl)+
wenzelm@9811
    67
      -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *}
wenzelm@9811
    68
  done
wenzelm@9811
    69
wenzelm@9811
    70
wenzelm@9811
    71
subsection {* Misc properties of par-beta *}
wenzelm@9811
    72
wenzelm@9941
    73
lemma par_beta_lift [rule_format, simp]:
wenzelm@9811
    74
    "\<forall>t' n. t => t' --> lift t n => lift t' n"
wenzelm@9811
    75
  apply (induct_tac t)
wenzelm@9811
    76
    apply fastsimp+
wenzelm@9811
    77
  done
wenzelm@9811
    78
wenzelm@9941
    79
lemma par_beta_subst [rule_format]:
wenzelm@9811
    80
    "\<forall>s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"
wenzelm@9811
    81
  apply (induct_tac t)
wenzelm@9811
    82
    apply (simp add: subst_Var)
wenzelm@9811
    83
   apply (intro strip)
wenzelm@9811
    84
   apply (erule par_beta_cases)
wenzelm@9811
    85
    apply simp
wenzelm@9811
    86
   apply (simp add: subst_subst [symmetric])
wenzelm@9811
    87
   apply (fastsimp intro!: par_beta_lift)
wenzelm@9811
    88
  apply fastsimp
wenzelm@9811
    89
  done
wenzelm@9811
    90
wenzelm@9811
    91
wenzelm@9811
    92
subsection {* Confluence (directly) *}
wenzelm@9811
    93
wenzelm@9811
    94
lemma diamond_par_beta: "diamond par_beta"
wenzelm@9811
    95
  apply (unfold diamond_def commute_def square_def)
wenzelm@9811
    96
  apply (rule impI [THEN allI [THEN allI]])
wenzelm@9811
    97
  apply (erule par_beta.induct)
wenzelm@9811
    98
     apply (blast intro!: par_beta_subst)+
wenzelm@9811
    99
  done
wenzelm@9811
   100
wenzelm@9811
   101
wenzelm@9811
   102
subsection {* Complete developments *}
nipkow@1120
   103
nipkow@1120
   104
consts
wenzelm@9811
   105
  "cd" :: "dB => dB"
wenzelm@9811
   106
recdef "cd" "measure size"
wenzelm@9811
   107
  "cd (Var n) = Var n"
wenzelm@9811
   108
  "cd (Var n $ t) = Var n $ cd t"
wenzelm@9811
   109
  "cd ((s1 $ s2) $ t) = cd (s1 $ s2) $ cd t"
wenzelm@9811
   110
  "cd (Abs u $ t) = (cd u)[cd t/0]"
wenzelm@9811
   111
  "cd (Abs s) = Abs (cd s)"
wenzelm@9811
   112
wenzelm@9941
   113
lemma par_beta_cd [rule_format]:
wenzelm@9811
   114
    "\<forall>t. s => t --> t => cd s"
wenzelm@9811
   115
  apply (induct_tac s rule: cd.induct)
wenzelm@9811
   116
      apply auto
wenzelm@9811
   117
  apply (fast intro!: par_beta_subst)
wenzelm@9811
   118
  done
nipkow@1120
   119
wenzelm@9811
   120
wenzelm@9811
   121
subsection {* Confluence (via complete developments) *}
wenzelm@9811
   122
wenzelm@9811
   123
lemma diamond_par_beta2: "diamond par_beta"
wenzelm@9811
   124
  apply (unfold diamond_def commute_def square_def)
wenzelm@9811
   125
  apply (blast intro: par_beta_cd)
wenzelm@9811
   126
  done
wenzelm@9811
   127
wenzelm@9811
   128
theorem beta_confluent: "confluent beta"
wenzelm@9811
   129
  apply (rule diamond_par_beta2 diamond_to_confluence
wenzelm@9811
   130
    par_beta_subset_beta beta_subset_par_beta)+
wenzelm@9811
   131
  done
wenzelm@9811
   132
wenzelm@9811
   133
end