Theory Reduction

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 (◇ ⇧∙ (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