Определение quotient_type в Isabelle

Question

Я все еще пытаюсь рассуждать о семантическом равенстве в Изабель. Я хочу сравнить две формулы и посмотреть, равны ли они. Мне сказали, что для этого мне нужны quotienttypes. Итак, я попытался определить себе тип quotiernttype, но, по моему мнению, мое определение не является полным, так как я, похоже, не умею писать код после моего определения. Моего кода до сих пор:

theory Scratch 
imports Main 
begin 
no_notation plus (infixl "+" 65) 

typedecl basicForm 
datatype form_rep = af basicForm 
axiomatization 
equals :: "form_rep ⇒ form_rep ⇒ bool" (infix "≐" 1) and 
plus :: "form_rep ⇒ form_rep ⇒ form_rep" (infixl "+" 35) 
    where 
    reflexive: "x ≐ x" and 
    symmetric: "x ≐ y ⟹ y ≐ x" and 
    transitiv: "x ≐ y ⟹ y ≐ z ⟹ x ≐ z" and 

    commut: "x + y   ≐ y + x" and 
    associatPlus: "(x + y) + z ≐ x + (y + z)" and 
    idemo: "x + x   ≐ x" 

quotient_type formula = "form_rep"/"equals" 

У меня есть некоторые основные формулы и сложный вариант этого и я хочу рассуждать над сложным типом, таким образом, я определен на равном с тремя аксиомами для равенства отношений и 3 дополнительных легкие аксиомы.

Редактирование: Порой я идиот, который забыл добавить котировочные знаки -.- до сих пор не знает, как продолжить дальше от мысли.

Answer 1

Команды quotient_type требуют правильного завершения проверки. Посмотрите на доказательство состояния, что нужно доказать. Такие вещи прямо или косвенно объясняются в руководстве isar-ref.

несвязанные примечания:

• Лучше избегать повторного использования элементарного обозначения как +. Панель Symbols в Prover IDE предоставляет множество альтернатив.

• Лучше избегать аксиоматизации свободной формы, особенно для первоначальных примеров. Просто то, что Isabelle/HOL предоставляет уже, и сделать определения на вершине, что (datatype, definition, inductive, fun и т.д.)

• верблюдах случай не используется в Изабеллу.