Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error

On 1/21/2013 8:55 AM, Andreas Lochbihler wrote:
The error remains because
1. you did not declare the axiom Ax_x as a code equation, and
2. it is not executable as the !x-quantifier ranges over sT for which you have not provided an implementation.

The code generator will not work unless you provide a concrete representation for the elements of sT.


"Satisfying the code generator" falls under what I had talked about needing, which is "knowing more". The learning curve for "more" in regards to the foundations of Isabelle is "huge", so I put that off for now. I consider what I'm trying to do as something that should be done by experts, but which the experts haven't taken time to do.

Still, the phrase "code generator" tells me what to search on to try and finish the problem, so thanks for the tip.

Even after only having made the statement "typedecl sT", HOL will prove
that "=" for type "sT" is reflexive, symmetric, and transitive.
No, it is not HOL that proves these three properties, = on any type is by axiom in HOL.thy reflexive, transitive and symmetric. As you use axiomatization, it is your job to make sure that your specification is consistent with HOL's axioms.

Being the argumentative type (GB::argumentative), I'm under the impression that I can restate any axiom or theorem and "prove it again", that with my reflexive, transitive, and symmetric proofs, I'm effectively proving "A --> A" for previous axioms or theorems "A" in HOL.thy. (I'm actually stating the 3 theorems after attaching additional properties to "=" with my axiom).

I had looked previously at the axioms for "=" here in HOL.thy:

axiomatization where
  refl: "t = (t::'a)" and
  subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and
  ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
-- {*Extensionality is built into the meta-logic, and this rule expresses a related property. It is an eta-expanded version of the traditional
         rule, and similar to the ABS rule of HOL*} and

  the_eq_trivial: "(THE x. x = a) = (a::'a)"

Number 1 is classic "reflexive", number 2 makes sense, but I quit at 3 and 4 at trying to understand why this gives us all the typical properties of equality.

In the past, I had wondered whether HOL "=" has any special properties that would result in inconsistencies once my axiom was attached to it for type sT. Makarius said, paraphrasing, "HOL equal just has the typical properties of equal." I decided, "Okay, then I'll consider that until I attach additional properties to it for my type sT, that it's simply reflexive, symmetric, and transitive." Consequently, I do proofs for those 3 things regardless of what I read in HOL.thy or what you or Makarius tell me.

I looked now a little further at this "equal is symmetric" theorem in HOL.thy:

lemma sym: "s = t ==> t = s"
  by (erule subst) (rule refl)

Still, my three theorems aren't exact restatements of anything in HOL. (I didn't actually look much past "lemma sym", so they could be.) If they are restatements, it doesn't hurt to prove them again after I add my own "equality" axiom.

If you say, "You're restating the obvious", I would say, "But in Isabelle, with automatic proof methods, it's so easy to restate and prove the obvious. So I do it to be explicit, and to show what I can't know or haven't taken time to know based on "imports Complex_Main".

As you use axiomatization, it is your job to make sure that your specification is consistent with HOL's axioms.

And that is a major concern of mine, and my fFOLdt and fFOLf idea was an attempt to deal with unknowns that might cause my logic to be inconsistent.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.