Theory Autogen.AutoLocality_Test0

(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
   SPDX-License-Identifier: MIT *)

(*<*)
theory AutoLocality_Test0
  imports AutoLens AutoLocality
begin
(*>*)

datatype_record foo =
  beef :: nat
  ham :: nat
  cheese :: nat

definition has_beef :: ‹foo ⇒ bool› where
  ‹has_beef f ≡ beef f > 0›

definition has_beef_many :: ‹foo ⇒ foo ⇒ bool› where
  ‹has_beef_many x y ≡ beef x > 0›

definition has_ham :: ‹foo ⇒ bool› where
  ‹has_ham f ≡ ham f > 0›

definition has_beef2 :: ‹foo ⇒ nat ⇒ bool› where
  ‹has_beef2 f n ≡ beef f > n›

definition set_beef :: ‹nat ⇒ foo ⇒ foo› where
  ‹set_beef k ≡ update_beef (λ_. k)›

definition set_ham :: ‹nat ⇒ foo ⇒ foo› where
  ‹set_ham k ≡ update_ham (λ_. k)›

definition set_ham2 :: ‹foo ⇒ nat ⇒ foo› where
  ‹set_ham2 n k ≡ update_ham (λ_. k) n›

abbreviation set_cheese :: ‹nat ⇒ foo ⇒ foo› where
  ‹set_cheese k ≡ update_cheese (λ_. k)›

definition set_cheese2 :: ‹foo ⇒ nat ⇒ foo› where
  ‹set_cheese2 n k ≡ update_cheese (λ_. k) n›

locality_lemma for foo: ‹set_ham› footprint [ham] .
locality_lemma for foo: ‹set_beef› footprint [beef] .

print_theorems

locality_lemma for foo: ‹has_beef› footprint [beef] .
locality_lemma for foo: ‹has_beef_many› [0] footprint [beef] .
locality_lemma for foo: ‹has_beef_many› [1] footprint [beef] .

print_theorems
print_locality_data

locality_lemma for foo: ‹has_ham› footprint [ham] .

print_theorems

locality_autoderive

print_theorems

locality_autoderive

print_theorems

print_locality_data for foo

locality_check

locality_lemma for foo: ‹has_beef2› footprint [beef] .
locality_lemma for foo: ‹set_cheese 10› footprint [cheese, beef] .
locality_lemma for foo: ‹set_cheese2› footprint [cheese] .

print_theorems

locality_check

locality_autoderive for foo

datatype_record ('a, 'b) foo2 =
  beef :: 'a
  ham :: 'b
  cheese :: 'b

local_setup ‹lens_autogen_defs "foo2"›
local_setup ‹lens_autogen_defining_equations @{attributes []} "foo2"›
local_setup ‹lens_autogen_prove_lens_validity @{attributes []} "foo2"›
ML ‹@{term ‹foo2.beef›}›
local_setup‹focus_autogen_make_field_foci @{attributes []} "foo2"›

export_code foo2_beef_focus in OCaml

value [code] ‹focus_view foo2_beef_focus (make_foo2 (0 :: nat) 0 (0 :: nat))›

definition set_bham :: ‹'b ⇒ ('a, 'b) foo2 ⇒ ('a, 'b) foo2› where
  ‹set_bham k ≡ update_ham (λ_. k)›
locality_lemma for foo2: set_bham footprint [ham]  .

definition set_bcheese :: ‹nat ⇒ ('a, nat) foo2 ⇒ ('a, nat) foo2› where
  ‹set_bcheese k ≡ update_cheese (λ_. k)›
locality_lemma for foo2: set_bcheese footprint [cheese] .

print_theorems
print_locality_data
locality_check

print_locality_data

thm AutoLocality_Test0_foo_locality_facts
thm AutoLocality_Test0_foo_commutativity_facts

lemma
  shows ‹has_ham (set_ham h (set_beef b X)) = has_ham (set_ham h X)›
using [[locality_cancel]] by simp

lemma
  shows ‹has_ham (set_ham h (foo.update_beef b (set_ham h2 (set_cheese2 (set_cheese2 X d) c)))) =
          has_ham (set_ham h (set_ham h2 X))›
using [[locality_cancel]] by simp

locale foo_locale =
    fixes some_fun :: ‹'a ⇒ 'a›
  assumes some_fun_invo: ‹some_fun ∘ some_fun = id›
begin

definition map_beef_via_fun :: ‹('a, 'a) foo2 ⇒ ('a, 'a) foo2› where
  ‹map_beef_via_fun ≡ update_beef some_fun›

locality_lemma for foo2: map_beef_via_fun footprint [beef]
  by (auto simp add: map_beef_via_fun_def)

definition map_ham_via_fun :: ‹('a, 'a) foo2 ⇒ ('a, 'a) foo2› where
  ‹map_ham_via_fun ≡ update_ham some_fun›

thm map_beef_via_fun_def

locality_lemma for foo2: map_ham_via_fun footprint [ham]
  by (auto simp add: map_ham_via_fun_def)

locality_autoderive for foo2

print_theorems
print_locality_data

end

print_locality_data

context foo_locale
begin

print_locality_data

end

datatype_record TestRec =
  my_field0 :: int
  my_field1 :: int

definition test_get0 :: ‹TestRec ⇒ int› where
  ‹test_get0 r ≡ my_field0 r›

context
begin

qualified datatype_record test_rec' =
  my_field0 :: int
  my_field :: int

qualified definition test_get0' :: ‹test_rec' ⇒ int› where
  ‹test_get0' r ≡ my_field0 r›

end

(*<*)
end
(*>*)