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