Geek Answers Handbook

Trying to look at class classes and subtypes, such as sets and subsets

This question is related to my previous SO question about class types . I ask this question to ask a future question about locales. I don't think class classes will work for what I'm trying to do, but how class classes work, they gave me an idea of ​​what I want from locales.

Below, when I use the curly brackets notation {0,0} , it is not the usual HOL curly braces, but 0 represents an empty set.

Some files if you want them

Discussion before discussion

I describe what I am doing in THY (which I include below), and then I basically ask: "Is there something I can do here to fix this so that I can use type classes?"

As in the SO question related to above, I am trying to link Groups.thy semigroup_add . I create a subtype of my sT type using typedef , and then try to raise some of my basic functional constants and operators to a new type, for example, my union operator geU , my empty emS set, my unordered pair sets paS and my predicate my inP .

This does not work because I am trying to handle a new type, such as a subset. In particular, my new type should represent the set { {0,0} } , which should be part of a trivial semigroup, a semigroup with one element.

The problem is that the axiom of an unordered pair states that if set x exists, then exists (paS xx) exists, and the union axiom claims that if x is set, then (geU x) . So, when I try to raise my union statement to my new type, the wizard knows what I need to prove (geU{0,0} = {0,0}) , which is wrong, but there is only one element {0,0} in my new type {0,0} , so it would have to be that way.

Question

Can this be fixed? In my opinion, I compare sets and subsets with types and subtypes, where I know that they do not match. Call my main type sT and my subtype subT . What do I need for all my statements that were defined with type sT , types such as sT => sT , to work with type subT when subT treated as type sT . New operators and constants that were defined using the subT type, such as a function of the subT => subT , that will somehow work as if they were magically supposed to work with these things.

Write a question

Here I indicate what happens by the line number in THY. Line numbers will be displayed in the PDF file and on the GitHub website.

Lines 21 through 71 have four sections where I combined related constants, notation, and axiom.

  • Type sT , inP/PIn and the equality axiom (from 21 to 33).
  • An empty emS/SEm and an empty axiom (37-45).
  • The disordered pair is the constant paS/SPa and the disordered axiom of the pair (from 49 to 58).
  • Union constant geU/UGe and association axiom (from 62 to 71).

Starting at line 75, I create a new type with typedef , and then create it as a class type semigroup_add .

No problem until I try to raise my unordered pair function {.x,y.} , Line 108 and my union function (geU x) , line 114.

Below the Isar commands, I show a conclusion that tells me that I need to prove that some sets are {0,0} , which cannot be proved.

Here is an ASCII-friendly source where I removed some comments and lines from the THY link linked above:

 theory A_i130424a imports Complex_Main begin --"AXIOM (sT type, inP predicate, and the equality axiom)" typedecl sT ("sT") consts PIn :: "sT => sT => bool" notation PIn ("in'_P") and PIn (infix "inP" 51) and PIn (infix "inP" 51) axiomatization where Ax_x: "(! x. x inP r <-> x inP s) <-> (r = s)" --"[END]" --"AXIOM (emS and the empty set axiom)" consts SEm :: "sT" ("emS") notation (input) SEm ("emS") axiomatization where Ax_em [simp]: "(x niP emS)" --"[END]" --"AXIOM (paS and the axiom of unordered pairs)" consts SPa :: "sT => sT => sT" notation SPa ("paS") and SPa ("({.(_),(_).})") axiomatization where Ax_pa [simp]: "(x inP {.r,s.}) <-> (x = r | x = s)" --"[END]" --"AXIOM (geU and the axiom of unions)" consts UGe :: "sT => sT" notation UGe ("geU") and UGe ("geU") axiomatization where Ax_un: "x inP geU r = (? u. x inP u & u inP r)" --"[END]" --"EXAMPLE (A typedef type cannot be treated as a set of type sT)" typedef tdLift = "{x::sT. x = {.emS,emS.}}" by(simp) setup_lifting type_definition_tdLift instantiation tdLift :: semigroup_add begin lift_definition plus_tdLift:: "tdLift => tdLift => tdLift" is "% x y. {.emS,emS.}" by(simp) instance proof fix nmq :: tdLift show "(n + m) + q = n + (m + q)" by(transfer,simp) qed end theorem "((n::tdLift) + m) + q = n + (m + q)" by(transfer,simp) class tdClass = fixes emSc :: "'a" ("emSk") fixes inPc :: "'a => 'a => bool" (infix "∈k" 51) fixes paSc :: "'a => 'a => 'a" ("({.(_),(_).}k)") fixes geUc :: "'a => 'a" ("⋃k") instantiation tdLift :: tdClass begin lift_definition inPc_tdLift:: "tdLift => tdLift => bool" is "% x y. x inP y" by(simp) lift_definition paSc_tdLift:: "tdLift => tdLift => tdLift" is "% x y. {.x,y.}" --"OUTPUT: 1. (!! (sT1 sT2). ([|(sT1 = emS); (sT2 = emS)|] ==> ({.sT1,sT2.} = emS)))" apply(auto) --"OUTPUT: 1. ({.emS.} = emS)" oops lift_definition geUc_tdLift:: "tdLift => tdLift" is "% x. geU x" --"OUTPUT: 1. (!! sT. ((sT = {.emS,emS.}) ==> ((geU sT) = {.emS,emS.})))" apply(auto) --"OUTPUT: 1. ((geU {.emS,emS.}) = {.emS,emS.})" oops lift_definition emSc_tdLift:: "tdLift" is "emS" --"OUTPUT: exception THM 1 raised (line 333 of drule.ML): RSN: no unifiers (?t = ?t) [name HOL.refl] ((emS = {.emS,emS.}) ==> (Lifting.invariant (% x. (x = {.emS,emS.})) emS emS))" oops instance .. end --"[END]" end
+1
source share
1 answer

I partially answer my question, and part of the reason is to refer to this when I ask a question about Isar subtypes. Apparently, my question and answer here are related to subtypes.

As for whether I can fix the problem with the types of classes that I described, I don't know about that.

(UPDATE: the likely solution for my use of type classes will be a combination of ideas, part of the solution of which is a type of coercion, as explained in the answer to my question SO: What is an Isabelle / HOL subtype? What Isar commands produce subtypes?

If you use locales in Group.thy, this is the way for me, then the corresponding class classes for these locales will probably work as well. I can instantiate a class such as semigroup_add , use lift_definition to define the plus operator, and even raise my statements that return bool to type. Operators that cannot be raised to a new type are in any case completely meaningless in the context of the new type, and the type of coercion can come into play in order to understand them for such things as union sets. The devil is in the details .)

With what I said, I want from types and subtypes, I realized that I get the form of this using typedef , the form is the Rep and Abs functions that I worked with a bit.

As described in isar-ref.pdf pg. 242 ,

For typedef t = A, the newly introduced type t is followed by a pair of morphisms to associate it with a representative set of the old type. By default, injection from type to set is called Rep t and its inverse abs ...

Below I use Rep and Abs in a small example to demonstrate that I can associate my main type sT with a new type, which I define with typedef , which is the type tsA .

I do not think class classes are crucial. There are two main things that I study,

  • can I associate myself with Groups.thy,
  • where the use of types is mainly used to restrict the domain and sodomain of binary operators of my semigroups, groups, etc.

For example, in Groups.thy there is

 locale semigroup = fixes f :: "'a => 'a => 'a" (infixl "*" 70) assumes assoc [ac_simps]: "a * b * c = a * (b * c)"

If I do not use subtypes, I think I will need to do something like this, where inP is my \<in> (I’m just starting with locales):

 locale sgA = fixes G :: sT fixes f :: "sT => sT => sT" (infixl "*" 70) assumes closed: "(a inP G) & (b inP G) --> (a * b) inP G" assumes assoc: "(a inP G) & (b inP G) & (c inP G) --> (a * b) * c = a * (b * c)"

Part of the answer when using Groups.semigroup may be to use Rep and Abs ; I use a type operator tsA => tsA => tsA for type tsA , but when elements of type tsA should be considered elements of type sT , I use Rep for them to match them to type sT .

I did not think about it or experimented enough to know what would work best, but I gave this partial answer to try to explain more of what is on my mind. There might be someone else out there with good information to add.

Subtypes of approaches may not be all up, as shown below by the last two theorem commands in the sample code. The left side of the consequences is necessary because I do not use the type power similar to closed and assoc above in locale sgA . However, despite this, this is not a problem for my simp rules, while theorems using Rep and Abs require metis to prove it, and it can take a lot of ugly overhead to make things work more smoothly.

Below I include the file A_iSemigroup_xp.thy . This is the ASCII version of iSemigroup_xp.thy . This requires importing MFZ.thy , where these 3 files are located in this GitHub folder .

 theory A_iSemigroup_xp imports MFZ begin --"[END]" --"EXAMPLE (Possible subtype for a trivial semigroup)" typedef tsA = "{x::sT. x = emS}" by(simp) theorem "(Rep_tsA x) inP {.Rep_tsA x.}" by(metis SSi_exists) theorem "! x::tsA. x = (Abs_tsA emS)" by(metis (lifting, full_types) Abs_tsA_cases mem_Collect_eq) theorem "! x. x inP {.emS.} --> x = emS" by(simp) theorem "! x. x inP {.z inP {.emS.} ¦ z = emS.} --> x = emS" by(simp) --"[END]" --"ISAR (Theory end)" end
+1
source

More articles:


All Articles