Re: [Hol-info] Conflicted "inv" pp_elements in relationTheory and realaxTheory

[Michael.Norrish]

There’s certainly a bug here: I want the superscript T for relations and the 
superscript -1 for reals, and the two need not mix.  I think there’s a 
straightforward enough solution that will allow “inv” to be used as an input 
method for both.

Michael

On 17/10/17, 06:57, "Chun Tian"  wrote:

I’m using HOL built from latest Git “master” branch; you’re using HOL 
Kananaskis-11 release.

—Chun

> Il giorno 16 ott 2017, alle ore 17:01, Mario Castelán Castro 
 ha scritto:
> 
> On 16/10/17 09:35, Chun Tian (binghe) wrote:
>> I'm fine with constant overloading. But I think the "term_name" used in
>> add_rule() doesn't know constant overloading at all. After realaxTheory 
is
>> loaded, the previous rule defined in relationTheory has absolutely no
>> effects, even I'm using "inv" for relations.
> 
> I do not know what is your situation. In my case (HOL4 Kananaskis-11),
> there is no custom parser rule for relation$inv:
> 
> “mario@svetlana [0] [/home/mario]
> $ hol
> 
> -
>   HOL-4 [Kananaskis 11 (stdknl, built Sun Aug 06 16:33:32 2017)]
> 
>   For introductory HOL help, type: help "hol";
>   To exit type -D
> -
>> ancestry "-";
> val it =
>   ["ConseqConv", "quantHeuristics", "ind_type", "operator", "while",
> "pair",
>"num", "relation", "prim_rec", "arithmetic", "numeral", "normalForms",
>"one", "marker", "combin", "min", "bool", "sat", "sum", "option",
>"basicSize", "numpair", "pred_set", "list", "rich_list"]: string list
>> “inv R”;
> <>
> val it = ``inv R``: term”
> 
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
> 
> 
--
> 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] line wrap length in hol-mode

[Mario Castelán Castro]

On 16/10/17 17:15, michael.norr...@data61.csiro.au wrote:
> You need to adjust Globals.linewidth (an int ref).
Thanks.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] line wrap length in hol-mode

[Michael.Norrish]

You need to adjust Globals.linewidth (an int ref).

Michael

On 17/10/17, 03:57, "Mario Castelán Castro"  wrote:

Hello. How can I change the column at which the pretty printer will wrap
expressions using hol-mode in GNU Emacs? I want it to use the full width
of the Emacs “window” (the cell that displays a buffer, not the whole
window).

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



--
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] Conflicted "inv" pp_elements in relationTheory and realaxTheory

[Mario Castelán Castro]

On 16/10/17 14:55, Chun Tian wrote:
> I’m using HOL built from latest Git “master” branch; you’re using HOL 
> Kananaskis-11 release.

Understood.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Conflicted "inv" pp_elements in relationTheory and realaxTheory

[Chun Tian]

I’m using HOL built from latest Git “master” branch; you’re using HOL 
Kananaskis-11 release.

—Chun

> Il giorno 16 ott 2017, alle ore 17:01, Mario Castelán Castro 
>  ha scritto:
> 
> On 16/10/17 09:35, Chun Tian (binghe) wrote:
>> I'm fine with constant overloading. But I think the "term_name" used in
>> add_rule() doesn't know constant overloading at all. After realaxTheory is
>> loaded, the previous rule defined in relationTheory has absolutely no
>> effects, even I'm using "inv" for relations.
> 
> I do not know what is your situation. In my case (HOL4 Kananaskis-11),
> there is no custom parser rule for relation$inv:
> 
> “mario@svetlana [0] [/home/mario]
> $ hol
> 
> -
>   HOL-4 [Kananaskis 11 (stdknl, built Sun Aug 06 16:33:32 2017)]
> 
>   For introductory HOL help, type: help "hol";
>   To exit type -D
> -
>> ancestry "-";
> val it =
>   ["ConseqConv", "quantHeuristics", "ind_type", "operator", "while",
> "pair",
>"num", "relation", "prim_rec", "arithmetic", "numeral", "normalForms",
>"one", "marker", "combin", "min", "bool", "sat", "sum", "option",
>"basicSize", "numpair", "pred_set", "list", "rich_list"]: string list
>> “inv R”;
> <>
> val it = ``inv R``: term”
> 
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
> 
> --
> 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



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
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

[Hol-info] line wrap length in hol-mode

[Mario Castelán Castro]

Hello. How can I change the column at which the pretty printer will wrap
expressions using hol-mode in GNU Emacs? I want it to use the full width
of the Emacs “window” (the cell that displays a buffer, not the whole
window).

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Conflicted "inv" pp_elements in relationTheory and realaxTheory

[Mario Castelán Castro]

On 16/10/17 09:35, Chun Tian (binghe) wrote:
> I'm fine with constant overloading. But I think the "term_name" used in
> add_rule() doesn't know constant overloading at all. After realaxTheory is
> loaded, the previous rule defined in relationTheory has absolutely no
> effects, even I'm using "inv" for relations.

I do not know what is your situation. In my case (HOL4 Kananaskis-11),
there is no custom parser rule for relation$inv:

“mario@svetlana [0] [/home/mario]
$ hol

-
   HOL-4 [Kananaskis 11 (stdknl, built Sun Aug 06 16:33:32 2017)]

   For introductory HOL help, type: help "hol";
   To exit type -D
-
> ancestry "-";
val it =
   ["ConseqConv", "quantHeuristics", "ind_type", "operator", "while",
"pair",
"num", "relation", "prim_rec", "arithmetic", "numeral", "normalForms",
"one", "marker", "combin", "min", "bool", "sat", "sum", "option",
"basicSize", "numpair", "pred_set", "list", "rich_list"]: string list
> “inv R”;
<>
val it = ``inv R``: term”

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Conflicted "inv" pp_elements in relationTheory and realaxTheory

[Chun Tian (binghe)]

I'm fine with constant overloading. But I think the "term_name" used in
add_rule() doesn't know constant overloading at all. After realaxTheory is
loaded, the previous rule defined in relationTheory has absolutely no
effects, even I'm using "inv" for relations.

But I don't mind if relation "inv" also uses "^{-1}" (so we should move the
rule from realaxTheory to relationTheory and remove the existing one in
relationTheory).

---
Chun

On 16 October 2017 at 16:02, Mario Castelán Castro 
wrote:

> On 16/10/17 08:23, Chun Tian (binghe) wrote:
> > Is this something can be fixed? (I don't know how) i.e. preserving the
> > pp_setting of  "inv" for relations and correctly define TeX notations for
> > both of them.
>
> “inv” has 2 possible resolutions after loading realTheory:
>
> > overload_info_for "inv";
> inv parses to:
>   realax$inv
>   (relation$inv :(α -> α -> bool) -> α -> α -> bool)
> inv might be printed from:
>   (relation$inv :(α -> α -> bool) -> α -> α -> bool)
>   realax$inv
> val it = (): unit
>
> Typically the correct one will be chosen by the parser because of type
> constraints. If you want to force one of them, you can write
> “relation$inv” or “realax$inv”. If you want to make the one from
> “relation” the default, then do “overload_on("inv",“relation$inv”):”. I
> do not know how to manipulate the TeX mapping.
>
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
>
>
> 
> --
> 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
>
>


-- 
Chun Tian (binghe)
University of Bologna (Italy)
--
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] Conflicted "inv" pp_elements in relationTheory and realaxTheory

[Mario Castelán Castro]

If you want to completely remove the mapping of “inv” to the constant
from “realax”, then do “remove_ovl_mapping "inv" {Name = "inv", Thy =
"realax"};”. This constant can then still be accessed with “realax$inv”.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Conflicted "inv" pp_elements in relationTheory and realaxTheory

[Mario Castelán Castro]

On 16/10/17 08:23, Chun Tian (binghe) wrote:
> Is this something can be fixed? (I don't know how) i.e. preserving the
> pp_setting of  "inv" for relations and correctly define TeX notations for
> both of them.

“inv” has 2 possible resolutions after loading realTheory:

> overload_info_for "inv";
inv parses to:
  realax$inv
  (relation$inv :(α -> α -> bool) -> α -> α -> bool)
inv might be printed from:
  (relation$inv :(α -> α -> bool) -> α -> α -> bool)
  realax$inv
val it = (): unit

Typically the correct one will be chosen by the parser because of type
constraints. If you want to force one of them, you can write
“relation$inv” or “realax$inv”. If you want to make the one from
“relation” the default, then do “overload_on("inv",“relation$inv”):”. I
do not know how to manipulate the TeX mapping.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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

[Hol-info] Conflicted "inv" pp_elements in relationTheory and realaxTheory

[Chun Tian (binghe)]

Hi,

In relationTheory there's a "inv" operatior for inverting a relation:

(* --
inverting a relation
   -- *)

val inv_DEF = new_definition(
  "inv_DEF",
  ``inv (R:'a->'b->bool) x y = R y x``);
(* superscript suffix T, for "transpose" *)
val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
   fixity = Suffix 2100,
   paren_style = OnlyIfNecessary,
   pp_elements = [TOK (UTF8.chr 0x1D40)],
   term_name = "inv"}

while there's another rule in realaxTheory, setting it differently:

val _ =
   add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
  fixity = Suffix 2100,
  paren_style = OnlyIfNecessary,
  pp_elements = [TOK (UnicodeChars.sup_minus ^
UnicodeChars.sup_1)],
  term_name = "inv"}

As a result, when I start HOL (in which relationTheory is loaded by
default), I see the "transpose" representation of ``inv R``:

-
   HOL-4 [Kananaskis 11 (expknl, built Mon Oct 16 12:19:37 2017)]
   For introductory HOL help, type: help "hol";
   To exit type -D
-
> ``inv R``;
<>
val it = “Rᵀ”: term

But after loading realTheory (directly or indirectly), it permanently
becomes $R^{-1}$:

> load "realTheory";
val it = (): unit
> ``inv R``;
<>
val it = “R⁻¹”: term
> ``inv (R :'a -> 'a -> bool)``;
val it = “R⁻¹”: term

Further more, their TeX notations were never defined, thus in TeX-based PDF
it simply shows "inv R".

Is this something can be fixed? (I don't know how) i.e. preserving the
pp_setting of  "inv" for relations and correctly define TeX notations for
both of them.

Regards,

Chun Tian

--
Chun Tian (binghe)
University of Bologna (Italy)
--
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] Converting ordinals from different type variables?

[Chun Tian (binghe)]

Hi Michael,

Thanks very much, this saves me lots of time trying to prove something
impossible.

Regards,

Chun Tian


On 16 October 2017 at 00:59,  wrote:

> The definition is fine, but will not have the nice properties you want
> (e.g., monotonicity) if the domain type is bigger than the range.  In
> particular if your domain includes \omega_1 and the range only has
> countable ordinals, then the result of c2a on \omega_1 will be
> unspecified.  This is because the RHS of the limit case will be invoking
> sup on the set of all possible ordinals in the range type.  Given that, you
> will not be able to prove that monotonicity holds.
>
> Michael
>
> On 15/10/17, 18:26, "Chun Tian"  wrote:
>
> Hi,
>
> If I have the following recursive function on ordinals, simply
> converting ‘c ordinals into the “same” ‘a ordinals:
>
> (* Construct a 'c ordinal from 'a ordinal *)
> val c2a_def = new_specification (
>"c2a_def", ["c2a"],
> ord_RECURSION |> INST_TYPE [``:'a`` |-> ``:'c``]
>   |> ISPEC ``0 :'a ordinal``(* z *)
>   |> Q.SPEC `\x r. ordSUC r`(* sf *)
>   |> Q.SPEC `\x rs. sup rs` (* lf *)
>   |> SIMP_RULE (srw_ss()) []);
>
> val it =
>|- (c2a 0o = 0) ∧ (∀α. c2a α⁺ = (c2a α)⁺) ∧
>∀α. 0o < α ∧ islimit α ⇒ (c2a α = sup (IMAGE c2a (preds α))):
>thm
>
> Is my definition correct? (especially for the “lf” part using “sup”)
>  And if so, what properties can I expect from this function?   Is it at
> least monotone? i.e.
>
>  ∀m n. m ≤ n ⇒ c2a m ≤ c2a n
>
> Regards,
>
> Chun Tian
>
>
>
> 
> --
> 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
>



-- 
Chun Tian (binghe)
University of Bologna (Italy)
--
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