# Theory ParRed

Up to index of Isabelle/HOL/Lambda

theory ParRed
imports Lambda Commutation
begin

    (*  Title:      HOL/Lambda/ParRed.thy
        ID:         $Id: ParRed.thy,v 1.18 2005/06/17 14:13:08 haftmann Exp $
        Author:     Tobias Nipkow
        Copyright   1995 TU Muenchen

    Properties of => and "cd", in particular the diamond property of => and
    confluence of beta.
    *)

    header {* Parallel reduction and a complete developments *}

    theory ParRed imports Lambda Commutation begin

    subsection {* Parallel reduction *}

    consts
      par_beta :: "(dB × dB) set"

    syntax
      par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
    translations
      "s => t" == "(s, t) ∈ par_beta"

    inductive par_beta
      intros
        var [simp, intro!]: "Var n => Var n"
        abs [simp, intro!]: "s => t ==> Abs s => Abs t"
        app [simp, intro!]: "[| s => s'; t => t' |] ==> s ° t => s' ° t'"
        beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) ° t => s'[t'/0]"

    inductive_cases par_beta_cases [elim!]:
      "Var n => t"
      "Abs s => Abs t"
      "(Abs s) ° t => u"
      "s ° t => u"
      "Abs s => t"

    subsection {* Inclusions *}

    text {* @{text "beta ⊆ par_beta ⊆ beta^*"} \medskip *}

    lemma par_beta_varL [simp]:
        "(Var n => t) = (t = Var n)"
      apply blast
      done

    lemma par_beta_refl [simp]: "t => t"  (* par_beta_refl [intro!] causes search to blow up *)
      apply (induct_tac t)
        apply simp_all
      done

    lemma beta_subset_par_beta: "beta <= par_beta"
      apply (rule subsetI)
      apply clarify
      apply (erule beta.induct)
         apply (blast intro!: par_beta_refl)+
      done

    lemma par_beta_subset_beta: "par_beta <= beta^*"
      apply (rule subsetI)
      apply clarify
      apply (erule par_beta.induct)
         apply blast
        apply (blast del: rtrancl_refl intro: rtrancl_into_rtrancl)+
          -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *}
      done

    subsection {* Misc properties of par-beta *}

    lemma par_beta_lift [rule_format, simp]:
        "∀t' n. t => t' --> lift t n => lift t' n"
      apply (induct_tac t)
        apply fastsimp+
      done

    lemma par_beta_subst [rule_format]:
        "∀s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"
      apply (induct_tac t)
        apply (simp add: subst_Var)
       apply (intro strip)
       apply (erule par_beta_cases)
        apply simp
       apply (simp add: subst_subst [symmetric])
       apply (fastsimp intro!: par_beta_lift)
      apply fastsimp
      done

    subsection {* Confluence (directly) *}

    lemma diamond_par_beta: "diamond par_beta"
      apply (unfold diamond_def commute_def square_def)
      apply (rule impI [THEN allI [THEN allI]])
      apply (erule par_beta.induct)
         apply (blast intro!: par_beta_subst)+
      done

    subsection {* Complete developments *}

    consts
      "cd" :: "dB => dB"
    recdef "cd" "measure size"
      "cd (Var n) = Var n"
      "cd (Var n ° t) = Var n ° cd t"
      "cd ((s1 ° s2) ° t) = cd (s1 ° s2) ° cd t"
      "cd (Abs u ° t) = (cd u)[cd t/0]"
      "cd (Abs s) = Abs (cd s)"

    lemma par_beta_cd [rule_format]:
        "∀t. s => t --> t => cd s"
      apply (induct_tac s rule: cd.induct)
          apply auto
      apply (fast intro!: par_beta_subst)
      done

    subsection {* Confluence (via complete developments) *}

    lemma diamond_par_beta2: "diamond par_beta"
      apply (unfold diamond_def commute_def square_def)
      apply (blast intro: par_beta_cd)
      done

    theorem beta_confluent: "confluent beta"
      apply (rule diamond_par_beta2 diamond_to_confluence
        par_beta_subset_beta beta_subset_par_beta)+
      done

    end

### Parallel reduction

lemmas par_beta_cases:

      [| Var n => t; t = Var n ==> P |] ==> P

      [| Abs s => Abs t; s => t ==> P |] ==> P

      [| Abs s ° t => u; !!s' t'. [| Abs s => s'; t => t'; u = s' ° t' |] ==> P;
         !!s' t'. [| s => s'; t => t'; u = s'[t'/0] |] ==> P |]
      ==> P

      [| s ° t => u; !!s' t'. [| s => s'; t => t'; u = s' ° t' |] ==> P;
         !!s s' t'. [| s => s'; t => t'; u = s'[t'/0]; s = Abs s |] ==> P |]
      ==> P

      [| Abs s => t; !!t. [| s => t; t = Abs t |] ==> P |] ==> P

### Inclusions

lemma par_beta_varL:

      (Var n => t) = (t = Var n)

lemma par_beta_refl:

      t => t

lemma beta_subset_par_beta:

      beta ⊆ op =>

lemma par_beta_subset_beta:

      op => ⊆ beta*

### Misc properties of par-beta

lemma par_beta_lift:

      t => t' ==> lift t n => lift t' n

lemma par_beta_subst:

      [| s => s'; t => t' |] ==> t[s/n] => t'[s'/n]

### Confluence (directly)

lemma diamond_par_beta:

      diamond op =>

### Complete developments

lemma par_beta_cd:

      s => t ==> t => cd s

### Confluence (via complete developments)

lemma diamond_par_beta2:

      diamond op =>

theorem beta_confluent:

      confluent beta