1459

1 
(* Title: CTT/ctt.ML

0

2 
ID: $Id$

1459

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1991 University of Cambridge


5 


6 
Tactics and lemmas for ctt.thy (Constructive Type Theory)


7 
*)


8 


9 
open CTT;


10 


11 
(*Formation rules*)


12 
val form_rls = [NF, ProdF, SumF, PlusF, EqF, FF, TF]


13 
and formL_rls = [ProdFL, SumFL, PlusFL, EqFL];


14 


15 


16 
(*Introduction rules


17 
OMITTED: EqI, because its premise is an eqelem, not an elem*)


18 
val intr_rls = [NI0, NI_succ, ProdI, SumI, PlusI_inl, PlusI_inr, TI]


19 
and intrL_rls = [NI_succL, ProdIL, SumIL, PlusI_inlL, PlusI_inrL];


20 


21 


22 
(*Elimination rules


23 
OMITTED: EqE, because its conclusion is an eqelem, not an elem


24 
TE, because it does not involve a constructor *)


25 
val elim_rls = [NE, ProdE, SumE, PlusE, FE]


26 
and elimL_rls = [NEL, ProdEL, SumEL, PlusEL, FEL];


27 


28 
(*OMITTED: eqC are TC because they make rewriting loop: p = un = un = ... *)


29 
val comp_rls = [NC0, NC_succ, ProdC, SumC, PlusC_inl, PlusC_inr];


30 


31 
(*rules with conclusion a:A, an elem judgement*)


32 
val element_rls = intr_rls @ elim_rls;


33 


34 
(*Definitions are (meta)equality axioms*)


35 
val basic_defs = [fst_def,snd_def];


36 


37 
(*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)

1294

38 
qed_goal "SumIL2" CTT.thy

0

39 
"[ c=a : A; d=b : B(a) ] ==> <c,d> = <a,b> : Sum(A,B)"


40 
(fn prems=>

1459

41 
[ (rtac sym_elem 1),


42 
(rtac SumIL 1),


43 
(ALLGOALS (rtac sym_elem )),

0

44 
(ALLGOALS (resolve_tac prems)) ]);


45 


46 
val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];


47 


48 
(*Exploit p:Prod(A,B) to create the assumption z:B(a).


49 
A more natural form of product elimination. *)

1294

50 
qed_goal "subst_prodE" CTT.thy

0

51 
"[ p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z) \


52 
\ ] ==> c(p`a): C(p`a)"


53 
(fn prems=>


54 
[ (REPEAT (resolve_tac (prems@[ProdE]) 1)) ]);


55 


56 
(** Tactics for type checking **)


57 

3929

58 
fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not (is_Var (head_of a))

0

59 
 is_rigid_elem _ = false;


60 


61 
(*Try solving a:A by assumption provided a is rigid!*)


62 
val test_assume_tac = SUBGOAL(fn (prem,i) =>


63 
if is_rigid_elem (Logic.strip_assums_concl prem)


64 
then assume_tac i else no_tac);


65 


66 
fun ASSUME tf i = test_assume_tac i ORELSE tf i;


67 


68 


69 
(*For simplification: type formation and checking,


70 
but no equalities between terms*)


71 
val routine_rls = form_rls @ formL_rls @ [refl_type] @ element_rls;


72 


73 
fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);


74 


75 


76 
(*Solve all subgoals "A type" using formation rules. *)


77 
val form_tac = REPEAT_FIRST (filt_resolve_tac(form_rls) 1);


78 


79 


80 
(*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)


81 
fun typechk_tac thms =


82 
let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3


83 
in REPEAT_FIRST (ASSUME tac) end;


84 


85 


86 
(*Solve a:A (a flexible, A rigid) by introduction rules.


87 
Cannot use stringtrees (filt_resolve_tac) since


88 
goals like ?a:SUM(A,B) have a trivial headstring *)


89 
fun intr_tac thms =


90 
let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1


91 
in REPEAT_FIRST (ASSUME tac) end;


92 


93 


94 
(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)


95 
fun equal_tac thms =


96 
let val rls = thms @ form_rls @ element_rls @ intrL_rls @


97 
elimL_rls @ [refl_elem]


98 
in REPEAT_FIRST (ASSUME (filt_resolve_tac rls 3)) end;


99 


100 
(*** Simplification ***)


101 


102 
(*To simplify the type in a goal*)

1294

103 
qed_goal "replace_type" CTT.thy

0

104 
"[ B = A; a : A ] ==> a : B"


105 
(fn prems=>

1459

106 
[ (rtac equal_types 1),


107 
(rtac sym_type 2),

0

108 
(ALLGOALS (resolve_tac prems)) ]);


109 


110 
(*Simplify the parameter of a unary type operator.*)

1294

111 
qed_goal "subst_eqtyparg" CTT.thy

3837

112 
"a=c : A ==> (!!z. z:A ==> B(z) type) ==> B(a)=B(c)"

0

113 
(fn prems=>

1459

114 
[ (rtac subst_typeL 1),


115 
(rtac refl_type 2),

0

116 
(ALLGOALS (resolve_tac prems)),


117 
(assume_tac 1) ]);


118 


119 
(*Make a reduction rule for simplification.


120 
A goal a=c becomes b=c, by virtue of a=b *)


121 
fun resolve_trans rl = rl RS trans_elem;


122 


123 
(*Simplification rules for Constructive Type Theory*)


124 
val reduction_rls = map resolve_trans comp_rls;


125 


126 
(*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.


127 
Uses other intro rules to avoid changing flexible goals.*)


128 
val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1));


129 


130 
(** Tactics that instantiate CTTrules.


131 
Vars in the given terms will be incremented!

1459

132 
The (rtac EqE i) lets them apply to equality judgements. **)

0

133 


134 
fun NE_tac (sp: string) i =

1459

135 
TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i;

0

136 


137 
fun SumE_tac (sp: string) i =

1459

138 
TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i;

0

139 


140 
fun PlusE_tac (sp: string) i =

1459

141 
TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i;

0

142 


143 
(** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **)


144 


145 
(*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)


146 
fun add_mp_tac i =

1459

147 
rtac subst_prodE i THEN assume_tac i THEN assume_tac i;

0

148 


149 
(*Finds P>Q and P in the assumptions, replaces implication by Q *)

1459

150 
fun mp_tac i = etac subst_prodE i THEN assume_tac i;

0

151 


152 
(*"safe" when regarded as predicate calculus rules*)

4440

153 
val safe_brls = sort (make_ord lessb)

0

154 
[ (true,FE), (true,asm_rl),


155 
(false,ProdI), (true,SumE), (true,PlusE) ];


156 


157 
val unsafe_brls =


158 
[ (false,PlusI_inl), (false,PlusI_inr), (false,SumI),


159 
(true,subst_prodE) ];


160 


161 
(*0 subgoals vs 1 or more*)


162 
val (safe0_brls, safep_brls) =


163 
partition (apl(0,op=) o subgoals_of_brl) safe_brls;


164 


165 
fun safestep_tac thms i =


166 
form_tac ORELSE


167 
resolve_tac thms i ORELSE


168 
biresolve_tac safe0_brls i ORELSE mp_tac i ORELSE


169 
DETERM (biresolve_tac safep_brls i);


170 


171 
fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i);


172 


173 
fun step_tac thms = safestep_tac thms ORELSE' biresolve_tac unsafe_brls;


174 


175 
(*Fails unless it solves the goal!*)


176 
fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms);


177 


178 
(** The elimination rules for fst/snd **)


179 

1294

180 
qed_goalw "SumE_fst" CTT.thy basic_defs

0

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

361

182 
(fn [major] =>


183 
[ (rtac (major RS SumE) 1),


184 
(assume_tac 1) ]);

0

185 


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

1294

187 
qed_goalw "SumE_snd" CTT.thy basic_defs

0

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


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

361

190 
(fn major::prems=>


191 
[ (rtac (major RS SumE) 1),


192 
(resolve_tac [SumC RS subst_eqtyparg RS replace_type] 1),


193 
(typechk_tac prems) ]);
