equal
deleted
inserted
replaced
54 |
54 |
55 lemma lift_definedE: "\<lbrakk>x \<noteq> \<bottom>; \<And>a. x = Def a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
55 lemma lift_definedE: "\<lbrakk>x \<noteq> \<bottom>; \<And>a. x = Def a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
56 by (cases x) simp_all |
56 by (cases x) simp_all |
57 |
57 |
58 text {* |
58 text {* |
59 For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text |
59 For @{term "x ~= UU"} in assumptions @{text defined} replaces @{text |
60 x} by @{text "Def a"} in conclusion. *} |
60 x} by @{text "Def a"} in conclusion. *} |
61 |
61 |
62 ML {* |
62 method_setup defined = {* |
63 local val lift_definedE = thm "lift_definedE" |
63 Scan.succeed (fn ctxt => SIMPLE_METHOD' |
64 in val def_tac = SIMPSET' (fn ss => |
64 (etac @{thm lift_definedE} THEN' asm_simp_tac (local_simpset_of ctxt))) |
65 etac lift_definedE THEN' asm_simp_tac ss) |
65 *} "" |
66 end; |
|
67 *} |
|
68 |
66 |
69 lemma DefE: "Def x = \<bottom> \<Longrightarrow> R" |
67 lemma DefE: "Def x = \<bottom> \<Longrightarrow> R" |
70 by simp |
68 by simp |
71 |
69 |
72 lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R" |
70 lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R" |