Wie generiert man einen Code für BNF?

Question

Ich versuche, einen benutzerdefinierten Satz Typ zu definieren:

notation bot ("⊥") 

typedef 'a myset = "UNIV :: 'a fset option set" .. 

definition myset :: "'a fset ⇒ 'a myset" where 
    "myset b = Abs_myset (Some b)" 

instantiation myset :: (type) bot 
begin 
definition "⊥ = Abs_myset None" 
instance .. 
end 

free_constructors case_myset for 
    myset 
| "⊥ :: 'a myset" 
    apply (simp_all add: bot_myset_def myset_def) 
    apply (metis Rep_myset_inverse option.collapse) 
    apply (metis Abs_myset_inverse iso_tuple_UNIV_I option.inject) 
    apply (metis Abs_myset_inverse iso_tuple_UNIV_I option.distinct(1)) 
    done 

copy_bnf 'a myset 

value "map_myset (λx. x + 1) (myset {|1::int,2|})" 

Es scheint, dass ein Code nicht für map_myset Funktion generiert wurde. So kann value den Ausdruck in der letzten Zeile nicht vereinfachen.

Ich versuche, den Code Gleichung für map_myset zu definieren: kann

lemma map_myset_code [code]: 
    "map_myset f xs = (case xs 
    of myset fxs ⇒ myset (f |`| fxs) 
    | ⊥ ⇒ ⊥)" 
    apply (simp add: map_myset_def) 
    apply (cases xs) 
    apply (auto simp add: myset_def Abs_myset_inverse) 

Aber ich nicht beweisen, dass es Korrektheit ist, weil map_myset definiert wird MySetTest.myset.option.map_option:

map_myset ≡ λf. Abs_myset ∘ MySetTest.myset.option.map_option f ∘ Rep_myset 

Wie finde ich eine Definition von diese Funktion? Ist es möglich, automatisch einen Code für eine BNF zu generieren?

Answer 1

Wenn Sie an Code interessiert sind, würde ich vorschlagen, das Heben/Transfer-Paket zu verwenden, anstatt direkt Abs/Rep usw. zu verwenden. Dann erhalten Sie in vielen Fällen Code kostenlos.

notation bot ("⊥") 

typedef 'a myset = "UNIV :: 'a fset option set" .. 

setup_lifting type_definition_myset 

lift_definition myset :: "'a fset ⇒ 'a myset" is Some . 

instantiation myset :: (type) bot 
begin 
lift_definition bot_myset :: "'a myset" is None . 
instance .. 
end 

lift_definition map_myset :: "('a ⇒ 'b) ⇒ 'a myset ⇒ 'b myset" 
    is "map_option o fimage" . 

lift_definition of_fset :: "'a fset ⇒ 'a myset" is Some . 

value "map_myset (λx. x + 1) (of_fset {|1::int,2|})" 

Ich hoffe, das hilft, René