author  noschinl 
Mon, 13 Apr 2015 20:11:12 +0200  
changeset 60054  ef4878146485 
parent 60047  58e5b16cbd94 
child 61383  6762c8445138 
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 

59975  11 
consts rewrite_HOLE :: "'a::{}" 
59739  12 
notation rewrite_HOLE ("HOLE") 
60047  13 
notation rewrite_HOLE ("\<hole>") 
59739  14 

15 
lemma eta_expand: 

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

59739  18 

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

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

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

21 
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

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

23 
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

24 
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

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

26 

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

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

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

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

30 
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

31 
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

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

33 

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

36 

37 
end 