(*  Title:      HOL/Metis_Examples/Proxies.thy
    Author:     Jasmin Blanchette, TU Muenchen

Example that exercises Metis's and Sledgehammer's logical symbol proxies for
rudimentary higher-order reasoning.
*)

section ‹
  that Exercises Metis's and Sledgehammer's Logical Symbol Proxies for
  Higher-Order Reasoning.
 ›

theory Proxies
imports Type_Encodings
begin

sledgehammer_params [prover = spass, fact_filter = mepo, slices = 1, timeout = 30,
  preplay_timeout = 0, dont_minimize]

text ‹Extensionality and set constants›

lemma plus_1_not_0: "n + (1::nat) ≠ 0"
by simp

definition inc :: "nat → nat" where
"inc x = x + 1"

lemma "inc ≠ (λy. 0)"
sledgehammer [expect = some] (inc_def plus_1_not_0)
by (metis_exhaust inc_def plus_1_not_0)

lemma "inc = (λy. y + 1)"
sledgehammer [expect = some]
by (metis_exhaust inc_def)

definition add_swap :: "nat → nat → nat" where
"add_swap = (λx y. y + x)"

lemma "add_swap m n = n + m"
sledgehammer [expect = some] (add_swap_def)
by (metis_exhaust add_swap_def)

definition "A = {xs::'a list. True}"

lemma "xs ∈ A"
(* The "add:" argument is unfortunate. *)
sledgehammer [expect = some] (add: A_def mem_Collect_eq)
by (metis_exhaust A_def mem_Collect_eq)

definition "B (y::int) ≡ y ≤ 0"
definition "C (y::int) ≡ y ≤ 1"

lemma int_le_0_imp_le_1: "x ≤ (0::int) ==> x ≤ 1"
by linarith

lemma "B ≤ C"
sledgehammer [expect = some]
by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)

text ‹Proxies for logical constants›

lemma "id (=) x x"
sledgehammer [type_enc = erased, expect = none] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis (full_types) id_apply)

lemma "id True"
sledgehammer [type_enc = erased, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)

lemma "¬ id False"
sledgehammer [type_enc = erased, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)

lemma "x = id True ∨ x = id False"
sledgehammer [type_enc = erased, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)

lemma "id x = id True ∨ id x = id False"
sledgehammer [type_enc = erased, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)

lemma "P True ==> P False ==> P x"
sledgehammer [type_enc = erased, expect = none] ()
sledgehammer [type_enc = poly_args, expect = none] ()
sledgehammer [type_enc = poly_tags??, expect = some] ()
sledgehammer [type_enc = poly_tags, expect = some] ()
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] ()
sledgehammer [type_enc = mono_tags??, expect = some] ()
sledgehammer [type_enc = mono_tags, expect = some] ()
sledgehammer [type_enc = mono_guards??, expect = some] ()
sledgehammer [type_enc = mono_guards, expect = some] ()
by (metis (full_types))

lemma "id (¬ a) ==> ¬ id a"
sledgehammer [type_enc = erased, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)

lemma "id (¬ ¬ a) ==> id a"
sledgehammer [type_enc = erased, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by metis_exhaust

lemma "id (¬ (id (¬ a))) ==> id a"
sledgehammer [type_enc = erased, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)

lemma "id (a ∧ b) ==> id a"
sledgehammer [type_enc = erased, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)

lemma "id (a ∧ b) ==> id b"
sledgehammer [type_enc = erased, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)

lemma "id a ==> id b ==> id (a ∧ b)"
sledgehammer [type_enc = erased, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)

lemma "id a ==> id (a ∨ b)"
sledgehammer [type_enc = erased, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)

lemma "id b ==> id (a ∨ b)"
sledgehammer [type_enc = erased, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)

lemma "id (¬ a) ==> id (¬ b) ==> id (¬ (a ∨ b))"
sledgehammer [type_enc = erased, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)

lemma "id (¬ a) ==> id (a ⟶ b)"
sledgehammer [type_enc = erased, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)

lemma "id (a ⟶ b) ⟷ id (¬ a ∨ b)"
sledgehammer [type_enc = erased, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
by (metis_exhaust id_apply)

end