src/CTT/CTT.ML
author paulson
Wed Jul 05 18:27:55 2000 +0200 (2000-07-05)
changeset 9251 bd57acd44fc1
parent 9249 c71db8c28727
child 15570 8d8c70b41bab
permissions -rw-r--r--
more tidying. also generalized some tactics to prove "Type A" and
"a = b : A" judgements
     1 (*  Title:      CTT/CTT.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Tactics and derived rules for Constructive Type Theory
     7 *)
     8 
     9 (*Formation rules*)
    10 val form_rls = [NF, ProdF, SumF, PlusF, EqF, FF, TF]
    11 and formL_rls = [ProdFL, SumFL, PlusFL, EqFL];
    12 
    13  
    14 (*Introduction rules
    15   OMITTED: EqI, because its premise is an eqelem, not an elem*)
    16 val intr_rls = [NI0, NI_succ, ProdI, SumI, PlusI_inl, PlusI_inr, TI]
    17 and intrL_rls = [NI_succL, ProdIL, SumIL, PlusI_inlL, PlusI_inrL];
    18 
    19 
    20 (*Elimination rules
    21   OMITTED: EqE, because its conclusion is an eqelem,  not an elem
    22            TE, because it does not involve a constructor *)
    23 val elim_rls = [NE, ProdE, SumE, PlusE, FE]
    24 and elimL_rls = [NEL, ProdEL, SumEL, PlusEL, FEL];
    25 
    26 (*OMITTED: eqC are TC because they make rewriting loop: p = un = un = ... *)
    27 val comp_rls = [NC0, NC_succ, ProdC, SumC, PlusC_inl, PlusC_inr];
    28 
    29 (*rules with conclusion a:A, an elem judgement*)
    30 val element_rls = intr_rls @ elim_rls;
    31 
    32 (*Definitions are (meta)equality axioms*)
    33 val basic_defs = [fst_def,snd_def];
    34 
    35 (*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
    36 Goal "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)";
    37 by (rtac sym_elem 1);
    38 by (rtac SumIL 1);
    39 by (ALLGOALS (rtac sym_elem ));
    40 by (ALLGOALS assume_tac) ;
    41 qed "SumIL2";
    42 
    43 val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];
    44 
    45 (*Exploit p:Prod(A,B) to create the assumption z:B(a).  
    46   A more natural form of product elimination. *)
    47 val prems = Goal "[| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z) \
    48 \    |] ==> c(p`a): C(p`a)";
    49 by (REPEAT (resolve_tac (ProdE::prems) 1)) ;
    50 qed "subst_prodE";
    51 
    52 (** Tactics for type checking **)
    53 
    54 fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not(is_Var (head_of a))
    55   | is_rigid_elem (Const("CTT.Eqelem",_) $ a $ _ $ _) = not(is_Var (head_of a))
    56   | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a))
    57   | is_rigid_elem _ = false;
    58 
    59 (*Try solving a:A or a=b:A by assumption provided a is rigid!*) 
    60 val test_assume_tac = SUBGOAL(fn (prem,i) =>
    61     if is_rigid_elem (Logic.strip_assums_concl prem)
    62     then  assume_tac i  else  no_tac);
    63 
    64 fun ASSUME tf i = test_assume_tac i  ORELSE  tf i;
    65 
    66 
    67 (*For simplification: type formation and checking,
    68   but no equalities between terms*)
    69 val routine_rls = form_rls @ formL_rls @ [refl_type] @ element_rls;
    70 
    71 fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
    72 
    73 
    74 (*Solve all subgoals "A type" using formation rules. *)
    75 val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(form_rls) 1));
    76 
    77 
    78 (*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
    79 fun typechk_tac thms =
    80   let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3
    81   in  REPEAT_FIRST (ASSUME tac)  end;
    82 
    83 
    84 (*Solve a:A (a flexible, A rigid) by introduction rules. 
    85   Cannot use stringtrees (filt_resolve_tac) since
    86   goals like ?a:SUM(A,B) have a trivial head-string *)
    87 fun intr_tac thms =
    88   let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1
    89   in  REPEAT_FIRST (ASSUME tac)  end;
    90 
    91 
    92 (*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
    93 fun equal_tac thms =
    94   let val rls = thms @ form_rls @ element_rls @ intrL_rls @
    95                 elimL_rls @ [refl_elem]
    96   in  REPEAT_FIRST (ASSUME (filt_resolve_tac rls 3))  end;
    97 
    98 (*** Simplification ***)
    99 
   100 (*To simplify the type in a goal*)
   101 Goal "[| B = A;  a : A |] ==> a : B";
   102 by (rtac equal_types 1);
   103 by (rtac sym_type 2);
   104 by (ALLGOALS assume_tac) ;
   105 qed "replace_type";
   106 
   107 (*Simplify the parameter of a unary type operator.*)
   108 val prems = Goal
   109      "[| a=c : A;  !!z. z:A ==> B(z) type |] ==> B(a)=B(c)";
   110 by (rtac subst_typeL 1);
   111 by (rtac refl_type 2);
   112 by (ALLGOALS (resolve_tac prems));
   113 by (assume_tac 1) ;
   114 qed "subst_eqtyparg";
   115 
   116 (*Make a reduction rule for simplification.
   117   A goal a=c becomes b=c, by virtue of a=b *)
   118 fun resolve_trans rl = rl RS trans_elem;
   119 
   120 (*Simplification rules for Constructive Type Theory*)
   121 val reduction_rls = map resolve_trans comp_rls;
   122 
   123 (*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
   124   Uses other intro rules to avoid changing flexible goals.*)
   125 val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1));
   126 
   127 (** Tactics that instantiate CTT-rules.
   128     Vars in the given terms will be incremented! 
   129     The (rtac EqE i) lets them apply to equality judgements. **)
   130 
   131 fun NE_tac (sp: string) i = 
   132   TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i;
   133 
   134 fun SumE_tac (sp: string) i = 
   135   TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i;
   136 
   137 fun PlusE_tac (sp: string) i = 
   138   TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i;
   139 
   140 (** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
   141 
   142 (*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
   143 fun add_mp_tac i = 
   144     rtac subst_prodE i  THEN  assume_tac i  THEN  assume_tac i;
   145 
   146 (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
   147 fun mp_tac i = etac subst_prodE i  THEN  assume_tac i;
   148 
   149 (*"safe" when regarded as predicate calculus rules*)
   150 val safe_brls = sort (make_ord lessb)
   151     [ (true,FE), (true,asm_rl), 
   152       (false,ProdI), (true,SumE), (true,PlusE) ];
   153 
   154 val unsafe_brls =
   155     [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI), 
   156       (true,subst_prodE) ];
   157 
   158 (*0 subgoals vs 1 or more*)
   159 val (safe0_brls, safep_brls) =
   160     partition (apl(0,op=) o subgoals_of_brl) safe_brls;
   161 
   162 fun safestep_tac thms i =
   163     form_tac  ORELSE  
   164     resolve_tac thms i  ORELSE
   165     biresolve_tac safe0_brls i  ORELSE  mp_tac i  ORELSE
   166     DETERM (biresolve_tac safep_brls i);
   167 
   168 fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i); 
   169 
   170 fun step_tac thms = safestep_tac thms  ORELSE'  biresolve_tac unsafe_brls;
   171 
   172 (*Fails unless it solves the goal!*)
   173 fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms);
   174 
   175 (** The elimination rules for fst/snd **)
   176 
   177 Goalw basic_defs "p : Sum(A,B) ==> fst(p) : A";
   178 by (etac SumE 1);
   179 by (assume_tac 1);
   180 qed "SumE_fst";
   181 
   182 (*The first premise must be p:Sum(A,B) !!*)
   183 val major::prems= Goalw basic_defs
   184     "[| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type \
   185 \    |] ==> snd(p) : B(fst(p))";
   186 by (rtac (major RS SumE) 1);
   187 by (resolve_tac [SumC RS subst_eqtyparg RS replace_type] 1);
   188 by (typechk_tac prems) ;
   189 qed "SumE_snd";