src/CCL/typecheck.ML

added some lemmas to the collection "abs_fresh"

the lemmas are of the form

finite (supp x) ==> (b # [a].x) = (b=a \/ b # x)

previously only lemmas of the form

(b # [a].x) = (b=a \/ b # x)

with the type-constraint that x is finitely supported
were included.

(*  Title:      CCL/typecheck.ML
    ID:         $Id$
    Author:     Martin Coen, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge
*)

(*** Lemmas for constructors and subtypes ***)

(* 0-ary constructors do not need additional rules as they are handled *)
(*                                      correctly by applying SubtypeI *)
(*
val Subtype_canTs =
       let fun tac prems = cut_facts_tac prems 1 THEN
                REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE
                        etac SubtypeE 1)
           fun solve s = prove_goal (the_context ()) s (fn prems => [tac prems])
       in map solve
           ["P(one) ==> one : {x:Unit.P(x)}",
            "P(true) ==> true : {x:Bool.P(x)}",
            "P(false) ==> false : {x:Bool.P(x)}",
            "a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}",
            "a : {x:A.P(inl(x))} ==> inl(a) : {x:A+B.P(x)}",
            "b : {x:B.P(inr(x))} ==> inr(b) : {x:A+B.P(x)}",
            "P(zero) ==> zero : {x:Nat.P(x)}",
            "a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}",
            "P([]) ==> [] : {x:List(A).P(x)}",
            "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
        ] end;
*)
val Subtype_canTs =
       let fun tac prems = cut_facts_tac prems 1 THEN
                REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE
                        etac SubtypeE 1)
           fun solve s = prove_goal (the_context ()) s (fn prems => [tac prems])
       in map solve
           ["a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}",
            "a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}",
            "b : {x:B. P(inr(x))} ==> inr(b) : {x:A+B. P(x)}",
            "a : {x:Nat. P(succ(x))} ==> succ(a) : {x:Nat. P(x)}",
            "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
        ] end;

val prems = goal (the_context ())
     "[| f(t):B;  ~t=bot  |] ==> let x be t in f(x) : B";
by (cut_facts_tac prems 1);
by (etac (letB RS ssubst) 1);
by (assume_tac 1);
qed "letT";

val prems = goal (the_context ())
     "[| a:A;  f : Pi(A,B)  |] ==> f ` a  : B(a)";
by (REPEAT (ares_tac (applyT::prems) 1));
qed "applyT2";

val prems = goal (the_context ())
    "[| a:A;  a:A ==> P(a) |] ==> a : {x:A. P(x)}";
by (fast_tac (type_cs addSIs prems) 1);
qed "rcall_lemma1";

val prems = goal (the_context ())
    "[| a:{x:A. Q(x)};  [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A. P(x)}";
by (cut_facts_tac prems 1);
by (fast_tac (type_cs addSIs prems) 1);
qed "rcall_lemma2";

val rcall_lemmas = [asm_rl,rcall_lemma1,SubtypeD1,rcall_lemma2];

(***********************************TYPECHECKING*************************************)

fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l)
  | bvars _ l = l;

fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t
  | get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t
  | get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
  | get_bno l n (Const("op :",_) $ t $ _) = get_bno l n t
  | get_bno l n (t $ s) = get_bno l n t
  | get_bno l n (Bound m) = (m-length(l),n);

(* Not a great way of identifying induction hypothesis! *)
fun could_IH x = could_unify(x,hd (prems_of rcallT)) orelse
                 could_unify(x,hd (prems_of rcall2T)) orelse
                 could_unify(x,hd (prems_of rcall3T));

fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
  let val bvs = bvars Bi [];
      val ihs = List.filter could_IH (Logic.strip_assums_hyp Bi);
      val rnames = map (fn x=>
                    let val (a,b) = get_bno [] 0 x
                    in (List.nth(bvs,a),b) end) ihs;
      fun try_IHs [] = no_tac
        | try_IHs ((x,y)::xs) = tac [("g",x)] (List.nth(rls,y-1)) i ORELSE (try_IHs xs);
  in try_IHs rnames end);

(*****)

val type_rls = canTs@icanTs@(applyT2::ncanTs)@incanTs@
               precTs@letrecTs@[letT]@Subtype_canTs;

fun is_rigid_prog t =
     case (Logic.strip_assums_concl t) of
        (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) => (term_vars a = [])
       | _ => false;

fun rcall_tac i = let fun tac ps rl i = res_inst_tac ps rl i THEN atac i;
                       in IHinst tac rcallTs i end THEN
                  eresolve_tac rcall_lemmas i;

fun raw_step_tac prems i = ares_tac (prems@type_rls) i ORELSE
                           rcall_tac i ORELSE
                           ematch_tac [SubtypeE] i ORELSE
                           match_tac [SubtypeI] i;

fun tc_step_tac prems = SUBGOAL (fn (Bi,i) =>
          if is_rigid_prog Bi then raw_step_tac prems i else no_tac);

fun typechk_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls)) i;

val tac = typechk_tac [] 1;


(*** Clean up Correctness Condictions ***)

val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([SubtypeE]@rmIHs) ORELSE'
                                 hyp_subst_tac);

val clean_ccs_tac =
       let fun tac ps rl i = eres_inst_tac ps rl i THEN atac i;
       in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE'
                       eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE'
                       hyp_subst_tac)) end;

fun gen_ccs_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls) THEN
                                     clean_ccs_tac) i;