Re: [Hol-info] How to prove this theorem about relations?

t. l = h::t /\ isAList t > > __ __ > > (where l ranges over a type large enough to encompass lists and lazy > lists both, and the isAList predicate is identifying the appropriate > subsets of that type). > > __ __ > > If the cases

Re: [Hol-info] How to prove this theorem about relations?

asy example for thinking about these sorts of things is lists. >> Imagine you have: >> >> >> >> isAList l ó l = [] \/ ?h t. l = h::t /\ isAList t >> >> >> >> (where l ranges over a type large enough to encompass lists and lazy >> li

Re: [Hol-info] How to prove this theorem about relations?

2017 at 21:58 To: hol-info <hol-info@lists.sourceforge.net> Subject: [Hol-info] How to prove this theorem about relations? Hi, Sorry for disturbing again, but I met new difficulties when proving theorems about relations. Suppose I have the following simple recursive datatype and a &

Re: [Hol-info] How to prove this theorem about relations?

, 19 January 2017 at 03:22 To: "Chun Tian (binghe)" <binghe.l...@gmail.com> Cc: hol-info <hol-info@lists.sourceforge.net> Subject: Re: [Hol-info] How to prove this theorem about relations? Hi Chun, TypeBase stores information about algebraic datatypes. So, you won'

Re: [Hol-info] How to prove this theorem about relations?

Hi Thomas, Thanks for pointing out the related source code! Looking at ML function Induct_on() and induct_on_type(), it's quite clear what they do exactly. From the way Induct_on() generating tactics (MAP_FIRST HO_MATCH_MP_TAC indth ORELSE induct_on_type st ty), I can see that, if the

Re: [Hol-info] How to prove this theorem about relations?

Hi Chun, TypeBase stores information about algebraic datatypes. So, you won't find information for your inductive relations or recursive functions in there. Use TypeBasePure.listItems (TypeBase.theTypeBase()) to get an idea what types are currently in the TypeBase. I found the reference to

Re: [Hol-info] How to prove this theorem about relations?

Hi, glad I could be of help. I forgot to mention TypeBase. This is where such theorems about a type are collected. It is used by tools like the case or induct tactics. So, some other nice way of getting such theorems is TypeBase.fetch ``:'a form`` or specialized ones via TypeBase.distinct_of

Re: [Hol-info] How to prove this theorem about relations?

Hi Chun, you are on the right way with the cases theorem. Essentially you need to rewrite once with it. Then you end up with ∀A a.(atom a = A) ∨ (∃B C. (atom a = dot B C) ∧ subF A B) ⇒ (A = atom a) Now you need to use the fact that "atom _ = dot B C" does not hold. This distinctiveness is

[Hol-info] How to prove this theorem about relations?

Hi, Sorry for disturbing again, but I met new difficulties when proving theorems about relations. Suppose I have the following simple recursive datatype and a "sub formula" relation about it: val _ = Datatype `form = atom 'a | dot form form`; val (subF_rules, subF_ind, subF_cases) = Hol_reln