| author | wenzelm |
| Sat, 07 Jul 2007 00:14:56 +0200 | |
| changeset 23615 | 40ab945ef5ff |
| parent 22271 | 51a80e238b29 |
| child 23750 | a1db5f819d00 |
| 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 |
|
| 22271 | 17 |
inductive2 IT :: "dB => bool" |
18 |
where |
|
19 |
Var [intro]: "listsp IT rs ==> IT (Var n \<degree>\<degree> rs)" |
|
20 |
| Lambda [intro]: "IT r ==> IT (Abs r)" |
|
21 |
| Beta [intro]: "IT ((r[s/0]) \<degree>\<degree> ss) ==> IT s ==> IT ((Abs r \<degree> s) \<degree>\<degree> ss)" |
|
| 9716 | 22 |
|
23 |
||
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
24 |
subsection {* Every term in IT terminates *}
|
| 9716 | 25 |
|
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
26 |
lemma double_induction_lemma [rule_format]: |
| 22271 | 27 |
"termi beta s ==> \<forall>t. termi beta t --> |
28 |
(\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> termi beta (Abs r \<degree> s \<degree>\<degree> ss))" |
|
| 9716 | 29 |
apply (erule acc_induct) |
30 |
apply (rule allI) |
|
31 |
apply (rule impI) |
|
| 18513 | 32 |
apply (erule thin_rl) |
| 9716 | 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) |
|
| 22271 | 39 |
apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI' |
| 9716 | 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 |
||
| 22271 | 44 |
lemma IT_implies_termi: "IT t ==> termi beta t" |
| 18241 | 45 |
apply (induct set: IT) |
| 22271 | 46 |
apply (drule rev_predicate1D [OF _ listsp_mono [where B="termi beta"]]) |
47 |
apply fast |
|
| 9716 | 48 |
apply (drule lists_accD) |
49 |
apply (erule acc_induct) |
|
50 |
apply (rule accI) |
|
51 |
apply (blast dest: head_Var_reduction) |
|
52 |
apply (erule acc_induct) |
|
53 |
apply (rule accI) |
|
54 |
apply blast |
|
55 |
apply (blast intro: double_induction_lemma) |
|
56 |
done |
|
57 |
||
58 |
||
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
59 |
subsection {* Every terminating term is in IT *}
|
| 9716 | 60 |
|
| 18241 | 61 |
declare Var_apps_neq_Abs_apps [symmetric, simp] |
| 9716 | 62 |
|
| 12011 | 63 |
lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts" |
| 18241 | 64 |
by (simp add: foldl_Cons [symmetric] del: foldl_Cons) |
| 9716 | 65 |
|
66 |
lemma [simp]: |
|
| 12011 | 67 |
"(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')" |
| 18241 | 68 |
by (simp add: foldl_Cons [symmetric] del: foldl_Cons) |
| 9716 | 69 |
|
| 22271 | 70 |
inductive_cases2 [elim!]: |
71 |
"IT (Var n \<degree>\<degree> ss)" |
|
72 |
"IT (Abs t)" |
|
73 |
"IT (Abs r \<degree> s \<degree>\<degree> ts)" |
|
| 9716 | 74 |
|
| 22271 | 75 |
theorem termi_implies_IT: "termi beta r ==> IT r" |
| 9716 | 76 |
apply (erule acc_induct) |
77 |
apply (rename_tac r) |
|
78 |
apply (erule thin_rl) |
|
79 |
apply (erule rev_mp) |
|
80 |
apply simp |
|
81 |
apply (rule_tac t = r in Apps_dB_induct) |
|
82 |
apply clarify |
|
83 |
apply (rule IT.intros) |
|
84 |
apply clarify |
|
85 |
apply (drule bspec, assumption) |
|
86 |
apply (erule mp) |
|
87 |
apply clarify |
|
| 22271 | 88 |
apply (drule_tac r=beta in conversepI) |
89 |
apply (drule_tac r="beta^--1" in ex_step1I, assumption) |
|
| 9716 | 90 |
apply clarify |
91 |
apply (rename_tac us) |
|
| 12011 | 92 |
apply (erule_tac x = "Var n \<degree>\<degree> us" in allE) |
| 9716 | 93 |
apply force |
94 |
apply (rename_tac u ts) |
|
95 |
apply (case_tac ts) |
|
96 |
apply simp |
|
| 11946 | 97 |
apply blast |
| 9716 | 98 |
apply (rename_tac s ss) |
99 |
apply simp |
|
100 |
apply clarify |
|
101 |
apply (rule IT.intros) |
|
102 |
apply (blast intro: apps_preserves_beta) |
|
103 |
apply (erule mp) |
|
104 |
apply clarify |
|
105 |
apply (rename_tac t) |
|
| 12011 | 106 |
apply (erule_tac x = "Abs u \<degree> t \<degree>\<degree> ss" in allE) |
| 9716 | 107 |
apply force |
108 |
done |
|
| 5261 | 109 |
|
| 11639 | 110 |
end |