equal
deleted
inserted
replaced
79 done |
79 done |
80 |
80 |
81 text {* tactic for tr-thms with case split *} |
81 text {* tactic for tr-thms with case split *} |
82 |
82 |
83 lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def |
83 lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def |
84 (* |
84 |
85 fun prover t = prove_goal thy t |
85 |
86 (fn prems => |
|
87 [ |
|
88 (res_inst_tac [("p","y")] trE 1), |
|
89 (REPEAT(asm_simp_tac (simpset() addsimps |
|
90 [o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1)) |
|
91 ]) |
|
92 *) |
|
93 text {* distinctness for type @{typ tr} *} |
86 text {* distinctness for type @{typ tr} *} |
94 |
87 |
95 lemma dist_less_tr [simp]: |
88 lemma dist_less_tr [simp]: |
96 "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT" |
89 "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT" |
97 by (simp_all add: tr_defs) |
90 by (simp_all add: tr_defs) |