src/CCL/typecheck.ML
 author clasohm Wed Nov 30 13:53:46 1994 +0100 (1994-11-30) changeset 757 2ca12511676d parent 642 0db578095e6a child 1459 d12da312eff4 permissions -rw-r--r--
```     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                         etac 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)}",
```
```    28             "h : {x:A. t : {y:List(A).P(x\$y)}} ==> h\$t : {x:List(A).P(x)}"
```
```    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                         etac 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)}",
```
```    41             "h : {x:A. t : {y:List(A).P(x\$y)}} ==> h\$t : {x:List(A).P(x)}"
```
```    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 by (etac (letB RS ssubst) 1);
```
```    48 by (assume_tac 1);
```
```    49 qed "letT";
```
```    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 qed "applyT2";
```
```    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 qed "rcall_lemma1";
```
```    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 qed "rcall_lemma2";
```
```    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
```