1(* Title: HOL/Proofs/Lambda/InductTermi.thy 2 Author: Tobias Nipkow 3 Copyright 1998 TU Muenchen 4 5Inductive characterization of terminating lambda terms. Goes back to 6Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995. Also 7rediscovered by Matthes and Joachimski. 8*) 9 10section \<open>Inductive characterization of terminating lambda terms\<close> 11 12theory InductTermi imports ListBeta begin 13 14subsection \<open>Terminating lambda terms\<close> 15 16inductive 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 23subsection \<open>Every term in \<open>IT\<close> terminates\<close> 24 25lemma 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 42lemma 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 57subsection \<open>Every terminating term is in \<open>IT\<close>\<close> 58 59declare Var_apps_neq_Abs_apps [symmetric, simp] 60 61lemma [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 64lemma [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 68inductive_cases [elim!]: 69 "IT (Var n \<degree>\<degree> ss)" 70 "IT (Abs t)" 71 "IT (Abs r \<degree> s \<degree>\<degree> ts)" 72 73theorem 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\<inverse>\<inverse>" 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 108end 109