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