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