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 predicateinP/PIn, and equality axiom (21 to 33). - Empty set
emS/SEmand empty set axiom (37 to 45). - Unordered pair constant
paS/SPaand unordered pair axiom (49 to 58). - Union constant
geU/UGeand 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
