Theory Lifting_Definition_Option_Examples

(*  Title:       Lifting Definition Option
    Author:      René Thiemann       <rene.thiemann@uibk.ac.at>
    Maintainer:  René Thiemann
    License:     LGPL
*)

(*
Copyright 2014 René Thiemann

This file is part of IsaFoR/CeTA.

IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the
terms of the GNU Lesser General Public License as published by the Free Software
Foundation, either version 3 of the License, or (at your option) any later
version.

IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.  See the GNU Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public License along
with IsaFoR/CeTA. If not, see <http://www.gnu.org/licenses/>.
*)
theory Lifting_Definition_Option_Examples
imports  
  Main
begin

section ‹Examples›

subsection ‹A simple restricted type without type-parameters›

typedef "restricted" = "{ i :: int. i mod 2 = 0}" morphisms base "restricted"
  by (intro exI[of _ 4]) auto
setup_lifting type_definition_restricted

text ‹Let us start with just using a sufficient criterion for testing for even numbers,
  without actually generating them, i.e., where the generator is just the identity function.›
lift_definition(code_dt) restricted_of_simple :: "int ⇒ restricted option" is 
  "λ x :: int. if x ∈ {0, 2, 4, 6} then Some x else None" by auto

text ‹We can also take several input arguments for the test, and generate a more complex value.›
lift_definition(code_dt) restricted_of_many_args :: "nat ⇒ int ⇒ bool ⇒ restricted option" is 
  "λ x y (b :: bool). if int x + y = 5 then Some ((int x + 1) * (y + 1)) else None"
by clarsimp presburger

text ‹No problem to use type parameters.›
lift_definition(code_dt) restricted_of_poly :: "'b list ⇒ restricted option" is 
  "λ xs :: 'b list. if length xs = 2 then Some (int (length (xs))) else None" by auto

subsection ‹Examples with type-parameters in the restricted type.›

typedef 'f restrictedf = "{ xs :: 'f list. length xs < 3}" morphisms basef restrictedf 
  by (intro exI[of _ Nil]) auto
setup_lifting type_definition_restrictedf

text ‹It does not matter, if we take the same or different type-parameters in the lift-definition.›
lift_definition(code_dt) test1 :: "'g ⇒ nat ⇒ 'g restrictedf option" is 
  "λ (e :: 'g) x. if x < 2 then Some (replicate x e) else None" by auto

lift_definition(code_dt) test2 :: "'f ⇒ nat ⇒ 'f restrictedf option" is 
  "λ (e :: 'f) x. if x < 2 then Some (replicate x e) else None" by auto

text ‹Tests with multiple type-parameters.›
 
typedef ('a,'f) restr = "{ (xs :: 'a list,ys :: 'f list) . length xs = length ys}" 
  morphisms base' restr
  by (rule exI[of _ "([], [])"], auto) 
setup_lifting type_definition_restr

lift_definition(code_dt) restr_of_pair :: "'g ⇒ 'e list ⇒ nat ⇒ nat ⇒ ('e,nat) restr option" is
  "λ (z :: 'g) (xs :: 'e list) (y :: nat) n. if length xs = n then Some (xs,replicate n y) else None"
by auto

subsection ‹Example from \isafor/\ceta›

text ‹An argument filter is a mapping @{term π} from n-ary function symbols into 
lists of positions, i.e., where each position is between 0 and n-1. In \isafor,
(Isabelle's Formalization of Rewriting) and \ceta 
\<^cite>‹"DBLP:conf/tphol/ThiemannS09"›, the corresponding certifier for 
term rewriting related properties,
this is modelled as follows, where a partial argument filter in a map is extended to a full one 
by means of an default filter.›

typedef 'f af = "{ (π :: 'f × nat ⇒ nat list). (∀ f n. set (π (f,n)) ⊆ {0 ..< n})}" 
  morphisms af Abs_af by (rule exI[of _ "λ _. []"], auto)

setup_lifting type_definition_af

type_synonym 'f af_impl = "(('f × nat) × nat list)list"

fun fun_of_map_fun :: "('a ⇒ 'b option) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'b)" where 
  "fun_of_map_fun m f a = (case m a of Some b ⇒ b | None ⇒ f a)"

lift_definition(code_dt) af_of :: "'f af_impl ⇒ 'f af option" is
  "λ s :: 'f af_impl. if (∀ fidx ∈ set s. (∀ i ∈ set (snd fidx). i < snd (fst fidx)))
     then Some (fun_of_map_fun (map_of s) (λ (f,n). [0 ..< n])) else None"
using map_of_SomeD by (fastforce split: option.splits)

subsection ‹Code generation tests and derived theorems›
export_code 
  restricted_of_many_args
  restricted_of_simple
  restricted_of_poly
  test1
  test2
  restr_of_pair
  af_of
in Haskell

lemma restricted_of_simple_Some: 
  "restricted_of_simple x = Some r ⟹ base r = x"
using restricted_of_simple.rep_eq[of x]
apply (split if_splits)
apply (simp_all only: option.map option.inject option.simps(3))
done

end