| author | wenzelm |
| Thu, 22 Dec 2005 00:29:20 +0100 | |
| changeset 18486 | bf8637d9d53b |
| parent 18241 | afdba6b3e383 |
| child 18513 | 791b53bf4073 |
| 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 |
|
| 16417 | 13 |
theory InductTermi imports ListBeta begin |
| 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 |
| 12011 | 22 |
Var [intro]: "rs : lists IT ==> Var n \<degree>\<degree> rs : IT" |
| 11946 | 23 |
Lambda [intro]: "r : IT ==> Abs r : IT" |
| 12011 | 24 |
Beta [intro]: "(r[s/0]) \<degree>\<degree> ss : IT ==> s : IT ==> (Abs r \<degree> s) \<degree>\<degree> 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 |
|
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
29 |
lemma double_induction_lemma [rule_format]: |
| 9716 | 30 |
"s : termi beta ==> \<forall>t. t : termi beta --> |
| 12011 | 31 |
(\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> Abs r \<degree> s \<degree>\<degree> ss : termi beta)" |
| 9716 | 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" |
|
| 18241 | 48 |
apply (induct set: IT) |
| 9716 | 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 |
|
| 18241 | 66 |
declare Var_apps_neq_Abs_apps [symmetric, simp] |
| 9716 | 67 |
|
| 12011 | 68 |
lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts" |
| 18241 | 69 |
by (simp add: foldl_Cons [symmetric] del: foldl_Cons) |
| 9716 | 70 |
|
71 |
lemma [simp]: |
|
| 12011 | 72 |
"(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')" |
| 18241 | 73 |
by (simp add: foldl_Cons [symmetric] del: foldl_Cons) |
| 9716 | 74 |
|
75 |
inductive_cases [elim!]: |
|
| 12011 | 76 |
"Var n \<degree>\<degree> ss : IT" |
| 9716 | 77 |
"Abs t : IT" |
| 12011 | 78 |
"Abs r \<degree> s \<degree>\<degree> ts : IT" |
| 9716 | 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) |
|
| 12011 | 97 |
apply (erule_tac x = "Var n \<degree>\<degree> us" in allE) |
| 9716 | 98 |
apply force |
99 |
apply (rename_tac u ts) |
|
100 |
apply (case_tac ts) |
|
101 |
apply simp |
|
| 11946 | 102 |
apply blast |
| 9716 | 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) |
|
| 12011 | 111 |
apply (erule_tac x = "Abs u \<degree> t \<degree>\<degree> ss" in allE) |
| 9716 | 112 |
apply force |
113 |
done |
|
| 5261 | 114 |
|
| 11639 | 115 |
end |