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