src/CTT/ctt.ML
changeset 0 a5a9c433f639
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CTT/ctt.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,249 @@
     1.4 +(*  Title: 	CTT/ctt.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1991  University of Cambridge
     1.8 +
     1.9 +Tactics and lemmas for ctt.thy (Constructive Type Theory)
    1.10 +*)
    1.11 +
    1.12 +open CTT;
    1.13 +
    1.14 +signature CTT_RESOLVE = 
    1.15 +  sig
    1.16 +  val add_mp_tac: int -> tactic
    1.17 +  val ASSUME: (int -> tactic) -> int -> tactic
    1.18 +  val basic_defs: thm list
    1.19 +  val comp_rls: thm list
    1.20 +  val element_rls: thm list
    1.21 +  val elimL_rls: thm list
    1.22 +  val elim_rls: thm list
    1.23 +  val eqintr_tac: tactic
    1.24 +  val equal_tac: thm list -> tactic
    1.25 +  val formL_rls: thm list
    1.26 +  val form_rls: thm list
    1.27 +  val form_tac: tactic
    1.28 +  val intrL2_rls: thm list
    1.29 +  val intrL_rls: thm list
    1.30 +  val intr_rls: thm list
    1.31 +  val intr_tac: thm list -> tactic
    1.32 +  val mp_tac: int -> tactic
    1.33 +  val NE_tac: string -> int -> tactic
    1.34 +  val pc_tac: thm list -> int -> tactic
    1.35 +  val PlusE_tac: string -> int -> tactic
    1.36 +  val reduction_rls: thm list
    1.37 +  val replace_type: thm
    1.38 +  val routine_rls: thm list   
    1.39 +  val routine_tac: thm list -> thm list -> int -> tactic
    1.40 +  val safe_brls: (bool * thm) list
    1.41 +  val safestep_tac: thm list -> int -> tactic
    1.42 +  val safe_tac: thm list -> int -> tactic
    1.43 +  val step_tac: thm list -> int -> tactic
    1.44 +  val subst_eqtyparg: thm
    1.45 +  val subst_prodE: thm
    1.46 +  val SumE_fst: thm
    1.47 +  val SumE_snd: thm
    1.48 +  val SumE_tac: string -> int -> tactic
    1.49 +  val SumIL2: thm
    1.50 +  val test_assume_tac: int -> tactic
    1.51 +  val typechk_tac: thm list -> tactic
    1.52 +  val unsafe_brls: (bool * thm) list
    1.53 +  end;
    1.54 +
    1.55 +
    1.56 +structure CTT_Resolve : CTT_RESOLVE = 
    1.57 +struct
    1.58 +
    1.59 +(*Formation rules*)
    1.60 +val form_rls = [NF, ProdF, SumF, PlusF, EqF, FF, TF]
    1.61 +and formL_rls = [ProdFL, SumFL, PlusFL, EqFL];
    1.62 +
    1.63 + 
    1.64 +(*Introduction rules
    1.65 +  OMITTED: EqI, because its premise is an eqelem, not an elem*)
    1.66 +val intr_rls = [NI0, NI_succ, ProdI, SumI, PlusI_inl, PlusI_inr, TI]
    1.67 +and intrL_rls = [NI_succL, ProdIL, SumIL, PlusI_inlL, PlusI_inrL];
    1.68 +
    1.69 +
    1.70 +(*Elimination rules
    1.71 +  OMITTED: EqE, because its conclusion is an eqelem,  not an elem
    1.72 +           TE, because it does not involve a constructor *)
    1.73 +val elim_rls = [NE, ProdE, SumE, PlusE, FE]
    1.74 +and elimL_rls = [NEL, ProdEL, SumEL, PlusEL, FEL];
    1.75 +
    1.76 +(*OMITTED: eqC are TC because they make rewriting loop: p = un = un = ... *)
    1.77 +val comp_rls = [NC0, NC_succ, ProdC, SumC, PlusC_inl, PlusC_inr];
    1.78 +
    1.79 +(*rules with conclusion a:A, an elem judgement*)
    1.80 +val element_rls = intr_rls @ elim_rls;
    1.81 +
    1.82 +(*Definitions are (meta)equality axioms*)
    1.83 +val basic_defs = [fst_def,snd_def];
    1.84 +
    1.85 +(*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
    1.86 +val SumIL2 = prove_goal CTT.thy
    1.87 +    "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)"
    1.88 + (fn prems=>
    1.89 +  [ (resolve_tac [sym_elem] 1),
    1.90 +    (resolve_tac [SumIL] 1),
    1.91 +    (ALLGOALS (resolve_tac [sym_elem])),
    1.92 +    (ALLGOALS (resolve_tac prems)) ]);
    1.93 +
    1.94 +val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];
    1.95 +
    1.96 +(*Exploit p:Prod(A,B) to create the assumption z:B(a).  
    1.97 +  A more natural form of product elimination. *)
    1.98 +val subst_prodE = prove_goal CTT.thy
    1.99 +    "[| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z) \
   1.100 +\    |] ==> c(p`a): C(p`a)"
   1.101 + (fn prems=>
   1.102 +  [ (REPEAT (resolve_tac (prems@[ProdE]) 1)) ]);
   1.103 +
   1.104 +(** Tactics for type checking **)
   1.105 +
   1.106 +fun is_rigid_elem (Const("Elem",_) $ a $ _) = not (is_Var (head_of a))
   1.107 +  | is_rigid_elem _ = false;
   1.108 +
   1.109 +(*Try solving a:A by assumption provided a is rigid!*) 
   1.110 +val test_assume_tac = SUBGOAL(fn (prem,i) =>
   1.111 +    if is_rigid_elem (Logic.strip_assums_concl prem)
   1.112 +    then  assume_tac i  else  no_tac);
   1.113 +
   1.114 +fun ASSUME tf i = test_assume_tac i  ORELSE  tf i;
   1.115 +
   1.116 +
   1.117 +(*For simplification: type formation and checking,
   1.118 +  but no equalities between terms*)
   1.119 +val routine_rls = form_rls @ formL_rls @ [refl_type] @ element_rls;
   1.120 +
   1.121 +fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
   1.122 +
   1.123 +
   1.124 +(*Solve all subgoals "A type" using formation rules. *)
   1.125 +val form_tac = REPEAT_FIRST (filt_resolve_tac(form_rls) 1);
   1.126 +
   1.127 +
   1.128 +(*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
   1.129 +fun typechk_tac thms =
   1.130 +  let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3
   1.131 +  in  REPEAT_FIRST (ASSUME tac)  end;
   1.132 +
   1.133 +
   1.134 +(*Solve a:A (a flexible, A rigid) by introduction rules. 
   1.135 +  Cannot use stringtrees (filt_resolve_tac) since
   1.136 +  goals like ?a:SUM(A,B) have a trivial head-string *)
   1.137 +fun intr_tac thms =
   1.138 +  let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1
   1.139 +  in  REPEAT_FIRST (ASSUME tac)  end;
   1.140 +
   1.141 +
   1.142 +(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
   1.143 +fun equal_tac thms =
   1.144 +  let val rls = thms @ form_rls @ element_rls @ intrL_rls @
   1.145 +                elimL_rls @ [refl_elem]
   1.146 +  in  REPEAT_FIRST (ASSUME (filt_resolve_tac rls 3))  end;
   1.147 +
   1.148 +(*** Simplification ***)
   1.149 +
   1.150 +(*To simplify the type in a goal*)
   1.151 +val replace_type = prove_goal CTT.thy
   1.152 +    "[| B = A;  a : A |] ==> a : B"
   1.153 + (fn prems=>
   1.154 +  [ (resolve_tac [equal_types] 1),
   1.155 +    (resolve_tac [sym_type] 2),
   1.156 +    (ALLGOALS (resolve_tac prems)) ]);
   1.157 +
   1.158 +(*Simplify the parameter of a unary type operator.*)
   1.159 +val subst_eqtyparg = prove_goal CTT.thy
   1.160 +    "a=c : A ==> (!!z.z:A ==> B(z) type) ==> B(a)=B(c)"
   1.161 + (fn prems=>
   1.162 +  [ (resolve_tac [subst_typeL] 1),
   1.163 +    (resolve_tac [refl_type] 2),
   1.164 +    (ALLGOALS (resolve_tac prems)),
   1.165 +    (assume_tac 1) ]);
   1.166 +
   1.167 +(*Make a reduction rule for simplification.
   1.168 +  A goal a=c becomes b=c, by virtue of a=b *)
   1.169 +fun resolve_trans rl = rl RS trans_elem;
   1.170 +
   1.171 +(*Simplification rules for Constructive Type Theory*)
   1.172 +val reduction_rls = map resolve_trans comp_rls;
   1.173 +
   1.174 +(*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
   1.175 +  Uses other intro rules to avoid changing flexible goals.*)
   1.176 +val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1));
   1.177 +
   1.178 +(** Tactics that instantiate CTT-rules.
   1.179 +    Vars in the given terms will be incremented! 
   1.180 +    The (resolve_tac [EqE] i) lets them apply to equality judgements. **)
   1.181 +
   1.182 +fun NE_tac (sp: string) i = 
   1.183 +  TRY (resolve_tac [EqE] i) THEN res_inst_tac [ ("p",sp) ] NE i;
   1.184 +
   1.185 +fun SumE_tac (sp: string) i = 
   1.186 +  TRY (resolve_tac [EqE] i) THEN res_inst_tac [ ("p",sp) ] SumE i;
   1.187 +
   1.188 +fun PlusE_tac (sp: string) i = 
   1.189 +  TRY (resolve_tac [EqE] i) THEN res_inst_tac [ ("p",sp) ] PlusE i;
   1.190 +
   1.191 +(** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
   1.192 +
   1.193 +(*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
   1.194 +fun add_mp_tac i = 
   1.195 +    resolve_tac [subst_prodE] i  THEN  assume_tac i  THEN  assume_tac i;
   1.196 +
   1.197 +(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
   1.198 +fun mp_tac i = eresolve_tac [subst_prodE] i  THEN  assume_tac i;
   1.199 +
   1.200 +(*"safe" when regarded as predicate calculus rules*)
   1.201 +val safe_brls = sort lessb 
   1.202 +    [ (true,FE), (true,asm_rl), 
   1.203 +      (false,ProdI), (true,SumE), (true,PlusE) ];
   1.204 +
   1.205 +val unsafe_brls =
   1.206 +    [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI), 
   1.207 +      (true,subst_prodE) ];
   1.208 +
   1.209 +(*0 subgoals vs 1 or more*)
   1.210 +val (safe0_brls, safep_brls) =
   1.211 +    partition (apl(0,op=) o subgoals_of_brl) safe_brls;
   1.212 +
   1.213 +fun safestep_tac thms i =
   1.214 +    form_tac  ORELSE  
   1.215 +    resolve_tac thms i  ORELSE
   1.216 +    biresolve_tac safe0_brls i  ORELSE  mp_tac i  ORELSE
   1.217 +    DETERM (biresolve_tac safep_brls i);
   1.218 +
   1.219 +fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i); 
   1.220 +
   1.221 +fun step_tac thms = safestep_tac thms  ORELSE'  biresolve_tac unsafe_brls;
   1.222 +
   1.223 +(*Fails unless it solves the goal!*)
   1.224 +fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms);
   1.225 +
   1.226 +(** The elimination rules for fst/snd **)
   1.227 +
   1.228 +val SumE_fst = prove_goal CTT.thy 
   1.229 +    "p : Sum(A,B) ==> fst(p) : A"
   1.230 + (fn prems=>
   1.231 +  [ (rewrite_goals_tac basic_defs),
   1.232 +    (resolve_tac elim_rls 1),
   1.233 +    (REPEAT (pc_tac prems 1)),
   1.234 +    (fold_tac basic_defs) ]);
   1.235 +
   1.236 +(*The first premise must be p:Sum(A,B) !!*)
   1.237 +val SumE_snd = prove_goal CTT.thy 
   1.238 +    "[| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type \
   1.239 +\    |] ==> snd(p) : B(fst(p))"
   1.240 + (fn prems=>
   1.241 +  [ (rewrite_goals_tac basic_defs),
   1.242 +    (resolve_tac elim_rls 1),
   1.243 +    (resolve_tac prems 1),
   1.244 +    (resolve_tac [replace_type] 1),
   1.245 +    (resolve_tac [subst_eqtyparg] 1),   (*like B(x) equality formation?*)
   1.246 +    (resolve_tac comp_rls 1),
   1.247 +    (typechk_tac prems),
   1.248 +    (fold_tac basic_defs) ]);
   1.249 +
   1.250 +end;
   1.251 +
   1.252 +open CTT_Resolve;