27 val forall_intr_frees : thm -> thm |
27 val forall_intr_frees : thm -> thm |
28 val forall_intr_vars : thm -> thm |
28 val forall_intr_vars : thm -> thm |
29 val forall_elim_list : cterm list -> thm -> thm |
29 val forall_elim_list : cterm list -> thm -> thm |
30 val forall_elim_var : int -> thm -> thm |
30 val forall_elim_var : int -> thm -> thm |
31 val forall_elim_vars : int -> thm -> thm |
31 val forall_elim_vars : int -> thm -> thm |
|
32 val forall_elim_vars_safe : thm -> thm |
32 val freeze_thaw : thm -> thm * (thm -> thm) |
33 val freeze_thaw : thm -> thm * (thm -> thm) |
33 val implies_elim_list : thm -> thm list -> thm |
34 val implies_elim_list : thm -> thm list -> thm |
34 val implies_intr_list : cterm list -> thm -> thm |
35 val implies_intr_list : cterm list -> thm -> thm |
35 val instantiate : |
36 val instantiate : |
36 (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm |
37 (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm |
97 val tag_assumption : 'a attribute |
98 val tag_assumption : 'a attribute |
98 val tag_internal : 'a attribute |
99 val tag_internal : 'a attribute |
99 val has_internal : tag list -> bool |
100 val has_internal : tag list -> bool |
100 val compose_single : thm * int * thm -> thm |
101 val compose_single : thm * int * thm -> thm |
101 val merge_rules : thm list * thm list -> thm list |
102 val merge_rules : thm list * thm list -> thm list |
|
103 val norm_hhf_eq : thm |
102 val triv_goal : thm |
104 val triv_goal : thm |
103 val rev_triv_goal : thm |
105 val rev_triv_goal : thm |
104 val freeze_all : thm -> thm |
106 val freeze_all : thm -> thm |
105 val mk_triv_goal : cterm -> thm |
107 val mk_triv_goal : cterm -> thm |
106 val mk_cgoal : cterm -> cterm |
108 val mk_cgoal : cterm -> cterm |
281 end; |
283 end; |
282 |
284 |
283 val forall_elim_var = PureThy.forall_elim_var; |
285 val forall_elim_var = PureThy.forall_elim_var; |
284 val forall_elim_vars = PureThy.forall_elim_vars; |
286 val forall_elim_vars = PureThy.forall_elim_vars; |
285 |
287 |
|
288 fun forall_elim_vars_safe th = |
|
289 forall_elim_vars_safe (forall_elim_var (#maxidx (Thm.rep_thm th) + 1) th) |
|
290 handle THM _ => th; |
|
291 |
|
292 |
286 (*Specialization over a list of cterms*) |
293 (*Specialization over a list of cterms*) |
287 fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th); |
294 fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th); |
288 |
295 |
289 (* maps [A1,...,An], B to [| A1;...;An |] ==> B *) |
296 (* maps [A1,...,An], B to [| A1;...;An |] ==> B *) |
290 fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th); |
297 fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th); |
490 |
497 |
491 (*rewriting conversion*) |
498 (*rewriting conversion*) |
492 fun rew_conv mode prover mss = rewrite_cterm mode mss prover; |
499 fun rew_conv mode prover mss = rewrite_cterm mode mss prover; |
493 |
500 |
494 (*Rewrite a theorem*) |
501 (*Rewrite a theorem*) |
495 fun rewrite_rule_aux _ [] th = th |
502 fun rewrite_rule_aux _ [] = (fn th => th) |
496 | rewrite_rule_aux prover thms th = |
503 | rewrite_rule_aux prover thms = |
497 fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms)) th; |
504 fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms)); |
498 |
505 |
499 fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss); |
506 fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss); |
500 fun rewrite_cterm mode prover mss = Thm.rewrite_cterm mode mss prover; |
507 fun rewrite_cterm mode prover mss = Thm.rewrite_cterm mode mss prover; |
501 |
508 |
502 (*Rewrite the subgoals of a proof state (represented by a theorem) *) |
509 (*Rewrite the subgoals of a proof state (represented by a theorem) *) |
575 let val PQ = read_prop "PROP phi ==> PROP psi" |
582 let val PQ = read_prop "PROP phi ==> PROP psi" |
576 and QP = read_prop "PROP psi ==> PROP phi" |
583 and QP = read_prop "PROP psi ==> PROP phi" |
577 in |
584 in |
578 store_standard_thm "equal_intr_rule" |
585 store_standard_thm "equal_intr_rule" |
579 (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) |
586 (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) |
|
587 end; |
|
588 |
|
589 |
|
590 (*(PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x)) |
|
591 Rewrite rule for HHF normalization. |
|
592 |
|
593 Note: the syntax of ProtoPure is insufficient to handle this |
|
594 statement; storing it would be asking for trouble, e.g. when someone |
|
595 tries to print the theory later. |
|
596 *) |
|
597 |
|
598 val norm_hhf_eq = |
|
599 let |
|
600 val cert = Thm.cterm_of proto_sign; |
|
601 val aT = TFree ("'a", Term.logicS); |
|
602 val all = Term.all aT; |
|
603 val x = Free ("x", aT); |
|
604 val phi = Free ("phi", propT); |
|
605 val psi = Free ("psi", aT --> propT); |
|
606 |
|
607 val cx = cert x; |
|
608 val cphi = cert phi; |
|
609 val lhs = cert (Logic.mk_implies (phi, all $ Abs ("x", aT, psi $ Bound 0))); |
|
610 val rhs = cert (all $ Abs ("x", aT, Logic.mk_implies (phi, psi $ Bound 0))); |
|
611 in |
|
612 Thm.equal_intr |
|
613 (Thm.implies_elim (Thm.assume lhs) (Thm.assume cphi) |
|
614 |> Thm.forall_elim cx |
|
615 |> Thm.implies_intr cphi |
|
616 |> Thm.forall_intr cx |
|
617 |> Thm.implies_intr lhs) |
|
618 (Thm.implies_elim |
|
619 (Thm.assume rhs |> Thm.forall_elim cx) (Thm.assume cphi) |
|
620 |> Thm.forall_intr cx |
|
621 |> Thm.implies_intr cphi |
|
622 |> Thm.implies_intr rhs) |
|
623 |> standard |> curry Thm.name_thm "ProtoPure.norm_hhf_eq" |
580 end; |
624 end; |
581 |
625 |
582 |
626 |
583 (*** Instantiate theorem th, reading instantiations under signature sg ****) |
627 (*** Instantiate theorem th, reading instantiations under signature sg ****) |
584 |
628 |