1 (* Title: CCL/typecheck |
1 (* Title: CCL/typecheck.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Martin Coen, Cambridge University Computer Laboratory |
3 Author: Martin Coen, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
|
6 *) |
5 *) |
7 |
6 |
8 (*** Lemmas for constructors and subtypes ***) |
7 (*** Lemmas for constructors and subtypes ***) |
9 |
8 |
10 (* 0-ary constructors do not need additional rules as they are handled *) |
9 (* 0-ary constructors do not need additional rules as they are handled *) |
11 (* correctly by applying SubtypeI *) |
10 (* correctly by applying SubtypeI *) |
12 (* |
11 (* |
13 val Subtype_canTs = |
12 val Subtype_canTs = |
14 let fun tac prems = cut_facts_tac prems 1 THEN |
13 let fun tac prems = cut_facts_tac prems 1 THEN |
15 REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE |
14 REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE |
16 etac SubtypeE 1) |
15 etac SubtypeE 1) |
17 fun solve s = prove_goal Type.thy s (fn prems => [tac prems]) |
16 fun solve s = prove_goal (the_context ()) s (fn prems => [tac prems]) |
18 in map solve |
17 in map solve |
19 ["P(one) ==> one : {x:Unit.P(x)}", |
18 ["P(one) ==> one : {x:Unit.P(x)}", |
20 "P(true) ==> true : {x:Bool.P(x)}", |
19 "P(true) ==> true : {x:Bool.P(x)}", |
21 "P(false) ==> false : {x:Bool.P(x)}", |
20 "P(false) ==> false : {x:Bool.P(x)}", |
22 "a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}", |
21 "a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}", |
26 "a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}", |
25 "a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}", |
27 "P([]) ==> [] : {x:List(A).P(x)}", |
26 "P([]) ==> [] : {x:List(A).P(x)}", |
28 "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}" |
27 "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}" |
29 ] end; |
28 ] end; |
30 *) |
29 *) |
31 val Subtype_canTs = |
30 val Subtype_canTs = |
32 let fun tac prems = cut_facts_tac prems 1 THEN |
31 let fun tac prems = cut_facts_tac prems 1 THEN |
33 REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE |
32 REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE |
34 etac SubtypeE 1) |
33 etac SubtypeE 1) |
35 fun solve s = prove_goal Type.thy s (fn prems => [tac prems]) |
34 fun solve s = prove_goal (the_context ()) s (fn prems => [tac prems]) |
36 in map solve |
35 in map solve |
37 ["a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}", |
36 ["a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}", |
38 "a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}", |
37 "a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}", |
39 "b : {x:B. P(inr(x))} ==> inr(b) : {x:A+B. P(x)}", |
38 "b : {x:B. P(inr(x))} ==> inr(b) : {x:A+B. P(x)}", |
40 "a : {x:Nat. P(succ(x))} ==> succ(a) : {x:Nat. P(x)}", |
39 "a : {x:Nat. P(succ(x))} ==> succ(a) : {x:Nat. P(x)}", |
41 "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}" |
40 "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}" |
42 ] end; |
41 ] end; |
43 |
42 |
44 val prems = goal Type.thy |
43 val prems = goal (the_context ()) |
45 "[| f(t):B; ~t=bot |] ==> let x be t in f(x) : B"; |
44 "[| f(t):B; ~t=bot |] ==> let x be t in f(x) : B"; |
46 by (cut_facts_tac prems 1); |
45 by (cut_facts_tac prems 1); |
47 by (etac (letB RS ssubst) 1); |
46 by (etac (letB RS ssubst) 1); |
48 by (assume_tac 1); |
47 by (assume_tac 1); |
49 qed "letT"; |
48 qed "letT"; |
50 |
49 |
51 val prems = goal Type.thy |
50 val prems = goal (the_context ()) |
52 "[| a:A; f : Pi(A,B) |] ==> f ` a : B(a)"; |
51 "[| a:A; f : Pi(A,B) |] ==> f ` a : B(a)"; |
53 by (REPEAT (ares_tac (applyT::prems) 1)); |
52 by (REPEAT (ares_tac (applyT::prems) 1)); |
54 qed "applyT2"; |
53 qed "applyT2"; |
55 |
54 |
56 val prems = goal Type.thy |
55 val prems = goal (the_context ()) |
57 "[| a:A; a:A ==> P(a) |] ==> a : {x:A. P(x)}"; |
56 "[| a:A; a:A ==> P(a) |] ==> a : {x:A. P(x)}"; |
58 by (fast_tac (type_cs addSIs prems) 1); |
57 by (fast_tac (type_cs addSIs prems) 1); |
59 qed "rcall_lemma1"; |
58 qed "rcall_lemma1"; |
60 |
59 |
61 val prems = goal Type.thy |
60 val prems = goal (the_context ()) |
62 "[| a:{x:A. Q(x)}; [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A. P(x)}"; |
61 "[| a:{x:A. Q(x)}; [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A. P(x)}"; |
63 by (cut_facts_tac prems 1); |
62 by (cut_facts_tac prems 1); |
64 by (fast_tac (type_cs addSIs prems) 1); |
63 by (fast_tac (type_cs addSIs prems) 1); |
65 qed "rcall_lemma2"; |
64 qed "rcall_lemma2"; |
66 |
65 |
69 (***********************************TYPECHECKING*************************************) |
68 (***********************************TYPECHECKING*************************************) |
70 |
69 |
71 fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l) |
70 fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l) |
72 | bvars _ l = l; |
71 | bvars _ l = l; |
73 |
72 |
74 fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t |
73 fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t |
75 | get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t |
74 | get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t |
76 | get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t |
75 | get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t |
77 | get_bno l n (Const("op :",_) $ t $ _) = get_bno l n t |
76 | get_bno l n (Const("op :",_) $ t $ _) = get_bno l n t |
78 | get_bno l n (t $ s) = get_bno l n t |
77 | get_bno l n (t $ s) = get_bno l n t |
79 | get_bno l n (Bound m) = (m-length(l),n); |
78 | get_bno l n (Bound m) = (m-length(l),n); |
96 (*****) |
95 (*****) |
97 |
96 |
98 val type_rls = canTs@icanTs@(applyT2::ncanTs)@incanTs@ |
97 val type_rls = canTs@icanTs@(applyT2::ncanTs)@incanTs@ |
99 precTs@letrecTs@[letT]@Subtype_canTs; |
98 precTs@letrecTs@[letT]@Subtype_canTs; |
100 |
99 |
101 fun is_rigid_prog t = |
100 fun is_rigid_prog t = |
102 case (Logic.strip_assums_concl t) of |
101 case (Logic.strip_assums_concl t) of |
103 (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) => (term_vars a = []) |
102 (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) => (term_vars a = []) |
104 | _ => false; |
103 | _ => false; |
105 |
104 |
106 fun rcall_tac i = let fun tac ps rl i = res_inst_tac ps rl i THEN atac i; |
105 fun rcall_tac i = let fun tac ps rl i = res_inst_tac ps rl i THEN atac i; |
107 in IHinst tac rcallTs i end THEN |
106 in IHinst tac rcallTs i end THEN |
123 (*** Clean up Correctness Condictions ***) |
122 (*** Clean up Correctness Condictions ***) |
124 |
123 |
125 val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([SubtypeE]@rmIHs) ORELSE' |
124 val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([SubtypeE]@rmIHs) ORELSE' |
126 hyp_subst_tac); |
125 hyp_subst_tac); |
127 |
126 |
128 val clean_ccs_tac = |
127 val clean_ccs_tac = |
129 let fun tac ps rl i = eres_inst_tac ps rl i THEN atac i; |
128 let fun tac ps rl i = eres_inst_tac ps rl i THEN atac i; |
130 in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE' |
129 in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE' |
131 eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE' |
130 eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE' |
132 hyp_subst_tac)) end; |
131 hyp_subst_tac)) end; |
133 |
132 |
134 fun gen_ccs_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls) THEN |
133 fun gen_ccs_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls) THEN |
135 clean_ccs_tac) i; |
134 clean_ccs_tac) i; |
136 |
|
137 |
|