src/ZF/Tools/typechk.ML
author paulson
Mon Dec 28 16:57:02 1998 +0100 (1998-12-28)
changeset 6049 7fef0169ab5e
child 6112 5e4871c5136b
permissions -rw-r--r--
moved from ZF to new subdirectory Tools
     1 (*  Title:      ZF/typechk
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Tactics for type checking -- from CTT
     7 *)
     8 
     9 fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 
    10       not (is_Var (head_of a))
    11   | is_rigid_elem _ = false;
    12 
    13 (*Try solving a:A by assumption provided a is rigid!*) 
    14 val test_assume_tac = SUBGOAL(fn (prem,i) =>
    15     if is_rigid_elem (Logic.strip_assums_concl prem)
    16     then  assume_tac i  else  eq_assume_tac i);
    17 
    18 (*Type checking solves a:?A (a rigid, ?A maybe flexible).  
    19   match_tac is too strict; would refuse to instantiate ?A*)
    20 fun typechk_step_tac tyrls =
    21     FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
    22 
    23 fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
    24 
    25 val ZF_typechecks =
    26     [if_type, lam_type, SigmaI, apply_type, split_type, consI1];
    27 
    28 (*Instantiates variables in typing conditions.
    29   drawback: does not simplify conjunctions*)
    30 fun type_auto_tac tyrls hyps = SELECT_GOAL
    31     (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
    32            ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
    33