On Wed, Jan 16, 2013 at 1:31 PM, Bill Richter <[email protected] > wrote:
> Thanks, Michael! As you see, I haven't read the HOL4 Description manual > carefully yet. I should, because I think it's quite possible you might > have some good explanations not in the HOL Light dox. Since HOL4 ports HOL > Light's finite cartesian products, maybe you can explain it! As you write > on p 84 of Description: > > dimindex(’b) is the cardinality of univ(:’b) > > That's easier to read that the HOL Light cart.ml code > > let dimindex = new_definition > `dimindex(s:A->bool) = if FINITE(:A) then CARD(:A) else 1`;; > > But it doesn't explain to me how to prove these theorems so necessary for > the vector types real^2 and real^3: > > # DIMINDEX_2;; > val it : thm = |- dimindex (:2) = 2 > # DIMINDEX_3;; > val it : thm = |- dimindex (:3) = 3 > > And as Rob says that eventually we should modify HOL to allow type > quantification, I missed where Rob said this. HOL-Omega has type quantification, and is backwards compatible with HOL4. http://www.trustworthytools.com/id17.html. I'm not sure if we mean the same thing by "type quantification" though. > maybe we should ask if we shouldn't allow terms to show up it types, so we > could define real^3 where 3 has type num, as it normally does, rather than > being a type that somehow satisfies dimindex (:3) = 3. > Allowing terms to show up in types probably means moving to a dependently typed logic. There are many theorem provers in that space: Coq, Agda, Matita, Idris, Epigram. > > -- > Best, > Bill > > > ------------------------------------------------------------------------------ > Master Java SE, Java EE, Eclipse, Spring, Hibernate, JavaScript, jQuery > and much more. Keep your Java skills current with LearnJavaNow - > 200+ hours of step-by-step video tutorials by Java experts. > SALE $49.99 this month only -- learn more at: > http://p.sf.net/sfu/learnmore_122612 > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info >
------------------------------------------------------------------------------ Master Java SE, Java EE, Eclipse, Spring, Hibernate, JavaScript, jQuery and much more. Keep your Java skills current with LearnJavaNow - 200+ hours of step-by-step video tutorials by Java experts. SALE $49.99 this month only -- learn more at: http://p.sf.net/sfu/learnmore_122612
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
