author | berghofe |
Tue, 01 Jun 2004 15:00:26 +0200 | |
changeset 14860 | e9e0d8618043 |
parent 14063 | e61a310cde02 |
child 15236 | f289e8ba2bb3 |
permissions | -rw-r--r-- |
14063
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
1 |
(* Title: HOL/Lambda/WeakNorm.thy |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
2 |
ID: $Id$ |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
3 |
Author: Stefan Berghofer |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
4 |
Copyright 2003 TU Muenchen |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
5 |
*) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
6 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
7 |
header {* Weak normalization for simply-typed lambda calculus *} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
8 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
9 |
theory WeakNorm = Type: |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
10 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
11 |
text {* |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
12 |
Formalization by Stefan Berghofer. Partly based on a paper proof by |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
13 |
Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}. |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
14 |
*} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
15 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
16 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
17 |
subsection {* Terms in normal form *} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
18 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
19 |
constdefs |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
20 |
listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
21 |
"listall P xs \<equiv> (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
22 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
23 |
declare listall_def [extraction_expand] |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
24 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
25 |
theorem listall_nil: "listall P []" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
26 |
by (simp add: listall_def) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
27 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
28 |
theorem listall_nil_eq [simp]: "listall P [] = True" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
29 |
by (rules intro: listall_nil) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
30 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
31 |
theorem listall_cons: "P x \<Longrightarrow> listall P xs \<Longrightarrow> listall P (x # xs)" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
32 |
apply (simp add: listall_def) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
33 |
apply (rule allI impI)+ |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
34 |
apply (case_tac i) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
35 |
apply simp+ |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
36 |
done |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
37 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
38 |
theorem listall_cons_eq [simp]: "listall P (x # xs) = (P x \<and> listall P xs)" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
39 |
apply (rule iffI) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
40 |
prefer 2 |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
41 |
apply (erule conjE) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
42 |
apply (erule listall_cons) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
43 |
apply assumption |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
44 |
apply (unfold listall_def) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
45 |
apply (rule conjI) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
46 |
apply (erule_tac x=0 in allE) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
47 |
apply simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
48 |
apply simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
49 |
apply (rule allI) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
50 |
apply (erule_tac x="Suc i" in allE) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
51 |
apply simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
52 |
done |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
53 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
54 |
lemma listall_conj1: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall P xs" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
55 |
by (induct xs) simp+ |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
56 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
57 |
lemma listall_conj2: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall Q xs" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
58 |
by (induct xs) simp+ |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
59 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
60 |
lemma listall_app: "listall P (xs @ ys) = (listall P xs \<and> listall P ys)" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
61 |
apply (induct xs) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
62 |
apply (rule iffI, simp, simp) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
63 |
apply (rule iffI, simp, simp) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
64 |
done |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
65 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
66 |
lemma listall_snoc [simp]: "listall P (xs @ [x]) = (listall P xs \<and> P x)" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
67 |
apply (rule iffI) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
68 |
apply (simp add: listall_app)+ |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
69 |
done |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
70 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
71 |
lemma listall_cong [cong, extraction_expand]: |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
72 |
"xs = ys \<Longrightarrow> listall P xs = listall P ys" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
73 |
-- {* Currently needed for strange technical reasons *} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
74 |
by (unfold listall_def) simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
75 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
76 |
consts NF :: "dB set" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
77 |
inductive NF |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
78 |
intros |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
79 |
App: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow> Var x \<degree>\<degree> ts \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
80 |
Abs: "t \<in> NF \<Longrightarrow> Abs t \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
81 |
monos listall_def |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
82 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
83 |
lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
84 |
apply (induct m) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
85 |
apply (case_tac n) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
86 |
apply (case_tac [3] na) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
87 |
apply (simp only: nat.simps, rules?)+ |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
88 |
done |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
89 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
90 |
lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
91 |
apply (induct m) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
92 |
apply (case_tac n) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
93 |
apply (case_tac [3] na) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
94 |
apply (simp del: simp_thms, rules?)+ |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
95 |
done |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
96 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
97 |
lemma App_NF_D: assumes NF: "Var n \<degree>\<degree> ts \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
98 |
shows "listall (\<lambda>t. t \<in> NF) ts" using NF |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
99 |
by cases simp_all |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
100 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
101 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
102 |
subsection {* Properties of @{text NF} *} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
103 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
104 |
lemma Var_NF: "Var n \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
105 |
apply (subgoal_tac "Var n \<degree>\<degree> [] \<in> NF") |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
106 |
apply simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
107 |
apply (rule NF.App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
108 |
apply simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
109 |
done |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
110 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
111 |
lemma subst_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow> |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
112 |
listall (\<lambda>t. \<forall>i j. t[Var i/j] \<in> NF) ts \<Longrightarrow> |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
113 |
listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
114 |
by (induct ts) simp+ |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
115 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
116 |
lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> (\<And>i j. t[Var i/j] \<in> NF)" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
117 |
apply (induct set: NF) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
118 |
apply simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
119 |
apply (frule listall_conj1) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
120 |
apply (drule listall_conj2) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
121 |
apply (drule_tac i=i and j=j in subst_terms_NF) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
122 |
apply assumption |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
123 |
apply (rule_tac m=x and n=j in nat_eq_dec [THEN disjE, standard]) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
124 |
apply simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
125 |
apply (erule NF.App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
126 |
apply (rule_tac m=j and n=x in nat_le_dec [THEN disjE, standard]) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
127 |
apply simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
128 |
apply (rules intro: NF.App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
129 |
apply simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
130 |
apply (rules intro: NF.App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
131 |
apply simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
132 |
apply (rules intro: NF.Abs) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
133 |
done |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
134 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
135 |
lemma app_Var_NF: "t \<in> NF \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
136 |
apply (induct set: NF) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
137 |
apply (subst app_last) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
138 |
apply (rule exI) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
139 |
apply (rule conjI) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
140 |
apply (rule rtrancl_refl) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
141 |
apply (rule NF.App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
142 |
apply (drule listall_conj1) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
143 |
apply (simp add: listall_app) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
144 |
apply (rule Var_NF) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
145 |
apply (rule exI) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
146 |
apply (rule conjI) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
147 |
apply (rule rtrancl_into_rtrancl) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
148 |
apply (rule rtrancl_refl) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
149 |
apply (rule beta) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
150 |
apply (erule subst_Var_NF) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
151 |
done |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
152 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
153 |
lemma lift_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow> |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
154 |
listall (\<lambda>t. \<forall>i. lift t i \<in> NF) ts \<Longrightarrow> |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
155 |
listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t i) ts)" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
156 |
by (induct ts) simp+ |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
157 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
158 |
lemma lift_NF: "t \<in> NF \<Longrightarrow> (\<And>i. lift t i \<in> NF)" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
159 |
apply (induct set: NF) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
160 |
apply (frule listall_conj1) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
161 |
apply (drule listall_conj2) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
162 |
apply (drule_tac i=i in lift_terms_NF) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
163 |
apply assumption |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
164 |
apply (rule_tac m=x and n=i in nat_le_dec [THEN disjE, standard]) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
165 |
apply simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
166 |
apply (rule NF.App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
167 |
apply assumption |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
168 |
apply simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
169 |
apply (rule NF.App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
170 |
apply assumption |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
171 |
apply simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
172 |
apply (rule NF.Abs) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
173 |
apply simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
174 |
done |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
175 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
176 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
177 |
subsection {* Main theorems *} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
178 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
179 |
lemma subst_type_NF: |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
180 |
"\<And>t e T u i. t \<in> NF \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow> u \<in> NF \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> \<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
181 |
(is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U") |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
182 |
proof (induct U) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
183 |
fix T t |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
184 |
let ?R = "\<lambda>t. \<forall>e T' u i. |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
185 |
e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> u \<in> NF \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF)" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
186 |
assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
187 |
assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
188 |
assume "t \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
189 |
thus "\<And>e T' u i. PROP ?Q t e T' u i T" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
190 |
proof induct |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
191 |
fix e T' u i assume uNF: "u \<in> NF" and uT: "e \<turnstile> u : T" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
192 |
{ |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
193 |
case (App ts x e_ T'_ u_ i_) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
194 |
assume appT: "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> ts : T'" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
195 |
from nat_eq_dec show "\<exists>t'. (Var x \<degree>\<degree> ts)[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
196 |
proof |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
197 |
assume eq: "x = i" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
198 |
show ?thesis |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
199 |
proof (cases ts) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
200 |
case Nil |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
201 |
with eq have "(Var x \<degree>\<degree> [])[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* u" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
202 |
with Nil and uNF show ?thesis by simp rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
203 |
next |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
204 |
case (Cons a as) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
205 |
with appT have "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> (a # as) : T'" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
206 |
then obtain Us |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
207 |
where varT': "e\<langle>i:T\<rangle> \<turnstile> Var x : Us \<Rrightarrow> T'" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
208 |
and argsT': "e\<langle>i:T\<rangle> \<tturnstile> a # as : Us" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
209 |
by (rule var_app_typesE) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
210 |
from argsT' obtain T'' Ts where Us: "Us = T'' # Ts" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
211 |
by (cases Us) (rule FalseE, simp+) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
212 |
from varT' and Us have varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : T'' \<Rightarrow> Ts \<Rrightarrow> T'" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
213 |
by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
214 |
from varT eq have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'" by cases auto |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
215 |
with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
216 |
from argsT' and Us have argsT: "e\<langle>i:T\<rangle> \<tturnstile> as : Ts" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
217 |
from argsT' and Us have argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
218 |
from argT uT refl have aT: "e \<turnstile> a[u/i] : T''" by (rule subst_lemma) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
219 |
have as: "\<And>Us. e\<langle>i:T\<rangle> \<tturnstile> as : Us \<Longrightarrow> listall ?R as \<Longrightarrow> |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
220 |
\<exists>as'. Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>* |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
221 |
Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<and> |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
222 |
Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
223 |
(is "\<And>Us. _ \<Longrightarrow> _ \<Longrightarrow> \<exists>as'. ?ex Us as as'") |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
224 |
proof (induct as rule: rev_induct) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
225 |
case (Nil Us) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
226 |
with Var_NF have "?ex Us [] []" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
227 |
thus ?case .. |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
228 |
next |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
229 |
case (snoc b bs Us) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
230 |
have "e\<langle>i:T\<rangle> \<tturnstile> bs @ [b] : Us" . |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
231 |
then obtain Vs W where Us: "Us = Vs @ [W]" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
232 |
and bs: "e\<langle>i:T\<rangle> \<tturnstile> bs : Vs" and bT: "e\<langle>i:T\<rangle> \<turnstile> b : W" by (rule types_snocE) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
233 |
from snoc have "listall ?R bs" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
234 |
with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
235 |
then obtain bs' where |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
236 |
bsred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) bs \<rightarrow>\<^sub>\<beta>\<^sup>* |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
237 |
Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) bs'" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
238 |
and bsNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) bs' \<in> NF" by rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
239 |
from snoc have "?R b" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
240 |
with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF" by rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
241 |
then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF" by rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
242 |
from bsNF have "listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t 0) bs')" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
243 |
by (rule App_NF_D) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
244 |
moreover have "lift b' 0 \<in> NF" by (rule lift_NF) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
245 |
ultimately have "listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t 0) (bs' @ [b']))" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
246 |
by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
247 |
hence "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) (bs' @ [b']) \<in> NF" by (rule NF.App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
248 |
moreover from bred have "lift (b[u/i]) 0 \<rightarrow>\<^sub>\<beta>\<^sup>* lift b' 0" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
249 |
by (rule lift_preserves_beta') |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
250 |
with bsred have |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
251 |
"(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) bs) \<degree> lift (b[u/i]) 0 \<rightarrow>\<^sub>\<beta>\<^sup>* |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
252 |
(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) bs') \<degree> lift b' 0" by (rule rtrancl_beta_App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
253 |
ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
254 |
thus ?case .. |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
255 |
qed |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
256 |
from App and Cons have "listall ?R as" by simp (rules dest: listall_conj2) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
257 |
with argsT have "\<exists>as'. ?ex Ts as as'" by (rule as) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
258 |
then obtain as' where |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
259 |
asred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>* |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
260 |
Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as'" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
261 |
and asNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<in> NF" by rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
262 |
from App and Cons have "?R a" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
263 |
with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> a' \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
264 |
by rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
265 |
then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "a' \<in> NF" by rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
266 |
from uNF have "lift u 0 \<in> NF" by (rule lift_NF) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
267 |
hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> u' \<in> NF" by (rule app_Var_NF) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
268 |
then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "u' \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
269 |
by rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
270 |
from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> ua \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
271 |
proof (rule MI1) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
272 |
have "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
273 |
proof (rule typing.App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
274 |
from uT' show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by (rule lift_type) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
275 |
show "e\<langle>0:T''\<rangle> \<turnstile> Var 0 : T''" by (rule typing.Var) simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
276 |
qed |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
277 |
with ured show "e\<langle>0:T''\<rangle> \<turnstile> u' : Ts \<Rrightarrow> T'" by (rule subject_reduction') |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
278 |
from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction') |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
279 |
qed |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
280 |
then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "ua \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
281 |
by rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
282 |
from ared have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* (lift u 0 \<degree> Var 0)[a'/0]" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
283 |
by (rule subst_preserves_beta2') |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
284 |
also from ured have "(lift u 0 \<degree> Var 0)[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u'[a'/0]" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
285 |
by (rule subst_preserves_beta') |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
286 |
also note uared |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
287 |
finally have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" . |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
288 |
hence uared': "u \<degree> a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
289 |
from T have "\<exists>r. (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r \<and> r \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
290 |
proof (rule MI2) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
291 |
have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as : T'" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
292 |
proof (rule list_app_typeI) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
293 |
show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'" by (rule typing.Var) simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
294 |
from uT argsT have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
295 |
by (rule substs_lemma) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
296 |
hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) : Ts" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
297 |
by (rule lift_types) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
298 |
thus "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift (t[u/i]) 0) as : Ts" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
299 |
by (simp_all add: map_compose [symmetric] o_def) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
300 |
qed |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
301 |
with asred show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' : T'" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
302 |
by (rule subject_reduction') |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
303 |
from argT uT refl have "e \<turnstile> a[u/i] : T''" by (rule subst_lemma) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
304 |
with uT' have "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'" by (rule typing.App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
305 |
with uared' show "e \<turnstile> ua : Ts \<Rrightarrow> T'" by (rule subject_reduction') |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
306 |
qed |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
307 |
then obtain r where rred: "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
308 |
and rnf: "r \<in> NF" by rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
309 |
from asred have |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
310 |
"(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
311 |
(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0]" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
312 |
by (rule subst_preserves_beta') |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
313 |
also from uared' have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
314 |
(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0]" by (rule subst_preserves_beta2') |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
315 |
also note rred |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
316 |
finally have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r" . |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
317 |
with rnf Cons eq show ?thesis |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
318 |
by (simp add: map_compose [symmetric] o_def) rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
319 |
qed |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
320 |
next |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
321 |
assume neq: "x \<noteq> i" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
322 |
show ?thesis |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
323 |
proof - |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
324 |
from appT obtain Us |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
325 |
where varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : Us \<Rrightarrow> T'" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
326 |
and argsT: "e\<langle>i:T\<rangle> \<tturnstile> ts : Us" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
327 |
by (rule var_app_typesE) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
328 |
have ts: "\<And>Us. e\<langle>i:T\<rangle> \<tturnstile> ts : Us \<Longrightarrow> listall ?R ts \<Longrightarrow> |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
329 |
\<exists>ts'. \<forall>x'. Var x' \<degree>\<degree> map (\<lambda>t. t[u/i]) ts \<rightarrow>\<^sub>\<beta>\<^sup>* Var x' \<degree>\<degree> ts' \<and> |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
330 |
Var x' \<degree>\<degree> ts' \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
331 |
(is "\<And>Us. _ \<Longrightarrow> _ \<Longrightarrow> \<exists>ts'. ?ex Us ts ts'") |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
332 |
proof (induct ts rule: rev_induct) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
333 |
case (Nil Us) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
334 |
with Var_NF have "?ex Us [] []" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
335 |
thus ?case .. |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
336 |
next |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
337 |
case (snoc b bs Us) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
338 |
have "e\<langle>i:T\<rangle> \<tturnstile> bs @ [b] : Us" . |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
339 |
then obtain Vs W where Us: "Us = Vs @ [W]" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
340 |
and bs: "e\<langle>i:T\<rangle> \<tturnstile> bs : Vs" and bT: "e\<langle>i:T\<rangle> \<turnstile> b : W" by (rule types_snocE) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
341 |
from snoc have "listall ?R bs" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
342 |
with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
343 |
then obtain bs' where |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
344 |
bsred: "\<And>x'. Var x' \<degree>\<degree> map (\<lambda>t. t[u/i]) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var x' \<degree>\<degree> bs'" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
345 |
and bsNF: "\<And>x'. Var x' \<degree>\<degree> bs' \<in> NF" by rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
346 |
from snoc have "?R b" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
347 |
with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF" by rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
348 |
then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF" by rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
349 |
from bsred bred have "\<And>x'. (Var x' \<degree>\<degree> map (\<lambda>t. t[u/i]) bs) \<degree> b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
350 |
(Var x' \<degree>\<degree> bs') \<degree> b'" by (rule rtrancl_beta_App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
351 |
moreover from bsNF [of 0] have "listall (\<lambda>t. t \<in> NF) bs'" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
352 |
by (rule App_NF_D) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
353 |
with bNF have "listall (\<lambda>t. t \<in> NF) (bs' @ [b'])" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
354 |
hence "\<And>x'. Var x' \<degree>\<degree> (bs' @ [b']) \<in> NF" by (rule NF.App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
355 |
ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
356 |
thus ?case .. |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
357 |
qed |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
358 |
from App have "listall ?R ts" by (rules dest: listall_conj2) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
359 |
with argsT have "\<exists>ts'. ?ex Ts ts ts'" by (rule ts) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
360 |
then obtain ts' where NF: "?ex Ts ts ts'" .. |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
361 |
from nat_le_dec show ?thesis |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
362 |
proof |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
363 |
assume "i < x" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
364 |
with NF show ?thesis by simp rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
365 |
next |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
366 |
assume "\<not> (i < x)" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
367 |
with NF neq show ?thesis by (simp add: subst_Var) rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
368 |
qed |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
369 |
qed |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
370 |
qed |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
371 |
next |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
372 |
case (Abs r e_ T'_ u_ i_) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
373 |
assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
374 |
then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle> \<turnstile> r : S" by (rule abs_typeE) simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
375 |
moreover have "lift u 0 \<in> NF" by (rule lift_NF) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
376 |
moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" by (rule lift_type) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
377 |
ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" by (rule Abs) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
378 |
thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
379 |
by simp (rules intro: rtrancl_beta_Abs NF.Abs) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
380 |
} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
381 |
qed |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
382 |
qed |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
383 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
384 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
385 |
consts -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
386 |
rtyping :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
387 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
388 |
syntax |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
389 |
"_rtyping" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |-\<^sub>R _ : _" [50, 50, 50] 50) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
390 |
syntax (xsymbols) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
391 |
"_rtyping" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
392 |
translations |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
393 |
"e \<turnstile>\<^sub>R t : T" \<rightleftharpoons> "(e, t, T) \<in> rtyping" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
394 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
395 |
inductive rtyping |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
396 |
intros |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
397 |
Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
398 |
Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
399 |
App: "e \<turnstile>\<^sub>R s : T \<Rightarrow> U \<Longrightarrow> e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile>\<^sub>R (s \<degree> t) : U" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
400 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
401 |
lemma rtyping_imp_typing: "e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile> t : T" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
402 |
apply (induct set: rtyping) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
403 |
apply (erule typing.Var) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
404 |
apply (erule typing.Abs) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
405 |
apply (erule typing.App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
406 |
apply assumption |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
407 |
done |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
408 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
409 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
410 |
theorem type_NF: assumes T: "e \<turnstile>\<^sub>R t : T" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
411 |
shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using T |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
412 |
proof induct |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
413 |
case Var |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
414 |
show ?case by (rules intro: Var_NF) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
415 |
next |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
416 |
case Abs |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
417 |
thus ?case by (rules intro: rtrancl_beta_Abs NF.Abs) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
418 |
next |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
419 |
case (App T U e s t) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
420 |
from App obtain s' t' where |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
421 |
sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and sNF: "s' \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
422 |
and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "t' \<in> NF" by rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
423 |
have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> u \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
424 |
proof (rule subst_type_NF) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
425 |
have "lift t' 0 \<in> NF" by (rule lift_NF) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
426 |
hence "listall (\<lambda>t. t \<in> NF) [lift t' 0]" by (rule listall_cons) (rule listall_nil) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
427 |
hence "Var 0 \<degree>\<degree> [lift t' 0] \<in> NF" by (rule NF.App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
428 |
thus "Var 0 \<degree> lift t' 0 \<in> NF" by simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
429 |
show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t' 0 : U" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
430 |
proof (rule typing.App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
431 |
show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
432 |
by (rule typing.Var) simp |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
433 |
from tred have "e \<turnstile> t' : T" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
434 |
by (rule subject_reduction') (rule rtyping_imp_typing) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
435 |
thus "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t' 0 : T" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
436 |
by (rule lift_type) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
437 |
qed |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
438 |
from sred show "e \<turnstile> s' : T \<Rightarrow> U" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
439 |
by (rule subject_reduction') (rule rtyping_imp_typing) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
440 |
qed |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
441 |
then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "u \<in> NF" by simp rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
442 |
from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
443 |
hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtrancl_trans) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
444 |
with unf show ?case by rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
445 |
qed |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
446 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
447 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
448 |
subsection {* Extracting the program *} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
449 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
450 |
declare NF.induct [ind_realizer] |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
451 |
declare rtrancl.induct [ind_realizer irrelevant] |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
452 |
declare rtyping.induct [ind_realizer] |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
453 |
lemmas [extraction_expand] = trans_def conj_assoc listall_cons_eq |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
454 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
455 |
extract type_NF |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
456 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
457 |
lemma rtranclR_rtrancl_eq: "((a, b) \<in> rtranclR r) = ((a, b) \<in> rtrancl (Collect r))" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
458 |
apply (rule iffI) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
459 |
apply (erule rtranclR.induct) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
460 |
apply (rule rtrancl_refl) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
461 |
apply (erule rtrancl_into_rtrancl) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
462 |
apply (erule CollectI) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
463 |
apply (erule rtrancl.induct) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
464 |
apply (rule rtranclR.rtrancl_refl) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
465 |
apply (erule rtranclR.rtrancl_into_rtrancl) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
466 |
apply (erule CollectD) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
467 |
done |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
468 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
469 |
lemma NFR_imp_NF: "(nf, t) \<in> NFR \<Longrightarrow> t \<in> NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
470 |
apply (erule NFR.induct) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
471 |
apply (rule NF.intros) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
472 |
apply (simp add: listall_def) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
473 |
apply (erule NF.intros) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
474 |
done |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
475 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
476 |
text_raw {* |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
477 |
\begin{figure} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
478 |
\renewcommand{\isastyle}{\scriptsize\it}% |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
479 |
@{thm [display,eta_contract=false,margin=100] subst_type_NF_def} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
480 |
\renewcommand{\isastyle}{\small\it}% |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
481 |
\caption{Program extracted from @{text subst_type_NF}} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
482 |
\label{fig:extr-subst-type-nf} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
483 |
\end{figure} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
484 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
485 |
\begin{figure} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
486 |
\renewcommand{\isastyle}{\scriptsize\it}% |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
487 |
@{thm [display,margin=100] subst_Var_NF_def} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
488 |
@{thm [display,margin=100] app_Var_NF_def} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
489 |
@{thm [display,margin=100] lift_NF_def} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
490 |
@{thm [display,eta_contract=false,margin=100] type_NF_def} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
491 |
\renewcommand{\isastyle}{\small\it}% |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
492 |
\caption{Program extracted from lemmas and main theorem} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
493 |
\label{fig:extr-type-nf} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
494 |
\end{figure} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
495 |
*} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
496 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
497 |
text {* |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
498 |
The program corresponding to the proof of the central lemma, which |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
499 |
performs substitution and normalization, is shown in Figure |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
500 |
\ref{fig:extr-subst-type-nf}. The correctness |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
501 |
theorem corresponding to the program @{text "subst_type_NF"} is |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
502 |
@{thm [display,margin=100] subst_type_NF_correctness |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
503 |
[simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
504 |
where @{text NFR} is the realizability predicate corresponding to |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
505 |
the datatype @{text NFT}, which is inductively defined by the rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
506 |
\pagebreak |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
507 |
@{thm [display,margin=90] NFR.App [of ts nfs x] NFR.Abs [of nf t]} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
508 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
509 |
The programs corresponding to the main theorem @{text "type_NF"}, as |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
510 |
well as to some lemmas, are shown in Figure \ref{fig:extr-type-nf}. |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
511 |
The correctness statement for the main function @{text "type_NF"} is |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
512 |
@{thm [display,margin=100] type_NF_correctness |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
513 |
[simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
514 |
where the realizability predicate @{text "rtypingR"} corresponding to the |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
515 |
computationally relevant version of the typing judgement is inductively |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
516 |
defined by the rules |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
517 |
@{thm [display,margin=100] rtypingR.Var [no_vars] |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
518 |
rtypingR.Abs [of ty, no_vars] rtypingR.App [of ty e s T U ty' t]} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
519 |
*} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
520 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
521 |
subsection {* Generating executable code *} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
522 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
523 |
consts_code |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
524 |
arbitrary :: "'a" ("(error \"arbitrary\")") |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
525 |
arbitrary :: "'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")") |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
526 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
527 |
generate_code |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
528 |
test = "type_NF" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
529 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
530 |
text {* |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
531 |
The following functions convert between Isabelle's built-in {\tt term} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
532 |
datatype and the generated {\tt dB} datatype. This allows to |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
533 |
generate example terms using Isabelle's parser and inspect |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
534 |
normalized terms using Isabelle's pretty printer. |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
535 |
*} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
536 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
537 |
ML {* |
14860
e9e0d8618043
Adapted to new name mangling function in code generator.
berghofe
parents:
14063
diff
changeset
|
538 |
fun nat_of_int 0 = id_0 |
14063
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
539 |
| nat_of_int n = Suc (nat_of_int (n-1)); |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
540 |
|
14860
e9e0d8618043
Adapted to new name mangling function in code generator.
berghofe
parents:
14063
diff
changeset
|
541 |
fun int_of_nat id_0 = 0 |
14063
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
542 |
| int_of_nat (Suc n) = 1 + int_of_nat n; |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
543 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
544 |
fun dBtype_of_typ (Type ("fun", [T, U])) = |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
545 |
Fun (dBtype_of_typ T, dBtype_of_typ U) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
546 |
| dBtype_of_typ (TFree (s, _)) = (case explode s of |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
547 |
["'", a] => Atom (nat_of_int (ord a - 97)) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
548 |
| _ => error "dBtype_of_typ: variable name") |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
549 |
| dBtype_of_typ _ = error "dBtype_of_typ: bad type"; |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
550 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
551 |
fun dB_of_term (Bound i) = dB_Var (nat_of_int i) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
552 |
| dB_of_term (t $ u) = dB_App (dB_of_term t, dB_of_term u) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
553 |
| dB_of_term (Abs (_, _, t)) = dB_Abs (dB_of_term t) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
554 |
| dB_of_term _ = error "dB_of_term: bad term"; |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
555 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
556 |
fun term_of_dB Ts (Type ("fun", [T, U])) (dB_Abs dBt) = |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
557 |
Abs ("x", T, term_of_dB (T :: Ts) U dBt) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
558 |
| term_of_dB Ts _ dBt = term_of_dB' Ts dBt |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
559 |
and term_of_dB' Ts (dB_Var n) = Bound (int_of_nat n) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
560 |
| term_of_dB' Ts (dB_App (dBt, dBu)) = |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
561 |
let val t = term_of_dB' Ts dBt |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
562 |
in case fastype_of1 (Ts, t) of |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
563 |
Type ("fun", [T, U]) => t $ term_of_dB Ts T dBu |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
564 |
| _ => error "term_of_dB: function type expected" |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
565 |
end |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
566 |
| term_of_dB' _ _ = error "term_of_dB: term not in normal form"; |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
567 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
568 |
fun typing_of_term Ts e (Bound i) = |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
569 |
rtypingT_Var (e, nat_of_int i, dBtype_of_typ (nth_elem (i, Ts))) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
570 |
| typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
571 |
Type ("fun", [T, U]) => rtypingT_App (e, dB_of_term t, |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
572 |
dBtype_of_typ T, dBtype_of_typ U, dB_of_term u, |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
573 |
typing_of_term Ts e t, typing_of_term Ts e u) |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
574 |
| _ => error "typing_of_term: function type expected") |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
575 |
| typing_of_term Ts e (Abs (s, T, t)) = |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
576 |
let val dBT = dBtype_of_typ T |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
577 |
in rtypingT_Abs (e, dBT, dB_of_term t, |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
578 |
dBtype_of_typ (fastype_of1 (T :: Ts, t)), |
14860
e9e0d8618043
Adapted to new name mangling function in code generator.
berghofe
parents:
14063
diff
changeset
|
579 |
typing_of_term (T :: Ts) (shift e id_0 dBT) t) |
14063
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
580 |
end |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
581 |
| typing_of_term _ _ _ = error "typing_of_term: bad term"; |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
582 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
583 |
fun dummyf _ = error "dummy"; |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
584 |
*} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
585 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
586 |
text {* |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
587 |
We now try out the extracted program @{text "type_NF"} on some example terms. |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
588 |
*} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
589 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
590 |
ML {* |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
591 |
val sg = sign_of (the_context()); |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
592 |
fun rd s = read_cterm sg (s, TypeInfer.logicT); |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
593 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
594 |
val ct1 = rd "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"; |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
595 |
val (dB1, _) = type_NF (typing_of_term [] dummyf (term_of ct1)); |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
596 |
val ct1' = cterm_of sg (term_of_dB [] (#T (rep_cterm ct1)) dB1); |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
597 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
598 |
val ct2 = rd |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
599 |
"%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"; |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
600 |
val (dB2, _) = type_NF (typing_of_term [] dummyf (term_of ct2)); |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
601 |
val ct2' = cterm_of sg (term_of_dB [] (#T (rep_cterm ct2)) dB2); |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
602 |
*} |
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
603 |
|
e61a310cde02
New proof of weak normalization with program extraction.
berghofe
parents:
diff
changeset
|
604 |
end |