equal
deleted
inserted
replaced
383 @{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ] |
383 @{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ] |
384 |
384 |
385 val apply_rules = [ |
385 val apply_rules = [ |
386 @{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast}, |
386 @{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast}, |
387 @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n" |
387 @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n" |
388 by (atomize(full)) fastsimp} ] |
388 by (atomize(full)) fastforce} ] |
389 |
389 |
390 val inst_rule = Z3_Proof_Tools.match_instantiate Thm.dest_arg |
390 val inst_rule = Z3_Proof_Tools.match_instantiate Thm.dest_arg |
391 |
391 |
392 fun apply_rule ct = |
392 fun apply_rule ct = |
393 (case get_first (try (inst_rule ct)) intro_rules of |
393 (case get_first (try (inst_rule ct)) intro_rules of |