Theory Kruskal_Examples

theory Kruskal_Examples
imports Kruskal
begin

datatype 'a tree = Node 'a "'a tree list"

fun node
where
  "node (Node f ts) = (f, length ts)"

fun succs
where
  "succs (Node f ts) = ts"

inductive_set trees for A
where
  "f ∈ A ⟹ ∀t ∈ set ts. t ∈ trees A ⟹ Node f ts ∈ trees A"

lemma [simp]:
  "trees UNIV = UNIV"
proof -
  { fix t :: "'a tree"
    have "t ∈ trees UNIV"
      by (induct t) (auto intro: trees.intros) }
  then show ?thesis by auto
qed

interpretation kruskal_tree_tree: kruskal_tree "A × UNIV" Node node succs "trees A" for A
  apply (unfold_locales)
  apply auto
  apply (case_tac [!] t rule: trees.cases)
  apply auto
  by (metis less_not_refl not_less_eq size_list_estimation)

thm kruskal_tree_tree.almost_full_on_trees
thm kruskal_tree_tree.kruskal

definition "tree_emb A P = kruskal_tree_tree.emb A (prod_le P (λ_ _. True))"

lemma wqo_on_trees:
  assumes "wqo_on P A"
  shows "wqo_on (tree_emb A P) (trees A)"
  using wqo_on_Sigma [OF assms wqo_on_UNIV, THEN kruskal_tree_tree.kruskal]
  by (simp add: tree_emb_def)

text ‹
If the type @{typ "'a"} is well-quasi-ordered by ‹P›, then trees of type @{typ "'a tree"}
are well-quasi-ordered by the homeomorphic embedding relation.
›
instantiation tree :: (wqo) wqo
begin
definition "s ≤ t ⟷ tree_emb UNIV (≤) s t"
definition "(s :: 'a tree) < t ⟷ s ≤ t ∧ ¬ (t ≤ s)"

instance
  by (rule wqo.intro_of_class)
     (auto simp: less_eq_tree_def [abs_def] less_tree_def [abs_def]
           intro: wqo_on_trees [of _ UNIV, simplified])
end

datatype ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"

fun root
where
  "root (Fun f ts) = (f, length ts)"

fun args
where
  "args (Fun f ts) = ts"

inductive_set gterms for F
where
  "(f, n) ∈ F ⟹ length ts = n ⟹ ∀s ∈ set ts. s ∈ gterms F ⟹ Fun f ts ∈ gterms F"

interpretation kruskal_term: kruskal_tree F Fun root args "gterms F" for F
  apply (unfold_locales)
  apply auto
  apply (case_tac [!] t rule: gterms.cases)
  apply auto
  by (metis less_not_refl not_less_eq size_list_estimation)

thm kruskal_term.almost_full_on_trees

inductive_set terms
where
  "∀t ∈ set ts. t ∈ terms ⟹ Fun f ts ∈ terms"

interpretation kruskal_variadic: kruskal_tree UNIV Fun root args terms
  apply (unfold_locales)
  apply auto
  apply (case_tac [!] t rule: terms.cases)
  apply auto
  by (metis less_not_refl not_less_eq size_list_estimation)

thm kruskal_variadic.almost_full_on_trees

datatype 'a exp = V 'a | C nat | Plus "'a exp" "'a exp"

datatype 'a symb = v 'a | c nat | p

fun mk
where
  "mk (v x) [] = V x" |
  "mk (c n) [] = C n" |
  "mk p [a, b] = Plus a b"

fun rt
where
  "rt (V x) = (v x, 0::nat)" |
  "rt (C n) = (c n, 0)" |
  "rt (Plus a b) = (p, 2)"

fun ags
where
  "ags (V x) = []" |
  "ags (C n) = []" |
  "ags (Plus a b) = [a, b]"

inductive_set exps
where
  "V x ∈ exps" |
  "C n ∈ exps" |
  "a ∈ exps ⟹ b ∈ exps ⟹ Plus a b ∈ exps"

lemma [simp]:
  assumes "length ts = 2"
  shows "rt (mk p ts) = (p, 2)"
  using assms by (induct ts) (auto, case_tac ts, auto)

lemma [simp]:
  assumes "length ts = 2"
  shows "ags (mk p ts) = ts"
  using assms by (induct ts) (auto, case_tac ts, auto)

interpretation kruskal_exp: kruskal_tree
  "{(v x, 0) | x. True} ∪ {(c n, 0) | n. True} ∪ {(p, 2)}"
  mk rt ags exps
apply (unfold_locales)
apply auto
apply (case_tac [!] t rule: exps.cases)
by auto

thm kruskal_exp.almost_full_on_trees

hide_const (open) tree_emb V C Plus v c p

end