Hello Petros, thank you for your fast answer.
Your tactic worked perfectly. Regards, Heiko On 07/04/2016 03:20 PM, Petros Papapanagiotou wrote: > Hello Heiko, > > Try: > e (REWRITE_TAC[distinctness "test"]);; > > HOL Light automatically produces distinctness theorems for inductive > types, accessed through the "distinctness" function. > > > Regards, > Petros > > > On 04/07/2016 13:36, Heiko Becker wrote: >> On 07/04/2016 02:34 PM, Heiko Becker wrote: >> >>> Hello everyone, >>> >>> >>> suppose I have an inductive type as follows: >>> >>> let test_IND, test_CASES = >>> define_type >>> "test = Foo num >>> |Bar int ";; >>> >>> Can someone explain to me how I can derive a contradiction given >>> equality as in the goal below? >>> >>> g `Foo 1 = Bar (&1) ==> F`;; >>> >>> Thanks in advance. >>> >>> Best regards, >>> >>> >>> Heiko >>> >> Forgot to add: >> I want to do the proof in HOL-Light. Sorry the double post. >> >> Best regards. >> >> ------------------------------------------------------------------------------ >> >> >> Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San >> Francisco, CA to explore cutting-edge tech and listen to tech luminaries >> present their vision of the future. This family event has something for >> everyone, including kids. Get more information and register today. >> http://sdm.link/attshape >> _______________________________________________ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info >> > ------------------------------------------------------------------------------ Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San Francisco, CA to explore cutting-edge tech and listen to tech luminaries present their vision of the future. This family event has something for everyone, including kids. Get more information and register today. http://sdm.link/attshape _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
