55 "0" :: "i" ("0") |
56 "0" :: "i" ("0") |
56 (*Pairing*) |
57 (*Pairing*) |
57 pair :: "[i,i]=>i" ("(1<_,/_>)") |
58 pair :: "[i,i]=>i" ("(1<_,/_>)") |
58 |
59 |
59 syntax |
60 syntax |
60 "@PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10) |
61 "_PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10) |
61 "@SUM" :: "[idt,t,t]=>t" ("(3SUM _:_./ _)" 10) |
62 "_SUM" :: "[idt,t,t]=>t" ("(3SUM _:_./ _)" 10) |
62 "@-->" :: "[t,t]=>t" ("(_ -->/ _)" [31,30] 30) |
|
63 "@*" :: "[t,t]=>t" ("(_ */ _)" [51,50] 50) |
|
64 |
|
65 translations |
63 translations |
66 "PROD x:A. B" => "Prod(A, %x. B)" |
64 "PROD x:A. B" == "Prod(A, %x. B)" |
67 "A --> B" => "Prod(A, %_. B)" |
65 "SUM x:A. B" == "Sum(A, %x. B)" |
68 "SUM x:A. B" => "Sum(A, %x. B)" |
66 |
69 "A * B" => "Sum(A, %_. B)" |
67 abbreviation |
70 |
68 Arrow :: "[t,t]=>t" (infixr "-->" 30) |
71 print_translation {* |
69 "A --> B == PROD _:A. B" |
72 [("Prod", dependent_tr' ("@PROD", "@-->")), |
70 Times :: "[t,t]=>t" (infixr "*" 50) |
73 ("Sum", dependent_tr' ("@SUM", "@*"))] |
71 "A * B == SUM _:A. B" |
74 *} |
72 |
75 |
73 const_syntax (xsymbols) |
|
74 Elem ("(_ /\<in> _)" [10,10] 5) |
|
75 Eqelem ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) |
|
76 Arrow (infixr "\<longrightarrow>" 30) |
|
77 Times (infixr "\<times>" 50) |
|
78 |
|
79 const_syntax (HTML output) |
|
80 Elem ("(_ /\<in> _)" [10,10] 5) |
|
81 Eqelem ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) |
|
82 Times (infixr "\<times>" 50) |
76 |
83 |
77 syntax (xsymbols) |
84 syntax (xsymbols) |
78 "@-->" :: "[t,t]=>t" ("(_ \<longrightarrow>/ _)" [31,30] 30) |
|
79 "@*" :: "[t,t]=>t" ("(_ \<times>/ _)" [51,50] 50) |
|
80 Elem :: "[i, t]=>prop" ("(_ /\<in> _)" [10,10] 5) |
|
81 Eqelem :: "[i,i,t]=>prop" ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) |
|
82 "@SUM" :: "[idt,t,t] => t" ("(3\<Sigma> _\<in>_./ _)" 10) |
85 "@SUM" :: "[idt,t,t] => t" ("(3\<Sigma> _\<in>_./ _)" 10) |
83 "@PROD" :: "[idt,t,t] => t" ("(3\<Pi> _\<in>_./ _)" 10) |
86 "@PROD" :: "[idt,t,t] => t" ("(3\<Pi> _\<in>_./ _)" 10) |
84 "lam " :: "[idts, i] => i" ("(3\<lambda>\<lambda>_./ _)" 10) |
87 "lam " :: "[idts, i] => i" ("(3\<lambda>\<lambda>_./ _)" 10) |
85 |
88 |
86 syntax (HTML output) |
89 syntax (HTML output) |
87 "@*" :: "[t,t]=>t" ("(_ \<times>/ _)" [51,50] 50) |
|
88 Elem :: "[i, t]=>prop" ("(_ /\<in> _)" [10,10] 5) |
|
89 Eqelem :: "[i,i,t]=>prop" ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) |
|
90 "@SUM" :: "[idt,t,t] => t" ("(3\<Sigma> _\<in>_./ _)" 10) |
90 "@SUM" :: "[idt,t,t] => t" ("(3\<Sigma> _\<in>_./ _)" 10) |
91 "@PROD" :: "[idt,t,t] => t" ("(3\<Pi> _\<in>_./ _)" 10) |
91 "@PROD" :: "[idt,t,t] => t" ("(3\<Pi> _\<in>_./ _)" 10) |
92 "lam " :: "[idts, i] => i" ("(3\<lambda>\<lambda>_./ _)" 10) |
92 "lam " :: "[idts, i] => i" ("(3\<lambda>\<lambda>_./ _)" 10) |
93 |
93 |
94 axioms |
94 axioms |
271 TI: "tt : T" |
271 TI: "tt : T" |
272 TE: "[| p : T; c : C(tt) |] ==> c : C(p)" |
272 TE: "[| p : T; c : C(tt) |] ==> c : C(p)" |
273 TEL: "[| p = q : T; c = d : C(tt) |] ==> c = d : C(p)" |
273 TEL: "[| p = q : T; c = d : C(tt) |] ==> c = d : C(p)" |
274 TC: "p : T ==> p = tt : T" |
274 TC: "p : T ==> p = tt : T" |
275 |
275 |
276 ML {* use_legacy_bindings (the_context ()) *} |
276 |
|
277 subsection "Tactics and derived rules for Constructive Type Theory" |
|
278 |
|
279 (*Formation rules*) |
|
280 lemmas form_rls = NF ProdF SumF PlusF EqF FF TF |
|
281 and formL_rls = ProdFL SumFL PlusFL EqFL |
|
282 |
|
283 (*Introduction rules |
|
284 OMITTED: EqI, because its premise is an eqelem, not an elem*) |
|
285 lemmas intr_rls = NI0 NI_succ ProdI SumI PlusI_inl PlusI_inr TI |
|
286 and intrL_rls = NI_succL ProdIL SumIL PlusI_inlL PlusI_inrL |
|
287 |
|
288 (*Elimination rules |
|
289 OMITTED: EqE, because its conclusion is an eqelem, not an elem |
|
290 TE, because it does not involve a constructor *) |
|
291 lemmas elim_rls = NE ProdE SumE PlusE FE |
|
292 and elimL_rls = NEL ProdEL SumEL PlusEL FEL |
|
293 |
|
294 (*OMITTED: eqC are TC because they make rewriting loop: p = un = un = ... *) |
|
295 lemmas comp_rls = NC0 NC_succ ProdC SumC PlusC_inl PlusC_inr |
|
296 |
|
297 (*rules with conclusion a:A, an elem judgement*) |
|
298 lemmas element_rls = intr_rls elim_rls |
|
299 |
|
300 (*Definitions are (meta)equality axioms*) |
|
301 lemmas basic_defs = fst_def snd_def |
|
302 |
|
303 (*Compare with standard version: B is applied to UNSIMPLIFIED expression! *) |
|
304 lemma SumIL2: "[| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)" |
|
305 apply (rule sym_elem) |
|
306 apply (rule SumIL) |
|
307 apply (rule_tac [!] sym_elem) |
|
308 apply assumption+ |
|
309 done |
|
310 |
|
311 lemmas intrL2_rls = NI_succL ProdIL SumIL2 PlusI_inlL PlusI_inrL |
|
312 |
|
313 (*Exploit p:Prod(A,B) to create the assumption z:B(a). |
|
314 A more natural form of product elimination. *) |
|
315 lemma subst_prodE: |
|
316 assumes "p: Prod(A,B)" |
|
317 and "a: A" |
|
318 and "!!z. z: B(a) ==> c(z): C(z)" |
|
319 shows "c(p`a): C(p`a)" |
|
320 apply (rule prems ProdE)+ |
|
321 done |
|
322 |
|
323 |
|
324 subsection {* Tactics for type checking *} |
|
325 |
|
326 ML {* |
|
327 |
|
328 local |
|
329 |
|
330 fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not(is_Var (head_of a)) |
|
331 | is_rigid_elem (Const("CTT.Eqelem",_) $ a $ _ $ _) = not(is_Var (head_of a)) |
|
332 | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a)) |
|
333 | is_rigid_elem _ = false |
|
334 |
|
335 in |
|
336 |
|
337 (*Try solving a:A or a=b:A by assumption provided a is rigid!*) |
|
338 val test_assume_tac = SUBGOAL(fn (prem,i) => |
|
339 if is_rigid_elem (Logic.strip_assums_concl prem) |
|
340 then assume_tac i else no_tac) |
|
341 |
|
342 fun ASSUME tf i = test_assume_tac i ORELSE tf i |
|
343 |
|
344 end; |
|
345 |
|
346 *} |
|
347 |
|
348 (*For simplification: type formation and checking, |
|
349 but no equalities between terms*) |
|
350 lemmas routine_rls = form_rls formL_rls refl_type element_rls |
|
351 |
|
352 ML {* |
|
353 local |
|
354 val routine_rls = thms "routine_rls"; |
|
355 val form_rls = thms "form_rls"; |
|
356 val intr_rls = thms "intr_rls"; |
|
357 val element_rls = thms "element_rls"; |
|
358 val equal_rls = form_rls @ element_rls @ thms "intrL_rls" @ |
|
359 thms "elimL_rls" @ thms "refl_elem" |
|
360 in |
|
361 |
|
362 fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4); |
|
363 |
|
364 (*Solve all subgoals "A type" using formation rules. *) |
|
365 val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(form_rls) 1)); |
|
366 |
|
367 (*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *) |
|
368 fun typechk_tac thms = |
|
369 let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3 |
|
370 in REPEAT_FIRST (ASSUME tac) end |
|
371 |
|
372 (*Solve a:A (a flexible, A rigid) by introduction rules. |
|
373 Cannot use stringtrees (filt_resolve_tac) since |
|
374 goals like ?a:SUM(A,B) have a trivial head-string *) |
|
375 fun intr_tac thms = |
|
376 let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1 |
|
377 in REPEAT_FIRST (ASSUME tac) end |
|
378 |
|
379 (*Equality proving: solve a=b:A (where a is rigid) by long rules. *) |
|
380 fun equal_tac thms = |
|
381 REPEAT_FIRST (ASSUME (filt_resolve_tac (thms @ equal_rls) 3)) |
277 |
382 |
278 end |
383 end |
|
384 |
|
385 *} |
|
386 |
|
387 |
|
388 subsection {* Simplification *} |
|
389 |
|
390 (*To simplify the type in a goal*) |
|
391 lemma replace_type: "[| B = A; a : A |] ==> a : B" |
|
392 apply (rule equal_types) |
|
393 apply (rule_tac [2] sym_type) |
|
394 apply assumption+ |
|
395 done |
|
396 |
|
397 (*Simplify the parameter of a unary type operator.*) |
|
398 lemma subst_eqtyparg: |
|
399 assumes "a=c : A" |
|
400 and "!!z. z:A ==> B(z) type" |
|
401 shows "B(a)=B(c)" |
|
402 apply (rule subst_typeL) |
|
403 apply (rule_tac [2] refl_type) |
|
404 apply (rule prems) |
|
405 apply assumption |
|
406 done |
|
407 |
|
408 (*Simplification rules for Constructive Type Theory*) |
|
409 lemmas reduction_rls = comp_rls [THEN trans_elem] |
|
410 |
|
411 ML {* |
|
412 local |
|
413 val EqI = thm "EqI"; |
|
414 val EqE = thm "EqE"; |
|
415 val NE = thm "NE"; |
|
416 val FE = thm "FE"; |
|
417 val ProdI = thm "ProdI"; |
|
418 val SumI = thm "SumI"; |
|
419 val SumE = thm "SumE"; |
|
420 val PlusE = thm "PlusE"; |
|
421 val PlusI_inl = thm "PlusI_inl"; |
|
422 val PlusI_inr = thm "PlusI_inr"; |
|
423 val subst_prodE = thm "subst_prodE"; |
|
424 val intr_rls = thms "intr_rls"; |
|
425 in |
|
426 |
|
427 (*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification. |
|
428 Uses other intro rules to avoid changing flexible goals.*) |
|
429 val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1)) |
|
430 |
|
431 (** Tactics that instantiate CTT-rules. |
|
432 Vars in the given terms will be incremented! |
|
433 The (rtac EqE i) lets them apply to equality judgements. **) |
|
434 |
|
435 fun NE_tac (sp: string) i = |
|
436 TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i |
|
437 |
|
438 fun SumE_tac (sp: string) i = |
|
439 TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i |
|
440 |
|
441 fun PlusE_tac (sp: string) i = |
|
442 TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i |
|
443 |
|
444 (** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **) |
|
445 |
|
446 (*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *) |
|
447 fun add_mp_tac i = |
|
448 rtac subst_prodE i THEN assume_tac i THEN assume_tac i |
|
449 |
|
450 (*Finds P-->Q and P in the assumptions, replaces implication by Q *) |
|
451 fun mp_tac i = etac subst_prodE i THEN assume_tac i |
|
452 |
|
453 (*"safe" when regarded as predicate calculus rules*) |
|
454 val safe_brls = sort (make_ord lessb) |
|
455 [ (true,FE), (true,asm_rl), |
|
456 (false,ProdI), (true,SumE), (true,PlusE) ] |
|
457 |
|
458 val unsafe_brls = |
|
459 [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI), |
|
460 (true,subst_prodE) ] |
|
461 |
|
462 (*0 subgoals vs 1 or more*) |
|
463 val (safe0_brls, safep_brls) = |
|
464 List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls |
|
465 |
|
466 fun safestep_tac thms i = |
|
467 form_tac ORELSE |
|
468 resolve_tac thms i ORELSE |
|
469 biresolve_tac safe0_brls i ORELSE mp_tac i ORELSE |
|
470 DETERM (biresolve_tac safep_brls i) |
|
471 |
|
472 fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i) |
|
473 |
|
474 fun step_tac thms = safestep_tac thms ORELSE' biresolve_tac unsafe_brls |
|
475 |
|
476 (*Fails unless it solves the goal!*) |
|
477 fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms) |
|
478 |
|
479 end |
|
480 *} |
|
481 |
|
482 use "rew.ML" |
|
483 |
|
484 |
|
485 subsection {* The elimination rules for fst/snd *} |
|
486 |
|
487 lemma SumE_fst: "p : Sum(A,B) ==> fst(p) : A" |
|
488 apply (unfold basic_defs) |
|
489 apply (erule SumE) |
|
490 apply assumption |
|
491 done |
|
492 |
|
493 (*The first premise must be p:Sum(A,B) !!*) |
|
494 lemma SumE_snd: |
|
495 assumes major: "p: Sum(A,B)" |
|
496 and "A type" |
|
497 and "!!x. x:A ==> B(x) type" |
|
498 shows "snd(p) : B(fst(p))" |
|
499 apply (unfold basic_defs) |
|
500 apply (rule major [THEN SumE]) |
|
501 apply (rule SumC [THEN subst_eqtyparg, THEN replace_type]) |
|
502 apply (tactic {* typechk_tac (thms "prems") *}) |
|
503 done |
|
504 |
|
505 end |