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