Theory Big_Step_Sterm

section ‹Big-step semantics›

theory Big_Step_Sterm
imports
  Rewriting_Sterm
  "../Terms/Term_as_Value"
begin

subsection ‹Big-step semantics evaluating to irreducible @{typ sterm}s›

inductive (in constructors) seval :: "srule list ⇒ (name, sterm) fmap ⇒ sterm ⇒ sterm ⇒ bool"  ("_, _/ ⊢⇩s/ _ ↓/ _" [50,0,50] 50) for rs where
const: "(name, rhs) ∈ set rs ⟹ rs, Γ ⊢⇩s Sconst name ↓ rhs" |
var: "fmlookup Γ name = Some val ⟹ rs, Γ ⊢⇩s Svar name ↓ val" |
abs: "rs, Γ ⊢⇩s Sabs cs ↓ Sabs (map (λ(pat, t). (pat, subst t (fmdrop_fset (frees pat) Γ))) cs)" |
comb: "
  rs, Γ ⊢⇩s t ↓ Sabs cs ⟹ rs, Γ ⊢⇩s u ↓ u' ⟹
  find_match cs u' = Some (env, _, rhs) ⟹
  rs, Γ ++⇩f env ⊢⇩s rhs ↓ val ⟹
  rs, Γ ⊢⇩s t $⇩s u ↓ val" |
constr: "
  name |∈| C ⟹
  list_all2 (seval rs Γ) ts us ⟹
  rs, Γ ⊢⇩s name $$ ts ↓ name $$ us"

lemma (in constructors) seval_closed:
  assumes "rs, Γ ⊢⇩s t ↓ u" "closed_srules rs" "closed_env Γ" "closed_except t (fmdom Γ)"
  shows "closed u"
using assms proof induction
  case (const name rhs Γ)
  thus ?case
    by (auto simp: list_all_iff)
next
  case (comb Γ t cs u u' env pat rhs val)
  hence "closed (Sabs cs)" "closed u'"
    by (auto simp: closed_except_def)
  moreover have "(pat, rhs) ∈ set cs" "match pat u' = Some env"
    using comb by (auto simp: find_match_elem)
  ultimately have "closed_except rhs (frees pat)"
    by (auto dest: closed_except_sabs)

  show ?case
    proof (rule comb)
      have "closed_env env"
        by (rule closed.match) fact+
      thus "closed_env (Γ ++⇩f env)"
        using ‹closed_env Γ› by auto
    next
      have "closed_except rhs (fmdom Γ |∪| frees pat)"
        using ‹closed_except rhs _›
        unfolding closed_except_def by auto
      hence "closed_except rhs (fmdom Γ |∪| fmdom env)"
        using ‹match pat u' = Some env› by (metis match_dom)
      thus "closed_except rhs (fmdom (Γ ++⇩f env))"
        using comb by simp
    qed fact
next
  case (abs Γ cs)
  show ?case
    apply (subst subst_sterm.simps[symmetric])
    apply (subst closed_except_def)
    apply (subst subst_frees)
    apply fact+
    apply (subst fminus_fsubset_conv)
    apply (subst closed_except_def[symmetric])
    apply (subst funion_fempty_right)
    apply fact
    done
next
  case (constr name Γ ts us)
  have "list_all closed us"
    using ‹list_all2 _ _ _› ‹closed_except (list_comb _ _) _›
    proof (induction ts us rule: list.rel_induct)
      case (Cons v vs u us)
      thus ?case
        using constr unfolding closed.list_comb
        by auto
    qed simp
  thus ?case
    unfolding closed.list_comb
    by (simp add: closed_except_def)
qed auto

lemma (in srules) seval_wellformed:
  assumes "rs, Γ ⊢⇩s t ↓ u" "wellformed t" "wellformed_env Γ"
  shows "wellformed u"
using assms proof induction
  case (const name rhs Γ)
  thus ?case
    using all_rules
    by (auto simp: list_all_iff)
next
  case (comb Γ t cs u u' env pat rhs val)
  hence "(pat, rhs) ∈ set cs" "match pat u' = Some env"
    by (auto simp: find_match_elem)

  show ?case
    proof (rule comb)
      show "wellformed rhs"
        using ‹(pat, rhs) ∈ set cs› comb
        by (auto simp: list_all_iff)
    next
      have "wellformed_env env"
        apply (rule wellformed.match)
         apply fact
        apply (rule comb)
        using comb apply simp
        apply fact+
        done
      thus "wellformed_env (Γ ++⇩f env)"
        using comb by auto
    qed
next
  case (abs Γ cs)
  thus ?case
    by (metis subst_sterm.simps subst_wellformed)
next
  case (constr name Γ ts us)
  have "list_all wellformed us"
    using ‹list_all2 _ _ _› ‹wellformed (list_comb _ _)›
    proof (induction ts us rule: list.rel_induct)
      case (Cons v vs u us)
      thus ?case
        using constr by (auto simp: wellformed.list_comb app_sterm_def)
    qed simp
  thus ?case
    by (simp add: wellformed.list_comb const_sterm_def)
qed auto

lemma (in constants) seval_shadows:
  assumes "rs, Γ ⊢⇩s t ↓ u" "¬ shadows_consts t"
  assumes "list_all (λ(_, rhs). ¬ shadows_consts rhs) rs"
  assumes "not_shadows_consts_env Γ"
  shows "¬ shadows_consts u"
using assms proof induction
  case (const name rhs Γ)
  thus ?case
    unfolding srules_def
    by (auto simp: list_all_iff)
next
  case (comb Γ t cs u u' env pat rhs val)
  hence "¬ shadows_consts (Sabs cs)" "¬ shadows_consts u'"
    by auto
  moreover from comb have "(pat, rhs) ∈ set cs" "match pat u' = Some env"
    by (auto simp: find_match_elem)
  ultimately have "¬ shadows_consts rhs"
    by (auto simp: list_ex_iff)

  moreover have "not_shadows_consts_env env"
    using comb ‹match pat u' = _› by (auto intro: shadows.match)

  ultimately show ?case
    using comb by blast
next
  case (abs Γ cs)
  show ?case
    apply (subst subst_sterm.simps[symmetric])
    apply (rule subst_shadows)
     apply fact+
    done
next
  case (constr name Γ ts us)
  have "list_all (Not ∘ shadows_consts) us"
    using ‹list_all2 _ _ _› ‹¬ shadows_consts (name $$ ts)›
    proof (induction ts us rule: list.rel_induct)
      case (Cons v vs u us)
      thus ?case
        using constr by (auto simp: shadows.list_comb const_sterm_def app_sterm_def)
    qed simp
  thus ?case
    by (auto simp: shadows.list_comb list_ex_iff list_all_iff const_sterm_def)
qed auto

lemma (in constructors) seval_list_comb_abs:
  assumes "rs, Γ ⊢⇩s name $$ args ↓ Sabs cs"
  shows "name ∈ dom (map_of rs)"
using assms
proof (induction Γ "name $$ args" "Sabs cs" arbitrary: args cs)
  case (constr name' _ _ us)
  hence "Sabs cs = name' $$ us" by simp
  hence False
    by (cases rule: list_comb_cases) (auto simp: const_sterm_def app_sterm_def)
  thus ?case ..
next
  case (comb Γ t cs' u u' env pat rhs)

  hence "strip_comb (t $⇩s u) = strip_comb (name $$ args)"
    by simp
  hence "strip_comb t = (Sconst name, butlast args)" "u = last args"
     apply -
    subgoal
      apply (simp add: strip_list_comb_const)
      apply (fold app_sterm_def const_sterm_def)
      by (auto split: prod.splits)
    subgoal
      apply (simp add: strip_list_comb_const)
      apply (fold app_sterm_def const_sterm_def)
      by (auto split: prod.splits)
    done
  hence "t = name $$ butlast args"
    apply (fold const_sterm_def)
    by (metis list_strip_comb fst_conv snd_conv)

  thus ?case
    using comb by auto
qed (auto elim: list_comb_cases simp: const_sterm_def app_sterm_def intro: weak_map_of_SomeI)

lemma (in constructors) is_value_eval_id:
  assumes "is_value t" "closed t"
  shows "rs, Γ ⊢⇩s t ↓ t"
using assms proof induction
  case (abs cs)

  have "rs, Γ ⊢⇩s Sabs cs ↓ Sabs (map (λ(pat, t). (pat, subst t (fmdrop_fset (frees pat) Γ))) cs)"
    by (rule seval.abs)
  moreover have "subst (Sabs cs) Γ = Sabs cs"
    using abs by (metis subst_closed_id)
  ultimately show ?case
    by simp
next
  case (constr vs name)
  have "list_all2 (seval rs Γ) vs vs"
    proof (rule list.rel_refl_strong)
      fix v
      assume "v ∈ set vs"
      moreover hence "closed v"
        using constr
        unfolding closed.list_comb
        by (auto simp: list_all_iff)
      ultimately show "rs, Γ ⊢⇩s v ↓ v"
        using ‹list_all _ _›
        by (force simp: list_all_iff)
    qed
    with ‹name |∈| C› show ?case
      by (rule seval.constr)
qed

lemma (in constructors) ssubst_eval:
  assumes "rs, Γ ⊢⇩s t ↓ t'" "Γ' ⊆⇩f Γ" "closed_env Γ" "value_env Γ"
  shows "rs, Γ ⊢⇩s subst t Γ' ↓ t'"
using assms proof induction
  case (var Γ name val)
  show ?case
    proof (cases "fmlookup Γ' name")
      case None
      thus ?thesis
        using var by (auto intro: seval.intros)
    next
      case (Some val')
      with var have "val' = val"
        unfolding fmsubset_alt_def by force
      show ?thesis
        apply simp
        apply (subst Some)
        apply (subst ‹val' = _›)
        apply simp
        apply (rule is_value_eval_id)
        using var by auto
    qed
next
  case (abs Γ cs)
  hence "subst (subst (Sabs cs) Γ') Γ = subst (Sabs cs) Γ"
    by (metis subst_twice fmsubset_pred)
  moreover have "rs, Γ ⊢⇩s subst (Sabs cs) Γ' ↓ subst (subst (Sabs cs) Γ') Γ"
    apply simp
    apply (subst map_map[symmetric])
    apply (rule seval.abs)
    done
  ultimately have "rs, Γ ⊢⇩s subst (Sabs cs) Γ' ↓ subst (Sabs cs) Γ"
    by metis
  thus ?case by simp
next
  case (constr name Γ ts us)
  hence "list_all2 (λt. seval rs Γ (subst t Γ')) ts us"
    by (blast intro: list.rel_mono_strong)
  with constr show ?case
    by (auto simp: subst_list_comb list_all2_map1 intro: seval.constr)
qed (auto intro: seval.intros)

lemma (in constructors) seval_agree_eq:
  assumes "rs, Γ ⊢⇩s t ↓ u" "fmrestrict_fset S Γ = fmrestrict_fset S Γ'" "closed_except t S"
  assumes "S |⊆| fmdom Γ" "closed_srules rs" "closed_env Γ"
  shows "rs, Γ' ⊢⇩s t ↓ u"
using assms proof (induction arbitrary: Γ' S)
  case (var Γ name val)
  hence "name |∈| S"
    by (simp add: closed_except_def)
  hence "fmlookup Γ name = fmlookup Γ' name"
    using ‹fmrestrict_fset S Γ = _›
    unfolding fmfilter_alt_defs
    including fmap.lifting
    by transfer' (auto simp: map_filter_def fun_eq_iff split: if_splits)
  with var show ?case
    by (auto intro: seval.var)
next
  case (abs Γ cs)

  ― ‹Intentionally local: not really a useful lemma outside of its scope›
  have *: "fmdrop_fset S (fmrestrict_fset T m) = fmrestrict_fset (T |∪| S) (fmdrop_fset S m)" for S T m
    unfolding fmfilter_alt_defs fmfilter_comp
    by (rule fmfilter_cong) auto

  {
    fix pat t
    assume "(pat, t) ∈ set cs"
    with abs have "closed_except t (S |∪| frees pat)"
      by (auto simp: Sterm.closed_except_simps list_all_iff)

    have
      "subst t (fmdrop_fset (frees pat) (fmrestrict_fset S Γ)) = subst t (fmdrop_fset (frees pat) Γ)"
      apply (subst *)
      apply (rule subst_restrict_closed)
      apply fact
      done

    moreover have
      "subst t (fmdrop_fset (frees pat) (fmrestrict_fset S Γ')) = subst t (fmdrop_fset (frees pat) Γ')"
      apply (subst *)
      apply (rule subst_restrict_closed)
      apply fact
      done

    ultimately have "subst t (fmdrop_fset (frees pat) Γ) = subst t (fmdrop_fset (frees pat) Γ')"
      using abs by metis
  }

  hence "map (λ(pat, t). (pat, subst t (fmdrop_fset (frees pat) Γ))) cs =
         map (λ(pat, t). (pat, subst t (fmdrop_fset (frees pat) Γ'))) cs"
    by auto

  thus ?case
    by (metis seval.abs)
next
  case (comb Γ t cs u u' env pat rhs val)
  have "fmdom env = frees pat"
    apply (rule match_dom)
    apply (rule find_match_elem)
    apply fact
    done

  show ?case
    proof (rule seval.comb)
      show "rs, Γ' ⊢⇩s t ↓ Sabs cs" "rs, Γ' ⊢⇩s u ↓ u'"
        using comb by (auto simp: Sterm.closed_except_simps)
    next
      show "rs, Γ' ++⇩f env ⊢⇩s rhs ↓ val"
        proof (rule comb)
          have "fmrestrict_fset (S |∪| fmdom env) (Γ ++⇩f env) = fmrestrict_fset (S |∪| fmdom env) (Γ' ++⇩f env)"
            using comb(8)
            unfolding fmfilter_alt_defs
            including fmap.lifting fset.lifting
            by transfer' (auto simp: map_filter_def fun_eq_iff map_add_def split: option.splits if_splits)

          thus "fmrestrict_fset (S |∪| frees pat) (Γ ++⇩f env) = fmrestrict_fset (S |∪| frees pat) (Γ' ++⇩f env)"
            unfolding ‹fmdom env = _› .
        next
          have "closed_except t S"
            using comb by (simp add: Sterm.closed_except_simps)

          have "closed (Sabs cs)"
            apply (rule seval_closed)
            apply fact+
            using ‹closed_except t S› ‹S |⊆| fmdom Γ›
            unfolding closed_except_def apply simp
            done

          have "(pat, rhs) ∈ set cs"
            using ‹find_match _ _ = _› by (rule find_match_elem)
          hence "closed_except rhs (frees pat)"
            using ‹closed (Sabs cs)› by (auto dest: closed_except_sabs)
          thus "closed_except rhs (S |∪| frees pat)"
            unfolding closed_except_def by auto
        next
          show "S |∪| frees pat |⊆| fmdom (Γ ++⇩f env)"
            apply simp
            apply (intro conjI)
            using comb(10) apply blast
            unfolding ‹fmdom env = _› by blast
        next
          have "closed_except u S"
            using comb by (auto simp: closed_except_def)

          show "closed_env (Γ ++⇩f env)"
            apply rule
             apply fact
            apply (rule closed.match[where t = u' and pat = pat])
            subgoal
              by (rule find_match_elem) fact
            subgoal
              apply (rule seval_closed)
                 apply fact+
              using ‹closed_except u S› ‹S |⊆| fmdom Γ› unfolding closed_except_def by blast
            done
        qed fact
    qed fact
next
  case (constr name Γ ts us)
  show ?case
    apply (rule seval.constr)
     apply fact
    apply (rule list.rel_mono_strong)
     apply fact
    using constr
    unfolding closed.list_comb list_all_iff
    by auto
qed (auto intro: seval.intros)


subsubsection ‹Correctness wrt @{const srewrite}›

context srules begin context begin

private lemma seval_correct0:
  assumes "rs, Γ ⊢⇩s t ↓ u" "closed_except t (fmdom Γ)" "closed_env Γ"
  shows "rs ⊢⇩s subst t Γ ⟶* u"
using assms proof induction
  case (const name rhs Γ)

  have "srewrite_step rs name rhs"
    by (rule srewrite_stepI) fact
  thus ?case
    by (auto intro: srewrite.intros)
next
  case (comb Γ t cs u u' env pat rhs val)
  hence "closed_except t (fmdom Γ)" "closed_except u (fmdom Γ)"
    by (simp add: Sterm.closed_except_simps)+
  moreover have "closed_srules rs"
    using all_rules
    unfolding list_all_iff by fastforce
  ultimately have "closed (Sabs cs)" "closed u'"
    using comb by (metis seval_closed)+

  from comb have "(pat, rhs) ∈ set cs" "match pat u' = Some env"
    by (auto simp: find_match_elem)
  hence "closed_except rhs (frees pat)"
    using ‹closed (Sabs cs)› by (auto dest: closed_except_sabs)
  hence "frees rhs |⊆| frees pat"
    by (simp add: closed_except_def)
  moreover have "fmdom env = frees pat"
    using ‹match pat u' = _› by (auto simp: match_dom)
  ultimately have "frees rhs |⊆| fmdom env"
    by simp
  hence "subst rhs (Γ ++⇩f env) = subst rhs env"
    by (rule subst_add_shadowed_env)

  have "rs ⊢⇩s subst t Γ $⇩s subst u Γ ⟶* Sabs cs $⇩s u'"
    using comb by (force intro: srewrite.rt_comb[unfolded app_sterm_def] simp: Sterm.closed_except_simps)
  also have "rs ⊢⇩s Sabs cs $⇩s u' ⟶* subst rhs env"
    using comb ‹closed u'› by (force intro: srewrite.beta find_match_rewrite_first)
  also have "rs ⊢⇩s subst rhs env ⟶* subst rhs (Γ ++⇩f env)"
    unfolding ‹subst rhs (Γ ++⇩f env) = _› by simp
  also have "rs ⊢⇩s subst rhs (Γ ++⇩f env) ⟶* val"
    proof (rule comb)
      show "closed_except rhs (fmdom (Γ ++⇩f env))"
        using comb ‹match pat u' = Some env› ‹fmdom env = _› ‹frees rhs |⊆| frees pat›
        by (auto simp: closed_except_def)
    next
      show "closed_env (Γ ++⇩f env)"
        using comb ‹match pat u' = Some env› ‹closed u'›
        by (blast intro: closed.match)
    qed

  finally show ?case by simp
next
  case (constr name Γ ts us)
  show ?case
    apply (simp add: subst_list_comb)
    apply (rule srewrite.rt_list_comb)
    subgoal
      apply (simp add: list.rel_map)
      apply (rule list.rel_mono_strong[OF constr(2)])
      apply clarify
      apply (elim impE)
      using constr(3) apply (erule closed.list_combE)
       apply (rule constr)+
      apply (auto simp: const_sterm_def)
      done
    subgoal by auto
    done
qed auto

corollary seval_correct:
  assumes "rs, fmempty ⊢⇩s t ↓ u" "closed t"
  shows "rs ⊢⇩s t ⟶* u"
proof -
  have "closed_except t (fmdom fmempty)"
    using assms by simp
  with assms have "rs ⊢⇩s subst t fmempty ⟶* u"
    by (fastforce intro!: seval_correct0)
  thus ?thesis
    by simp
qed

end end

end