0

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 headstring *)


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 CTTrules.


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_goal CTT.thy


226 
"p : Sum(A,B) ==> fst(p) : A"


227 
(fn prems=>


228 
[ (rewrite_goals_tac basic_defs),


229 
(resolve_tac elim_rls 1),


230 
(REPEAT (pc_tac prems 1)),


231 
(fold_tac basic_defs) ]);


232 


233 
(*The first premise must be p:Sum(A,B) !!*)


234 
val SumE_snd = prove_goal CTT.thy


235 
"[ p: Sum(A,B); A type; !!x. x:A ==> B(x) type \


236 
\ ] ==> snd(p) : B(fst(p))"


237 
(fn prems=>


238 
[ (rewrite_goals_tac basic_defs),


239 
(resolve_tac elim_rls 1),


240 
(resolve_tac prems 1),


241 
(resolve_tac [replace_type] 1),


242 
(resolve_tac [subst_eqtyparg] 1), (*like B(x) equality formation?*)


243 
(resolve_tac comp_rls 1),


244 
(typechk_tac prems),


245 
(fold_tac basic_defs) ]);


246 


247 
end;


248 


249 
open CTT_Resolve;
