src/HOL/Proofs/Lambda/ParRed.thy
author haftmann
Sat, 05 Jul 2014 11:01:53 +0200
changeset 57514 bdc2c6b40bf2
parent 57442 2373b4c61111
child 58889 5b7a9633cfa8
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 36862
diff changeset
     1
(*  Title:      HOL/Proofs/Lambda/ParRed.thy
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
     2
    Author:     Tobias Nipkow
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
     3
    Copyright   1995 TU Muenchen
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
     4
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
     5
Properties of => and "cd", in particular the diamond property of => and
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
     6
confluence of beta.
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
     7
*)
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
     8
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
     9
header {* Parallel reduction and a complete developments *}
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    10
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 12011
diff changeset
    11
theory ParRed imports Lambda Commutation begin
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    12
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    13
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    14
subsection {* Parallel reduction *}
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    15
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    16
inductive par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    17
  where
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    18
    var [simp, intro!]: "Var n => Var n"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    19
  | abs [simp, intro!]: "s => t ==> Abs s => Abs t"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    20
  | app [simp, intro!]: "[| s => s'; t => t' |] ==> s \<degree> t => s' \<degree> t'"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    21
  | beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) \<degree> t => s'[t'/0]"
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    22
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    23
inductive_cases par_beta_cases [elim!]:
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    24
  "Var n => t"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    25
  "Abs s => Abs t"
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11638
diff changeset
    26
  "(Abs s) \<degree> t => u"
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11638
diff changeset
    27
  "s \<degree> t => u"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    28
  "Abs s => t"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    29
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    30
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    31
subsection {* Inclusions *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    32
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    33
text {* @{text "beta \<subseteq> par_beta \<subseteq> beta^*"} \medskip *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    34
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    35
lemma par_beta_varL [simp]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    36
    "(Var n => t) = (t = Var n)"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    37
  by blast
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    38
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    39
lemma par_beta_refl [simp]: "t => t"  (* par_beta_refl [intro!] causes search to blow up *)
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    40
  by (induct t) simp_all
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    41
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    42
lemma beta_subset_par_beta: "beta <= par_beta"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    43
  apply (rule predicate2I)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    44
  apply (erule beta.induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    45
     apply (blast intro!: par_beta_refl)+
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    46
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    47
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    48
lemma par_beta_subset_beta: "par_beta <= beta^**"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    49
  apply (rule predicate2I)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    50
  apply (erule par_beta.induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    51
     apply blast
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    52
    apply (blast del: rtranclp.rtrancl_refl intro: rtranclp.rtrancl_into_rtrancl)+
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    53
      -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    54
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    55
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    56
25972
94b15338da8d tuned document;
wenzelm
parents: 23750
diff changeset
    57
subsection {* Misc properties of @{text "par_beta"} *}
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    58
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    59
lemma par_beta_lift [simp]:
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    60
    "t => t' \<Longrightarrow> lift t n => lift t' n"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 39157
diff changeset
    61
  by (induct t arbitrary: t' n) fastforce+
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    62
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    63
lemma par_beta_subst:
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    64
    "s => s' \<Longrightarrow> t => t' \<Longrightarrow> t[s/n] => t'[s'/n]"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19363
diff changeset
    65
  apply (induct t arbitrary: s s' t' n)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    66
    apply (simp add: subst_Var)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    67
   apply (erule par_beta_cases)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    68
    apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    69
   apply (simp add: subst_subst [symmetric])
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 39157
diff changeset
    70
   apply (fastforce intro!: par_beta_lift)
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 39157
diff changeset
    71
  apply fastforce
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    72
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    73
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    74
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    75
subsection {* Confluence (directly) *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    76
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    77
lemma diamond_par_beta: "diamond par_beta"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    78
  apply (unfold diamond_def commute_def square_def)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    79
  apply (rule impI [THEN allI [THEN allI]])
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    80
  apply (erule par_beta.induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    81
     apply (blast intro!: par_beta_subst)+
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    82
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    83
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    84
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    85
subsection {* Complete developments *}
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    86
35440
bdf8ad377877 killed more recdefs
krauss
parents: 25972
diff changeset
    87
fun
57442
2373b4c61111 removed obsolete Isar system commands -- raw ML console is normally used for system tinkering;
wenzelm
parents: 44890
diff changeset
    88
  cd :: "dB => dB"
35440
bdf8ad377877 killed more recdefs
krauss
parents: 25972
diff changeset
    89
where
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    90
  "cd (Var n) = Var n"
35440
bdf8ad377877 killed more recdefs
krauss
parents: 25972
diff changeset
    91
| "cd (Var n \<degree> t) = Var n \<degree> cd t"
bdf8ad377877 killed more recdefs
krauss
parents: 25972
diff changeset
    92
| "cd ((s1 \<degree> s2) \<degree> t) = cd (s1 \<degree> s2) \<degree> cd t"
bdf8ad377877 killed more recdefs
krauss
parents: 25972
diff changeset
    93
| "cd (Abs u \<degree> t) = (cd u)[cd t/0]"
bdf8ad377877 killed more recdefs
krauss
parents: 25972
diff changeset
    94
| "cd (Abs s) = Abs (cd s)"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    95
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    96
lemma par_beta_cd: "s => t \<Longrightarrow> t => cd s"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19363
diff changeset
    97
  apply (induct s arbitrary: t rule: cd.induct)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    98
      apply auto
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    99
  apply (fast intro!: par_beta_subst)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   100
  done
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
   101
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   102
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   103
subsection {* Confluence (via complete developments) *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   104
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   105
lemma diamond_par_beta2: "diamond par_beta"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   106
  apply (unfold diamond_def commute_def square_def)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   107
  apply (blast intro: par_beta_cd)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   108
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   109
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   110
theorem beta_confluent: "confluent beta"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   111
  apply (rule diamond_par_beta2 diamond_to_confluence
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   112
    par_beta_subset_beta beta_subset_par_beta)+
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   113
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   114
11638
2c3dee321b4b inductive: no collective atts;
wenzelm
parents: 9941
diff changeset
   115
end