src/HOL/Lambda/ParRed.thy
author nipkow
Thu Dec 11 08:52:50 2008 +0100 (2008-12-11)
changeset 29106 25e28a4070f3
parent 25972 94b15338da8d
child 35440 bdf8ad377877
permissions -rw-r--r--
Testfile for Stefan's code generator
     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 inductive par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
    18   where
    19     var [simp, intro!]: "Var n => Var n"
    20   | abs [simp, intro!]: "s => t ==> Abs s => Abs t"
    21   | app [simp, intro!]: "[| s => s'; t => t' |] ==> s \<degree> t => s' \<degree> t'"
    22   | beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) \<degree> t => s'[t'/0]"
    23 
    24 inductive_cases par_beta_cases [elim!]:
    25   "Var n => t"
    26   "Abs s => Abs t"
    27   "(Abs s) \<degree> t => u"
    28   "s \<degree> t => u"
    29   "Abs s => t"
    30 
    31 
    32 subsection {* Inclusions *}
    33 
    34 text {* @{text "beta \<subseteq> par_beta \<subseteq> beta^*"} \medskip *}
    35 
    36 lemma par_beta_varL [simp]:
    37     "(Var n => t) = (t = Var n)"
    38   by blast
    39 
    40 lemma par_beta_refl [simp]: "t => t"  (* par_beta_refl [intro!] causes search to blow up *)
    41   by (induct t) simp_all
    42 
    43 lemma beta_subset_par_beta: "beta <= par_beta"
    44   apply (rule predicate2I)
    45   apply (erule beta.induct)
    46      apply (blast intro!: par_beta_refl)+
    47   done
    48 
    49 lemma par_beta_subset_beta: "par_beta <= beta^**"
    50   apply (rule predicate2I)
    51   apply (erule par_beta.induct)
    52      apply blast
    53     apply (blast del: rtranclp.rtrancl_refl intro: rtranclp.rtrancl_into_rtrancl)+
    54       -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *}
    55   done
    56 
    57 
    58 subsection {* Misc properties of @{text "par_beta"} *}
    59 
    60 lemma par_beta_lift [simp]:
    61     "t => t' \<Longrightarrow> lift t n => lift t' n"
    62   by (induct t arbitrary: t' n) fastsimp+
    63 
    64 lemma par_beta_subst:
    65     "s => s' \<Longrightarrow> t => t' \<Longrightarrow> t[s/n] => t'[s'/n]"
    66   apply (induct t arbitrary: s s' t' n)
    67     apply (simp add: subst_Var)
    68    apply (erule par_beta_cases)
    69     apply simp
    70    apply (simp add: subst_subst [symmetric])
    71    apply (fastsimp intro!: par_beta_lift)
    72   apply fastsimp
    73   done
    74 
    75 
    76 subsection {* Confluence (directly) *}
    77 
    78 lemma diamond_par_beta: "diamond par_beta"
    79   apply (unfold diamond_def commute_def square_def)
    80   apply (rule impI [THEN allI [THEN allI]])
    81   apply (erule par_beta.induct)
    82      apply (blast intro!: par_beta_subst)+
    83   done
    84 
    85 
    86 subsection {* Complete developments *}
    87 
    88 consts
    89   "cd" :: "dB => dB"
    90 recdef "cd" "measure size"
    91   "cd (Var n) = Var n"
    92   "cd (Var n \<degree> t) = Var n \<degree> cd t"
    93   "cd ((s1 \<degree> s2) \<degree> t) = cd (s1 \<degree> s2) \<degree> cd t"
    94   "cd (Abs u \<degree> t) = (cd u)[cd t/0]"
    95   "cd (Abs s) = Abs (cd s)"
    96 
    97 lemma par_beta_cd: "s => t \<Longrightarrow> t => cd s"
    98   apply (induct s arbitrary: t rule: cd.induct)
    99       apply auto
   100   apply (fast intro!: par_beta_subst)
   101   done
   102 
   103 
   104 subsection {* Confluence (via complete developments) *}
   105 
   106 lemma diamond_par_beta2: "diamond par_beta"
   107   apply (unfold diamond_def commute_def square_def)
   108   apply (blast intro: par_beta_cd)
   109   done
   110 
   111 theorem beta_confluent: "confluent beta"
   112   apply (rule diamond_par_beta2 diamond_to_confluence
   113     par_beta_subset_beta beta_subset_par_beta)+
   114   done
   115 
   116 end