author  obua 
Fri, 16 Sep 2005 21:02:15 +0200  
changeset 17440  df77edc4f5d0 
parent 15570  8d8c70b41bab 
child 17441  5b5feca0344a 
permissions  rwrr 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

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 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

6 
Tactics and derived rules for Constructive Type Theory 
0  7 
*) 
8 

9 
(*Formation rules*) 

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

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

12 

13 

14 
(*Introduction rules 

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

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

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

18 

19 

20 
(*Elimination rules 

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

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

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

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

25 

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

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

28 

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

30 
val element_rls = intr_rls @ elim_rls; 

31 

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

33 
val basic_defs = [fst_def,snd_def]; 

34 

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

36 
Goal "[ c=a : A; d=b : B(a) ] ==> <c,d> = <a,b> : Sum(A,B)"; 
9249  37 
by (rtac sym_elem 1); 
38 
by (rtac SumIL 1); 

39 
by (ALLGOALS (rtac sym_elem )); 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

40 
by (ALLGOALS assume_tac) ; 
9249  41 
qed "SumIL2"; 
0  42 

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

44 

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

46 
A more natural form of product elimination. *) 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

47 
val prems = Goal "[ p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z) \ 
9249  48 
\ ] ==> c(p`a): C(p`a)"; 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

49 
by (REPEAT (resolve_tac (ProdE::prems) 1)) ; 
9249  50 
qed "subst_prodE"; 
0  51 

52 
(** Tactics for type checking **) 

53 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

54 
fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not(is_Var (head_of a)) 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

55 
 is_rigid_elem (Const("CTT.Eqelem",_) $ a $ _ $ _) = not(is_Var (head_of a)) 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

56 
 is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a)) 
0  57 
 is_rigid_elem _ = false; 
58 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

59 
(*Try solving a:A or a=b:A by assumption provided a is rigid!*) 
0  60 
val test_assume_tac = SUBGOAL(fn (prem,i) => 
61 
if is_rigid_elem (Logic.strip_assums_concl prem) 

62 
then assume_tac i else no_tac); 

63 

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

65 

66 

67 
(*For simplification: type formation and checking, 

68 
but no equalities between terms*) 

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

70 

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

72 

73 

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

75 
val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(form_rls) 1)); 
0  76 

77 

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

79 
fun typechk_tac thms = 

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

81 
in REPEAT_FIRST (ASSUME tac) end; 

82 

83 

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

85 
Cannot use stringtrees (filt_resolve_tac) since 

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

87 
fun intr_tac thms = 

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

89 
in REPEAT_FIRST (ASSUME tac) end; 

90 

91 

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

93 
fun equal_tac thms = 

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

95 
elimL_rls @ [refl_elem] 

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

97 

98 
(*** Simplification ***) 

99 

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

101 
Goal "[ B = A; a : A ] ==> a : B"; 
9249  102 
by (rtac equal_types 1); 
103 
by (rtac sym_type 2); 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

104 
by (ALLGOALS assume_tac) ; 
9249  105 
qed "replace_type"; 
0  106 

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

108 
val prems = Goal 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

109 
"[ a=c : A; !!z. z:A ==> B(z) type ] ==> B(a)=B(c)"; 
9249  110 
by (rtac subst_typeL 1); 
111 
by (rtac refl_type 2); 

112 
by (ALLGOALS (resolve_tac prems)); 

113 
by (assume_tac 1) ; 

114 
qed "subst_eqtyparg"; 

0  115 

116 
(*Make a reduction rule for simplification. 

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

118 
fun resolve_trans rl = rl RS trans_elem; 

119 

120 
(*Simplification rules for Constructive Type Theory*) 

121 
val reduction_rls = map resolve_trans comp_rls; 

122 

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

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

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

126 

127 
(** Tactics that instantiate CTTrules. 

128 
Vars in the given terms will be incremented! 

1459  129 
The (rtac EqE i) lets them apply to equality judgements. **) 
0  130 

131 
fun NE_tac (sp: string) i = 

1459  132 
TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i; 
0  133 

134 
fun SumE_tac (sp: string) i = 

1459  135 
TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i; 
0  136 

137 
fun PlusE_tac (sp: string) i = 

1459  138 
TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i; 
0  139 

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

141 

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

143 
fun add_mp_tac i = 

1459  144 
rtac subst_prodE i THEN assume_tac i THEN assume_tac i; 
0  145 

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

1459  147 
fun mp_tac i = etac subst_prodE i THEN assume_tac i; 
0  148 

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

4440  150 
val safe_brls = sort (make_ord lessb) 
0  151 
[ (true,FE), (true,asm_rl), 
152 
(false,ProdI), (true,SumE), (true,PlusE) ]; 

153 

154 
val unsafe_brls = 

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

156 
(true,subst_prodE) ]; 

157 

158 
(*0 subgoals vs 1 or more*) 

159 
val (safe0_brls, safep_brls) = 

15570  160 
List.partition (apl(0,op=) o subgoals_of_brl) safe_brls; 
0  161 

162 
fun safestep_tac thms i = 

163 
form_tac ORELSE 

164 
resolve_tac thms i ORELSE 

165 
biresolve_tac safe0_brls i ORELSE mp_tac i ORELSE 

166 
DETERM (biresolve_tac safep_brls i); 

167 

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

169 

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

171 

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

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

174 

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

176 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

177 
Goalw basic_defs "p : Sum(A,B) ==> fst(p) : A"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

178 
by (etac SumE 1); 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

179 
by (assume_tac 1); 
9249  180 
qed "SumE_fst"; 
0  181 

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

183 
val major::prems= Goalw basic_defs 
0  184 
"[ p: Sum(A,B); A type; !!x. x:A ==> B(x) type \ 
9249  185 
\ ] ==> snd(p) : B(fst(p))"; 
186 
by (rtac (major RS SumE) 1); 

187 
by (resolve_tac [SumC RS subst_eqtyparg RS replace_type] 1); 

188 
by (typechk_tac prems) ; 

189 
qed "SumE_snd"; 