Suppose I have a binary operator f :: "sT => sT => sT"
. I want to define f
so that it implements a 4x4 multiplication table for the Klein four group, shown here on the Wiki:
http://en.wikipedia.org/wiki/Klein_four-group
Here, all I'm attempting to do is create a table with 16 entries. First, I define four constants like this:
consts
k_1::sT
k_a::sT
k_b::sT
k_ab::sT
Then I define my function to implement the 16 entries in the table:
k_1 * k_1 = k_1
k_1 * k_a = k_a
...
k_ab * k_ab = k_1
I don't know how to do any normal-like programming in Isar, and I've seen on the Isabelle user's list where it was said that (certain) programming-like constructs have been intentionally de-emphasized in the language.
The other day, I was trying to create a simple, contrived function, and after finding the use of if, then, else
in a source file, I couldn't find a reference to those commands in isar-ref.pdf.
In looking at the tutorials, I see definition
for defining functions in a straightforward way, and other than that, I only see information on recursive and inductive functions, which require datatype
, and my situation is more simple than that.
If left to my own devices, I guess I would try and define a datatype
for those 4 constants shown above, and then create some conversion functions so that I end up with a binary operator f :: sT => sT => sT
. I messed around a little with trying to use fun
, but it wasn't turning out to be a simple deal.
I had done a little experimenting with fun
and inductive
UPDATE: I add some material here in response to the comment telling me that Programming and Proving is where I'll find the answers. It seems I might be going astray of the ideal Stackoverflow format.
I had done some basic experimenting, mainly with fun
, but also with inductive
. I gave up on inductive fairly fast. Here's the type of error I got from simple examples:
consts
k1::sT
inductive k4gI :: "sT => sT => sT" where
"k4gI k1 k1 = k1"
--"OUTPUT ERROR:"
--{*Proofs for inductive predicate(s) "k4gI"
Ill-formed introduction rule ""
((k4gI k1 k1) = k1)
Conclusion of introduction rule must be an inductive predicate
*}
My multiplication table isn't inductive, so I didn't see that inductive
was what I should spend my time chasing.
"Pattern matching" seems a key idea here, so I experimented with fun
. Here's some really messed up code trying to use fun
with only a standard function type:
consts
k1::sT
fun k4gF :: "sT => sT => sT" where
"k4gF k1 k1 = k1"
--"OUTPUT ERROR:"
--"Malformed definition:
Non-constructor pattern not allowed in sequential mode.
((k4gF k1 k1) = k1)"
I got that kind of error, and I had read things like this in Programming and Proving:
"Recursive functions are defined with fun by pattern matching over datatype constructors.
That all gives a novice the impression that fun
requires datatype
. As far its big brother function
, I don't know about that.
It seems here, all I need is a recursive function with 16 base cases, and that would define my multiplication table.
Is function
the answer?
In editing this question, I remembered function
from the past, and here's function
at work:
consts
k1::sT
function k4gF :: "sT => sT => sT" where
"k4gF k1 k1 = k1"
try
The output of try is telling me it can be proved (Update: I think it's actually telling me that only 1 of the proof steps can be prove.):
Trying "solve_direct", "quickcheck", "try0", "sledgehammer", and "nitpick"...
Timestamp: 00:47:27.
solve_direct: (((k1, k1) = (k1, k1)) ⟹ (k1 = k1)) can be solved directly with
HOL.arg_cong: ((?x = ?y) ⟹ ((?f ?x) = (?f ?y))) [name "HOL.arg_cong", kind "lemma"]
HOL.refl: (?t = ?t) [name "HOL.refl"]
MFZ.HOL⇣'eq⇣'is⇣'reflexive: (?r = ?r) [name "MFZ.HOL⇣'eq⇣'is⇣'reflexive", kind "theorem"]
MFZ.HOL_eq_is_reflexive: (?r = ?r) [name "MFZ.HOL_eq_is_reflexive", kind "lemma"]
Product_Type.Pair_inject:
(⟦((?a, ?b) = (?a', ?b')); (⟦(?a = ?a'); (?b = ?b')⟧ ⟹ ?R)⟧ ⟹ ?R)
[name "Product_Type.Pair_inject", kind "lemma"]
I don't know what that means. I only know about function
because of trying to prove an inconsistency. I only know it doesn't complain as much. If using function
like this is how I define my multiplication table, then I'm happy.
Still, being an argumentative type, I didn't learn about function
in a tutorial. I learned about it several months ago in a reference manual, and I still don't know much about how to use it.
I have a function
which I prove with auto
, but the function is probably no good, fortunately. That adds to the function
's mystery. There's information on function
in Defining Recursive Functions in Isabelle/HOL, and it compares fun
and function
.
However, I haven't seen one example of fun
or function
that doesn't use a recursive datatype, such as nat
or 'a list
. Maybe I didn't look hard enough.
Sorry for being verbose and this not ending up as a direct question, but there's no tutorial with Isabelle that takes a person directly from A to B.
inductive
do require data types. Both are general constructs. A good point to start if you are interested in programming inside HOL would be Programming and Proving in Isabelle/HOL. – chrisdatatype
is not required, and that I don't need to work through that PDF, but I don't expect to find an example in that PDF that I can use as a plug'n'play example. – user2190811datatype
to makefun
happy. It seems to me all I need is some simple pattern matching. All of my basic experimenting and surfing through the docs did nothing but give me the impression thatfun
needs an inductive datatype, because it does recursion. Everything I've read in the basic docs, as far as pattern matching, emphasizes the connections betweenfun
,inductive
, anddatatype
. It helps to knowdatatype
is not required, but it's not obvious where to learn the basics to not usedatatype
. – user2190811fun
withdatatype
? Looking at Haskell, according to this page, a new Haskell type requires it be defined when it's created. Isar allows an arbitrary undefined type withtypedecl
, and arbitrary constants withconsts
. If someone doesn't want to answer a question, that's understandable, but frequently pointing to a 57 pg PDF for every "beginner question" is not that helpful. – user2190811