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