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