Trying to Treat Type Classes and Sub-types Like Sets and Subsets

Question

This question is related to my previous SO question about type classes. I ask this question to set up a future question about locales. I don't think type classes will work for what I'm trying to do, but how type classes work have given me ideas about what I want out of locales.

Below, when I use the braces notation {0,0}, it doesn't represent the normal HOL braces, and 0 represents the empty set.

Some files if you want them

A_i130424a.thy - ASCII friendly THY.
i130424a.thy - non-ASCII friendly THY.
i130424a_DOC.pdf - PDF showing line numbers.
MFZ_DOC.pdf - Main project this is related to.
GitHub folder for this question and MFZ GitHub folder.

Pre-question talk

I describe what I'm doing in the THY (which I include at the bottom), 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 linked to above, I'm trying to tie into Groups.thy semigroup_add. What I do is create a subtype of my type sT using typedef, and I then try to lift some of my essential function constants and operators into the new type, such as my union operator geU, my empty set emS, my unordered pair sets paS, and my membership predicate inP.

This doesn't work because I'm trying to treat the new type like a subset. In particular, my new type is supposed to represent the set { {0,0} }, which is intended to be part of the trivial semigroup, a semigroup with only one element.

The problem is that the unordered pair axiom states that if set x exists, then set (paS x x) exists, and the union axiom states that if set x exists, then set (geU x) exists. So, when I try to lift my union operator into my new type, the prover magically knows I need to prove (geU{0,0} = {0,0}), which is not true, but there's only one element {0,0} in my new type, so it would have to be that way.

Question

Can I fix this? In my mind, I'm comparing sets and subsets with types and sub-types, where I know they're not the same. Call my main type sT and my subtype subT. What I need is for all my operators that have been defined with type sT, types such as sT => sT, to work for type subT when subT is being treated as type sT. The new operators and constants that have been defined using type subT, such as a function of type subT => subT, that would somehow work out like things are magically supposed to work with these things.

Post question talk

Here, I point out what's happening by line number in the THY. The line numbers will show up in the PDF and on the GitHub site.

In lines 21 to 71 there are four sections where I combined related constants, notation, and an axiom.

Type sT, membership predicate inP/PIn, and equality axiom (21 to 33).
Empty set emS/SEm and empty set axiom (37 to 45).
Unordered pair constant paS/SPa and unordered pair axiom (49 to 58).
Union constant geU/UGe and union axiom (62 to 71).

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

There are no problems until I try to lift my unordered pair function {.x,y.}, line 108, and my union function (geU x), line 114.

Below the Isar commands, I show the output that's telling me I need to prove that certain sets are equal to {0,0}, a fact that cannot be proved.

Here is the ASCII friendly source, where I've deleted some comments and lines from the THY linked to 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 n m q :: 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

Trying to Treat Type Classes and Sub-types Like Sets and Subsets

Some files if you want them

Pre-question talk

Question

Post question talk

Answers (1)

Related Questions