Theory Evaluate_Clock

section "Simplifiying the definition"

theory Evaluate_Clock
imports Evaluate_Termination
begin

hide_const (open) sem_env.v

lemma fix_clock:
  "fix_clock s1 (s2, x) = (s, x) ⟹ clock s ≤ clock s1"
  "fix_clock s1 (s2, x) = (s, x) ⟹ clock s ≤ clock s2"
unfolding fix_clock_alt_def by auto

lemma dec_clock[simp]: "clock (dec_clock st) = clock st - 1"
unfolding dec_clock_def by auto

context begin

private lemma fun_evaluate_clock0:
  "clock (fst (fun_evaluate_match s1 env v p v')) ≤ clock s1"
  "clock (fst (fun_evaluate s1 env e)) ≤ clock s1"
proof (induction rule: fun_evaluate_match_fun_evaluate.induct)
  case (2 st env e1 e2 es)

  obtain st' r where *[simp]: "fix_clock st (fun_evaluate st env [e1]) = (st', r)"
    by force

  show ?case
    apply (auto split: prod.splits result.splits)
    subgoal
      using 2(2)[OF *[symmetric]]
      by (smt "*" fix_clock(1) fix_clock.simps fst_conv le_trans prod.collapse)
    subgoal
      using 2(2)[OF *[symmetric]]
      by (smt "*" fix_clock(1) fix_clock.simps fst_conv le_trans prod.collapse)
    subgoal
      by (metis "*" fix_clock(1) fix_clock.simps prod.collapse prod.sel(2))
    done
next
  case (5 st env e pes)

  obtain st' r where *[simp]: "fix_clock st (fun_evaluate st env [e]) = (st', r)"
    by force

  show ?case
    apply (auto split: prod.splits result.splits)
    subgoal
      by (metis "*" fix_clock(1) fix_clock.simps prod.collapse prod.sel(2))
    subgoal
      using 5(2)[OF *[symmetric]]
      by (smt "*" "5.IH"(1) dual_order.trans eq_fst_iff error_result.exhaust error_result.simps(5) error_result.simps(6) fix_clock(2) fix_clock.simps)
    done
next
  case (9 st env op1 es)

  obtain st' r where *[simp]: "fix_clock st (fun_evaluate st env (rev es)) = (st', r)"
    by force

  note do_app.simps[simp del]

  show ?case
    apply (auto split: prod.splits result.splits option.splits if_splits)
    subgoal
      by (metis "*" fix_clock(1) fix_clock.simps prod.collapse prod.sel(2))
    subgoal
      by (metis "*" fix_clock(1) fix_clock.simps prod.collapse prod.sel(2))
    subgoal
      by (smt "*" "9.IH"(2) One_nat_def Suc_pred dec_clock dual_order.trans fix_clock(1) fix_clock.simps fst_conv le_imp_less_Suc nat_less_le prod.collapse)
    subgoal
      by (metis "*" fix_clock(1) fix_clock.simps fst_conv prod.collapse)
    subgoal
      using 9(2)[OF *[symmetric], simplified]
      by (smt "*" Suc_pred dual_order.trans fix_clock(1) fix_clock.simps le_imp_less_Suc less_irrefl_nat nat_le_linear prod.collapse prod.sel(2))
    subgoal
      by (metis "*" fix_clock(1) fix_clock.simps prod.collapse prod.sel(2))
    subgoal
      using 9(2)[OF *[symmetric], simplified]
      by (smt "*" Suc_pred dual_order.trans fix_clock(1) fix_clock.simps le_imp_less_Suc less_irrefl_nat nat_le_linear prod.collapse prod.sel(2))
    done
next
  case (10 st env lop e1 e2)

  obtain st' r where *[simp]: "fix_clock st (fun_evaluate st env [e1]) = (st', r)"
    by force

  show ?case
    apply (auto split: prod.splits result.splits option.splits exp_or_val.splits)
    subgoal
      by (metis "*" fix_clock(1) fix_clock.simps fst_conv prod.collapse)
    subgoal
      using 10(2)[OF *[symmetric]]
      by (metis (no_types, lifting) "*" dual_order.trans fix_clock(1) fix_clock.simps fstI prod.collapse)
    subgoal
      by (metis "*" fix_clock(1) fix_clock.simps prod.collapse snd_conv)
    subgoal
      by (metis "*" fix_clock(1) fix_clock.simps fst_conv prod.exhaust_sel)
    done
next
  case (11 st env e1 e2 e3)

  obtain st' r where *[simp]: "fix_clock st (fun_evaluate st env [e1]) = (st', r)"
    by force

  show ?case
    apply (auto split: prod.splits result.splits option.splits)
    subgoal
      by (metis "*" fix_clock(1) fix_clock.simps fst_conv prod.collapse)
    subgoal
      using 11(2)[OF *[symmetric]]
      by (metis (no_types, lifting) "*" dual_order.trans eq_fst_iff fix_clock(1) fix_clock.simps)
    subgoal
      by (metis "*" fix_clock(1) fix_clock.simps fst_conv prod.exhaust_sel)
    done
next
  case (12 st env e pes)

  obtain st' r where *[simp]: "fix_clock st (fun_evaluate st env [e]) = (st', r)"
    by force

  show ?case
    apply (auto split: prod.splits result.splits option.splits)
    subgoal
      using 12(2)[OF *[symmetric]]
      by (metis (no_types, lifting) "*" dual_order.trans eq_fst_iff fix_clock(1) fix_clock.simps)
    subgoal
      by (metis "*" fix_clock(1) fix_clock.simps fst_conv prod.exhaust_sel)
    done
next
  case (13 st env xo e1 e2)

  obtain st' r where *[simp]: "fix_clock st (fun_evaluate st env [e1]) = (st', r)"
    by force

  show ?case
    apply (auto split: prod.splits result.splits option.splits)
    subgoal
      using 13(2)[OF *[symmetric]]
      by (metis (no_types, lifting) "*" dual_order.trans eq_fst_iff fix_clock(1) fix_clock.simps)
    subgoal
      by (metis "*" fix_clock(1) fix_clock.simps fst_conv prod.exhaust_sel)
    done
qed (auto split: prod.splits result.splits option.splits match_result.splits)

lemma fun_evaluate_clock:
  "fun_evaluate_match s1 env v p v' = (s2, r) ⟹ clock s2 ≤ clock s1"
  "fun_evaluate s1 env e = (s2, r) ⟹ clock s2 ≤ clock s1"
using fun_evaluate_clock0 by (metis fst_conv)+

end

lemma fix_clock_evaluate[simp]:
  "fix_clock s1 (fun_evaluate s1 env e) = fun_evaluate s1 env e"
unfolding fix_clock_alt_def
using fun_evaluate_clock by (fastforce split: prod.splits)

declare fun_evaluate.simps[simp del]
declare fun_evaluate_match.simps[simp del]

lemmas fun_evaluate_simps[simp] =
  fun_evaluate.simps[unfolded fix_clock_evaluate]
  fun_evaluate_match.simps[unfolded fix_clock_evaluate]

lemmas fun_evaluate_induct =
  fun_evaluate_match_fun_evaluate.induct[unfolded fix_clock_evaluate]

lemma fun_evaluate_length:
  "fun_evaluate_match s env v pes err_v = (s', res) ⟹ (case res of Rval vs ⇒ length vs = 1 | _ ⇒ True)"
  "fun_evaluate s env es = (s', res) ⟹ (case res of Rval vs ⇒ length vs = length es | _ ⇒ True)"
proof (induction arbitrary: s' res and s' res rule: fun_evaluate_match_fun_evaluate.induct)
  case (9 st env op1 es)
  then show ?case
    supply do_app.simps[simp del]
    apply (fastforce
        split: if_splits prod.splits result.splits option.splits exp_or_val.splits match_result.splits error_result.splits
        simp: list_result_alt_def)
    done
qed (fastforce
      split: if_splits prod.splits result.splits option.splits exp_or_val.splits
             match_result.splits error_result.splits)+

lemma fun_evaluate_matchE:
  assumes "fun_evaluate_match s env v pes err_v = (s', Rval vs)"
  obtains v where "vs = [v]"
using fun_evaluate_length(1)[OF assms]
by (cases vs) auto

end