Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation for a subtype with free_constr...


view this post on Zulip Email Gateway (Mar 02 2021 at 11:55):

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