src/CCL/typecheck.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 3837 d7f033c74b38
child 15570 8d8c70b41bab
permissions -rw-r--r--
tidying
     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 = SUBGOAL (fn (Bi,i) =>
    87   let val bvs = bvars Bi [];
    88       val ihs = filter could_IH (Logic.strip_assums_hyp Bi);
    89       val rnames = map (fn x=>
    90                     let val (a,b) = get_bno [] 0 x
    91                     in (nth_elem(a,bvs),b) end) ihs;
    92       fun try_IHs [] = no_tac
    93         | try_IHs ((x,y)::xs) = tac [("g",x)] (nth_elem(y-1,rls)) i ORELSE (try_IHs xs);
    94   in try_IHs rnames end);
    95 
    96 (*****)
    97 
    98 val type_rls = canTs@icanTs@(applyT2::ncanTs)@incanTs@
    99                precTs@letrecTs@[letT]@Subtype_canTs;
   100 
   101 fun is_rigid_prog t = 
   102      case (Logic.strip_assums_concl t) of 
   103         (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) => (term_vars a = [])
   104        | _ => false;
   105 
   106 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
   108                   eresolve_tac rcall_lemmas i;
   109 
   110 fun raw_step_tac prems i = ares_tac (prems@type_rls) i ORELSE
   111                            rcall_tac i ORELSE
   112                            ematch_tac [SubtypeE] i ORELSE
   113                            match_tac [SubtypeI] i;
   114 
   115 fun tc_step_tac prems = SUBGOAL (fn (Bi,i) =>
   116           if is_rigid_prog Bi then raw_step_tac prems i else no_tac);
   117 
   118 fun typechk_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls)) i;
   119 
   120 val tac = typechk_tac [] 1;
   121 
   122 
   123 (*** Clean up Correctness Condictions ***)
   124 
   125 val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([SubtypeE]@rmIHs) ORELSE'
   126                                  hyp_subst_tac);
   127 
   128 val clean_ccs_tac = 
   129        let fun tac ps rl i = eres_inst_tac ps rl i THEN atac i;
   130        in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE'
   131                        eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE'
   132                        hyp_subst_tac)) end;
   133 
   134 fun gen_ccs_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls) THEN
   135                                      clean_ccs_tac) i;
   136 
   137