Theory Rhombus_HOL_Countermodels

(* SPDX-License-Identifier: 0BSD *)
(* Original countermodels over Isabelle/HOL's Nitpick interface. *)

theory Rhombus_HOL_Countermodels
  imports "HOL.Nitpick"
begin

text ‹These finite abstractions remove HOLZF's axiomatized universe from the
Nitpick search problem. Each datatype retains exactly the guard-relevant state.›

datatype ctype = CNum | CBool | CFun ctype ctype
datatype cterm =
    CFree nat ctype
  | CBound nat ctype
  | CConstant nat ctype
  | CApp cterm cterm
  | CLam ctype cterm

fun ctype_of :: "cterm ⇒ ctype option" where
  "ctype_of (CFree _ ty) = Some ty"
| "ctype_of (CBound _ ty) = Some ty"
| "ctype_of (CConstant _ ty) = Some ty"
| "ctype_of (CLam ty body) = map_option (CFun ty) (ctype_of body)"
| "ctype_of (CApp f x) =
    (case (ctype_of f, ctype_of x) of
       (Some (CFun dty cod), Some aty) ⇒ if dty = aty then Some cod else None
     | _ ⇒ None)"

fun guarded_check :: "ctype list ⇒ cterm ⇒ bool" where
  "guarded_check _ (CFree _ _) = True"
| "guarded_check env (CBound i ty) =
    (i < length env ∧ env ! i = ty)"
| "guarded_check _ (CConstant _ _) = True"
| "guarded_check env (CApp f x) =
    (guarded_check env f ∧ guarded_check env x ∧
      (case (ctype_of f, ctype_of x) of
         (Some (CFun dty _), Some aty) ⇒ dty = aty
       | _ ⇒ False))"
| "guarded_check env (CLam ty body) = guarded_check (ty # env) body"

fun weakened_check :: "ctype list ⇒ cterm ⇒ bool" where
  "weakened_check _ (CFree _ _) = True"
| "weakened_check env (CBound i _) = (i < length env)"
| "weakened_check _ (CConstant _ _) = True"
| "weakened_check env (CApp f x) =
    (weakened_check env f ∧ weakened_check env x ∧
      (case (ctype_of f, ctype_of x) of
         (Some (CFun dty _), Some aty) ⇒ dty = aty
       | _ ⇒ False))"
| "weakened_check env (CLam ty body) = weakened_check (ty # env) body"

fun subst_zero :: "cterm ⇒ cterm ⇒ cterm" where
  "subst_zero arg (CBound 0 _) = arg"
| "subst_zero _ (CBound (Suc i) ty) = CBound i ty"
| "subst_zero _ (CFree n ty) = CFree n ty"
| "subst_zero _ (CConstant n ty) = CConstant n ty"
| "subst_zero arg (CApp f x) = CApp (subst_zero arg f) (subst_zero arg x)"
| "subst_zero arg (CLam ty body) = CLam ty (subst_zero arg body)"

lemma binder_type_guard_countermodel:
  "∃aty body arg rty.
    weakened_check [] (CApp (CLam aty body) arg) ∧
    ctype_of (CApp (CLam aty body) arg) = Some rty ∧
    ctype_of (subst_zero arg body) ≠ Some rty"
  nitpick [card = 1-5, satisfy, expect = genuine, timeout = 30]
  by (rule exI[of _ CNum], rule exI[of _ "CBound 0 CBool"],
      rule exI[of _ "CConstant 0 CNum"], rule exI[of _ CBool]) simp

record cstamp =
  csid :: nat
  cgen :: nat
  cancestors :: "nat set"

definition comparable :: "cstamp ⇒ cstamp ⇒ bool" where
  "comparable a b ⟷ csid a ∈ cancestors b ∨ csid b ∈ cancestors a"

record cbranch =
  branch_stamp :: cstamp
  zero_meaning :: bool

definition safe_merge :: "cbranch ⇒ cbranch ⇒ cbranch option" where
  "safe_merge a b = (if comparable (branch_stamp a) (branch_stamp b)
    then Some b else None)"

definition generation_only_merge :: "cbranch ⇒ cbranch ⇒ cbranch option" where
  "generation_only_merge a b = (if cgen (branch_stamp a) = cgen (branch_stamp b)
    then Some b else None)"

definition conflicting_zero :: "cbranch ⇒ cbranch ⇒ bool" where
  "conflicting_zero a b ⟷ zero_meaning a ≠ zero_meaning b"

lemma lineage_sibling_countermodel:
  "∃a b. generation_only_merge a b = Some b ∧ safe_merge a b = None ∧
    conflicting_zero a b"
  nitpick [card = 1-5, satisfy, expect = genuine, timeout = 30]
  by (rule exI[of _
        "⦇branch_stamp = ⦇csid = 1, cgen = 1, cancestors = {0, 1}⦈,
           zero_meaning = False⦈"],
      rule exI[of _
        "⦇branch_stamp = ⦇csid = 2, cgen = 1, cancestors = {0, 2}⦈,
           zero_meaning = True⦈"])
    (simp add: generation_only_merge_def safe_merge_def comparable_def
      conflicting_zero_def)

datatype csymbol = CSymbol0 | CSymbol1

record csnapshot =
  snapshot_stamp :: cstamp
  declared_symbols :: "csymbol set"

record cproof =
  proof_stamp :: cstamp
  used_symbols :: "csymbol set"
definition proof_wf :: "csnapshot ⇒ cproof ⇒ bool" where
  "proof_wf thy th ⟷
    csid (proof_stamp th) ∈ cancestors (snapshot_stamp thy) ∧
    used_symbols th ⊆ declared_symbols thy"

definition stale_result :: "csnapshot ⇒ csymbol ⇒ cproof" where
  "stale_result old late =
    ⦇proof_stamp = snapshot_stamp old, used_symbols = {late}⦈"

lemma stale_stamp_countermodel:
  "∃old current late.
    late ∉ declared_symbols old ∧ late ∈ declared_symbols current ∧
    proof_wf current (stale_result old late) ∧
    ¬ proof_wf old (stale_result old late)"
  nitpick [card = 1-5, satisfy, expect = genuine, timeout = 30]
  by (rule exI[of _
        "⦇snapshot_stamp = ⦇csid = 0, cgen = 0, cancestors = {0}⦈,
           declared_symbols = {}⦈"],
      rule exI[of _
        "⦇snapshot_stamp = ⦇csid = 1, cgen = 1, cancestors = {0, 1}⦈,
           declared_symbols = {CSymbol1}⦈"],
      rule exI[of _ CSymbol1])
    (simp add: proof_wf_def stale_result_def)

datatype cinst_target = CInstVariable nat | CInstArbitrary cterm

fun replace_free :: "nat ⇒ cterm ⇒ cterm ⇒ cterm" where
  "replace_free n replacement (CFree m ty) =
    (if n = m then replacement else CFree m ty)"
| "replace_free _ _ (CBound i ty) = CBound i ty"
| "replace_free _ _ (CConstant n ty) = CConstant n ty"
| "replace_free n replacement (CApp f x) =
    CApp (replace_free n replacement f) (replace_free n replacement x)"
| "replace_free n replacement (CLam ty body) =
    CLam ty (replace_free n replacement body)"

fun guarded_inst :: "cinst_target ⇒ cterm ⇒ cterm ⇒ cterm option" where
  "guarded_inst (CInstVariable n) replacement source =
    Some (replace_free n replacement source)"
| "guarded_inst (CInstArbitrary _) _ _ = None"

fun weakened_inst :: "cinst_target ⇒ cterm ⇒ cterm ⇒ cterm option" where
  "weakened_inst (CInstVariable n) replacement source =
    Some (replace_free n replacement source)"
| "weakened_inst (CInstArbitrary _) _ source = Some source"

lemma inst_target_guard_countermodel:
  "∃target replacement source.
    weakened_inst target replacement source = Some source ∧
    guarded_inst target replacement source = None"
  nitpick [card = 1-5, satisfy, expect = genuine, timeout = 30]
  by (rule exI[of _ "CInstArbitrary (CConstant 0 CBool)"],
      rule exI[of _ "CConstant 1 CBool"],
      rule exI[of _ "CConstant 2 CBool"]) simp

definition definition_model_exists :: "bool ⇒ bool ⇒ bool" where
  "definition_model_exists closed scoped ⟷
    (∃constant_value. ∀free_value type_instance.
      constant_value =
        (if closed then if scoped then False else type_instance else free_value))"

definition weakened_definition_guard :: "bool ⇒ bool ⇒ bool" where
  "weakened_definition_guard closed scoped ⟷ closed ∨ scoped"

lemma definition_closedness_guard_countermodel:
  "∃closed scoped. weakened_definition_guard closed scoped ∧
    ¬ definition_model_exists closed scoped"
  nitpick [card = 1-5, satisfy, expect = genuine, timeout = 30]
  by (rule exI[of _ False], rule exI[of _ True])
    (auto simp: weakened_definition_guard_def definition_model_exists_def)

lemma definition_scope_guard_countermodel:
  "∃closed scoped. weakened_definition_guard closed scoped ∧
    ¬ definition_model_exists closed scoped"
  nitpick [card = 1-5, satisfy, expect = genuine, timeout = 30]
  by (rule exI[of _ True], rule exI[of _ False])
    (auto simp: weakened_definition_guard_def definition_model_exists_def)

definition type_extension_constructible ::
  "(bool ⇒ bool) ⇒ bool ⇒ bool ⇒ bool" where
  "type_extension_constructible pred fresh distinct_names ⟷
    (∃witness. pred witness) ∧ fresh ∧ distinct_names"

definition weakened_type_definition_guard ::
  "(bool ⇒ bool) ⇒ bool ⇒ bool ⇒ bool" where
  "weakened_type_definition_guard pred fresh distinct_names ⟷
    fresh ∧ distinct_names"

lemma type_definition_guard_countermodel:
  "∃pred fresh distinct_names.
    weakened_type_definition_guard pred fresh distinct_names ∧
    ¬ type_extension_constructible pred fresh distinct_names"
  nitpick [card = 1-5, satisfy, expect = genuine, timeout = 30]
  by (rule exI[of _ "λ_. False"], rule exI[of _ True],
      rule exI[of _ True])
    (simp add: weakened_type_definition_guard_def
      type_extension_constructible_def)

record cname =
  identity :: nat
  display_name :: bool

definition same_display :: "cname ⇒ cname ⇒ bool" where
  "same_display a b ⟷ display_name a = display_name b"

definition identity_insert :: "cname ⇒ cname list ⇒ cname list" where
  "identity_insert x xs = (if x ∈ set xs then xs else xs @ [x])"

definition display_insert :: "cname ⇒ cname list ⇒ cname list" where
  "display_insert x xs =
    (if ∃y∈set xs. same_display x y then xs else xs @ [x])"

lemma same_printing_symbol_countermodel:
  "∃a b. a ≠ b ∧ same_display a b ∧
    length (display_insert b (display_insert a [])) = 1 ∧
    length (identity_insert b (identity_insert a [])) = 2"
  nitpick [card = 1-5, satisfy, expect = genuine, timeout = 30]
  by (rule exI[of _ "⦇identity = 0, display_name = False⦈"],
      rule exI[of _ "⦇identity = 1, display_name = False⦈"])
    (simp add: same_display_def display_insert_def identity_insert_def)

end