src/CTT/ctt.ML

adapted to qualified names;

(*  Title: 	CTT/ctt.ML
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

Tactics and lemmas for ctt.thy (Constructive Type Theory)
*)

open CTT;

signature CTT_RESOLVE = 
  sig
  val add_mp_tac: int -> tactic
  val ASSUME: (int -> tactic) -> int -> tactic
  val basic_defs: thm list
  val comp_rls: thm list
  val element_rls: thm list
  val elimL_rls: thm list
  val elim_rls: thm list
  val eqintr_tac: tactic
  val equal_tac: thm list -> tactic
  val formL_rls: thm list
  val form_rls: thm list
  val form_tac: tactic
  val intrL2_rls: thm list
  val intrL_rls: thm list
  val intr_rls: thm list
  val intr_tac: thm list -> tactic
  val mp_tac: int -> tactic
  val NE_tac: string -> int -> tactic
  val pc_tac: thm list -> int -> tactic
  val PlusE_tac: string -> int -> tactic
  val reduction_rls: thm list
  val replace_type: thm
  val routine_rls: thm list   
  val routine_tac: thm list -> thm list -> int -> tactic
  val safe_brls: (bool * thm) list
  val safestep_tac: thm list -> int -> tactic
  val safe_tac: thm list -> int -> tactic
  val step_tac: thm list -> int -> tactic
  val subst_eqtyparg: thm
  val subst_prodE: thm
  val SumE_fst: thm
  val SumE_snd: thm
  val SumE_tac: string -> int -> tactic
  val SumIL2: thm
  val test_assume_tac: int -> tactic
  val typechk_tac: thm list -> tactic
  val unsafe_brls: (bool * thm) list
  end;


structure CTT_Resolve : CTT_RESOLVE = 
struct

(*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! *)
val SumIL2 = prove_goal CTT.thy
    "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)"
 (fn prems=>
  [ (resolve_tac [sym_elem] 1),
    (resolve_tac [SumIL] 1),
    (ALLGOALS (resolve_tac [sym_elem])),
    (ALLGOALS (resolve_tac prems)) ]);

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 subst_prodE = prove_goal CTT.thy
    "[| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z) \
\    |] ==> c(p`a): C(p`a)"
 (fn prems=>
  [ (REPEAT (resolve_tac (prems@[ProdE]) 1)) ]);

(** Tactics for type checking **)

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

(*Try solving a: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 (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*)
val replace_type = prove_goal CTT.thy
    "[| B = A;  a : A |] ==> a : B"
 (fn prems=>
  [ (resolve_tac [equal_types] 1),
    (resolve_tac [sym_type] 2),
    (ALLGOALS (resolve_tac prems)) ]);

(*Simplify the parameter of a unary type operator.*)
val subst_eqtyparg = prove_goal CTT.thy
    "a=c : A ==> (!!z.z:A ==> B(z) type) ==> B(a)=B(c)"
 (fn prems=>
  [ (resolve_tac [subst_typeL] 1),
    (resolve_tac [refl_type] 2),
    (ALLGOALS (resolve_tac prems)),
    (assume_tac 1) ]);

(*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 (resolve_tac [EqE] i) lets them apply to equality judgements. **)

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

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

fun PlusE_tac (sp: string) i = 
  TRY (resolve_tac [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 = 
    resolve_tac [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 = eresolve_tac [subst_prodE] i  THEN  assume_tac i;

(*"safe" when regarded as predicate calculus rules*)
val safe_brls = sort 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) =
    partition (apl(0,op=) 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 **)

val SumE_fst = prove_goal CTT.thy 
    "p : Sum(A,B) ==> fst(p) : A"
 (fn prems=>
  [ (rewrite_goals_tac basic_defs),
    (resolve_tac elim_rls 1),
    (REPEAT (pc_tac prems 1)),
    (fold_tac basic_defs) ]);

(*The first premise must be p:Sum(A,B) !!*)
val SumE_snd = prove_goal CTT.thy 
    "[| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type \
\    |] ==> snd(p) : B(fst(p))"
 (fn prems=>
  [ (rewrite_goals_tac basic_defs),
    (resolve_tac elim_rls 1),
    (resolve_tac prems 1),
    (resolve_tac [replace_type] 1),
    (resolve_tac [subst_eqtyparg] 1),   (*like B(x) equality formation?*)
    (resolve_tac comp_rls 1),
    (typechk_tac prems),
    (fold_tac basic_defs) ]);

end;

open CTT_Resolve;