Quelle  Reduction.thy

subsection ‹Reduction relation›

theory Reduction
  imports Substitution
begin

inductive red_term :: "[trm, trm] ==> bool"  (infixl ‹<----› 50) 
      and red_cmd :: "[cmd, cmd] ==> bool"  (infixl ‹_C<----› 50)
where
  beta   [intro]: "(λ T : t)🍋r <---- t[r/0]^T" |
  struct [intro]: "(μ (T1→T2) : c)🍋s <---- μ T2 : (c[0 = 0 (♢ ^\<bullet> (liftM_trm s 0))]^C)" |
  rename [intro]: "[ 0 ∉ (fmv_trm t 0) ] ==> (μ T : (<0> t)) <---- dropM_trm t 0" |
  mueta  [intro]: "<i> (μ T : c) _C<---- (dropM_cmd (c[0 = i ♢]^C) i)" |

  lambda [intro]: "[ s <---- t ] ==> (λ T : s) <---- (λ T : t)" |
  appL   [intro]: "[ s <---- u ] ==> (s🍋t) <---- (u🍋t)" |
  appR   [intro]: "[ t <---- u ] ==> (s🍋t) <---- (s🍋u)" |
  mu     [intro]: "[ c _C<---- d ] ==> (μ T : c) <---- (μ T : d)" |
  cmd    [intro]: "[ t <---- s ] ==> (<i> t) _C<---- (<i> s)"

inductive_cases redE [elim]:
  "`i <---- s"
  "(λ T : t) <---- s"
  "s🍋t <---- u"
  "(μ T : c) <---- t"
  "<i> t _C<---- c"

text‹Reflexive transitive closure›

inductive beta_rtc_term :: "[trm, trm] ==> bool"  (infixl ‹<----^*› 50) where
  refl_term [iff]: "s <----^* s" |
  step_term: "[s <---- t; t <----^* u] ==> s <----^* u"

lemma step_term2: "[s <----^* t; t <---- u] ==> s <----^* u"
  by (induct rule: beta_rtc_term.induct) (auto intro: step_term)

inductive beta_rtc_command :: "[cmd, cmd] ==> bool"  (infixl ‹_C<----^*› 50) where
  refl_command [iff]: "c _C<----^* c" |
  step_command: "c _C<---- d ==> d _C<----^* e ==> c _C<----^* e"

text‹The beta reduction relation is included in the reflexive transitive closure.›
lemma rtc_term_incl [intro]: "s <---- t ==> s <----^* t"
  by (meson beta_rtc_term.simps)

lemma [intro]: "c _C<---- d ==> c _C<----^* d"
  by(auto intro: step_command)

text‹Proof that the reflexive transitive closure as defined above is transitive.›
  
lemma rtc_term_trans [intro]: "s <----^* t ==> t <----^* u ==> s <----^* u"
  by(induction rule: beta_rtc_term.induct) (auto simp add: step_term)

lemma rtc_command_trans[intro]: "c _C<----^* d ==> d _C<----^* e ==> c _C<----^* e"
  by(induction rule: beta_rtc_command.induct) (auto simp add: step_command)

text‹Congruence rules for the reflexive transitive closure.›

lemma rtc_lambda: "s <----^* t ==> (λ T : s) <----^* (λ T : t)"
  apply(induction rule: beta_rtc_term.induct)
  by force (meson red_term_red_cmd.lambda step_term)

lemma rtc_appL: "s <----^* u ==> (s🍋t) <----^* (u🍋t)"
  apply(induction rule: beta_rtc_term.induct)
  by force (meson appL step_term)
    
end