equal
deleted
inserted
replaced
62 val mk_union: term * term -> term |
62 val mk_union: term * term -> term |
63 val fold_union: term list -> term |
63 val fold_union: term list -> term |
64 val fold_append: term list -> term |
64 val fold_append: term list -> term |
65 val mk_conj: term * term -> term |
65 val mk_conj: term * term -> term |
66 val fold_conj: term list -> term |
66 val fold_conj: term list -> term |
|
67 val fold_conj_balanced: term list -> term |
67 |
68 |
68 (* functions for de-Bruijn open terms *) |
69 (* functions for de-Bruijn open terms *) |
69 val mk_binop_env: typ list -> string -> term * term -> term |
70 val mk_binop_env: typ list -> string -> term * term -> term |
70 val mk_union_env: typ list -> term * term -> term |
71 val mk_union_env: typ list -> term * term -> term |
71 val fold_union_env: typ list -> term list -> term |
72 val fold_union_env: typ list -> term list -> term |
92 val transform_prem1: Proof.context -> string list -> thm -> thm |
93 val transform_prem1: Proof.context -> string list -> thm -> thm |
93 val transform_prem2: Proof.context -> string list -> thm -> thm |
94 val transform_prem2: Proof.context -> string list -> thm -> thm |
94 |
95 |
95 (* transformation into the object logic *) |
96 (* transformation into the object logic *) |
96 val atomize: thm -> thm |
97 val atomize: thm -> thm |
|
98 val atomize_rule: int -> thm -> thm |
|
99 val atomize_concl: thm -> thm |
97 |
100 |
98 (* applies a tactic to a formula composed of conjunctions *) |
101 (* applies a tactic to a formula composed of conjunctions *) |
99 val conj_tac: (int -> tactic) -> int -> tactic |
102 val conj_tac: (int -> tactic) -> int -> tactic |
100 end |
103 end |
101 |
104 |
247 fun mk_conj (t1, @{term "True"}) = t1 |
250 fun mk_conj (t1, @{term "True"}) = t1 |
248 | mk_conj (@{term "True"}, t2) = t2 |
251 | mk_conj (@{term "True"}, t2) = t2 |
249 | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) |
252 | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) |
250 |
253 |
251 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} |
254 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} |
|
255 fun fold_conj_balanced ts = Balanced_Tree.make HOLogic.mk_conj ts |
252 |
256 |
253 |
257 |
254 (* functions for de-Bruijn open terms *) |
258 (* functions for de-Bruijn open terms *) |
255 |
259 |
256 fun mk_binop_env tys c (t, u) = |
260 fun mk_binop_env tys c (t, u) = |
474 fun transform_prem2 ctxt names thm = |
478 fun transform_prem2 ctxt names thm = |
475 map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm |
479 map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm |
476 |
480 |
477 |
481 |
478 (* transformes a theorem into one of the object logic *) |
482 (* transformes a theorem into one of the object logic *) |
479 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars |
483 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars; |
|
484 fun atomize_rule i thm = |
|
485 Conv.fconv_rule (Conv.concl_conv i Object_Logic.atomize) thm |
|
486 fun atomize_concl thm = atomize_rule (length (prems_of thm)) thm |
|
487 |
|
488 |
480 |
489 |
481 (* applies a tactic to a formula composed of conjunctions *) |
490 (* applies a tactic to a formula composed of conjunctions *) |
482 fun conj_tac tac i = |
491 fun conj_tac tac i = |
483 let |
492 let |
484 fun select (trm, i) = |
493 fun select (trm, i) = |