equal
deleted
inserted
replaced
16 val init: cterm -> thm |
16 val init: cterm -> thm |
17 val protect: thm -> thm |
17 val protect: thm -> thm |
18 val conclude: thm -> thm |
18 val conclude: thm -> thm |
19 val finish: thm -> thm |
19 val finish: thm -> thm |
20 val norm_hhf: thm -> thm |
20 val norm_hhf: thm -> thm |
|
21 val norm_hhf': thm -> thm |
21 val compose_hhf: thm -> int -> thm -> thm Seq.seq |
22 val compose_hhf: thm -> int -> thm -> thm Seq.seq |
22 val compose_hhf_tac: thm -> int -> tactic |
23 val compose_hhf_tac: thm -> int -> tactic |
23 val comp_hhf: thm -> thm -> thm |
24 val comp_hhf: thm -> thm -> thm |
24 val prove_multi: theory -> string list -> term list -> term list -> |
25 val prove_multi: theory -> string list -> term list -> term list -> |
25 (thm list -> tactic) -> thm list |
26 (thm list -> tactic) -> thm list |
72 |
73 |
73 (** results **) |
74 (** results **) |
74 |
75 |
75 (* HHF normal form *) |
76 (* HHF normal form *) |
76 |
77 |
77 val norm_hhf = |
78 val norm_hhf_ss = |
|
79 MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss |
|
80 addsimps [Drule.norm_hhf_eq]; |
|
81 |
|
82 val norm_hhf_ss' = norm_hhf_ss addeqcongs [Drule.protect_cong]; |
|
83 |
|
84 fun gen_norm_hhf protected = |
78 (not o Drule.is_norm_hhf o Thm.prop_of) ? |
85 (not o Drule.is_norm_hhf o Thm.prop_of) ? |
79 MetaSimplifier.simplify_aux (K (K NONE)) true [Drule.norm_hhf_eq] |
86 Drule.fconv_rule (MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) |
|
87 (if protected then norm_hhf_ss else norm_hhf_ss')) |
80 #> Thm.adjust_maxidx_thm |
88 #> Thm.adjust_maxidx_thm |
81 #> Drule.gen_all; |
89 #> Drule.gen_all; |
|
90 |
|
91 val norm_hhf = gen_norm_hhf true; |
|
92 val norm_hhf' = gen_norm_hhf false; |
82 |
93 |
83 |
94 |
84 (* composition of normal results *) |
95 (* composition of normal results *) |
85 |
96 |
86 fun compose_hhf tha i thb = |
97 fun compose_hhf tha i thb = |