Re: [Hol-info] How were type variables added to higher order logic?

[Jeremy Dawson]

I'm not sure if this is of interest to readers of this thread, but here 
goes:

Elements of Functional Programming, by Chris Reade (a student level 
textbook) has this to say, at pp 396-7:

(talking about type inference)

(quote)
Note that in these inferences, we used T, T-1, ..., as meta type 
variables standing for unknown types and these unknown types may involve 
ordinary type variables such as \alpha, \beta, ... and so on.  There is 
a conceptual distinction between meta variables which we use (outside 
the system) to stand for any type and type variables which are part of 
the type system and also stand for any type.  However we can 
conveniently borrow ordinary type variables for use as meta 
type-variables to simplify the development of an algorithm.
(end quote)

Ie, the last sentence seems to say that although it is a significant 
conceptual distinction, it doesn't really matter.

A related point:  Isabelle (though not HOL) has explicitly variable 
variables (for both types and terms), ?a and ?'a, as well as fixed 
variables, a and 'a. The ? variables can be substituted for, the others 
can't.  But when a theorem is proved, the non-? variables can be changed 
to ? variables.

I've never really thought about it, but if you'd asked me I would have 
said that I suppose the non-? variables are part of the object language 
and the ? variables are a sort of meta level device.  Which may again 
suggest that a conceptual distinction is not practically significant.

Another related question: Peter has raised the issue of whether a type 
variable is a meta level or an object level notion.
Does it make sense equally to consider whether a non-variable type 
assertion, say x : int, is an object-level assertion, or a meta-level 
statement about an object level term x? I would find it more natural to 
say the former.  But does the answer to that question matter?

Jeremy Dawson



-
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK  win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100url=/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] prove a goal in HOL4

[Jeremy Dawson]

liy_...@encs.concordia.ca wrote:
 I have to prove a goal in HOL4 as following:

 g `!a b c. (indep bern a c) /\ (indep bern b c) ==
(a IN events bern) /\ (b IN events bern) /\ (c IN events bern) /\
(prob bern (a INTER b INTER c) = prob bern (a INTER b) * prob bern c)`;

 Here, a and c are independant, also b and c are independant. However,  
 a depends b.

 Could anybody give me some hints? I really appreciate!

 Regards,
 Liya
   
I can't guess what bern and events mean, but if prob and indep have a 
usual meaning, then it's not true.

eg let 3 coins, X, Y, Z be tossed independently.

Let event A be coins X and Y fall the same way

Let event B be coins X and Z fall the same way

Let event C be coins Z and Y fall the same way

Then each two of the three events A,B,C are independent.  But A  B is 
not independent of C (which is what, I understand, the last line of your 
conclusion says)

Regards,

Jeremy


--
Download Intel#174; Parallel Studio Eval
Try the new software tools for yourself. Speed compiling, find bugs
proactively, and fine-tune applications for parallel performance.
See why Intel Parallel Studio got high marks during beta.
http://p.sf.net/sfu/intel-sw-dev
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] useful HOL statistics to show the amount of proof work?

[Jeremy Dawson]

Ramana Kumar wrote:
 On Mon, May 21, 2012 at 3:29 AM, Lu Zhao luz...@cs.utah.edu wrote:
   
 This is particularly dangerous when I have proof automation scripts that
 try different rewriting rules. The number reported is not representative
 on the complexity of the problem, but the number of inference steps
 conducted by HOL, which is not necessarily related to a correct proof
 construction that actually verifies a theorem.

 Since HOL is not designed for automatic reasoning,
 

 I can't let this one by. HOL is designed to allow one to automate as
 much reasoning as possible with tactics. Whether or not good enough
 automation tactics have been written is another story, but I think
   
An important part of this story is the fact that the tools are there for 
you to write your own according to the features of the problem at hand, 
so long as you are comfortable with not-quite-trivial Standard ML 
programming.

Jeremy

 there are quite good ones (including integrations with other, stronger
 purely automatic tools).

   
 so reporting the
 number of inference steps can be misleading in measuring the
 implementation complexity of solving problems, especially when using
 proof automation scripts with lots of rewriting rules.
 

 Now, to answer your question, as Michael suggested you may find using
 the Opentheory proof-logging kernel useful.
 It builds a proof object for every theorem, so once your final theorem
 is proved you can simply count the number of inference steps in its
 proof.
 This will not count any of the inference steps built along the
 dead-end attempts.
 (Indeed if you export the theorem into an Opentheory article, the
 opentheory tool (not include with HOL) will perform easy
 simplifications on the proof and count the primitive inferences by
 type for you.)

   


--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Proof assistants for way more people

[Jeremy Dawson]

Mark wrote:
 on 9/7/12 5:48 PM, Cris Perdue c...@perdues.com wrote:

   
 

 What I was talking about though is ease of use of software products,
 and a proof assistant is definitely a software product. To get many
 people to use a software product, especially one that is not just a
 minor variation on one they know, it has to be amazingly simple to
 use.  This of course will be a huge challenge for this kind of technology.
 

 Actually I don't think it's particularly difficult to do.  It's just that
 no-one's done it yet!

   
Actually I think it is probably extraordinarily difficult.  I recall a 
comment made about certain sorts of user interfaces (actually it was 
about GUIs but I think equally applicable to a certain style or 
philosophy of designing user interfaces for complicated software), that 
they make easy tasks easy and difficult tasks impossible.

Theorem proving is a difficult task - or, more to the point - when you 
break it down into its myriad of subtasks, they are all different.  The 
tool that does them all will not be amazingly simple to use

Jeremy


--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] merging duplicate subgoals

[Jeremy Dawson]

Yes, indeed.  When the subgoals are identical (including the 
assumptions), Tactical.USE_SG_THEN ACCEPT_TAC should do it.

Otherwise, the doc for USE_SG_THEN gives a couple of examples how it can 
be used.

This requires you to identify which subgoal is to be used in proving 
which other.  They need not be identical.  But I guess something could 
be written to trawl through the list of subgoals looking for pairs where 
one proves the other without effort (ie, same conclusion, same or subset 
assumptions)

Cheers,

Jeremy


On 01/02/15 16:46, Ramana Kumar wrote:
 Is it possible to merge duplicate (or alpha-convertible) subgoals during
 a proof, to reduce the total number of subgoals? Maybe using list tactics?


 --
 Dive into the World of Parallel Programming. The Go Parallel Website,
 sponsored by Intel and developed in partnership with Slashdot Media, is your
 hub for all things parallel software development, from weekly thought
 leadership blogs to news, videos, case studies, tutorials and more. Take a
 look and join the conversation now. http://goparallel.sourceforge.net/



 ___
 hol-info mailing list
 hol-info@lists.sourceforge.net
 https://lists.sourceforge.net/lists/listinfo/hol-info


--
Dive into the World of Parallel Programming. The Go Parallel Website,
sponsored by Intel and developed in partnership with Slashdot Media, is your
hub for all things parallel software development, from weekly thought
leadership blogs to news, videos, case studies, tutorials and more. Take a
look and join the conversation now. http://goparallel.sourceforge.net/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] irule vs MP_CANON

[Jeremy Dawson]

Hi Ramana,

Well, they are both ways of matching the final consequent of a1 ==> a2 
==> a3 ==> ... ==> c with the goal.

Until I saw your question I hadn't been aware of the existence of 
MP_CANON.

Possibly the biggest difference is that irule will produce multiple new 
subgoals (eg, in the above case, one for each ai - except as noted below).

There's a bit of reimplementation of irule recently and continuing, 
involving the behaviour when there are variables some of the ai but not 
in c, (like MATCH_MP_TAC, it introduces existentials, which also may 
require collecting together some of the ai) which may affect ordering 
and exact form of the new subgoals.

Cheers,

Jeremy



On 16/11/15 22:28, Ramana Kumar wrote:
> What is the difference between irule and (match_mp_tac o MP_CANON)?
>
> I'm more interested in differences in the intended design than in minor
> details in the implementation. Which is preferred style? Which should
> get more developer time?
>
> Maybe they're actually rather different, but as far as I saw, from a
> brief look, they are intended to do the same thing.
>
>
> --
> Presto, an open source distributed SQL query engine for big data, initially
> developed by Facebook, enables you to easily query your data on Hadoop in a
> more interactive manner. Teradata is also now providing full enterprise
> support for Presto. Download a free open source copy now.
> http://pubads.g.doubleclick.net/gampad/clk?id=250295911=/4140
>
>
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>

--
Presto, an open source distributed SQL query engine for big data, initially
developed by Facebook, enables you to easily query your data on Hadoop in a 
more interactive manner. Teradata is also now providing full enterprise
support for Presto. Download a free open source copy now.
http://pubads.g.doubleclick.net/gampad/clk?id=250295911=/4140
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] map_option

[Jeremy Dawson]

Hi Ramana,

It's rather a similar situation to what I wrote about in

http://users.cecs.anu.edu.au/~jeremy/pubs/fgc/fgs/fgs.pdf

and also

http://users.cecs.anu.edu.au/~jeremy/pubs/fgc/cats/fgc.ps

except that I seem to have used sets instead of lists (which I don't 
think should make a difference), and I seem to not have noticed that I 
was reinventing the standard option type.

I used these types to represent a non-deterministic computation with the 
possibility of non-termination.

For the 'a set option result type, a computation is regarded as (let's 
say) "unreliable" and so non-terminating, when there is only the 
possibility of non-termination.
For the 'a option set result type, you are interested in the possible 
(terminating) results even when non-termination is also possible.

Both types, ie, 'a option set, and 'a set option, are compound monads, 
and your function is a monad morphism, which is also used in a certain 
construction which can be used to prove that the latter is indeed a 
compound monad.

Cheers,

Jeremy

On 20/09/15 18:08, Ramana Kumar wrote:
> Hi all,
>
> I think this must be some neat combination of category theory things.
> Does anyone know which? Or if it's already defined somewhere?
>
> val map_option_def = Define`
>(map_option [] = SOME []) ∧
>(map_option (NONE::_) = NONE) ∧
>(map_option (SOME x::ls) =
> case map_option ls of
> | SOME ls => SOME(x::ls)
> | NONE => NONE)`;
>
> Cheers,
> Ramana
>
> --
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>

--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] About the use of symbol | in HOL4

[Jeremy Dawson]

Hi Ada,

In the first case you're trying to define a function in the HOL logic.

In the second case you're defining a SML function

Jeremy


On 29/11/15 22:15, Ada wrote:
> Hey guys,
>
> I am learning to use HOL. I find an interesting thing about the use of
> symbol | in HOL4.
> I defined an function named fir, as follows:
> - val fir_def = Define`
>  (fir []  n = [] ) |
>  (fir p 0 = [])`;
> But failed , it responsed that:
> Don't expect to find a | in this position after a 
> at line 5, character 22 and in compiler-generated text.
> Exception raised at Absyn.Absyn:
> in compiler-generated text:
> Don't expect to find a | in this position after a 
> at line 5, character 22 and in compiler-generated text.
> ! Uncaught exception:
> ! HOL_ERR
> Then, I tried again , as follows:
> - fun fir ([] , n) = []
> | fir (p ,0 )= [] ;
> It succeeded.
> Now, I have two questions:
> 1、Why  can't  the symbol | be used in "Define"?
> 2、What are the differences between "Define" and "fun"?
> Thanks! --Wish.
>
>
> --
>
>
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>

--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] some questions about the use of HD and TL in listTheory

[Jeremy Dawson]

Hi Ada,

when you enter

  first ([0,1,0,1,0],3);

this refers to the SML function first whose type is given by

first ;
val it = fn: ('a -> bool) -> 'a list -> 'a

What you want is the HOL term

``first ([0,1,0,1,0],3)``
which will also give you a type error, since your definition of first 
requires it to be used as follows

``first [(0,1,0,1,0)] 3``

To help you see what's happening,

show_types := true ;
val it = (): unit
 > ``first`` ;
<>
val it =
``(first :α list -> num -> α list)``:

Suggest you get familiar with types in SML before spending too much time 
on HOL

Cheers,

Jeremy

On 30/11/15 18:42, Ada wrote:
> Hey guys,
>
> I am learning to use HOL4. I defined a function named "first" in HOL4.
> This function can get the first n elements in a list. As follows:
> - val first_def = Define`(first [] n = [] )
> /\ (first (p::pl) 0 = [] )
> /\ (first (p::pl) n = HD (p::pl) :: first (TL
> (p::pl)) (n-1)) `;
> <>
> Equations stored under "first_def".
> Induction stored under "first_ind".
>> val first_def =
>  |- (!n. first [] n = []) /\ (!pl p. first (p::pl) 0 = []) /\
> !v4 pl p.
>   first (p::pl) (SUC v4) =
>   HD (p::pl)::first (TL (p::pl)) (SUC v4 - 1) : thm
> In which, I saw HD and TL had been defined in listTheory. HD gets the
> first element in a list, TL gets the last.
> But , when I tried to use "first", failed. As followes:
> - first ([0,1,0,1,0],3);
> ! Toplevel input:
> ! first ([0,1,0,1,0],3);
> ! ^
> ! Type clash: expression of type
> !   ('a -> bool) -> 'a list -> 'a
> ! cannot have type
> !   'b * 'c -> 'a list -> 'a
>
> - first  [0,1,0,1,0] 3;
> ! Toplevel input:
> ! first  [0,1,0,1,0] 3;
> ! ^^
> ! Type clash: expression of type
> !   'a list
> ! cannot have type
> !   'b -> bool
> I was wondering why it failed. Could anyone find the reasion?
> Thanks! --Wish.
>
>
> --
> Go from Idea to Many App Stores Faster with Intel(R) XDK
> Give your users amazing mobile app experiences with Intel(R) XDK.
> Use one codebase in this all-in-one HTML5 development environment.
> Design, debug & build mobile apps & 2D/3D high-impact games for multiple OSs.
> http://pubads.g.doubleclick.net/gampad/clk?id=254741551=/4140
>
>
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>

--
Go from Idea to Many App Stores Faster with Intel(R) XDK
Give your users amazing mobile app experiences with Intel(R) XDK.
Use one codebase in this all-in-one HTML5 development environment.
Design, debug & build mobile apps & 2D/3D high-impact games for multiple OSs.
http://pubads.g.doubleclick.net/gampad/clk?id=254741911=/4140
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] [SPAM] some questions about the proving process in HOL4

[Jeremy Dawson]

Hi Ada,

You need to search for suitable theorems.

In this case

 > apropos ``TAKE 0`` ;
<>
val it =
[(("list", "TAKE_0"), (|- TAKE 0 l = [], Thm)),

so from the initial goal

e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute);

e (ASM_REWRITE_TAC [listTheory.TAKE_0]) ;

This should work but doesn't - when all else fails, look at the types:
show_types := true ;
and you see that they are different.
Do it this way instead.

e (ASM_REWRITE_TAC [listTheory.TAKE_0, listTheory.LENGTH_EQ_NUM_compute]) ;

then you're almost there.

If you didn't have the theorem TAKE_0 you would have to use the 
definition of TAKE, namely listTheory.TAKE_def, and use
Cases_on `p`

Cheers,

Jeremy



On 15/12/15 14:27, Ada wrote:
> Hey guys,
>
> I am learning to use HOL4. There is  a function named "TAKE" in HOL4,
> which can get the first n elements in a list.
> When I was proving one property of TAKE, I find an interesting thing. As
> follows:
> - g`!p:bool list n:num. (LENGTH p = 0) ==> (TAKE 0 p = p) `;
> - e (REPEAT STRIP_TAC);
> OK..
> 1 subgoal:
>> val it =
>  TAKE 0 p = p
>  
>LENGTH p = 0
>   : proof
> - e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute);
> OK..
> 1 subgoal:
>  > val it =
>  TAKE 0 p = p
>  
>0.  LENGTH p = 0
>1.  !l. (LENGTH l = 0) <=> (l = [])
>2.  !l n.
>  (LENGTH l = NUMERAL (BIT1 n)) <=>
>  ?h l'. (LENGTH l' = NUMERAL (BIT1 n) - 1) /\ (l = h::l')
>3.  !l n.
>  (LENGTH l = NUMERAL (BIT2 n)) <=>
>  ?h l'. (LENGTH l' = NUMERAL (BIT1 n)) /\ (l = h::l')
>4.  !l n1 n2.
>  (LENGTH l = n1 + n2) <=>
>  ?l1 l2. (LENGTH l1 = n1) /\ (LENGTH l2 = n2) /\ (l = l1 ++ l2)
>   : proof
> The conditions of " LENGTH p = 0" and "!l. (LENGTH l = 0) <=> (l = [])"
> have already been in assumption list, so I think it is natural to get
> "p=[]", then "TAKE 0 [] = []". But I tried many times , I can't prove
> that. Could anyone prove it?
> Thanks! --Wish.
>
>
> --
>
>
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>

--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to transform list format from "(cx l q p)" to "l"

[Jeremy Dawson]

It might be easier to avoid using TAKE_DROP_LENGTH
but instead try to simplify your subgoal using
LENGTH_TAKE_EQ and LENGTH_DROP

Then I think you'll have to instantiate your subgoal 0  once with p,q 
and once with q,p

Cheers,

Jeremy

On 28/02/16 22:48, Ada wrote:
> Hey,guys
>
> I am learning to use HOL4. Here are some questions about my proving:
>
> g`!p q:bool list l:num list. (LENGTH p = LENGTH q) ==> (LENGTH (cx l p
> q) = LENGTH p) `;
>
> e (Induct_on `l`);
>
> e (RW_TAC list_ss [cx_defn]);
>
> - e (RW_TAC list_ss [cx_defn]);
>
> OK..
>
> 1 subgoal:
>
>> val it =
>
> LENGTH (DROP h (cx l q p)) +
>
> LENGTH (TAKE h (cx l p q)) =
>
> LENGTH q
>
> 
>
> 0.!p q.
>
> (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p)
>
> 1.LENGTH p = LENGTH q
>
> : proof
>
> The definition of “cx” is following:
>
> |- (!q p. cx [] p q = p) /\
>
> !v5 v4 q p.
>
> cx (v4::v5) p q =
>
> TAKE (HD (v4::v5)) (cx (TL (v4::v5)) p q) ++
>
> DROP (HD (v4::v5)) (cx (TL (v4::v5)) q p) : thm
>
> Where,“TAKE” is in listtheory in HOL4. It means that get firs n
> elements,“DROP” is in listtheory in HOL4. It means that get after n
> elements,
>
> I have proved that “!p q:bool list n:num. (LENGTH p = LENGTH q) ==>
> (LENGTH (DROP n q) + LENGTH (TAKE n p) = LENGTH q)”, named
> “TAKE_DROP_LENGTH”.
>
> But I can’t prove the initial goal g`!p q:bool list l:num list. (LENGTH
> p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p) `. I think that, the
> problem is that in the goal the form is “DROP h (cx l q p)”, but the
> actual form is “DROP h l”, where the format of “(cx l q p)” is not equal
> to “l”. But I can’t find a good transform between them.
>
> Could anyone give me some advices?
>
> Thank you!
>
>
>
> --
> Site24x7 APM Insight: Get Deep Visibility into Application Performance
> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> Monitor end-to-end web transactions and take corrective actions now
> Troubleshoot faster and improve end-user experience. Signup Now!
> http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140
>
>
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>

--
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

[Jeremy Dawson]

Hi Chun,

I don't think your example captures the distinction, since, as you 
prove, AList and BList are the same.

you're right about

 > 1. [] is List
 > and
 > 2. If l = h::t and t is List, then l is List.

In fact the only subset satisfying these (which is therefore both the 
least and the greatest) is the set of all lists.

Think instead about

Hol_reln `P (SUC n) ==> P n` ; (* no numbers *)
Hol_coreln `Q (SUC n) ==> Q n` ; (* all numbers *)

Cheers,

Jeremy

On 20/01/17 22:07, Chun Tian (binghe) wrote:
> Hi Michael,
>
> It took me some time to think about your words and learn co-induction.
> I'm no expert, but I don't agree with the opinion that "leastness is
> captured by the induction principle". Here is my argument:
>
> 1. Your "AList" definition must come from the following Hol_reln definition:
>
> val (AList_rules, AList_ind, AList_cases) = Hol_reln
>`(!l. (l = []) ==> isAList l) /\
> (!l h t. (l = h::t) /\ isAList t ==> isAList l)`;
>
> because the generated AList_cases is exactly the same as the one you gave:
>
> val AList_cases =
>|- ∀a0. isAList a0 ⇔ (a0 = []) ∨ ∃h t. (a0 = h::t) ∧ isAList t:
>thm
>
> val AList_ind =
>|- ∀isAList'.
>  (∀l. (l = []) ⇒ isAList' l) ∧
>  (∀l h t. (l = h::t) ∧ isAList' t ⇒ isAList' l) ⇒
>  ∀a0. isAList a0 ⇒ isAList' a0:
>thm
>
> val AList_rules =
>|- (∀l. (l = []) ⇒ isAList l) ∧
>∀l h t. (l = h::t) ∧ isAList t ⇒ isAList l:
>thm
>
> 2. You're right that, an co-induction of the same relation (or we should
> say, the same rules), would give us the same cases theorem, so let me
> define it with a different name, BList:
>
> val (BList_rules, BList_coind, BList_cases) = Hol_coreln
>`(!l. (l = []) ==> isBList l) /\
> (!l h t. (l = h::t) /\ isBList t ==> isBList l)`;
>
> it generated the following things:
>
> val BList_cases =
>|- ∀a0. isBList a0 ⇔ (a0 = []) ∨ ∃h t. (a0 = h::t) ∧ isBList t:
>thm
>
> val BList_coind =
>|- ∀isBList'.
>  (∀a0. isBList' a0 ⇒ (a0 = []) ∨ ∃h t. (a0 = h::t) ∧ isBList' t) ⇒
>  ∀a0. isBList' a0 ⇒ isBList a0:
>thm
>
> val BList_rules =
>|- (∀l. (l = []) ⇒ isBList l) ∧
>∀l h t. (l = h::t) ∧ isBList t ⇒ isBList l:
>thm
>
> 3. Now I can formally prove AList and BList is really the same thing
> (!l. isBList l = isAList l):
>
> val A2B = store_thm ("A2B", ``!l. isAList l ==> isBList l``,
> HO_MATCH_MP_TAC AList_ind
>  >> RW_TAC bool_ss [BList_rules]);
>
> val B2A = store_thm ("B2A", ``!l. isBList l ==> isAList l``,
> Induct
>  >| [ RW_TAC bool_ss [AList_rules, BList_rules],
>   STRIP_TAC
>>> ONCE_REWRITE_TAC [BList_cases]
>>> ONCE_REWRITE_TAC [AList_cases]
>>> REPEAT STRIP_TAC
>>| [ ASM_REWRITE_TAC [],
> SIMP_TAC list_ss []
>  >> `t = l` by PROVE_TAC [CONS_11]
>  >> PROVE_TAC [] ] ]);
>
> val AB_same = store_thm ("AB_same", ``!l. isBList l = isAList l``,
> PROVE_TAC [A2B, B2A]);
>
> now I want to say AList_ind and BList_coind are actually derived from
> the same rules for the same relation, they themselves didn't show any
> essential characteristics of the defined object (AList or BList here).
>
> P. S. This sounds like we could have another stronger Hol_reln (or
> Hol_coreln), which could return both induction and coinduction theorems
> at the same time for the same given rules.
>
> 4. So where are the words "least" and "maximal" coming from inductive
> and coinductive definitions? I think for the *same* relation we can
> always define it using either inductive or coinductive ways:
>
> (Inductive) A "List" is defined as the least subset of HOL type "list",
> such that:
>
> 1. [] is List
> and
> 2. If l = h::t and t is List, then l is List.
>
> The defined concept "List" is the interaction of all 1-ary relation
> satisfying above property. Consider the extreme case: List = (\l. T)
> also satisfy above property.
>
> (Co-inductive) A "List" is defined as the maximal (greatest) subset of
> HOL type "list", such that:
>
> If l is List, then
> 1. l is []
> or
> 2. ?h t. (l = h::t and t is List)
>
> The defined concept "List" is the union of all 1-ary relation satisfying
> above property. Consider the extreme case: List = (\l. F) also satisfy
> above property.
>
> Both Hol_reln and Hol_coreln only accept the inductive approach when
> defining any relation, that is, conjunction clauses having "==> R x y"
> as the conclusion part. Thus, we must *always* understand these rules as
> the *least* relation satisfying the rules.
>
> As for the purpose of induction theorems and co-induction theorems, I
> think they help us to prove different kinds of theorems on relations.
> Watching the position of "P l" in the conclusion part of these
> (co)induction theorems:
>
> val AList_ind =
>|- ∀P.
>  (∀l. l = [] ⇒ P l) ∧
>  (∀l. (∀h t. l = h::t ∧ P t) ⇒ P l) ⇒
>  ∀l. isAList l ⇒ P l:
>thm
>
> val BList_coind =
>|- ∀P.
>  (∀l. P l ⇒ l = [] ∨ (∃h t. l = h::t ∧ P t)) ⇒
>  ∀l. P l ⇒ isBList l:
>thm
>
> Suppose I 

Re: [Hol-info] Strange tactics bug when using match_mp_tac

[Jeremy Dawson]

I've been caught out with the same thing for MATCH_MP, I defined

(* MATCH_MP2 delays raising an exception until second argument is seen,
 *)
fun MATCH_MP2 th1 th2 = MATCH_MP th1 th2 ;

Jeremy

On 23/08/17 17:03, michael.norr...@data61.csiro.au wrote:

You are being caught by the fact that match_mp_tac thm can throw an exception 
before the tactic is ever applied to a goal.  In particular, if the theorem 
passed to match_mp_tac is not an implication an exception is thrown immediately.

You can fix this by handling that possible exception:

   fun simple_apply thm = ACCEPT_TAC thm ORELSE (match_mp_tac thm handle HOL_ERR _ 
=> ALL_TAC)

This arguably a poor design for match_mp_tac, and should perhaps be changed.

Michael



On 23/8/17, 16:55, "Heiko Becker"  wrote:

Hello everyone,

while working on some custom tactics, I noticed some strange behavior
related to combining tactics with match_mp_tac and the ORELSE tactical:

I am trying to write a tactic takes a theorem and first tries out
whether it is already a proof of the current goal with ACCEPT_TAC.
If this does not succeed, the tactic should try matching the theorem
with match_mp_tac.

Here is what I have come up with:

 fun simple_apply thm = (ACCEPT_TAC thm) ORELSE (match_mp_tac thm);

I have defined a test tactic, to see whether ACCEPT_TAC works as I
expect it to work:

 fun dumb_apply thm = (ACCEPT_TAC thm) ORELSE (FAIL_TAC "Unreachable");

Strangely the simple_apply tactic does not work in cases, where the
dumb_apply tactic works:

 val test_thm = Q.prove (
   ` !(n:num) (P:num -> bool).
P n ==>
P n`,
   rpt gen_tac
   DISCH_THEN ASSUME_TAC
   qpat_x_assum `P n` (fn thm => simple_apply thm) (* Fails with "No
parse of quotation leads to success" *)
   qpat_x_assum `P n` (fn thm => dumb_apply thm)  (* Proves the goal *)
   );


Can someone explain to me what I did wrong with the simple_apply tactic?


Thanks,


Heiko


--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info


--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info



--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

[Jeremy Dawson]

Hi Mario,

Slightly off-topic, I had experience with the type system of HOL-Omega 
(system F, if I recall the terminology right, not dependent types, so my 
experience may not be very relevant)


My dominant recollection is the difficulty of getting the system to do 
the right type inference, and getting terms to typecheck.  I was forever 
working out where I needed to put in type annotations.  Quite 
frustrating after my experience with regular HOL, and Isabelle.


It led me to conclude that the systems offering automatic inference of a 
principal type really occupy a "sweet spot", ie the best compromise 
between ease of use and expressive power.


Cheers,

Jeremy Dawson

On 06/10/17 03:46, Mario Castelán Castro wrote:

On 04/10/17 20:09, Ramana Kumar wrote:

Perhaps it would make more sense to ask people who are using rich type
systems what their motivations are :)
(On this list it's probably mostly people who are satisfied with simple
type theory.)


Yes, you are right. I wrote to this list because I am interesting in the
opinion of informed “outsiders”, not only “insiders”, so to speak.



--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot



___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info



--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

[Jeremy Dawson]

Hi Mario,

I don't mind the question, but the answer may not be much use because 
it's a comparison between the 2005 version of Isabelle which I use and 
HOL4.


In terms of the type systems they are identical.

Isabelle has schematic variables and type classes, both of which can 
make proof easier.  Otherwise, I don't find major differences.


Turning to modern day Isabelle - other factors may be:

  - the extent of unnecessarily incompatible changes between one 
version of Isabelle and the next (which is in fact why I'm still using 
the 2005 version, when I'm not using HOL)


  - the difficulty of using ML to program complex proof tactics - 
mandatory for a small proportion of my work (I've had various and highly 
conflicting reports of whether this is possible or reasonably easy in 
current Isabelle)


  - documentation, and willingness of developers to help with questions 
(and for me, location at GMT+10 means I can often get an immediate answer)


In HOL4 the source code is effectively available for users to look at 
(in Isabelle they can look at it, but it - or a lot of it - is highly 
obfuscated).


Cheers,

Jeremy

On 06/10/17 04:49, Mario Castelán Castro wrote:

On 05/10/17 11:53, Jeremy Dawson wrote:

Hi Mario,

Slightly off-topic, I had experience with the type system of HOL-Omega
(system F, if I recall the terminology right, not dependent types, so my
experience may not be very relevant)

My dominant recollection is the difficulty of getting the system to do
the right type inference, and getting terms to typecheck.  I was forever
working out where I needed to put in type annotations.  Quite
frustrating after my experience with regular HOL, and Isabelle.

It led me to conclude that the systems offering automatic inference of a
principal type really occupy a "sweet spot", ie the best compromise
between ease of use and expressive power.


Hello Jeremy. Thanks for your answer! If you do not mind an off-topic
question, what differences in terms of usability and ease of formalizing
pure mathematics did you experience find between Isabelle and HOL4 (or
HOL Light if that is the one you use)?.



--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot



___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info



--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

[Jeremy Dawson]

Hi Chun Tian,

I don't know much about rich(er) type systems, and I'm not well 
acquainted with Coq, but I'd say that what can be done in Isabelle or 
HOL should be possible also in richer type systems.


Regarding modelling of a proof, the context of what I said is 
describing, in HOL or Isabelle, a proof system for some logic, and 
describing proofs in that proof system.


This is to be contrasted with an approach which I believe may be 
available in constructive logic systems, which is to do a proof in (say) 
Coq, then from that proof, to obtain a function which implements that 
proof, so in a sense you are getting an object representing the proof.


But I may be talking nonsense here, so you need the comments of someone 
more familiar with Coq or similar systems


Cheers,

Jeremy


On 06/10/17 05:38, Chun Tian (binghe) wrote:

Hi Jeremy,

I have a relevant question: one time we talked about the differences between Coq and 
HOL (thread title: "Difficulties when migrating proof scripts from Coq”), and 
you said:

"There's a distinction between an inductively defined set (in Isabelle or
HOL) and a datatype, though they can look similar.  I don't know which
corresponds better to your Coq code

You can model a proof by a proof tree "object" by using a datatype
definition - then you have something of which you can define functions
to give, eg, its' height, number of rule applications, etc.”

Is the ability for theorem provers to do reasoning directly on “proofs” (or can 
we say “proofs” are 1st-class objects?) also a consequence of “rich” type 
systems?

Regards,

Chun Tian


Il giorno 05 ott 2017, alle ore 18:53, Jeremy Dawson <jeremy.daw...@anu.edu.au> 
ha scritto:

Hi Mario,

Slightly off-topic, I had experience with the type system of HOL-Omega (system 
F, if I recall the terminology right, not dependent types, so my experience may 
not be very relevant)

My dominant recollection is the difficulty of getting the system to do the 
right type inference, and getting terms to typecheck.  I was forever working 
out where I needed to put in type annotations.  Quite frustrating after my 
experience with regular HOL, and Isabelle.

It led me to conclude that the systems offering automatic inference of a principal type 
really occupy a "sweet spot", ie the best compromise between ease of use and 
expressive power.

Cheers,

Jeremy Dawson

On 06/10/17 03:46, Mario Castelán Castro wrote:

On 04/10/17 20:09, Ramana Kumar wrote:

Perhaps it would make more sense to ask people who are using rich type
systems what their motivations are :)
(On this list it's probably mostly people who are satisfied with simple
type theory.)


Yes, you are right. I wrote to this list because I am interesting in the
opinion of informed “outsiders”, not only “insiders”, so to speak.



--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot



___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info



--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info




--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Proof about sorting

[Jeremy Dawson]

You might like to try the following

(1) a predicate sorted, to mean each list member is <= the next one
(2) a lemma that inserting an element into a sorted list gives a sorted list

Jeremy

On 04/12/17 12:58, Liu Gengyang wrote:

Hi,

Recently I am meeting a problem, it has been confusing me a few days,
seeking for help.

I defined a sorting predicate mySort:

val insert_def = Define `
(insert x [] = [x]) /\
(insert x (h::t) = if x <= h
   then (x::h::t)
   else (h::(insert x t)))`;

val mySort_def = Define `
  (mySort [] = []) /\
  (mySort (h::t) = (insert h (mySort t)))`;

EVAL ``mySort [2;4;1;5;3;2]``

val it = |- mySort [2; 4; 1; 5; 3; 2] = [1; 2; 2; 3; 4; 5] : thm


Now I want to prove the property0: for any pop: list, if it is sorted by
mySort, the first element in pop will less than or equal to other
elements in pop.

I try to represent property0 in HOL4, but I meet a question, that is
``mySort pop`` isn't a bool term, so I use two ways to solve it:

1, !pop. (pop = mySort pop) ==> EVERY(\x. (HD pop) <= x) pop

2, !pop. EVERY (\x. HD (mySort pop) <= x) (mySort pop)

However, I can't prove both of them. When I used the Induct tactic to
`pop` or `mySort pop`, the goal will be more and more complex, and the
property0 can't reflect in the proving process, it seems unsolvable.
Does the representation of 1 and 2 is wrong, or the definition of mySort
is wrong too？How can I prove the property0?

By the way, I prove 3 property about mySort and insert during I prove 1
and 2.

val INSNOTNULL_POP = prove(``!h pop.insert h pop <> []``,
RW_TAC std_ss [] >>
Cases_on `pop` >-
  RW_TAC list_ss [insert_def] >>
RW_TAC list_ss [insert_def]);
val SORTNOTNULL_POP = prove(``!pop. pop <> [] ==> mySort pop <> [] /\
(mySort pop= insert (HD pop) (mySort (TL pop)))``,
RW_TAC list_ss [] >| [
Cases_on `pop` >-
  RW_TAC list_ss [mySort_def] >>
RW_TAC list_ss [mySort_def,INSNOTNULL_POP],
Induct_on `pop` >-
  RW_TAC list_ss [] >>
RW_TAC list_ss [] >>
RW_TAC list_ss [mySort_def]
]);
val SORTNULL_POP = prove(``!pop. (pop = []) <=>(mySort pop = [])``,
GEN_TAC >>
EQ_TAC >-
  RW_TAC list_ss [mySort_def] >>
Induct_on `pop` >-
  RW_TAC list_ss [] >>
RW_TAC list_ss [mySort_def] >>
Cases_on `pop` >-
  RW_TAC list_ss [mySort_def,insert_def] >>
RW_TAC list_ss [mySort_def,INSNOTNULL_POP]);

Regards,

Liu


--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot



___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info



--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] INVERSE of function?

[Jeremy Dawson]

Hi Chun,

See LINV and RINV in pred_set.

I found the definitions of these pointlessly restrictive since they only 
applied for an injective/surjective function.  So I changed things to 
define them both in terms of LINV_OPT which I defined.  (Hence the old 
theorem names LINV_DEF and RINV_DEF.)


see my commits
4e806d114105079ead99b4a27a86c08dd5515d68
f3fcad057ccfff3130edc82912ec54155901f085

So, rather than a multiplicity of similarly defined functions (where the 
obvious relations between them would not be provable because of the 
indeterminacy of @), I'd suggest defining INVERSE in terms of LINV

(eg, I think it would be INVERSE f y = LINV f UNIV y)

Jeremy

On 05/28/2018 12:01 PM, Chun Tian wrote:

Hi,

I saw the following definition in the current pending request  (vector theory 
#513):

val INVERSE_DEF = Define `INVERSE f = \y. @x. f x = y`;

But isn’t this too common to be already somewhere in HOL’s theory library? If 
so, where is it?

Regards,

Chun



--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot



___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info



--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Formalizing logical puzzles

[Jeremy Dawson]

Hi Dylan,

I'm familiar with HOL4 not HOL Light, but it looks as though they are 
similar at this point: you have made a definition of a function called 
goldInsc and you have named that definition (ie the theorem stating the 
definition) goldInsc


Jeremy

On 06/27/2018 12:37 AM, Dylan Melville wrote:

Correcting a mistake: the goldInsc definition was supposed to be

# let goldInsc = new_definition `goldInsc gc <=> ~ gc`;;

On Jun 26, 2018, at 10:35 AM, Dylan Melville > wrote:


I’m working on learning the basics of using HOL to solve logic 
puzzles, such as the ‘Portia’s Suitor’ problem:


Portia has a gold casket and a silver casket and has placed a
picture of herself in one of them. On the caskets, she has written
the following inscriptions:


• Gold: The portrait is not in here
• Silver: Exactly one of these inscriptions is true.

Portia explains to her suitor that each inscription may be true or
false, but that she has placed her portrait in one of the caskets
in a manner that is consistent with the truth or falsity of the
inscriptions.
If the suitor can choose the casket with her portrait, she will
marry him.


Obviously this is a very simple problem, but when inputting the proof 
into HOL Light, I had an issue. The first axiom, the gold inscription 
I formalized as


# let goldInsc = new_definition `goldInsc gc = not gc`;;

Then attempted the silver inscription as

# let silvInsc = new_definition `silvInsc gc <=> silvInsc gc <=> ~ 
(goldInsc gc)`;;


Which doesn’t work as intended, obviously since goldInsc is a theorem, 
not an actual function. What is the proper way to express the silver 
inscription?




--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot



___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info



--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] working proof that shouldn't need to be so complicated

[Jeremy Dawson]

Sorry if I've missed your point (just a quick reply) but

On 01/06/2018 05:18 AM, Michael Beeson wrote:

SIMP isn't a conversion


SIMP_CONV is a conversion, which may give what you want

And if RHS_CONV would do what you want, no need to use PAT_CONV

Jeremy

--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Share list of terms with later theories

[Jeremy Dawson]

A related question: some time back I was looking at how datatypes are 
constructed, and found stuff in theory ind_type, and theorems like 
list_TY_DEF (which one finds by doing find "ty_def")


But it seems that there are also theorems created which define the 
constructors of the list datatype in terms of ind_type$CONSTR, 
ind_type$BOTTOM, ind_type$FCONS, etc, but that these theorems are very 
well hidden.  I intended to investigate more to find how these theorems 
are hidden, and where if possible to find them, but never got back to it.


Can anyone help me on that question?  And is it relevant to this current 
discussion?


Cheers,

Jeremy


On 01/17/2018 10:28 AM, michael.norr...@data61.csiro.au wrote:

If people wanting to store these “uninteresting” theorems are happy to wrap and 
unwrap the OMITs, this would be one approach.

I had been thinking of adding a

   save_private_thm(name, privatedbname, thm)

entrypoint to Theory.sml.  You’d want multiple possible “private dbs”, so there 
would be an entry-point along the lines of

   get_private_db : string -> (string,thm) Binarymap.dict

Every time a theory was loaded, this private_db would change, so in many 
applications it might not be appropriate to store the result of

   get_private_db “cakeml/translator”

but to instead write

   val th = Binarymap.peek(get_private_db “cakeml/translator”, “theorem-name”)

Michael

On 16/1/18, 18:35, "Magnus Myreen"  wrote:

 Hi all,
 
 How about defining:
 
   OMIT x = x
 
 in markerScript.sml and making it print as ... and adjust HOL so that

 a theorem with a top-level OMIT does not show up in DB searches.
 
 Cheers,

 Magnus
 
 
 On 12 January 2018 at 00:00,   wrote:

 > I was thinking along these lines, yeah.  Such theorems could also be 
stopped from appearing in the Theory.sig file.
 >
 > Michael
 >
 > On 12/1/18, 07:31, "Konrad Slind"  wrote:
 >
 > Theorems that need to persist between sessions are most easily 
stored by name
 > in theories. Maybe some kind of PolyML database magic could also be
 > used, I don't
 > know. As far as DB searches, it wouldn't be hard to implement a
 > refined DB search
 > mechanism that first discarded all theorems that met some kind of
 > naming convention
 > (e.g., those starting with an underscore or something like that) and
 > then did the usual
 > search (which can be on name fragment or pattern).
 >
 > Konrad.
 >
 >
 > On Wed, Jan 10, 2018 at 7:09 PM, Magnus Myreen  
wrote:
 > > Ah, I didn't realise this existed. Thanks for the pointers!
 > >
 > > How does storing of theorems work in this setting? One can't 
construct
 > > a theorem from a string in a decode function.
 > >
 > > I guess the string could refer to a theorem name that's stored in 
the
 > > theory, but this is a bit inconvenient because some of the 
theorems in
 > > the translator's state are currently not stored in the theory 
(other
 > > than in the automatically produced theorem that is an encoding of 
the
 > > entire state). I guess an encode function could invent an unused 
name
 > > and store the theorem while it's producing the encoding. This can 
lead
 > > to some strange things turning up in DB searches (as is the case 
with
 > > the current approach).
 > >
 > > Cheers,
 > > Magnus
 > >
 > >
 > > On 11 January 2018 at 11:24,   
wrote:
 > >> That level of generality is already possible, and has always been 
a desideratum for the design.  (The grammar update information stored is about that 
complicated for example; consider the types that occur in a call to add_rule.)
 > >>
 > >> The painful part is that you have to write functions to encode 
and decode the types into and out of strings (because these strings are written into the 
theory files).  There are functions for doing basic SML types in src/parse/Coding, and 
the handling of terms is handled by writing functions that take functions for doing this 
as parameters.  See the bottom of src/parse/term_grammar for the encoding and decoding, 
and src/parse/GrammarDeltas for the way this is put together for the grammar example.
 > >>
 > >> You can see the fundamental building blocks at the 
LoadableThyData structure in src/postkernel/Theory.
 > >>
 > >> Certainly, providing a method for going through a generic 
s-expression type might be easiest for users to understand, so perhaps I can build that 
as well as term lists.
 > >>
 > >> Michael
 > >>
 > >> On 11/1/18, 11:08, "Magnus Myreen" 

Re: [Hol-info] Applying a theorem to a specific subgoal

[Jeremy Dawson]

Hi Dylan,

from HOL/help/Docfiles/HTML/Tactical.NTH_GOAL.html
(or  help "NTH_GOAL" ; )

Where tac1 and tac2 are tactics, tac1 THEN_LT NTH_GOAL n tac2 
applies tac1 to a goal, and then applies tac2 to the n’th resulting subgoal.


Cheers,

Jeremy


On 08/08/2018 03:24 PM, Dylan Melville wrote:

When a goal is separated into multiple subgoals during a proof of the form

# prove(thm,tactic);;


Where the last tactic is something like

REPEAT CONJ_TAC

Is there a way to specify that the next tactic should be applied to a specific 
subgoal? In the proof I’m working on, it was applied to all subgoals.


--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info



--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Using Assumptions

[Jeremy Dawson]

Also, if ever giving a pattern to match your chosen assumption doesn't 
suit, you can use ASSUM_LIST - which gives you a list of all assumptions 
to use in constructing your next tactic, and you can pick one of that 
list.


But note the caveat in the doc page about relying on the order of 
assumptions.


Cheers,

Jeremy

On 08/17/2018 03:58 AM, Chun Tian (binghe) wrote:

Hi.

you can use PAT_ASSUM or PAT_X_ASSUM (or their versions in Q structure) to 
match an assumption and then use it as a theorem for your next tactic. 
PAT_ASSUM will keep the assumption untouched, while PAT_X_ASSUM will remove it, 
both are useful in certain cases.

For example, if there’s an assumption like ``!x. P x`` (P could be anything), 
and you want to move it to goal as an antecedent, a tactic like:

Q.PAT_X_ASSUM `!x. P x` MP_TAC

or

Q.PAT_X_ASSUM `!x. P x` (fn thm => MP_TAC thm)

will do the job. In case you want to further treatment of that theorem before 
calling MP_TAC, just expand above 2nd form inside the lambda-function. Check 
reference manual for more details.

Hope this helps,

—Chun


Il giorno 16 ago 2018, alle ore 18:07, Dylan Melville  
ha scritto:

Is there anyway to reference a specific assumption of the current goal as a 
theorem?
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info




--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot



___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info



--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] About the experimental kernel

[Jeremy Dawson]

On 12/04/18 01:59, Mario Xerxes Castelán Castro wrote:

  for explicit lazy beta
conversions (with an internal explicit substitution calculus)


I assume this refers to Clos, mk_clos etc in src/0/Term.sml

My questions is: is this actually used?  I can't see where anything in 
the source code creates a Clos where there isn't already one existing.


This would be odd, so I guess I've overlooked it somewhere - but where?

Jeremy

--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] assumption matching in SPLIT_LT

[Jeremy Dawson]

Hi Waqar,

Firstly (simplest),

SPLIT_LT 2 (ALLGOALS tac1, ALL_LT)

applies tac1 to the first two subgoals and does nothing to the 
remainder.  Then you can work on the remaining goal.


But you want to also apply EVERY [tac2, tac3, ...] to the third subgoal 
(which is the only remaining one), together in the same step.

  To package this as a list-tactic, you could do

val tac23 = EVERY [tac2, tac3, ...]

then val lt23 = ALLGOALS tac23
or val lt23 = TACS_TO_LT [tac23]

then what you ask would be achieved by
SPLIT_LT 2 (ALLGOALS tac1, lt23)

Cheers,

Jeremy


On 10/13/2018 03:38 AM, Waqar Ahmad via hol-info wrote:

Hi,

Suppose, I have 3 subgoals where first 2 subgoals can be proved by apply 
tac1 and the third goal may takes some set of tacts, say tac2, tac3...


Is it possible that I can use SPLIT_LT in a way such that first two 
subgoals are discharged by applying tac1 and I only end up proving the 
third subgoal?



On Fri, Sep 21, 2018 at 3:00 AM > wrote:


match_mp_tac is indeed causing an error because it is not applicable
in the other subgoals.

__ __

Michael

__ __

*From: *Waqar Ahmad via hol-info mailto:hol-info@lists.sourceforge.net>>
*Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk
>
*Date: *Friday, 21 September 2018 at 08:39
*To: *"konrad.sl...@gmail.com "
mailto:konrad.sl...@gmail.com>>
*Cc: *hol-info mailto:hol-info@lists.sourceforge.net>>
*Subject: *Re: [Hol-info] assumption matching in SPLIT_LT

__ __

Hi, 

__ __

Thanks for the reply. I think the match_mp_tac is causing the error
since if I only pop the assumption the tactic works on first
subgoal.

__ __

rw [] \\ (pop_assum (mp_tac)) THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS
(rw[]))

__ __

__ __

 > val it =



    SG3

    

     A1 ==> B1





    SG2

    

     A1 ==> B1





    (A1 ==> B1) ==> B1





3 subgoals

    : proof

__ __

__ __

__ __

__ __

On Thu, Sep 20, 2018 at 6:21 PM Konrad Slind mailto:konrad.sl...@gmail.com>> wrote:

Seems like the rw[] is breaking the proof into 3 subgoals, and
only on the first one is the pop_assum match_mp_tac succeeding.
So the proof is failing before it gets to the THEN_LT. 

__ __

Konrad.

__ __

__ __

On Thu, Sep 20, 2018 at 2:05 PM Waqar Ahmad via hol-info
mailto:hol-info@lists.sourceforge.net>> wrote:

Hi, 

__ __

I'm trying to use the tactical SPLIT_LT to multiple
subgoals. However, I'm facing error with assumption
matching. For instance, I've a proof goal of this form:

__ __

`(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`

__ __

rw [] 

\\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1
(ALL_LT, ALLGOALS (rw[]))

__ __

I'm getting following matching error...

__ __

Exception raised at Tactic.MATCH_MP_TAC:

No match

Exception-

    HOL_ERR

      {message = "No match", origin_function =
"MATCH_MP_TAC",

       origin_structure = "Tactic"} raised

__ __

It works otherwise for handling them individually...

-- 

Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/

___
hol-info mailing list
hol-info@lists.sourceforge.net

https://lists.sourceforge.net/lists/listinfo/hol-info




__ __

-- 

Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/

___
hol-info mailing list
hol-info@lists.sourceforge.net 
https://lists.sourceforge.net/lists/listinfo/hol-info



--
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/

Re: [Hol-info] New grammar of defining theorems?

[Jeremy Dawson]

This summary seems to make it clear that this new feature achieves very 
little, with the following costs:

- it gives users yet something else (as if there isn't already enough!) 
to lookup in the documentation, or ask questions about
- it's positively confusing, in that
"Theorem name ... " has totally different meanings, depending on which 
case applies (eg, in one case, name must already exist, in the other, it 
ought not to already exist)

This idea looks like the start of the path followed in Isabelle and Coq, 
of having a multitude of commands, some with a multitude of variants (eg 
optional arguments) with no coherent consistent grammar rules - just so 
that the user doesn't need to type a few punctuation symbols.

Jeremy

On 8/1/19 2:41 pm, Konrad Slind wrote:
> Isn't it clear just from the form?
> 
>    Theorem name quote (ML)    --> val name = Q.store_thm(name,quote,ML)
>    Theorem name (ML)              --> val name = save_thm(name,ML)
> 
> 

___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] New grammar of defining theorems?

[Jeremy Dawson]

On 8/1/19 4:49 pm, michael.norr...@data61.csiro.au wrote:
> I think you've misunderstood. 

that's true, sorry.

> Here the advantage is quite clear and valuable: in the existing system, you 
> have to type the same string of symbols twice in order to avoid annoying 
> maintenance issues when theorems get moved.  There's no utility in allowing 
> people to write things like
> 
> val foo = save_thm("bar", ...)
> 
> and it just leads to real pain.
> 
there's certainly a discernible advantage in this particular case, I agree

> Slippery slope arguments cut no mustard.
> 
Let's hope it's not the start of one.  And do work out a way of getting 
it into the online documentation (eg, in 
HOL/help/src-sml/htmlsigs/idIndex.html)

Jeremy

___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Jeremy Dawson]

Sorry for my previous confusing email, this is something I didn't know 
about. It seems now TL and TL_T are the same.

Jeremy

On 02/15/2019 09:59 AM, michael.norr...@data61.csiro.au wrote:
> the updated definition of TL.

___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] CFP - ICFEM 2020 - Int'l Conf on Formal Engineering Methods

[Jeremy Dawson]

CALL FOR PAPERS


22nd International Conference on Formal Engineering Methods (ICFEM 
2020), 2-6 November 2020, Singapore.


http://formal-analysis.com/icfem/2020/

Since 1997, ICFEM provides a forum for both researchers and 
practitioners who are interested in developing practical formal methods 
for software engineering or applying existing formal techniques to 
improve the software development process in practice systems. Formal 
Methods for the development of computer systems have been extensively 
researched and studied. We now have good theoretical understandings of 
how to describe what programs do, how they do it, and why they work. A 
range of semantic theories, specification languages, design techniques, 
verification methods, and supporting tools have been developed and 
applied to the construction of programs of moderate size that are used 
in critical applications. The remaining challenge now is how to deal 
with problems in developing and maintaining large scale and complex 
computer systems.


The goal of this conference is to bring together industrial, academic, 
and government experts, from a variety of user domains and software 
disciplines, to help advance state of the art. Researchers, 
practitioners, tool developers, users, and technology transfer experts 
are all welcome. We are interested in work that has been incorporated 
into real production systems, and in theoretical work that promises to 
bring practical, tangible engineering benefits.


Scope and Topics:
Submissions related to the following principal themes are encouraged, 
but any topics relevant to the field of formal engineering methods and 
their practical applications will also be considered:


- Abstraction, refinement, and evolution
- Formal specification and modelling
- Formal verification and analysis
- Model checking
- Formal approaches to software testing and inspection
- Formal methods for self-adaptive systems
- Formal methods for object-oriented systems
- Formal methods for component-based systems
- Formal methods for concurrent and real-time systems
- Formal methods for cloud computing
- Formal methods for cyber-physical systems
- Formal methods for software safety and security
- Formal methods for software reliability and dependability
- Development, integration, and experiments involving verified systems
- Formal certification of products under international standards
- Formal model-based development and code generation

Important Dates:
Full Paper Submissions: 1 May 2020 (AoE)
Workshop/Tutorial Proposals: 20 March 2020
Acceptance/Rejection Notification: 19 June 2020
Camera-ready: 17 July 2020

Submission and Publication:
Submissions to the conference must not have been published or be 
concurrently considered for publication elsewhere. All submissions will 
be judged on the basis of originality, contribution to the field, 
technical and presentation quality, and relevance to the conference. The 
proceedings will be published in the Springer Lecture Notes in Computer 
Science series.


Papers should be written in English and should not exceed 16 pages in 
LNCS format (more details here). Submissions should be made through the 
ICFEM 2020 submission page, handled by the EasyChair conference 
management system.


https://easychair.org/conferences/?conf=icfem20

Workshop or tutorial proposals should be directly sent to the Workshop 
Chair via email. Each proposal should include (1) title, scope, and 
aims, (2) brief bio of the organizer or lecturer, and (3) postal and 
email addresses.


Organising Committee:

General Co-Chairs
Jin Song Dong, National University of Singapore and Griffith University, 
Singapore/Australia

Jim McCarthy, Defence Science and Technology, Australia

Program Co-Chairs
Shang-Wei Lin, Nanyang Technological University, Singapore
Zhe Hou, Griffith University, Australia
Brendan Mahony, Defence Science and Technology, Australia

Finance Chair
Yang Liu, Nanyang Technological University, Singapore
Jun Sun, Singapore University of Technology and Design, Singapore

Workshop Chair
Hadrien Bride, Griffith University, Australia

Doctoral Symposium Chair
Lei Ma, Kyushu University, Japan


___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] ICFEM'20 - submission deadline extended

[Jeremy Dawson]

Due to the requests from authors, the submission deadline of ICFEM 2020 
has been extended to 24 May 2020 (AOE).


Here is the revised CFP

---
CALL FOR PAPERS
---

22nd International Conference on Formal Engineering Methods (ICFEM 
2020), 2-6 November 2020, Singapore (subject to changes, including 
backup options such as postponing the conference or hosting it online).


http://formal-analysis.com/icfem/2020/

Extended deadlines:
Full Paper Submissions Due: 24 May 2020 (AoE)
Workshop/Tutorial Proposals Due: 20 March 2020
Acceptance/Rejection Notification: 5 July 2020
Camera-ready Due: 17 July 2020

Since 1997, ICFEM provides a forum for both researchers and 
practitioners who are interested in developing practical formal methods 
for software engineering or applying existing formal techniques to 
improve software development process in practice systems. Formal Methods 
for the development of computer systems have been extensively researched 
and studied. We now have good theoretical understandings of how to 
describe what programs do, how they do it, and why they work. A range of 
semantic theories, specification languages, design techniques, 
verification methods, and supporting tools have been developed and 
applied to the construction of programs of moderate size that are used 
in critical applications. The remaining challenge now is how to deal 
with problems in developing and maintaining large scale and complex 
computer systems.


The goal of this conference is to bring together industrial, academic, 
and government experts, from a variety of user domains and software 
disciplines, to help advance state of the art. Researchers, 
practitioners, tool developers and users, and technology transfer 
experts are all welcome. We are interested in work that has been 
incorporated into real production systems, and in theoretical work that 
promises to bring practical, tangible engineering benefits.


Scope and Topics:
Submissions related to the following principal themes are encouraged, 
but any topics relevant to the field of formal engineering methods and 
their practical applications will also be considered:


• Abstraction, refinement and evolution
• Formal specification and modelling
• Formal verification and analysis
• Model checking
• Formal approaches to software testing and inspection
• Formal methods for self-adaptive systems
• Formal methods for object-oriented systems
• Formal methods for component-based systems
• Formal methods for concurrent and real-time systems
• Formal methods for cloud computing
• Formal methods for cyber-physical systems
• Formal methods for software safety and security
• Formal methods for software reliability and dependability
• Development, integration and experiments involving verified systems
• Formal certification of products under international standards
• Formal model-based development and code generation

Submission and Publication:
Submissions to the conference must not have been published or be 
concurrently considered for publication elsewhere. All submissions will 
be judged on the basis of originality, contribution to the field, 
technical and presentation quality, and relevance to the conference. The 
proceedings will be published in the Springer Lecture Notes in Computer 
Science series.


Papers should be written in English and should not exceed 16 pages in 
LNCS format. Submissions should be made through the ICFEM 2020 
submission page, handled by the EasyChair conference management system.


https://easychair.org/conferences/?conf=icfem20

Workshop or tutorial proposals should be directly sent to the Workshop 
Chair via email. Each proposal should include (1) title, scope, and 
aims, (2) brief bio of the organizer or lecturer, and (3) postal and 
email addresses.


Organising Committee:

General Chair
Jin Song Dong, National University of Singapore and Griffith University, 
Singapore/Australia

Jim McCarthy, Defence Science and Technology, Australia​

Program Co-Chairs
Shang-Wei Lin, Nanyang Technological University, Singapore
Zhe Hou, Griffith University, Australia
Brendan Mahony, Defence Science and Technology, Australia​

Finance Chair
Yang Liu, Nanyang Technological University, Singapore
Jun Sun, Singapore University of Technology and Design, Singapore

Workshop Chair
Hadrien Bride, Griffith University, Australia

Doctoral Symposium Chair
Lei Ma, Kyushu University, Japan



___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] ICFEM'20 deadline extended to 17th May 2020

[Jeremy Dawson]

 Sinica, Taiwan
Yean-Ru Chen, National Cheng Kung University, Taiwan
Wei-Ngan Chin, National University of Singapore, Singapore
Ranald Clouston, Australian National University, Australia
Sylvain Conchon, Universite Paris-Sud, France
Florin Craciun, Babes-Bolyai University, Romania
Jeremy Dawson, Australian National University, Australia
Frank De Boer, Centrum Wiskunde & Informatica (CWI), Netherlands
Yuxin Deng, East China Normal University, China
Jin Song Dong, Griffith University and NUS, Australia
Naipeng Dong, University of Queensland, Australia
Zhenhua Duan, Xidian University, China​
Marc Frappier, Université de Sherbrooke, Canada
Lindsay Groves, Victoria University of Wellington, New Zealand
Ichiro Hasuo, National Institute of Informatics, Japan
Xudong He, Florida International University, United States
Zhe Hou, Griffith University, Australia
Pao-Ann Hsiung, National Chung Cheng University, Taiwan
Fuyuki Ishikawa, National Institute of Informatics, Japan
Fabrice Kordon, LIP6/Sorbonne Universite & CNRS, France
Yi Li, Nanyang Technological University, Singapore
Xuandong Li, Nanjing University, China
Shang-Wei Lin, Nanyang Technological University, Singapore
Yang Liu, Nanyang Technological University, Singapore
Zhiming Liu, Southwest University, China
Shuang Liu, Tianjin University, China
Brendan Mahony, DSTO, Australia
Jim McCarthy, Defence Science and Technology, Australia​
Dominique Mery, Université de Lorraine, France
Stephan Merz, Inria Nancy, France
Shin Nakajima, National Institute of Informatics, Japan
Jun Pang, University of Luxembourg, Luxembourg
Yu Pei, The Hong Kong Polytechnic University, China
Shengchao Qin, Teesside University, United Kingdom
Silvio Ranise, FBK-Irst, Italy
Elvinia Riccobene, University of Milan, Italy
Adrian Riesco, Universidad Complutense de Madrid, Spain
David Sanan, Nanyang Technological University, Singapore
Klaus-Dieter Schewe, Zhejiang University, China
Harald Sondergaard, The University of Melbourne, Australia
Meng Sun, Peking University, China
Jing Sun, The University of Auckland, New Zealand
Jun Sun, Singapore University of Technology and Design, Singapore
Alwen Tiu, The Australian National University, Australia
Elena Troubitsyna, KTH, Sweden
Hai H. Wang, University of Aston, United Kingdom
Bow-Yaw Wang, Academia Sinica, Taiwan
Virginie Wiels, ONERA / DTIM, France
Zhiwu Xu, Shenzhen University, China
Naijun Zhan, Chinese Academy of Sciences, China
Jian Zhang, Chinese Academy of Sciences, China
Jaco van de Pol, Aarhus University, Denmark
Peter Ölveczky, University of Oslo, Norway


___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info