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
```