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