author  wenzelm 
Sat, 10 Oct 2015 16:40:43 +0200  
changeset 61383  6762c8445138 
parent 60054  ef4878146485 
child 69605  a96320074298 
permissions  rwrr 
59975  1 
(* Title: HOL/Library/Rewrite.thy 
2 
Author: Christoph Traut, Lars Noschinski, TU Muenchen 

3 

4 
Proof method "rewrite" with support for subtermselection based on patterns. 

5 
*) 

6 

59739  7 
theory Rewrite 
8 
imports Main 

9 
begin 

10 

61383  11 
consts rewrite_HOLE :: "'a::{}" ("\<hole>") 
59739  12 

13 
lemma eta_expand: 

59975  14 
fixes f :: "'a::{} \<Rightarrow> 'b::{}" 
15 
shows "f \<equiv> \<lambda>x. f x" . 

59739  16 

60054
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60047
diff
changeset

17 
lemma rewr_imp: 
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60047
diff
changeset

18 
assumes "PROP A \<equiv> PROP B" 
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60047
diff
changeset

19 
shows "(PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B \<Longrightarrow> PROP C)" 
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60047
diff
changeset

20 
apply (rule Pure.equal_intr_rule) 
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60047
diff
changeset

21 
apply (drule equal_elim_rule2[OF assms]; assumption) 
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60047
diff
changeset

22 
apply (drule equal_elim_rule1[OF assms]; assumption) 
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60047
diff
changeset

23 
done 
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60047
diff
changeset

24 

ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60047
diff
changeset

25 
lemma imp_cong_eq: 
61383  26 
"(PROP A \<Longrightarrow> (PROP B \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP C')) \<equiv> 
27 
((PROP B \<Longrightarrow> PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP A \<Longrightarrow> PROP C'))" 

60054
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60047
diff
changeset

28 
apply (intro Pure.equal_intr_rule) 
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60047
diff
changeset

29 
apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+ 
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60047
diff
changeset

30 
apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+ 
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60047
diff
changeset

31 
done 
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60047
diff
changeset

32 

59739  33 
ML_file "cconv.ML" 
34 
ML_file "rewrite.ML" 

35 

36 
end 