0
|
1 |
(* Title: CCL/typecheck
|
|
2 |
ID: $Id$
|
|
3 |
Author: Martin Coen, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
|
6 |
*)
|
|
7 |
|
|
8 |
(*** Lemmas for constructors and subtypes ***)
|
|
9 |
|
|
10 |
(* 0-ary constructors do not need additional rules as they are handled *)
|
|
11 |
(* correctly by applying SubtypeI *)
|
|
12 |
(*
|
|
13 |
val Subtype_canTs =
|
|
14 |
let fun tac prems = cut_facts_tac prems 1 THEN
|
|
15 |
REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE
|
|
16 |
eresolve_tac [SubtypeE] 1)
|
|
17 |
fun solve s = prove_goal Type.thy s (fn prems => [tac prems])
|
|
18 |
in map solve
|
|
19 |
["P(one) ==> one : {x:Unit.P(x)}",
|
|
20 |
"P(true) ==> true : {x:Bool.P(x)}",
|
|
21 |
"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)}",
|
|
23 |
"a : {x:A.P(inl(x))} ==> inl(a) : {x:A+B.P(x)}",
|
|
24 |
"b : {x:B.P(inr(x))} ==> inr(b) : {x:A+B.P(x)}",
|
|
25 |
"P(zero) ==> zero : {x:Nat.P(x)}",
|
|
26 |
"a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}",
|
|
27 |
"P([]) ==> [] : {x:List(A).P(x)}",
|
289
|
28 |
"h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
|
0
|
29 |
] end;
|
|
30 |
*)
|
|
31 |
val Subtype_canTs =
|
|
32 |
let fun tac prems = cut_facts_tac prems 1 THEN
|
|
33 |
REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE
|
|
34 |
eresolve_tac [SubtypeE] 1)
|
|
35 |
fun solve s = prove_goal Type.thy s (fn prems => [tac prems])
|
|
36 |
in map solve
|
|
37 |
["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)}",
|
|
39 |
"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)}",
|
289
|
41 |
"h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
|
0
|
42 |
] end;
|
|
43 |
|
|
44 |
val prems = goal Type.thy
|
|
45 |
"[| f(t):B; ~t=bot |] ==> let x be t in f(x) : B";
|
|
46 |
by (cut_facts_tac prems 1);
|
|
47 |
be (letB RS ssubst) 1;
|
|
48 |
ba 1;
|
|
49 |
val letT = result();
|
|
50 |
|
|
51 |
val prems = goal Type.thy
|
|
52 |
"[| a:A; f : Pi(A,B) |] ==> f ` a : B(a)";
|
|
53 |
by (REPEAT (ares_tac (applyT::prems) 1));
|
|
54 |
val applyT2 = result();
|
|
55 |
|
|
56 |
val prems = goal Type.thy
|
|
57 |
"[| a:A; a:A ==> P(a) |] ==> a : {x:A.P(x)}";
|
|
58 |
by (fast_tac (type_cs addSIs prems) 1);
|
|
59 |
val rcall_lemma1 = result();
|
|
60 |
|
|
61 |
val prems = goal Type.thy
|
|
62 |
"[| a:{x:A.Q(x)}; [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A.P(x)}";
|
|
63 |
by (cut_facts_tac prems 1);
|
|
64 |
by (fast_tac (type_cs addSIs prems) 1);
|
|
65 |
val rcall_lemma2 = result();
|
|
66 |
|
|
67 |
val rcall_lemmas = [asm_rl,rcall_lemma1,SubtypeD1,rcall_lemma2];
|
|
68 |
|
|
69 |
(***********************************TYPECHECKING*************************************)
|
|
70 |
|
|
71 |
fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l)
|
|
72 |
| bvars _ l = l;
|
|
73 |
|
|
74 |
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
|
|
76 |
| 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
|
|
78 |
| get_bno l n (t $ s) = get_bno l n t
|
|
79 |
| get_bno l n (Bound m) = (m-length(l),n);
|
|
80 |
|
|
81 |
(* Not a great way of identifying induction hypothesis! *)
|
|
82 |
fun could_IH x = could_unify(x,hd (prems_of rcallT)) orelse
|
|
83 |
could_unify(x,hd (prems_of rcall2T)) orelse
|
|
84 |
could_unify(x,hd (prems_of rcall3T));
|
|
85 |
|
|
86 |
fun IHinst tac rls i = STATE (fn state =>
|
|
87 |
let val (_,_,Bi,_) = dest_state(state,i);
|
|
88 |
val bvs = bvars Bi [];
|
|
89 |
val ihs = filter could_IH (Logic.strip_assums_hyp Bi);
|
|
90 |
val rnames = map (fn x=>
|
|
91 |
let val (a,b) = get_bno [] 0 x
|
|
92 |
in (nth_elem(a,bvs),b) end) ihs;
|
|
93 |
fun try_IHs [] = no_tac
|
|
94 |
| try_IHs ((x,y)::xs) = tac [("g",x)] (nth_elem(y-1,rls)) i ORELSE (try_IHs xs);
|
|
95 |
in try_IHs rnames end);
|
|
96 |
|
|
97 |
(*****)
|
|
98 |
|
|
99 |
val type_rls = canTs@icanTs@(applyT2::ncanTs)@incanTs@
|
|
100 |
precTs@letrecTs@[letT]@Subtype_canTs;
|
|
101 |
|
|
102 |
fun is_rigid_prog t =
|
|
103 |
case (Logic.strip_assums_concl t) of
|
|
104 |
(Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) => (term_vars a = [])
|
|
105 |
| _ => false;
|
|
106 |
|
|
107 |
fun rcall_tac i = let fun tac ps rl i = res_inst_tac ps rl i THEN atac i;
|
|
108 |
in IHinst tac rcallTs i end THEN
|
|
109 |
eresolve_tac rcall_lemmas i;
|
|
110 |
|
|
111 |
fun raw_step_tac prems i = ares_tac (prems@type_rls) i ORELSE
|
|
112 |
rcall_tac i ORELSE
|
|
113 |
ematch_tac [SubtypeE] i ORELSE
|
|
114 |
match_tac [SubtypeI] i;
|
|
115 |
|
|
116 |
fun tc_step_tac prems i = STATE(fn state =>
|
|
117 |
if (i>length(prems_of state))
|
|
118 |
then no_tac
|
|
119 |
else let val (_,_,c,_) = dest_state(state,i)
|
|
120 |
in if is_rigid_prog c then raw_step_tac prems i else no_tac
|
|
121 |
end);
|
|
122 |
|
|
123 |
fun typechk_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls)) i;
|
|
124 |
|
|
125 |
val tac = typechk_tac [] 1;
|
|
126 |
|
|
127 |
|
|
128 |
(*** Clean up Correctness Condictions ***)
|
|
129 |
|
|
130 |
val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([SubtypeE]@rmIHs) ORELSE'
|
|
131 |
hyp_subst_tac);
|
|
132 |
|
|
133 |
val clean_ccs_tac =
|
|
134 |
let fun tac ps rl i = eres_inst_tac ps rl i THEN atac i;
|
|
135 |
in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE'
|
|
136 |
eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE'
|
|
137 |
hyp_subst_tac)) end;
|
|
138 |
|
|
139 |
fun gen_ccs_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls) THEN
|
|
140 |
clean_ccs_tac) i;
|
|
141 |
|
|
142 |
|