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