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