|
(* Title: HOL/Library/Rewrite.thy
Author: Christoph Traut, Lars Noschinski, TU Muenchen
Proof method "rewrite" with support for subterm-selection based on patterns.
*)
theory Rewrite
imports Main
begin
consts rewrite_HOLE :: "'a::{}" ("\")
lemma eta_expand:
fixes f :: "'a::{} \ 'b::{}"
shows "f \ \x. f x" .
lemma rewr_imp:
assumes "PROP A \ PROP B"
shows "(PROP A \ PROP C) \ (PROP B \ PROP C)"
apply (rule Pure.equal_intr_rule)
apply (drule equal_elim_rule2[OF assms]; assumption)
apply (drule equal_elim_rule1[OF assms]; assumption)
done
lemma imp_cong_eq:
"(PROP A \ (PROP B \ PROP C) \ (PROP B' \ PROP C')) \
((PROP B \<Longrightarrow> PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP A \<Longrightarrow> PROP C'))"
apply (intro Pure.equal_intr_rule)
apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
done
ML_file \<open>cconv.ML\<close>
ML_file \<open>rewrite.ML\<close>
end
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
