| author | wenzelm |
| Mon, 08 Feb 2010 21:26:52 +0100 | |
| changeset 35053 | 43175817d83b |
| parent 26806 | 40b411ec05aa |
| child 36862 | 952b2b102a0a |
| 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 |
|
| 23750 | 17 |
inductive IT :: "dB => bool" |
| 22271 | 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 |
||
| 25972 | 24 |
subsection {* Every term in @{text "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]: |
| 23750 | 27 |
"termip beta s ==> \<forall>t. termip beta t --> |
28 |
(\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> termip beta (Abs r \<degree> s \<degree>\<degree> ss))" |
|
29 |
apply (erule accp_induct) |
|
| 9716 | 30 |
apply (rule allI) |
31 |
apply (rule impI) |
|
| 18513 | 32 |
apply (erule thin_rl) |
| 23750 | 33 |
apply (erule accp_induct) |
| 9716 | 34 |
apply clarify |
| 23750 | 35 |
apply (rule accp.accI) |
| 9771 | 36 |
apply (safe elim!: apps_betasE) |
| 9716 | 37 |
apply (blast intro: subst_preserves_beta apps_preserves_beta) |
| 23750 | 38 |
apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtranclp_converseI |
39 |
dest: accp_downwards) (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *) |
|
| 9716 | 40 |
apply (blast dest: apps_preserves_betas) |
41 |
done |
|
42 |
||
| 23750 | 43 |
lemma IT_implies_termi: "IT t ==> termip beta t" |
| 18241 | 44 |
apply (induct set: IT) |
| 23750 | 45 |
apply (drule rev_predicate1D [OF _ listsp_mono [where B="termip beta"]]) |
| 26806 | 46 |
apply (fast intro!: predicate1I) |
| 9716 | 47 |
apply (drule lists_accD) |
| 23750 | 48 |
apply (erule accp_induct) |
49 |
apply (rule accp.accI) |
|
| 9716 | 50 |
apply (blast dest: head_Var_reduction) |
| 23750 | 51 |
apply (erule accp_induct) |
52 |
apply (rule accp.accI) |
|
| 9716 | 53 |
apply blast |
54 |
apply (blast intro: double_induction_lemma) |
|
55 |
done |
|
56 |
||
57 |
||
| 25972 | 58 |
subsection {* Every terminating term is in @{text "IT"} *}
|
| 9716 | 59 |
|
| 18241 | 60 |
declare Var_apps_neq_Abs_apps [symmetric, simp] |
| 9716 | 61 |
|
| 12011 | 62 |
lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts" |
| 18241 | 63 |
by (simp add: foldl_Cons [symmetric] del: foldl_Cons) |
| 9716 | 64 |
|
65 |
lemma [simp]: |
|
| 12011 | 66 |
"(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')" |
| 18241 | 67 |
by (simp add: foldl_Cons [symmetric] del: foldl_Cons) |
| 9716 | 68 |
|
| 23750 | 69 |
inductive_cases [elim!]: |
| 22271 | 70 |
"IT (Var n \<degree>\<degree> ss)" |
71 |
"IT (Abs t)" |
|
72 |
"IT (Abs r \<degree> s \<degree>\<degree> ts)" |
|
| 9716 | 73 |
|
| 23750 | 74 |
theorem termi_implies_IT: "termip beta r ==> IT r" |
75 |
apply (erule accp_induct) |
|
| 9716 | 76 |
apply (rename_tac r) |
77 |
apply (erule thin_rl) |
|
78 |
apply (erule rev_mp) |
|
79 |
apply simp |
|
80 |
apply (rule_tac t = r in Apps_dB_induct) |
|
81 |
apply clarify |
|
82 |
apply (rule IT.intros) |
|
83 |
apply clarify |
|
84 |
apply (drule bspec, assumption) |
|
85 |
apply (erule mp) |
|
86 |
apply clarify |
|
| 22271 | 87 |
apply (drule_tac r=beta in conversepI) |
88 |
apply (drule_tac r="beta^--1" in ex_step1I, assumption) |
|
| 9716 | 89 |
apply clarify |
90 |
apply (rename_tac us) |
|
| 12011 | 91 |
apply (erule_tac x = "Var n \<degree>\<degree> us" in allE) |
| 9716 | 92 |
apply force |
93 |
apply (rename_tac u ts) |
|
94 |
apply (case_tac ts) |
|
95 |
apply simp |
|
| 11946 | 96 |
apply blast |
| 9716 | 97 |
apply (rename_tac s ss) |
98 |
apply simp |
|
99 |
apply clarify |
|
100 |
apply (rule IT.intros) |
|
101 |
apply (blast intro: apps_preserves_beta) |
|
102 |
apply (erule mp) |
|
103 |
apply clarify |
|
104 |
apply (rename_tac t) |
|
| 12011 | 105 |
apply (erule_tac x = "Abs u \<degree> t \<degree>\<degree> ss" in allE) |
| 9716 | 106 |
apply force |
107 |
done |
|
| 5261 | 108 |
|
| 11639 | 109 |
end |