# File CTT.ML

    (*  Title:      CTT/CTT.ML
        ID:         $Id: CTT.ML,v 1.12 2005/09/20 06:22:27 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1991  University of Cambridge

    Tactics and derived rules for Constructive Type Theory
    *)

    (*Formation rules*)
    val form_rls = [NF, ProdF, SumF, PlusF, EqF, FF, TF]
    and formL_rls = [ProdFL, SumFL, PlusFL, EqFL];

    (*Introduction rules
      OMITTED: EqI, because its premise is an eqelem, not an elem*)
    val intr_rls = [NI0, NI_succ, ProdI, SumI, PlusI_inl, PlusI_inr, TI]
    and intrL_rls = [NI_succL, ProdIL, SumIL, PlusI_inlL, PlusI_inrL];

    (*Elimination rules
      OMITTED: EqE, because its conclusion is an eqelem,  not an elem
               TE, because it does not involve a constructor *)
    val elim_rls = [NE, ProdE, SumE, PlusE, FE]
    and elimL_rls = [NEL, ProdEL, SumEL, PlusEL, FEL];

    (*OMITTED: eqC are TC because they make rewriting loop: p = un = un = ... *)
    val comp_rls = [NC0, NC_succ, ProdC, SumC, PlusC_inl, PlusC_inr];

    (*rules with conclusion a:A, an elem judgement*)
    val element_rls = intr_rls @ elim_rls;

    (*Definitions are (meta)equality axioms*)
    val basic_defs = [fst_def,snd_def];

    (*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
    Goal "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)";
    by (rtac sym_elem 1);
    by (rtac SumIL 1);
    by (ALLGOALS (rtac sym_elem ));
    by (ALLGOALS assume_tac) ;
    qed "SumIL2";

    val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];

    (*Exploit p:Prod(A,B) to create the assumption z:B(a).
      A more natural form of product elimination. *)
    val prems = Goal "[| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z) \
    \    |] ==> c(p`a): C(p`a)";
    by (REPEAT (resolve_tac (ProdE::prems) 1)) ;
    qed "subst_prodE";

    (** Tactics for type checking **)

    fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not(is_Var (head_of a))
      | is_rigid_elem (Const("CTT.Eqelem",_) $ a $ _ $ _) = not(is_Var (head_of a))
      | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a))
      | is_rigid_elem _ = false;

    (*Try solving a:A or a=b:A by assumption provided a is rigid!*)
    val test_assume_tac = SUBGOAL(fn (prem,i) =>
        if is_rigid_elem (Logic.strip_assums_concl prem)
        then  assume_tac i  else  no_tac);

    fun ASSUME tf i = test_assume_tac i  ORELSE  tf i;

    (*For simplification: type formation and checking,
      but no equalities between terms*)
    val routine_rls = form_rls @ formL_rls @ [refl_type] @ element_rls;

    fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);

    (*Solve all subgoals "A type" using formation rules. *)
    val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(form_rls) 1));

    (*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
    fun typechk_tac thms =
      let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3
      in  REPEAT_FIRST (ASSUME tac)  end;

    (*Solve a:A (a flexible, A rigid) by introduction rules.
      Cannot use stringtrees (filt_resolve_tac) since
      goals like ?a:SUM(A,B) have a trivial head-string *)
    fun intr_tac thms =
      let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1
      in  REPEAT_FIRST (ASSUME tac)  end;

    (*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
    fun equal_tac thms =
      let val rls = thms @ form_rls @ element_rls @ intrL_rls @
                    elimL_rls @ [refl_elem]
      in  REPEAT_FIRST (ASSUME (filt_resolve_tac rls 3))  end;

    (*** Simplification ***)

    (*To simplify the type in a goal*)
    Goal "[| B = A;  a : A |] ==> a : B";
    by (rtac equal_types 1);
    by (rtac sym_type 2);
    by (ALLGOALS assume_tac) ;
    qed "replace_type";

    (*Simplify the parameter of a unary type operator.*)
    val prems = Goal
         "[| a=c : A;  !!z. z:A ==> B(z) type |] ==> B(a)=B(c)";
    by (rtac subst_typeL 1);
    by (rtac refl_type 2);
    by (ALLGOALS (resolve_tac prems));
    by (assume_tac 1) ;
    qed "subst_eqtyparg";

    (*Make a reduction rule for simplification.
      A goal a=c becomes b=c, by virtue of a=b *)
    fun resolve_trans rl = rl RS trans_elem;

    (*Simplification rules for Constructive Type Theory*)
    val reduction_rls = map resolve_trans comp_rls;

    (*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
      Uses other intro rules to avoid changing flexible goals.*)
    val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1));

    (** Tactics that instantiate CTT-rules.
        Vars in the given terms will be incremented!
        The (rtac EqE i) lets them apply to equality judgements. **)

    fun NE_tac (sp: string) i =
      TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i;

    fun SumE_tac (sp: string) i =
      TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i;

    fun PlusE_tac (sp: string) i =
      TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i;

    (** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)

    (*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
    fun add_mp_tac i =
        rtac subst_prodE i  THEN  assume_tac i  THEN  assume_tac i;

    (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
    fun mp_tac i = etac subst_prodE i  THEN  assume_tac i;

    (*"safe" when regarded as predicate calculus rules*)
    val safe_brls = sort (make_ord lessb)
        [ (true,FE), (true,asm_rl),
          (false,ProdI), (true,SumE), (true,PlusE) ];

    val unsafe_brls =
        [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI),
          (true,subst_prodE) ];

    (*0 subgoals vs 1 or more*)
    val (safe0_brls, safep_brls) =
        List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;

    fun safestep_tac thms i =
        form_tac  ORELSE
        resolve_tac thms i  ORELSE
        biresolve_tac safe0_brls i  ORELSE  mp_tac i  ORELSE
        DETERM (biresolve_tac safep_brls i);

    fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i);

    fun step_tac thms = safestep_tac thms  ORELSE'  biresolve_tac unsafe_brls;

    (*Fails unless it solves the goal!*)
    fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms);

    (** The elimination rules for fst/snd **)

    Goalw basic_defs "p : Sum(A,B) ==> fst(p) : A";
    by (etac SumE 1);
    by (assume_tac 1);
    qed "SumE_fst";

    (*The first premise must be p:Sum(A,B) !!*)
    val major::prems= Goalw basic_defs
        "[| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type \
    \    |] ==> snd(p) : B(fst(p))";
    by (rtac (major RS SumE) 1);
    by (resolve_tac [SumC RS subst_eqtyparg RS replace_type] 1);
    by (typechk_tac prems) ;
    qed "SumE_snd";