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

Note that the cases theorem does not capture “leastness”. A coinductive definition of the same relation would give you the same cases theorem. The cases theorem is just giving you the fix-point property. One easy example for thinking about these sorts of things is lists. Imagine you have:

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

If you want to see the stored rule induction principles, you might use: ThmSetData.all_data "rule_induction"; Or IndDefLib.thy_rule_inductions "list"; where you get to provide the theory name. Michael From: Thomas Tuerk Date: Thursday, 19 January 2017 at 03:22

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] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

Hi Makarius, Yeah, this is why I never succeeded in building PolyML on Windows in Cygwin or MinGW. When the building process stopped at some assembly code files, I thought they're for Microsoft compilers only. I don't believe PolyML depends on any deep GCC feature which is only available in old

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

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

On 17/01/17 15:24, Chun Tian (binghe) wrote: > Sorry, I re-checked my Isabelle environment and found that the PolyML in > Isabelle is actually built by GCC (mingw versions), so my statement > about "PolyML cannot be built in ..." was completely wrong. The rest > ideas should still hold. It 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