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 > -- Petros Papapanagiotou, Ph.D. CISA, School of Informatics The University of Edinburgh Email: p...@ed.ac.uk --- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ 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
