45 proof -; |
45 proof -; |
46 assume "a |- e :: t"; |
46 assume "a |- e :: t"; |
47 thus ?thesis (is "?P a e t"); |
47 thus ?thesis (is "?P a e t"); |
48 proof (rule has_type.induct); (* FIXME induct method *) |
48 proof (rule has_type.induct); (* FIXME induct method *) |
49 fix a n; |
49 fix a n; |
50 assume "n < length a"; |
50 assume "n < length (a::typ list)"; |
51 hence "n < length (map ($ s) a)"; by simp; |
51 hence "n < length (map ($ s) a)"; by simp; |
52 hence "map ($ s) a |- Var n :: map ($ s) a ! n"; |
52 hence "map ($ s) a |- Var n :: map ($ s) a ! n"; |
53 by (rule has_type.VarI); |
53 by (rule has_type.VarI); |
54 also; have "map ($ s) a ! n = $ s (a ! n)"; |
54 also; have "map ($ s) a ! n = $ s (a ! n)"; |
55 by (rule nth_map); |
55 by (rule nth_map); |
56 also; have "map ($ s) a = $ s a"; |
56 also; have "map ($ s) a = $ s a"; |
57 by (simp only: app_subst_list); (* FIXME unfold fails!? *) |
57 by (simp only: app_subst_list); |
58 finally; show "?P a (Var n) (a ! n)"; .; |
58 finally; show "?P a (Var n) (a ! n)"; .; |
59 next; |
59 next; |
60 fix a e t1 t2; |
60 fix a e t1 t2; |
61 assume "?P (t1 # a) e t2"; |
61 assume "?P (t1 # a) e t2"; |
62 hence "$ s t1 # map ($ s) a |- e :: $ s t2"; |
62 hence "$ s t1 # map ($ s) a |- e :: $ s t2"; |
110 fix e; assume hyp: "?P e"; |
110 fix e; assume hyp: "?P e"; |
111 show "?P (Abs e)"; |
111 show "?P (Abs e)"; |
112 proof (intro allI impI); |
112 proof (intro allI impI); |
113 fix a s t m n; |
113 fix a s t m n; |
114 assume "Ok (s, t, m) = W (Abs e) a n"; |
114 assume "Ok (s, t, m) = W (Abs e) a n"; |
115 hence "EX t'. t = s n -> t' & |
115 thus "$ s a |- Abs e :: t"; |
116 Ok (s, t', m) = W e (TVar n # a) (Suc n)"; |
116 obtain t' in "t = s n -> t'" "Ok (s, t', m) = W e (TVar n # a) (Suc n)"; |
117 by (rule rev_mp) simp; |
117 by (rule rev_mp) simp; |
118 with hyp; show "$ s a |- Abs e :: t"; |
118 with hyp; show ?thesis; by (force intro: has_type.AbsI); |
119 by (force intro: has_type.AbsI); |
119 qed; |
120 qed; |
120 qed; |
121 next; |
121 next; |
122 fix e1 e2; assume hyp1: "?P e1" and hyp2: "?P e2"; |
122 fix e1 e2; assume hyp1: "?P e1" and hyp2: "?P e2"; |
123 show "?P (App e1 e2)"; |
123 show "?P (App e1 e2)"; |
124 proof (intro allI impI); |
124 proof (intro allI impI); |
125 fix a s t m n; assume "Ok (s, t, m) = W (App e1 e2) a n"; |
125 fix a s t m n; assume "Ok (s, t, m) = W (App e1 e2) a n"; |
126 hence "EX s1 t1 n1 s2 t2 n2 u. |
|
127 s = $ u o $ s2 o s1 & t = u n2 & |
|
128 mgu ($ s2 t1) (t2 -> TVar n2) = Ok u & |
|
129 W e2 ($ s1 a) n1 = Ok (s2, t2, n2) & |
|
130 W e1 a n = Ok (s1, t1, n1)"; |
|
131 by (rule rev_mp) (simp, force); (* FIXME force fails !??*) |
|
132 thus "$ s a |- App e1 e2 :: t"; |
126 thus "$ s a |- App e1 e2 :: t"; |
133 proof (elim exE conjE); |
127 obtain s1 t1 n1 s2 t2 n2 u in |
134 fix s1 t1 n1 s2 t2 n2 u; |
128 s: "s = $ u o $ s2 o s1" |
135 assume s: "s = $ u o $ s2 o s1" |
|
136 and t: "t = u n2" |
129 and t: "t = u n2" |
137 and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u" |
130 and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u" |
138 and W1_ok: "W e1 a n = Ok (s1, t1, n1)" |
131 and W1_ok: "W e1 a n = Ok (s1, t1, n1)" |
139 and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)"; |
132 and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)"; |
|
133 by (rule rev_mp) simp; |
140 show ?thesis; |
134 show ?thesis; |
141 proof (rule has_type.AppI); |
135 proof (rule has_type.AppI); |
142 from s; have s': "$ u ($ s2 ($ s1 a)) = $s a"; |
136 from s; have s': "$ u ($ s2 ($ s1 a)) = $s a"; |
143 by (simp add: subst_comp_tel o_def); |
137 by (simp add: subst_comp_tel o_def); |
144 show "$s a |- e1 :: $ u t2 -> t"; |
138 show "$s a |- e1 :: $ u t2 -> t"; |