src/ZF/typechk.ML
changeset 6053 8a1059aa01f0
parent 6052 4f093e55beeb
child 6054 4a4f6ad607a1
     1.1 --- a/src/ZF/typechk.ML	Mon Dec 28 16:58:11 1998 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,33 +0,0 @@
     1.4 -(*  Title:      ZF/typechk
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1991  University of Cambridge
     1.8 -
     1.9 -Tactics for type checking -- from CTT
    1.10 -*)
    1.11 -
    1.12 -fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 
    1.13 -      not (is_Var (head_of a))
    1.14 -  | is_rigid_elem _ = false;
    1.15 -
    1.16 -(*Try solving a:A by assumption provided a is rigid!*) 
    1.17 -val test_assume_tac = SUBGOAL(fn (prem,i) =>
    1.18 -    if is_rigid_elem (Logic.strip_assums_concl prem)
    1.19 -    then  assume_tac i  else  eq_assume_tac i);
    1.20 -
    1.21 -(*Type checking solves a:?A (a rigid, ?A maybe flexible).  
    1.22 -  match_tac is too strict; would refuse to instantiate ?A*)
    1.23 -fun typechk_step_tac tyrls =
    1.24 -    FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
    1.25 -
    1.26 -fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
    1.27 -
    1.28 -val ZF_typechecks =
    1.29 -    [if_type, lam_type, SigmaI, apply_type, split_type, consI1];
    1.30 -
    1.31 -(*Instantiates variables in typing conditions.
    1.32 -  drawback: does not simplify conjunctions*)
    1.33 -fun type_auto_tac tyrls hyps = SELECT_GOAL
    1.34 -    (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
    1.35 -           ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
    1.36 -