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