From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
Dear all,
I define some general term type
datatype 'a trm = App "'a trm" "'a trm" | Const string | Var 'a
Now I want to embed a specific type of terms into this general type,
namely a type of order terms. The inequality between two variables x and
y would be
App (App (Const ''LE'') (Var x)) (Var y)
In order to achieve this, I first define a predicate on 'a trm which is
true for terms that are order terms. Then I use typedef to introduce a
subtype that only contains order terms. Since I also want to define
functions using pattern matching on this subtype, I am using
free_constructors to introduce constructors for the different types of
order terms; however, generating code for the following lifted definition
lift_definition trm_of_order_trm :: "'a order_trm ⇒ 'a trm" is id .
now doesn't work since it now uses Rep_order_trm. One can prove the code
equation manually (see below) but is there a way to derive it automatically?
Cheers,
Lukas
Full example:
theory Scratch imports Main
begin
datatype 'a trm = App "'a trm" "'a trm" | Const string | Var 'a
fun is_order_trm :: "'a trm ⇒ bool" where
"is_order_trm (App (App (Const c) (Var x)) (Var y)) ⟷ c = ''LE'' ∨ c = ''LT'' ∨ c = ''EQ''" |
"is_order_trm _ ⟷ False"
typedef 'a order_trm = "{t::'a trm. is_order_trm t}"
by (metis is_order_trm.simps(1) mem_Collect_eq)
setup_lifting type_definition_order_trm
abbreviation (input) "App2ConstVars c x y ≡ (App (App ((Const c)) (Var x)) (Var y))"
abbreviation (input) "CtorOrder c x y ≡ Abs_order_trm (App2ConstVars c x y)"
definition "CtorLE ≡ CtorOrder ''LE''"
definition "CtorLT ≡ CtorOrder ''LT''"
definition "CtorEQ ≡ CtorOrder ''EQ''"
lemmas order_ctor_defs = CtorLE_def CtorLT_def CtorEQ_def
lemma order_trm_cases:
fixes t :: "'a order_trm"
obtains
(LE) x y where "t = CtorLE x y"
| (LT) x y where "t = CtorLT x y"
| (EQ) x y where "t = CtorEQ x y"
proof(cases t)
case (Abs_order_trm t')
then have "is_order_trm t'"
by simp
then show ?thesis using that Abs_order_trm
apply(induction t' rule: is_order_trm.induct)
by (auto simp: order_ctor_defs)
qed
lift_definition trm_of_order_trm :: "'a order_trm ⇒ 'a trm" is id .
free_constructors case_order_trm for
"CtorLE" | "CtorLT" | "CtorEQ"
apply(fact order_trm_cases)
by (auto simp: order_ctor_defs Abs_order_trm_inject)
text ‹I want to define functions on @{typ "'a order_trm"} using pattern matching›
fun sem :: "'a rel ⇒ 'a order_trm ⇒ bool" where
"sem r (CtorLE x y) ⟷ (x, y) ∈ r" |
"sem r (CtorLT x y) ⟷ (x, y) ∈ r ∧ x ≠ y" |
"sem r (CtorEQ x y) ⟷ x = y"
definition "Sem r A ≡ (∀t ∈ A. sem r t)"
lemma "¬ Sem r {CtorLT x y, CtorEQ x y}"
unfolding Sem_def
by simp
text ‹
Exporting code only works if I prove the following code equation manually.
Can it be derived automatically?
›
lemma [code]:
"Rep_order_trm t = (case t of
CtorLE x y ⇒ App2ConstVars ''LE'' x y
| CtorLT x y ⇒ App2ConstVars ''LT'' x y
| CtorEQ x y ⇒ App2ConstVars ''EQ'' x y)"
by (auto split: order_trm.splits simp: Abs_order_trm_inverse order_ctor_defs)
export_code sem trm_of_order_trm in SML
value "Sem {(1::nat, 2)} {(CtorEQ 1 2), (CtorLT 1 2)}"
Last updated: Mar 29 2024 at 12:28 UTC