Theory Context_Free_Grammar_Example

theory Context_Free_Grammar_Example
imports "HOL-Library.Code_Prolog"
begin
(*
declare mem_def[code_pred_inline]
*)

subsection ‹Alternative rules for length›

definition size_list :: "'a list => nat"
where "size_list = size"

lemma size_list_simps:
  "size_list [] = 0"
  "size_list (x # xs) = Suc (size_list xs)"
by (auto simp add: size_list_def)

declare size_list_simps[code_pred_def]
declare size_list_def[symmetric, code_pred_inline]


setup ‹
  Context.theory_map
    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
›

datatype alphabet = a | b

inductive_set S⇩1 and A⇩1 and B⇩1 where
  "[] ∈ S⇩1"
| "w ∈ A⇩1 ⟹ b # w ∈ S⇩1"
| "w ∈ B⇩1 ⟹ a # w ∈ S⇩1"
| "w ∈ S⇩1 ⟹ a # w ∈ A⇩1"
| "w ∈ S⇩1 ⟹ b # w ∈ S⇩1"
| "⟦v ∈ B⇩1; v ∈ B⇩1⟧ ⟹ a # v @ w ∈ B⇩1"

lemma
  "S⇩1p w ⟹ w = []"
quickcheck[tester = prolog, iterations=1, expect = counterexample]
oops

definition "filter_a = filter (λx. x = a)"

lemma [code_pred_def]: "filter_a [] = []"
unfolding filter_a_def by simp

lemma [code_pred_def]: "filter_a (x#xs) = (if x = a then x # filter_a xs else filter_a xs)"
unfolding filter_a_def by simp

declare filter_a_def[symmetric, code_pred_inline]

definition "filter_b = filter (λx. x = b)"

lemma [code_pred_def]: "filter_b [] = []"
unfolding filter_b_def by simp

lemma [code_pred_def]: "filter_b (x#xs) = (if x = b then x # filter_b xs else filter_b xs)"
unfolding filter_b_def by simp

declare filter_b_def[symmetric, code_pred_inline]

setup ‹Code_Prolog.map_code_options (K
  {ensure_groundness = true,
  limit_globally = NONE,
  limited_types = [],
  limited_predicates = [(["s1p", "a1p", "b1p"], 2)],
  replacing = [(("s1p", "limited_s1p"), "quickcheck")],
  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]})›


theorem S⇩1_sound:
"S⇩1p w ⟹ length [x ← w. x = a] = length [x ← w. x = b]"
quickcheck[tester = prolog, iterations=1, expect = counterexample]
oops


inductive_set S⇩2 and A⇩2 and B⇩2 where
  "[] ∈ S⇩2"
| "w ∈ A⇩2 ⟹ b # w ∈ S⇩2"
| "w ∈ B⇩2 ⟹ a # w ∈ S⇩2"
| "w ∈ S⇩2 ⟹ a # w ∈ A⇩2"
| "w ∈ S⇩2 ⟹ b # w ∈ B⇩2"
| "⟦v ∈ B⇩2; v ∈ B⇩2⟧ ⟹ a # v @ w ∈ B⇩2"


setup ‹Code_Prolog.map_code_options (K
  {ensure_groundness = true,
  limit_globally = NONE,
  limited_types = [],
  limited_predicates = [(["s2p", "a2p", "b2p"], 3)],
  replacing = [(("s2p", "limited_s2p"), "quickcheck")],
  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]})›


theorem S⇩2_sound:
  "S⇩2p w ⟶ length [x ← w. x = a] = length [x ← w. x = b]"
quickcheck[tester = prolog, iterations=1, expect = counterexample]
oops

inductive_set S⇩3 and A⇩3 and B⇩3 where
  "[] ∈ S⇩3"
| "w ∈ A⇩3 ⟹ b # w ∈ S⇩3"
| "w ∈ B⇩3 ⟹ a # w ∈ S⇩3"
| "w ∈ S⇩3 ⟹ a # w ∈ A⇩3"
| "w ∈ S⇩3 ⟹ b # w ∈ B⇩3"
| "⟦v ∈ B⇩3; w ∈ B⇩3⟧ ⟹ a # v @ w ∈ B⇩3"


setup ‹Code_Prolog.map_code_options (K
  {ensure_groundness = true,
  limit_globally = NONE,
  limited_types = [],
  limited_predicates = [(["s3p", "a3p", "b3p"], 6)],
  replacing = [(("s3p", "limited_s3p"), "quickcheck")],
  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]})›

lemma S⇩3_sound:
  "S⇩3p w ⟶ length [x ← w. x = a] = length [x ← w. x = b]"
quickcheck[tester = prolog, iterations=1, size=1, expect = no_counterexample]
oops


(*
setup {* Code_Prolog.map_code_options (K
  {ensure_groundness = true,
  limit_globally = NONE,
  limited_types = [],
  limited_predicates = [],
  replacing = [],
  manual_reorder = [],
  timeout = seconds 10.0,
  prolog_system = Code_Prolog.SWI_PROLOG}) *}


theorem S⇩3_complete:
"length [x ← w. x = a] = length [x ← w. x = b] ⟶ w ∈ S⇩3"
quickcheck[tester = prolog, size=1, iterations=1]
oops
*)

inductive_set S⇩4 and A⇩4 and B⇩4 where
  "[] ∈ S⇩4"
| "w ∈ A⇩4 ⟹ b # w ∈ S⇩4"
| "w ∈ B⇩4 ⟹ a # w ∈ S⇩4"
| "w ∈ S⇩4 ⟹ a # w ∈ A⇩4"
| "⟦v ∈ A⇩4; w ∈ A⇩4⟧ ⟹ b # v @ w ∈ A⇩4"
| "w ∈ S⇩4 ⟹ b # w ∈ B⇩4"
| "⟦v ∈ B⇩4; w ∈ B⇩4⟧ ⟹ a # v @ w ∈ B⇩4"


setup ‹Code_Prolog.map_code_options (K
  {ensure_groundness = true,
  limit_globally = NONE,
  limited_types = [],
  limited_predicates = [(["s4p", "a4p", "b4p"], 6)],
  replacing = [(("s4p", "limited_s4p"), "quickcheck")],
  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]})›


theorem S⇩4_sound:
  "S⇩4p w ⟶ length [x ← w. x = a] = length [x ← w. x = b]"
quickcheck[tester = prolog, size=1, iterations=1, expect = no_counterexample]
oops

(*
theorem S⇩4_complete:
"length [x ← w. x = a] = length [x ← w. x = b] ⟶ w ∈ S⇩4"
oops
*)

hide_const a b


end