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