src/ZF/Tools/typechk.ML
 changeset 6049 7fef0169ab5e child 6112 5e4871c5136b
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/ZF/Tools/typechk.ML	Mon Dec 28 16:57:02 1998 +0100
1.3 @@ -0,0 +1,33 @@
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 +
```