|
5261
|
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.
|
|
|
7 |
Goes back to
|
|
|
8 |
Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995.
|
|
|
9 |
Also rediscovered by Matthes and Joachimski.
|
|
|
10 |
*)
|
|
|
11 |
|
|
9716
|
12 |
theory InductTermi = ListBeta:
|
|
5261
|
13 |
|
|
9716
|
14 |
consts
|
|
|
15 |
IT :: "dB set"
|
|
|
16 |
|
|
5261
|
17 |
inductive IT
|
|
9716
|
18 |
intros
|
|
|
19 |
Var: "rs : lists IT ==> Var n $$ rs : IT"
|
|
|
20 |
Lambda: "r : IT ==> Abs r : IT"
|
|
|
21 |
Beta: "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT"
|
|
|
22 |
|
|
|
23 |
|
|
|
24 |
text {* Every term in IT terminates. *}
|
|
|
25 |
|
|
|
26 |
lemma double_induction_lemma [rulify]:
|
|
|
27 |
"s : termi beta ==> \<forall>t. t : termi beta -->
|
|
|
28 |
(\<forall>r ss. t = r[s/0] $$ ss --> Abs r $ s $$ ss : termi beta)"
|
|
|
29 |
apply (erule acc_induct)
|
|
|
30 |
apply (erule thin_rl)
|
|
|
31 |
apply (rule allI)
|
|
|
32 |
apply (rule impI)
|
|
|
33 |
apply (erule acc_induct)
|
|
|
34 |
apply clarify
|
|
|
35 |
apply (rule accI)
|
|
9771
|
36 |
apply (safe elim!: apps_betasE)
|
|
9716
|
37 |
apply assumption
|
|
|
38 |
apply (blast intro: subst_preserves_beta apps_preserves_beta)
|
|
|
39 |
apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI
|
|
|
40 |
dest: acc_downwards) (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
|
|
|
41 |
apply (blast dest: apps_preserves_betas)
|
|
|
42 |
done
|
|
|
43 |
|
|
|
44 |
lemma IT_implies_termi: "t : IT ==> t : termi beta"
|
|
|
45 |
apply (erule IT.induct)
|
|
|
46 |
apply (drule rev_subsetD)
|
|
|
47 |
apply (rule lists_mono)
|
|
|
48 |
apply (rule Int_lower2)
|
|
|
49 |
apply simp
|
|
|
50 |
apply (drule lists_accD)
|
|
|
51 |
apply (erule acc_induct)
|
|
|
52 |
apply (rule accI)
|
|
|
53 |
apply (blast dest: head_Var_reduction)
|
|
|
54 |
apply (erule acc_induct)
|
|
|
55 |
apply (rule accI)
|
|
|
56 |
apply blast
|
|
|
57 |
apply (blast intro: double_induction_lemma)
|
|
|
58 |
done
|
|
|
59 |
|
|
|
60 |
|
|
|
61 |
text {* Every terminating term is in IT *}
|
|
|
62 |
|
|
|
63 |
declare Var_apps_neq_Abs_apps [THEN not_sym, simp]
|
|
|
64 |
|
|
|
65 |
lemma [simp, THEN not_sym, simp]: "Var n $$ ss ~= Abs r $ s $$ ts"
|
|
|
66 |
apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
|
|
|
67 |
done
|
|
|
68 |
|
|
|
69 |
lemma [simp]:
|
|
|
70 |
"(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r=r' \<and> s=s' \<and> ss=ss')"
|
|
|
71 |
apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
|
|
|
72 |
done
|
|
|
73 |
|
|
|
74 |
inductive_cases [elim!]:
|
|
|
75 |
"Var n $$ ss : IT"
|
|
|
76 |
"Abs t : IT"
|
|
|
77 |
"Abs r $ s $$ ts : IT"
|
|
|
78 |
|
|
|
79 |
|
|
|
80 |
theorem termi_implies_IT: "r : termi beta ==> r : IT"
|
|
|
81 |
apply (erule acc_induct)
|
|
|
82 |
apply (rename_tac r)
|
|
|
83 |
apply (erule thin_rl)
|
|
|
84 |
apply (erule rev_mp)
|
|
|
85 |
apply simp
|
|
|
86 |
apply (rule_tac t = r in Apps_dB_induct)
|
|
|
87 |
apply clarify
|
|
|
88 |
apply (rule IT.intros)
|
|
|
89 |
apply clarify
|
|
|
90 |
apply (drule bspec, assumption)
|
|
|
91 |
apply (erule mp)
|
|
|
92 |
apply clarify
|
|
|
93 |
apply (drule converseI)
|
|
|
94 |
apply (drule ex_step1I, assumption)
|
|
|
95 |
apply clarify
|
|
|
96 |
apply (rename_tac us)
|
|
|
97 |
apply (erule_tac x = "Var n $$ us" in allE)
|
|
|
98 |
apply force
|
|
|
99 |
apply (rename_tac u ts)
|
|
|
100 |
apply (case_tac ts)
|
|
|
101 |
apply simp
|
|
|
102 |
apply (blast intro: IT.intros)
|
|
|
103 |
apply (rename_tac s ss)
|
|
|
104 |
apply simp
|
|
|
105 |
apply clarify
|
|
|
106 |
apply (rule IT.intros)
|
|
|
107 |
apply (blast intro: apps_preserves_beta)
|
|
|
108 |
apply (erule mp)
|
|
|
109 |
apply clarify
|
|
|
110 |
apply (rename_tac t)
|
|
|
111 |
apply (erule_tac x = "Abs u $ t $$ ss" in allE)
|
|
|
112 |
apply force
|
|
|
113 |
done
|
|
5261
|
114 |
|
|
|
115 |
end
|