# Theory InductTermi

Up to index of Isabelle/HOL/Lambda

theory InductTermi
imports ListBeta
begin

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

    Inductive characterization of terminating lambda terms.  Goes back to
    Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995.  Also
    rediscovered by Matthes and Joachimski.
    *)

    header {* Inductive characterization of terminating lambda terms *}

    theory InductTermi imports ListBeta begin

    subsection {* Terminating lambda terms *}

    consts
      IT :: "dB set"

    inductive IT
      intros
        Var [intro]: "rs : lists IT ==> Var n °° rs : IT"
        Lambda [intro]: "r : IT ==> Abs r : IT"
        Beta [intro]: "(r[s/0]) °° ss : IT ==> s : IT ==> (Abs r ° s) °° ss : IT"

    subsection {* Every term in IT terminates *}

    lemma double_induction_lemma [rule_format]:
      "s : termi beta ==> ∀t. t : termi beta -->
        (∀r ss. t = r[s/0] °° ss --> Abs r ° s °° ss : termi beta)"
      apply (erule acc_induct)
      apply (erule thin_rl)
      apply (rule allI)
      apply (rule impI)
      apply (erule acc_induct)
      apply clarify
      apply (rule accI)
      apply (safe elim!: apps_betasE)
         apply assumption
        apply (blast intro: subst_preserves_beta apps_preserves_beta)
       apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI
         dest: acc_downwards)  (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
      apply (blast dest: apps_preserves_betas)
      done

    lemma IT_implies_termi: "t : IT ==> t : termi beta"
      apply (erule IT.induct)
        apply (drule rev_subsetD)
         apply (rule lists_mono)
         apply (rule Int_lower2)
        apply simp
        apply (drule lists_accD)
        apply (erule acc_induct)
        apply (rule accI)
        apply (blast dest: head_Var_reduction)
       apply (erule acc_induct)
       apply (rule accI)
       apply blast
      apply (blast intro: double_induction_lemma)
      done

    subsection {* Every terminating term is in IT *}

    declare Var_apps_neq_Abs_apps [THEN not_sym, simp]

    lemma [simp, THEN not_sym, simp]: "Var n °° ss ≠ Abs r ° s °° ts"
      apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
      done

    lemma [simp]:
      "(Abs r ° s °° ss = Abs r' ° s' °° ss') = (r = r' ∧ s = s' ∧ ss = ss')"
      apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
      done

    inductive_cases [elim!]:
      "Var n °° ss : IT"
      "Abs t : IT"
      "Abs r ° s °° ts : IT"

    theorem termi_implies_IT: "r : termi beta ==> r : IT"
      apply (erule acc_induct)
      apply (rename_tac r)
      apply (erule thin_rl)
      apply (erule rev_mp)
      apply simp
      apply (rule_tac t = r in Apps_dB_induct)
       apply clarify
       apply (rule IT.intros)
       apply clarify
       apply (drule bspec, assumption)
       apply (erule mp)
       apply clarify
       apply (drule converseI)
       apply (drule ex_step1I, assumption)
       apply clarify
       apply (rename_tac us)
       apply (erule_tac x = "Var n °° us" in allE)
       apply force
       apply (rename_tac u ts)
       apply (case_tac ts)
        apply simp
        apply blast
       apply (rename_tac s ss)
       apply simp
       apply clarify
       apply (rule IT.intros)
        apply (blast intro: apps_preserves_beta)
       apply (erule mp)
       apply clarify
       apply (rename_tac t)
       apply (erule_tac x = "Abs u ° t °° ss" in allE)
       apply force
       done

    end

### Terminating lambda terms

### Every term in IT terminates

lemma double_induction_lemma:

      [| s ∈ termi beta; t ∈ termi beta; t = r[s/0] °° ss |]
      ==> Abs r ° s °° ss ∈ termi beta

lemma IT_implies_termi:

      t ∈ IT ==> t ∈ termi beta

### Every terminating term is in IT

lemma

      Abs r1 ° s1 °° ts1 ≠ Var n1 °° ss1

lemma

      (Abs r ° s °° ss = Abs r' ° s' °° ss') = (r = r' ∧ s = s' ∧ ss = ss')

lemmas

      [| Var n °° ss ∈ IT; ss ∈ lists IT ==> P |] ==> P

      [| Abs t ∈ IT; t ∈ IT ==> P |] ==> P

      [| Abs r ° s °° ts ∈ IT; [| r[s/0] °° ts ∈ IT; s ∈ IT |] ==> P |] ==> P

theorem termi_implies_IT:

      r ∈ termi beta ==> r ∈ IT