src/HOL/Lambda/InductTermi.thy
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 11639 4213422388c4
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
     1 (*  Title:      HOL/Lambda/InductTermi.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1998 TU Muenchen
     5 
     6 Inductive characterization of terminating lambda terms.  Goes back to
     7 Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995.  Also
     8 rediscovered by Matthes and Joachimski.
     9 *)
    10 
    11 header {* Inductive characterization of terminating lambda terms *}
    12 
    13 theory InductTermi = ListBeta:
    14 
    15 subsection {* Terminating lambda terms *}
    16 
    17 consts
    18   IT :: "dB set"
    19 
    20 inductive IT
    21   intros
    22     Var: "rs : lists IT ==> Var n $$ rs : IT"
    23     Lambda: "r : IT ==> Abs r : IT"
    24     Beta: "[| (r[s/0]) $$ ss : IT; s : IT |] ==> (Abs r $ s) $$ ss : IT"
    25 
    26 
    27 subsection {* Every term in IT terminates *}
    28 
    29 lemma double_induction_lemma [rule_format]:
    30   "s : termi beta ==> \<forall>t. t : termi beta -->
    31     (\<forall>r ss. t = r[s/0] $$ ss --> Abs r $ s $$ ss : termi beta)"
    32   apply (erule acc_induct)
    33   apply (erule thin_rl)
    34   apply (rule allI)
    35   apply (rule impI)
    36   apply (erule acc_induct)
    37   apply clarify
    38   apply (rule accI)
    39   apply (safe elim!: apps_betasE)
    40      apply assumption
    41     apply (blast intro: subst_preserves_beta apps_preserves_beta)
    42    apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI
    43      dest: acc_downwards)  (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
    44   apply (blast dest: apps_preserves_betas)
    45   done
    46 
    47 lemma IT_implies_termi: "t : IT ==> t : termi beta"
    48   apply (erule IT.induct)
    49     apply (drule rev_subsetD)
    50      apply (rule lists_mono)
    51      apply (rule Int_lower2)
    52     apply simp
    53     apply (drule lists_accD)
    54     apply (erule acc_induct)
    55     apply (rule accI)
    56     apply (blast dest: head_Var_reduction)
    57    apply (erule acc_induct)
    58    apply (rule accI)
    59    apply blast
    60   apply (blast intro: double_induction_lemma)
    61   done
    62 
    63 
    64 subsection {* Every terminating term is in IT *}
    65 
    66 declare Var_apps_neq_Abs_apps [THEN not_sym, simp]
    67 
    68 lemma [simp, THEN not_sym, simp]: "Var n $$ ss ~= Abs r $ s $$ ts"
    69   apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
    70   done
    71 
    72 lemma [simp]:
    73   "(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r = r' \<and> s = s' \<and> ss = ss')"
    74   apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
    75   done
    76 
    77 inductive_cases [elim!]:
    78   "Var n $$ ss : IT"
    79   "Abs t : IT"
    80   "Abs r $ s $$ ts : IT"
    81 
    82 theorem termi_implies_IT: "r : termi beta ==> r : IT"
    83   apply (erule acc_induct)
    84   apply (rename_tac r)
    85   apply (erule thin_rl)
    86   apply (erule rev_mp)
    87   apply simp
    88   apply (rule_tac t = r in Apps_dB_induct)
    89    apply clarify
    90    apply (rule IT.intros)
    91    apply clarify
    92    apply (drule bspec, assumption)
    93    apply (erule mp)
    94    apply clarify
    95    apply (drule converseI)
    96    apply (drule ex_step1I, assumption)
    97    apply clarify
    98    apply (rename_tac us)
    99    apply (erule_tac x = "Var n $$ us" in allE)
   100    apply force
   101    apply (rename_tac u ts)
   102    apply (case_tac ts)
   103     apply simp
   104     apply (blast intro: IT.intros)
   105    apply (rename_tac s ss)
   106    apply simp
   107    apply clarify
   108    apply (rule IT.intros)
   109     apply (blast intro: apps_preserves_beta)
   110    apply (erule mp)
   111    apply clarify
   112    apply (rename_tac t)
   113    apply (erule_tac x = "Abs u $ t $$ ss" in allE)
   114    apply force
   115    done
   116 
   117 end