Theory Sterm

section ‹Terms with sequential pattern matching›

theory Sterm
imports Strong_Term
begin

datatype sterm =
  Sconst name |
  Svar name |
  Sabs (clauses: "(term × sterm) list") |
  Sapp sterm sterm (infixl "$⇩s" 70)

datatype_compat sterm

derive linorder sterm

abbreviation Sabs_single ("Λ⇩s _. _" [0, 50] 50) where
"Sabs_single x rhs ≡ Sabs [(Free x, rhs)]"

type_synonym sclauses = "(term × sterm) list"

lemma sterm_induct[case_names Sconst Svar Sabs Sapp]:
  assumes "⋀x. P (Sconst x)"
  assumes "⋀x. P (Svar x)"
  assumes "⋀cs. (⋀pat t. (pat, t) ∈ set cs ⟹ P t) ⟹ P (Sabs cs)"
  assumes "⋀t u. P t ⟹ P u ⟹ P (t $⇩s u)"
  shows "P t"
using assms
  apply induction_schema
    apply pat_completeness
   apply lexicographic_order
  done

instantiation sterm :: pre_term begin

definition app_sterm where
"app_sterm t u = t $⇩s u"

fun unapp_sterm where
"unapp_sterm (t $⇩s u) = Some (t, u)" |
"unapp_sterm _ = None"

definition const_sterm where
"const_sterm = Sconst"

fun unconst_sterm where
"unconst_sterm (Sconst name) = Some name" |
"unconst_sterm _ = None"

fun unfree_sterm where
"unfree_sterm (Svar name) = Some name" |
"unfree_sterm _ = None"

definition free_sterm where
"free_sterm = Svar"

fun frees_sterm where
"frees_sterm (Svar name) = {|name|}" |
"frees_sterm (Sconst _) = {||}" |
"frees_sterm (Sabs cs) = ffUnion (fset_of_list (map (λ(pat, rhs). frees_sterm rhs - frees pat) cs))" |
"frees_sterm (t $⇩s u) = frees_sterm t |∪| frees_sterm u"

fun subst_sterm where
"subst_sterm (Svar s) env = (case fmlookup env s of Some t ⇒ t | None ⇒ Svar s)" |
"subst_sterm (t⇩1 $⇩s t⇩2) env = subst_sterm t⇩1 env $⇩s subst_sterm t⇩2 env" |
"subst_sterm (Sabs cs) env = Sabs (map (λ(pat, rhs). (pat, subst_sterm rhs (fmdrop_fset (frees pat) env))) cs)" |
"subst_sterm t env = t"

fun consts_sterm :: "sterm ⇒ name fset" where
"consts_sterm (Svar _) = {||}" |
"consts_sterm (Sconst name) = {|name|}" |
"consts_sterm (Sabs cs) = ffUnion (fset_of_list (map (λ(_, rhs). consts_sterm rhs) cs))" |
"consts_sterm (t $⇩s u) = consts_sterm t |∪| consts_sterm u"

instance
by standard
   (auto
      simp: app_sterm_def const_sterm_def free_sterm_def
      elim: unapp_sterm.elims unconst_sterm.elims unfree_sterm.elims
      split: option.splits)

end

instantiation sterm :: "term" begin

definition abs_pred_sterm :: "(sterm ⇒ bool) ⇒ sterm ⇒ bool" where
[code del]: "abs_pred P t ⟷ (∀cs. t = Sabs cs ⟶ (∀pat t. (pat, t) ∈ set cs ⟶ P t) ⟶ P t)"

lemma abs_pred_stermI[intro]:
  assumes "⋀cs. (⋀pat t. (pat, t) ∈ set cs ⟹ P t) ⟹ P (Sabs cs)"
  shows "abs_pred P t"
using assms unfolding abs_pred_sterm_def by auto

instance proof (standard, goal_cases)
  case (1 P t)
  then show ?case
    by (induction t) (auto simp: const_sterm_def free_sterm_def app_sterm_def abs_pred_sterm_def)
next
  case (2 t)
  show ?case
    apply rule
    apply auto
    apply (subst (3) list.map_id[symmetric])
    apply (rule list.map_cong0)
    apply auto
    by blast
next
  case (3 x t)
  show ?case
    apply rule
    apply clarsimp
    subgoal for cs env pat rhs
      apply (cases "x |∈| frees pat")
      subgoal
        apply (rule arg_cong[where f = "subst rhs"])
        by (auto intro: fmap_ext)
      subgoal premises prems[rule_format]
        apply (subst (2) prems(1)[symmetric, where pat = pat])
        subgoal by fact
        subgoal
          using prems
          unfolding ffUnion_alt_def
          by (auto simp add: fset_of_list.rep_eq elim!: fBallE)
        subgoal
          apply (rule arg_cong[where f = "subst rhs"])
          by (auto intro: fmap_ext)
        done
      done
    done
next
  case (4 t)
  show ?case
    apply rule
    apply clarsimp
    subgoal premises prems[rule_format]
      apply (rule prems(1)[OF prems(4)])
      subgoal using prems by auto
      subgoal using prems unfolding fdisjnt_alt_def by auto
      done
    done
next
  case 5
  show ?case
    proof (intro abs_pred_stermI allI impI, goal_cases)
      case (1 cs env)
      show ?case
        proof safe
          fix name
          assume "name |∈| frees (subst (Sabs cs) env)"
          then obtain pat rhs
            where "(pat, rhs) ∈ set cs"
              and "name |∈| frees (subst rhs (fmdrop_fset (frees pat) env))"
              and "name |∉| frees pat"
            by (auto simp: fset_of_list_elem case_prod_twice comp_def ffUnion_alt_def)

          hence "name |∈| frees rhs |-| fmdom (fmdrop_fset (frees pat) env)"
            using 1 by (simp add: fmpred_drop_fset)

          hence "name |∈| frees rhs |-| frees pat"
            using ‹name |∉| frees pat› by blast

          show "name |∈| frees (Sabs cs)"
            apply (simp add: ffUnion_alt_def)
            apply (rule fBexI[where x = "(pat, rhs)"])
            unfolding prod.case
             apply (fact ‹name |∈| frees rhs |-| frees pat›)
            unfolding fset_of_list_elem
            by fact

          assume "name |∈| fmdom env"
          thus False
            using ‹name |∈| frees rhs |-| fmdom (fmdrop_fset (frees pat) env)› ‹name |∉| frees pat›
            by fastforce
        next
          fix name
          assume "name |∈| frees (Sabs cs)" "name |∉| fmdom env"

          then obtain pat rhs
            where "(pat, rhs) ∈ set cs" "name |∈| frees rhs" "name |∉| frees pat"
            by (auto simp: fset_of_list_elem ffUnion_alt_def)

          moreover hence "name |∈| frees rhs |-| fmdom (fmdrop_fset (frees pat) env) |-| frees pat"
            using ‹name |∉| fmdom env› by fastforce

          ultimately have "name |∈| frees (subst rhs (fmdrop_fset (frees pat) env)) |-| frees pat"
            using 1 by (simp add: fmpred_drop_fset)

          show "name |∈| frees (subst (Sabs cs) env)"
            apply (simp add: case_prod_twice comp_def)
            unfolding ffUnion_alt_def
            apply (rule fBexI)
             apply (fact ‹name |∈| frees (subst rhs (fmdrop_fset (frees pat) env)) |-| frees pat›)
            apply (subst fimage_iff)
            apply (rule fBexI[where x = "(pat, rhs)"])
             apply simp
            using ‹(pat, rhs) ∈ set cs›
            by (auto simp: fset_of_list_elem)
        qed
    qed
next
  case 6
  show ?case
    proof (intro abs_pred_stermI allI impI, goal_cases)
      case (1 cs env)

      ― ‹some property on various operations that is only useful in here›
      have *: "fbind (fmimage m (fbind A g)) f = fbind A (λx. fbind (fmimage m (g x)) f)"
        for m A f g
        including fset.lifting fmap.lifting
        by transfer' force

      have "consts (subst (Sabs cs) env) = fbind (fset_of_list cs) (λ(pat, rhs). consts rhs |∪| ffUnion (consts |`| fmimage (fmdrop_fset (frees pat) env) (frees rhs)))"
        apply (simp add: funion_image_bind_eq)
        apply (rule fbind_cong[OF refl])
        apply (clarsimp split: prod.splits)
        apply (subst 1)
         apply (subst (asm) fset_of_list_elem, assumption)
        apply simp
        by (simp add: funion_image_bind_eq)
      also have "… = fbind (fset_of_list cs) (consts ∘ snd) |∪| fbind (fset_of_list cs) (λ(pat, rhs). ffUnion (consts |`| fmimage (fmdrop_fset (frees pat) env) (frees rhs)))"
        apply (subst fbind_fun_funion[symmetric])
        apply (rule fbind_cong[OF refl])
        by auto
      also have "… = consts (Sabs cs) |∪| fbind (fset_of_list cs) (λ(pat, rhs). ffUnion (consts |`| fmimage (fmdrop_fset (frees pat) env) (frees rhs)))"
        apply (rule cong[OF cong, OF refl _ refl, where f1 = "funion"])
        apply (subst funion_image_bind_eq[symmetric])
        unfolding consts_sterm.simps
        apply (rule arg_cong[where f = ffUnion])
        apply (subst fset_of_list_map)
        apply (rule fset.map_cong[OF refl])
        by auto
      also have "… = consts (Sabs cs) |∪| fbind (fmimage env (fbind (fset_of_list cs) (λ(pat, rhs). frees rhs |-| frees pat))) consts"
        apply (subst funion_image_bind_eq)
        apply (subst fmimage_drop_fset)
        apply (rule cong[OF cong, OF refl refl, where f1 = "funion"])
        apply (subst *)
        apply (rule fbind_cong[OF refl])
        by auto
      also have "… = consts (Sabs cs) |∪| ffUnion (consts |`| fmimage env (frees (Sabs cs)))"
        by (simp only: frees_sterm.simps fset_of_list_map  fmimage_Union funion_image_bind_eq)

      finally show ?case .
    qed
qed (auto simp: abs_pred_sterm_def)

end

lemma no_abs_abs[simp]: "¬ no_abs (Sabs cs)"
by (subst no_abs.simps) (auto simp: term_cases_def)

lemma closed_except_simps:
  "closed_except (Svar x) S ⟷ x |∈| S"
  "closed_except (t⇩1 $⇩s t⇩2) S ⟷ closed_except t⇩1 S ∧ closed_except t⇩2 S"
  "closed_except (Sabs cs) S ⟷ list_all (λ(pat, t). closed_except t (S |∪| frees pat)) cs"
  "closed_except (Sconst name) S ⟷ True"
proof goal_cases
  case 3
  show ?case
    proof (standard, goal_cases)
      case 1
      then show ?case
        apply (auto simp: list_all_iff ffUnion_alt_def fset_of_list_elem closed_except_def)
        apply (drule ffUnion_least_rev)
        apply auto
        by (smt case_prod_conv fbspec fimageI fminusI fset_of_list_elem fset_rev_mp)
    next
      case 2
      then show ?case
        by (fastforce simp: list_all_iff ffUnion_alt_def fset_of_list_elem closed_except_def)
    qed
qed (auto simp: ffUnion_alt_def closed_except_def)

lemma closed_except_sabs:
  assumes "closed (Sabs cs)" "(pat, rhs) ∈ set cs"
  shows "closed_except rhs (frees pat)"
using assms unfolding closed_except_def
apply auto
by (metis bot.extremum_uniqueI fempty_iff ffUnion_subset_elem fimageI fminusI fset_of_list_elem old.prod.case)

instantiation sterm :: strong_term  begin

fun wellformed_sterm :: "sterm ⇒ bool" where
"wellformed_sterm (t⇩1 $⇩s t⇩2) ⟷ wellformed_sterm t⇩1 ∧ wellformed_sterm t⇩2" |
"wellformed_sterm (Sabs cs) ⟷ list_all (λ(pat, t). linear pat ∧ wellformed_sterm t) cs ∧ distinct (map fst cs) ∧ cs ≠ []" |
"wellformed_sterm _ ⟷ True"

primrec all_frees_sterm :: "sterm ⇒ name fset" where
"all_frees_sterm (Svar x) = {|x|}" |
"all_frees_sterm (t⇩1 $⇩s t⇩2) = all_frees_sterm t⇩1 |∪| all_frees_sterm t⇩2" |
"all_frees_sterm (Sabs cs) = ffUnion (fset_of_list (map (λ(P, T). P |∪| T) (map (map_prod frees all_frees_sterm) cs)))" |
"all_frees_sterm (Sconst _) = {||}"

instance proof (standard, goal_cases)
  case (7 t)
  show ?case
    apply (intro abs_pred_stermI allI impI)
    apply simp
    apply (rule ffUnion_least)
    apply (rule fBallI)
    apply auto
    apply (subst ffUnion_alt_def)
    apply simp
    apply (rule_tac x = "(a, b)" in fBexI)
    by (auto simp: fset_of_list_elem)
next
  case (8 t)
  show ?case
    apply (intro abs_pred_stermI allI impI)
    apply (simp add: list.pred_map comp_def case_prod_twice, safe)
    subgoal
      apply (subst list_all_iff)
      apply (rule ballI)
      apply safe[1]
       apply (fastforce simp: list_all_iff)
      subgoal premises prems[rule_format]
        apply (rule prems)
          apply (fact prems)
        using prems apply (fastforce simp: list_all_iff)
        using prems by force
      done
    subgoal
      apply (subst map_cong[OF refl])
      by auto
    done
qed (auto simp: const_sterm_def free_sterm_def app_sterm_def)

end

lemma match_sabs[simp]: "¬ is_free t ⟹ match t (Sabs cs) = None"
by (cases t) auto

context pre_constants begin

lemma welldefined_sabs: "welldefined (Sabs cs) ⟷ list_all (λ(_, t). welldefined t) cs"
apply (auto simp: list_all_iff ffUnion_alt_def dest!: ffUnion_least_rev)
 apply (subst (asm) list_all_iff_fset[symmetric])
 apply (auto simp: list_all_iff fset_of_list_elem)
done

lemma shadows_consts_sterm_simps[simp]:
  "shadows_consts (t⇩1 $⇩s t⇩2) ⟷ shadows_consts t⇩1 ∨ shadows_consts t⇩2"
  "shadows_consts (Svar name) ⟷ name |∈| all_consts"
  "shadows_consts (Sabs cs) ⟷ list_ex (λ(pat, t). ¬ fdisjnt all_consts (frees pat) ∨ shadows_consts t) cs"
  "shadows_consts (Sconst name) ⟷ False"
proof (goal_cases)
  case 3
  show ?case
    unfolding shadows_consts_def list_ex_iff
    apply rule
    subgoal
      by (force simp: ffUnion_alt_def fset_of_list_elem fdisjnt_alt_def elim!: ballE)
    subgoal
      apply (auto simp: fset_of_list_elem fdisjnt_alt_def)
      by (auto simp: fset_eq_empty_iff ffUnion_alt_def fset_of_list_elem elim!: allE fBallE)
    done
qed (auto simp: shadows_consts_def fdisjnt_alt_def)

(* FIXME derive from axioms? *)
lemma subst_shadows:
  assumes "¬ shadows_consts (t::sterm)" "not_shadows_consts_env Γ"
  shows "¬ shadows_consts (subst t Γ)"
using assms proof (induction t arbitrary: Γ rule: sterm_induct)
  case (Sabs cs)
  show ?case
    apply (simp add: list_ex_iff case_prod_twice)
    apply (rule ballI)
    subgoal for c
      apply (cases c, hypsubst_thin, simp)
      apply (rule conjI)
      subgoal using Sabs(2) by (fastforce simp: list_ex_iff)
      apply (rule Sabs(1))
        apply assumption
      subgoal using Sabs(2) by (fastforce simp: list_ex_iff)
      subgoal using Sabs(3) by force
      done
    done
qed (auto split: option.splits)

end

end