| author | wenzelm |
| Mon, 24 Sep 2012 16:13:56 +0200 | |
| changeset 49550 | 0a82e98fd4a3 |
| parent 39157 | b98909faaea8 |
| child 58889 | 5b7a9633cfa8 |
| permissions | -rw-r--r-- |
|
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
36862
diff
changeset
|
1 |
(* Title: HOL/Proofs/Lambda/InductTermi.thy |
| 5261 | 2 |
Author: Tobias Nipkow |
3 |
Copyright 1998 TU Muenchen |
|
4 |
||
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
5 |
Inductive characterization of terminating lambda terms. Goes back to |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
6 |
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
|
7 |
rediscovered by Matthes and Joachimski. |
| 5261 | 8 |
*) |
9 |
||
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
10 |
header {* Inductive characterization of terminating lambda terms *}
|
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
11 |
|
| 16417 | 12 |
theory InductTermi imports ListBeta begin |
| 5261 | 13 |
|
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
14 |
subsection {* Terminating lambda terms *}
|
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
15 |
|
| 23750 | 16 |
inductive IT :: "dB => bool" |
| 22271 | 17 |
where |
18 |
Var [intro]: "listsp IT rs ==> IT (Var n \<degree>\<degree> rs)" |
|
19 |
| Lambda [intro]: "IT r ==> IT (Abs r)" |
|
20 |
| Beta [intro]: "IT ((r[s/0]) \<degree>\<degree> ss) ==> IT s ==> IT ((Abs r \<degree> s) \<degree>\<degree> ss)" |
|
| 9716 | 21 |
|
22 |
||
| 25972 | 23 |
subsection {* Every term in @{text "IT"} terminates *}
|
| 9716 | 24 |
|
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
25 |
lemma double_induction_lemma [rule_format]: |
| 23750 | 26 |
"termip beta s ==> \<forall>t. termip beta t --> |
27 |
(\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> termip beta (Abs r \<degree> s \<degree>\<degree> ss))" |
|
28 |
apply (erule accp_induct) |
|
| 9716 | 29 |
apply (rule allI) |
30 |
apply (rule impI) |
|
| 18513 | 31 |
apply (erule thin_rl) |
| 23750 | 32 |
apply (erule accp_induct) |
| 9716 | 33 |
apply clarify |
| 23750 | 34 |
apply (rule accp.accI) |
| 9771 | 35 |
apply (safe elim!: apps_betasE) |
| 9716 | 36 |
apply (blast intro: subst_preserves_beta apps_preserves_beta) |
| 23750 | 37 |
apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtranclp_converseI |
38 |
dest: accp_downwards) (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *) |
|
| 9716 | 39 |
apply (blast dest: apps_preserves_betas) |
40 |
done |
|
41 |
||
| 23750 | 42 |
lemma IT_implies_termi: "IT t ==> termip beta t" |
| 18241 | 43 |
apply (induct set: IT) |
| 23750 | 44 |
apply (drule rev_predicate1D [OF _ listsp_mono [where B="termip beta"]]) |
| 26806 | 45 |
apply (fast intro!: predicate1I) |
| 9716 | 46 |
apply (drule lists_accD) |
| 23750 | 47 |
apply (erule accp_induct) |
48 |
apply (rule accp.accI) |
|
| 9716 | 49 |
apply (blast dest: head_Var_reduction) |
| 23750 | 50 |
apply (erule accp_induct) |
51 |
apply (rule accp.accI) |
|
| 9716 | 52 |
apply blast |
53 |
apply (blast intro: double_induction_lemma) |
|
54 |
done |
|
55 |
||
56 |
||
| 25972 | 57 |
subsection {* Every terminating term is in @{text "IT"} *}
|
| 9716 | 58 |
|
| 18241 | 59 |
declare Var_apps_neq_Abs_apps [symmetric, simp] |
| 9716 | 60 |
|
| 12011 | 61 |
lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts" |
| 18241 | 62 |
by (simp add: foldl_Cons [symmetric] del: foldl_Cons) |
| 9716 | 63 |
|
64 |
lemma [simp]: |
|
| 12011 | 65 |
"(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')" |
| 18241 | 66 |
by (simp add: foldl_Cons [symmetric] del: foldl_Cons) |
| 9716 | 67 |
|
| 23750 | 68 |
inductive_cases [elim!]: |
| 22271 | 69 |
"IT (Var n \<degree>\<degree> ss)" |
70 |
"IT (Abs t)" |
|
71 |
"IT (Abs r \<degree> s \<degree>\<degree> ts)" |
|
| 9716 | 72 |
|
| 23750 | 73 |
theorem termi_implies_IT: "termip beta r ==> IT r" |
74 |
apply (erule accp_induct) |
|
| 9716 | 75 |
apply (rename_tac r) |
76 |
apply (erule thin_rl) |
|
77 |
apply (erule rev_mp) |
|
78 |
apply simp |
|
79 |
apply (rule_tac t = r in Apps_dB_induct) |
|
80 |
apply clarify |
|
81 |
apply (rule IT.intros) |
|
82 |
apply clarify |
|
83 |
apply (drule bspec, assumption) |
|
84 |
apply (erule mp) |
|
85 |
apply clarify |
|
| 22271 | 86 |
apply (drule_tac r=beta in conversepI) |
87 |
apply (drule_tac r="beta^--1" in ex_step1I, assumption) |
|
| 9716 | 88 |
apply clarify |
89 |
apply (rename_tac us) |
|
| 12011 | 90 |
apply (erule_tac x = "Var n \<degree>\<degree> us" in allE) |
| 9716 | 91 |
apply force |
92 |
apply (rename_tac u ts) |
|
93 |
apply (case_tac ts) |
|
94 |
apply simp |
|
| 11946 | 95 |
apply blast |
| 9716 | 96 |
apply (rename_tac s ss) |
97 |
apply simp |
|
98 |
apply clarify |
|
99 |
apply (rule IT.intros) |
|
100 |
apply (blast intro: apps_preserves_beta) |
|
101 |
apply (erule mp) |
|
102 |
apply clarify |
|
103 |
apply (rename_tac t) |
|
| 12011 | 104 |
apply (erule_tac x = "Abs u \<degree> t \<degree>\<degree> ss" in allE) |
| 9716 | 105 |
apply force |
106 |
done |
|
| 5261 | 107 |
|
| 11639 | 108 |
end |