src/HOL/Lambda/InductTermi.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 26806 40b411ec05aa
child 36862 952b2b102a0a
permissions -rw-r--r--
added lemmas
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
haftmann@16417
    13
theory InductTermi imports ListBeta begin
nipkow@5261
    14
wenzelm@9811
    15
subsection {* Terminating lambda terms *}
wenzelm@9811
    16
berghofe@23750
    17
inductive IT :: "dB => bool"
berghofe@22271
    18
  where
berghofe@22271
    19
    Var [intro]: "listsp IT rs ==> IT (Var n \<degree>\<degree> rs)"
berghofe@22271
    20
  | Lambda [intro]: "IT r ==> IT (Abs r)"
berghofe@22271
    21
  | Beta [intro]: "IT ((r[s/0]) \<degree>\<degree> ss) ==> IT s ==> IT ((Abs r \<degree> s) \<degree>\<degree> ss)"
wenzelm@9716
    22
wenzelm@9716
    23
wenzelm@25972
    24
subsection {* Every term in @{text "IT"} terminates *}
wenzelm@9716
    25
wenzelm@9941
    26
lemma double_induction_lemma [rule_format]:
berghofe@23750
    27
  "termip beta s ==> \<forall>t. termip beta t -->
berghofe@23750
    28
    (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> termip beta (Abs r \<degree> s \<degree>\<degree> ss))"
berghofe@23750
    29
  apply (erule accp_induct)
wenzelm@9716
    30
  apply (rule allI)
wenzelm@9716
    31
  apply (rule impI)
wenzelm@18513
    32
  apply (erule thin_rl)
berghofe@23750
    33
  apply (erule accp_induct)
wenzelm@9716
    34
  apply clarify
berghofe@23750
    35
  apply (rule accp.accI)
wenzelm@9771
    36
  apply (safe elim!: apps_betasE)
wenzelm@9716
    37
    apply (blast intro: subst_preserves_beta apps_preserves_beta)
berghofe@23750
    38
   apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtranclp_converseI
berghofe@23750
    39
     dest: accp_downwards)  (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
wenzelm@9716
    40
  apply (blast dest: apps_preserves_betas)
wenzelm@9716
    41
  done
wenzelm@9716
    42
berghofe@23750
    43
lemma IT_implies_termi: "IT t ==> termip beta t"
wenzelm@18241
    44
  apply (induct set: IT)
berghofe@23750
    45
    apply (drule rev_predicate1D [OF _ listsp_mono [where B="termip beta"]])
berghofe@26806
    46
    apply (fast intro!: predicate1I)
wenzelm@9716
    47
    apply (drule lists_accD)
berghofe@23750
    48
    apply (erule accp_induct)
berghofe@23750
    49
    apply (rule accp.accI)
wenzelm@9716
    50
    apply (blast dest: head_Var_reduction)
berghofe@23750
    51
   apply (erule accp_induct)
berghofe@23750
    52
   apply (rule accp.accI)
wenzelm@9716
    53
   apply blast
wenzelm@9716
    54
  apply (blast intro: double_induction_lemma)
wenzelm@9716
    55
  done
wenzelm@9716
    56
wenzelm@9716
    57
wenzelm@25972
    58
subsection {* Every terminating term is in @{text "IT"} *}
wenzelm@9716
    59
wenzelm@18241
    60
declare Var_apps_neq_Abs_apps [symmetric, simp]
wenzelm@9716
    61
wenzelm@12011
    62
lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts"
wenzelm@18241
    63
  by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
wenzelm@9716
    64
wenzelm@9716
    65
lemma [simp]:
wenzelm@12011
    66
  "(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')"
wenzelm@18241
    67
  by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
wenzelm@9716
    68
berghofe@23750
    69
inductive_cases [elim!]:
berghofe@22271
    70
  "IT (Var n \<degree>\<degree> ss)"
berghofe@22271
    71
  "IT (Abs t)"
berghofe@22271
    72
  "IT (Abs r \<degree> s \<degree>\<degree> ts)"
wenzelm@9716
    73
berghofe@23750
    74
theorem termi_implies_IT: "termip beta r ==> IT r"
berghofe@23750
    75
  apply (erule accp_induct)
wenzelm@9716
    76
  apply (rename_tac r)
wenzelm@9716
    77
  apply (erule thin_rl)
wenzelm@9716
    78
  apply (erule rev_mp)
wenzelm@9716
    79
  apply simp
wenzelm@9716
    80
  apply (rule_tac t = r in Apps_dB_induct)
wenzelm@9716
    81
   apply clarify
wenzelm@9716
    82
   apply (rule IT.intros)
wenzelm@9716
    83
   apply clarify
wenzelm@9716
    84
   apply (drule bspec, assumption)
wenzelm@9716
    85
   apply (erule mp)
wenzelm@9716
    86
   apply clarify
berghofe@22271
    87
   apply (drule_tac r=beta in conversepI)
berghofe@22271
    88
   apply (drule_tac r="beta^--1" in ex_step1I, assumption)
wenzelm@9716
    89
   apply clarify
wenzelm@9716
    90
   apply (rename_tac us)
wenzelm@12011
    91
   apply (erule_tac x = "Var n \<degree>\<degree> us" in allE)
wenzelm@9716
    92
   apply force
wenzelm@9716
    93
   apply (rename_tac u ts)
wenzelm@9716
    94
   apply (case_tac ts)
wenzelm@9716
    95
    apply simp
wenzelm@11946
    96
    apply blast
wenzelm@9716
    97
   apply (rename_tac s ss)
wenzelm@9716
    98
   apply simp
wenzelm@9716
    99
   apply clarify
wenzelm@9716
   100
   apply (rule IT.intros)
wenzelm@9716
   101
    apply (blast intro: apps_preserves_beta)
wenzelm@9716
   102
   apply (erule mp)
wenzelm@9716
   103
   apply clarify
wenzelm@9716
   104
   apply (rename_tac t)
wenzelm@12011
   105
   apply (erule_tac x = "Abs u \<degree> t \<degree>\<degree> ss" in allE)
wenzelm@9716
   106
   apply force
wenzelm@9716
   107
   done
nipkow@5261
   108
wenzelm@11639
   109
end