# Theory ListBeta

Up to index of Isabelle/HOL/Lambda

theory ListBeta
imports ListApplication ListOrder
begin

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

    header {* Lifting beta-reduction to lists *}

    theory ListBeta imports ListApplication ListOrder begin

    text {*
      Lifting beta-reduction to lists of terms, reducing exactly one element.
    *}

    syntax
      "_list_beta" :: "dB => dB => bool"   (infixl "=>" 50)
    translations
      "rs => ss" == "(rs, ss) : step1 beta"

    lemma head_Var_reduction_aux:
      "v -> v' ==> ∀rs. v = Var n °° rs --> (∃ss. rs => ss ∧ v' = Var n °° ss)"
      apply (erule beta.induct)
         apply simp
        apply (rule allI)
        apply (rule_tac xs = rs in rev_exhaust)
         apply simp
        apply (force intro: append_step1I)
       apply (rule allI)
       apply (rule_tac xs = rs in rev_exhaust)
        apply simp
        apply (auto 0 3 intro: disjI2 [THEN append_step1I])
      done

    lemma head_Var_reduction:
      "Var n °° rs -> v ==> (∃ss. rs => ss ∧ v = Var n °° ss)"
      apply (drule head_Var_reduction_aux)
      apply blast
      done

    lemma apps_betasE_aux:
      "u -> u' ==> ∀r rs. u = r °° rs -->
        ((∃r'. r -> r' ∧ u' = r' °° rs) ∨
         (∃rs'. rs => rs' ∧ u' = r °° rs') ∨
         (∃s t ts. r = Abs s ∧ rs = t # ts ∧ u' = s[t/0] °° ts))"
      apply (erule beta.induct)
         apply (clarify del: disjCI)
         apply (case_tac r)
           apply simp
          apply (simp add: App_eq_foldl_conv)
          apply (split split_if_asm)
           apply simp
           apply blast
          apply simp
         apply (simp add: App_eq_foldl_conv)
         apply (split split_if_asm)
          apply simp
         apply simp
        apply (clarify del: disjCI)
        apply (drule App_eq_foldl_conv [THEN iffD1])
        apply (split split_if_asm)
         apply simp
         apply blast
        apply (force intro!: disjI1 [THEN append_step1I])
       apply (clarify del: disjCI)
       apply (drule App_eq_foldl_conv [THEN iffD1])
       apply (split split_if_asm)
        apply simp
        apply blast
       apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
      done

    lemma apps_betasE [elim!]:
      "[| r °° rs -> s; !!r'. [| r -> r'; s = r' °° rs |] ==> R;
        !!rs'. [| rs => rs'; s = r °° rs' |] ==> R;
        !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] °° us |] ==> R |]
      ==> R"
    proof -
      assume major: "r °° rs -> s"
      case rule_context
      show ?thesis
        apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
        apply (assumption | rule refl | erule prems exE conjE impE disjE)+
        done
    qed

    lemma apps_preserves_beta [simp]:
        "r -> s ==> r °° ss -> s °° ss"
      apply (induct_tac ss rule: rev_induct)
      apply auto
      done

    lemma apps_preserves_beta2 [simp]:
        "r ->> s ==> r °° ss ->> s °° ss"
      apply (erule rtrancl_induct)
       apply blast
      apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
      done

    lemma apps_preserves_betas [rule_format, simp]:
        "∀ss. rs => ss --> r °° rs -> r °° ss"
      apply (induct_tac rs rule: rev_induct)
       apply simp
      apply simp
      apply clarify
      apply (rule_tac xs = ss in rev_exhaust)
       apply simp
      apply simp
      apply (drule Snoc_step1_SnocD)
      apply blast
      done

    end

lemma head_Var_reduction_aux:

      v -> v' ==> ∀rs. v = Var n °° rs --> (∃ss. rs => ss ∧ v' = Var n °° ss)

lemma head_Var_reduction:

      Var n °° rs -> v ==> ∃ss. rs => ss ∧ v = Var n °° ss

lemma apps_betasE_aux:

      u -> u'
      ==> ∀r rs. u = r °° rs -->
                 (∃r'. r -> r' ∧ u' = r' °° rs) ∨
                 (∃rs'. rs => rs' ∧ u' = r °° rs') ∨
                 (∃s t ts. r = Abs s ∧ rs = t # ts ∧ u' = s[t/0] °° ts)

lemma apps_betasE:

      [| r °° rs -> s; !!r'. [| r -> r'; s = r' °° rs |] ==> R;
         !!rs'. [| rs => rs'; s = r °° rs' |] ==> R;
         !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] °° us |] ==> R |]
      ==> R

lemma apps_preserves_beta:

      r -> s ==> r °° ss -> s °° ss

lemma apps_preserves_beta2:

      r ->> s ==> r °° ss ->> s °° ss

lemma apps_preserves_betas:

      rs => ss ==> r °° rs -> r °° ss