Intentar tratar clases y subtipos de tipos como conjuntos y subconjuntos
Esta pregunta está relacionada con mi pregunta anterior sobre SOclases de tipo. Hago esta pregunta para configurar una pregunta futura sobre locales. No creo que las clases tipográficas funcionen para lo que estoy tratando de hacer, pero la forma en que funcionan las clases tipográficas me ha dado ideas sobre lo que quiero de los entornos locales.
Abajo, cuando uso la notación de llaves.{0,0}, no representa las llaves normales de HOL, y0 representa el conjunto vacío.
Describo lo que estoy haciendo en el THY (que incluyo en la parte inferior), y luego básicamente pregunto: "¿Hay algo que pueda hacer aquí para solucionar esto y poder usar clases de texto?"
Como en la pregunta de SO vinculada a arriba, estoy tratando de vincularme conGrupos.thy semigroup_add. Lo que hago es crear un subtipo de mi tiposT utilizandotypedef, y luego trato de incorporar algunas de mis constantes de funciones esenciales y operadores al nuevo tipo, como mi operador sindicalgeUmi conjunto vacíoemS, mis conjuntos de pares desordenadospaSy mi predicado de membresíainP.
Esto no funciona porque estoy tratando de tratar el nuevo tipo como un subconjunto. En particular, mi nuevo tipo se supone que representa el conjunto{ {0,0} }, que pretende ser parte del semigrupo trivial, un semigrupo con un solo elemento.
El problema es que el axioma de par desordenado indica que si se establecex existe, entonces establece(paS x x) Existe, y el axioma de unión establece que si se establecex existe, entonces establece(geU x) existe Entonces, cuando trato de incorporar a mi operador sindical a mi nuevo tipo, el prover mágicamente sabe que necesito probar(geU{0,0} = {0,0}), lo cual no es cierto, pero solo hay un elemento{0,0} en mi nuevo tipo, por lo que tendría que ser así.
¿Puedo arreglar esto? En mi opinión, estoy comparando conjuntos y subconjuntos con tipos y subtipos, donde sé que no son lo mismo. Llama a mi tipo principalsT y mi subtiposubT. Lo que necesito es para todos mis operadores que han sido definidos con tiposT, tipos comosT => sT, para trabajar por tiposubT cuandosubT está siendo tratado como tiposT. Los nuevos operadores y constantes que se han definido utilizando tipo.subT, tal como una función de tiposubT => subT, Eso de alguna manera funcionaría como si las cosas supieran mágicamente trabajar con estas cosas.
Aquí, señalo lo que está pasando por el número de línea en el THY. Los números de línea se mostrarán en el PDF y en el sitio de GitHub.
En las líneas 21 a 71 hay cuatro secciones donde combiné constantes relacionadas, notación y un axioma.
TiposTpredicado de membresíainP/PIn, y el axioma de igualdad (21 a 33).Conjunto vacioemS/SEm y vacíe el conjunto de axiomas (37 a 45).Constante de pares desordenadospaS/SPa y axioma de pares desordenados (49 a 58).Unión constantegeU/UGe y axioma de unión (62 a 71).A partir de la línea 75 es donde creo un nuevo tipo contypedef y luego instanciarlo como tipo de clasesemigroup_add.
No hay problemas hasta que intento levantar mi función de par desordenado{.x,y.}, línea 108, y mi función sindical.(geU x)linea 114.
Debajo de los comandos de Isar, muestro la salida que me dice que necesito probar que ciertos conjuntos son iguales a{0,0}, un hecho que no puede ser probado.
Aquí está la fuente amigable de ASCII, donde he eliminado algunos comentarios y líneas del THY enlazado anteriormente:
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