HasCASL subsort coding: make subsort graph explicit

[till]

When coding out subsorting, make the subsort graph explicit, such that reasoning about the subsorts is possible. That is, introduce something like in the attached Isabelle file (which can also be translated to HasCASL). Possibly use graphs (only available in Isabelle 2007) instead of relations.

There should also be a direct CASL to Isabelle coding using this technology. This is needed for CspCASL-Prover, but it will also be useful for other means. The advantage of oging directly from CASL to Isabelle (without the way through HasCASL) is the avoidance of option types, one can use a polymorphic definedness predicate instead.

[maeder]

For data types with sub-sorts the injections are constructors that still need to be created individually.

[maeder]

Next problem: For subtypes of data types pattern matching does not longer work. This also happens with tuples in Categories_Coproduct.

[ewaryst]

I added a subtype predicate and the injection and projection function symbols with their axioms and some lemmas to the MainHCPairs.thy file. The following should suffice to have a good reasoning support for subtypes:

1. Don't add gn_inj and gn_proj during export to Isabelle, there are already in the MainHC...

2. Producing axioms for the subtype relations as "!!(x::Subtype) (y::Supertype). subt x y" for each subtype information. Alternativeley one can write it as:

"subt (x\<Colon>Subtype) (y\<Colon>Supertype)"

3. Predicate subtypes need type annotations in between the two arbitrary polymorphic functions defOp and gn_proj as in:

"ALL x. defOp (gn_proj(x)\<Colon>Subtype partial) = Subtypepredicate(x)"

in place of

"ALL x. defOp (gn_proj(x)) = Subtypepredicate(x)"

4. The point 3. generalizes to other "arbitrary polymorphic" function applications. One has to provide type annotations to fix the type variables to a single type. Arbitrary polymorphic means that the domain type is not inferable from the range type and vice versa. Consider this example:

"restrictOp (makePartial (a /' makeTotal (gn_proj(b))))

(defOp (gn_proj(b)))"

In the first occurrence of gn_proj one can infer its type from the type of b and from the types of the not arbitrary polymorphic functions makeTotal, makePartial and restrictOp. In the second occurrence we have an application of defOp to gn_proj, both arbitrary polymorphic functions, hence here we need type annotations to fix the type to the same type as of the first occurrence. Note that there are also terms where gn_proj or gn_inj occur with different type instantiations!

[maeder]

I need to generate the functions and all axioms anyway, because coding out sub-typing is a HasCASL to HasCASL translation (but I may omit the generation of the corresponding Isabelle functions)

X_gn_inj :: "'a => 'b" ("gn'_inj/'(_')" [3] 999)
X_gn_proj :: "'a => 'b partial" ("gn'_proj/'(_')" [3] 999)
X_gn_subt :: "'a => 'b => bool" ("gn'_subt/'(_,/ _')" [3,3] 999)

On the Isabelle side I do create all variables with types now. (This is not enough yet to disambiguate "(defOp (gn_proj(b)))".) Currently only constants can be type-annotated in our Isabelle logic, so I may generate the type instances for the above three functions.

I wonder why the injection function is total, but not "applicable" to types that are not in the subtype relation. Should "gn_inj" be a partial function (in HasCASL!), too?

[maeder]

The current state seems to work for Hets-lib/HasCASL/Real3D/SolidWorks/SolidWorks.het, X_gn_proj is output with its profile.

[maeder]

The monotonicities for the symbols in the overload relation need to be generated, too.