src/HOL/Lambda/ParRed.thy
 author wenzelm Wed Oct 31 22:05:37 2001 +0100 (2001-10-31) changeset 12011 1a3a7b3cd9bb parent 11638 2c3dee321b4b child 16417 9bc16273c2d4 permissions -rw-r--r--
tuned notation (degree instead of dollar);
```     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 = Lambda + Commutation:
```
```    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
```