src/HOL/Proofs/Lambda/InductTermi.thy
author wenzelm
Thu May 24 17:25:53 2012 +0200 (2012-05-24)
changeset 47988 e4b69e10b990
parent 39157 b98909faaea8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Proofs/Lambda/InductTermi.thy
     2     Author:     Tobias Nipkow
     3     Copyright   1998 TU Muenchen
     4 
     5 Inductive characterization of terminating lambda terms.  Goes back to
     6 Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995.  Also
     7 rediscovered by Matthes and Joachimski.
     8 *)
     9 
    10 header {* Inductive characterization of terminating lambda terms *}
    11 
    12 theory InductTermi imports ListBeta begin
    13 
    14 subsection {* Terminating lambda terms *}
    15 
    16 inductive IT :: "dB => bool"
    17   where
    18     Var [intro]: "listsp IT rs ==> IT (Var n \<degree>\<degree> rs)"
    19   | Lambda [intro]: "IT r ==> IT (Abs r)"
    20   | Beta [intro]: "IT ((r[s/0]) \<degree>\<degree> ss) ==> IT s ==> IT ((Abs r \<degree> s) \<degree>\<degree> ss)"
    21 
    22 
    23 subsection {* Every term in @{text "IT"} terminates *}
    24 
    25 lemma double_induction_lemma [rule_format]:
    26   "termip beta s ==> \<forall>t. termip beta t -->
    27     (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> termip beta (Abs r \<degree> s \<degree>\<degree> ss))"
    28   apply (erule accp_induct)
    29   apply (rule allI)
    30   apply (rule impI)
    31   apply (erule thin_rl)
    32   apply (erule accp_induct)
    33   apply clarify
    34   apply (rule accp.accI)
    35   apply (safe elim!: apps_betasE)
    36     apply (blast intro: subst_preserves_beta apps_preserves_beta)
    37    apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtranclp_converseI
    38      dest: accp_downwards)  (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
    39   apply (blast dest: apps_preserves_betas)
    40   done
    41 
    42 lemma IT_implies_termi: "IT t ==> termip beta t"
    43   apply (induct set: IT)
    44     apply (drule rev_predicate1D [OF _ listsp_mono [where B="termip beta"]])
    45     apply (fast intro!: predicate1I)
    46     apply (drule lists_accD)
    47     apply (erule accp_induct)
    48     apply (rule accp.accI)
    49     apply (blast dest: head_Var_reduction)
    50    apply (erule accp_induct)
    51    apply (rule accp.accI)
    52    apply blast
    53   apply (blast intro: double_induction_lemma)
    54   done
    55 
    56 
    57 subsection {* Every terminating term is in @{text "IT"} *}
    58 
    59 declare Var_apps_neq_Abs_apps [symmetric, simp]
    60 
    61 lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts"
    62   by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
    63 
    64 lemma [simp]:
    65   "(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')"
    66   by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
    67 
    68 inductive_cases [elim!]:
    69   "IT (Var n \<degree>\<degree> ss)"
    70   "IT (Abs t)"
    71   "IT (Abs r \<degree> s \<degree>\<degree> ts)"
    72 
    73 theorem termi_implies_IT: "termip beta r ==> IT r"
    74   apply (erule accp_induct)
    75   apply (rename_tac r)
    76   apply (erule thin_rl)
    77   apply (erule rev_mp)
    78   apply simp
    79   apply (rule_tac t = r in Apps_dB_induct)
    80    apply clarify
    81    apply (rule IT.intros)
    82    apply clarify
    83    apply (drule bspec, assumption)
    84    apply (erule mp)
    85    apply clarify
    86    apply (drule_tac r=beta in conversepI)
    87    apply (drule_tac r="beta^--1" in ex_step1I, assumption)
    88    apply clarify
    89    apply (rename_tac us)
    90    apply (erule_tac x = "Var n \<degree>\<degree> us" in allE)
    91    apply force
    92    apply (rename_tac u ts)
    93    apply (case_tac ts)
    94     apply simp
    95     apply blast
    96    apply (rename_tac s ss)
    97    apply simp
    98    apply clarify
    99    apply (rule IT.intros)
   100     apply (blast intro: apps_preserves_beta)
   101    apply (erule mp)
   102    apply clarify
   103    apply (rename_tac t)
   104    apply (erule_tac x = "Abs u \<degree> t \<degree>\<degree> ss" in allE)
   105    apply force
   106    done
   107 
   108 end