# HG changeset patch # User oheimb # Date 902926846 -7200 # Node ID 4ce5539aa969faa2d8d3e64c965254c1e1f52c03 # Parent 92ea5ff34c793d0696958083b9fc448b8bad4d4a added ospec AddIffs [elem_o2s] diff -r 92ea5ff34c79 -r 4ce5539aa969 src/HOL/Option.ML --- a/src/HOL/Option.ML Wed Aug 12 14:56:56 1998 +0200 +++ b/src/HOL/Option.ML Wed Aug 12 15:00:46 1998 +0200 @@ -19,10 +19,7 @@ dtac (not_None_eq RS iffD1) 1, etac exE 1, eresolve_tac prems 1]); -fun optionE_tac s i = EVERY [ - res_inst_tac [("opt",s)] optionE i, - hyp_subst_tac (i+1), - hyp_subst_tac i]; +fun optionE_tac s = res_inst_tac [("opt",s)] optionE THEN_ALL_NEW hyp_subst_tac; qed_goal "option_caseE" thy "[|case x of None => P | Some y => Q y; \ \ [|x = None; P |] ==> R; \ @@ -60,11 +57,15 @@ section "o2s"; +qed_goal "ospec" thy + "!!x. [| !x:o2s A. P x; A = Some x |] ==> P x" (K [Auto_tac]); +claset_ref() := claset() addSaltern ("ospec", dtac ospec THEN' atac); + val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)" (K [optionE_tac "xo" 1, Auto_tac]); -AddSDs [elem_o2s RS iffD1]; -Addsimps [elem_o2s]; +AddIffs [elem_o2s]; val o2s_empty_eq = prove_goal thy "(o2s xo = {}) = (xo = None)" (K [optionE_tac "xo" 1, Auto_tac]); Addsimps [o2s_empty_eq]; +