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