theory Usable_Rules_NJ_Impl
imports
Usable_Rules_NJ
"Check-NT.Tcap_Impl"
"Check-NT.Inductive_Set_Impl"
begin
context usable_rules_reachability
begin
lemma U0_generic: "U0 lr t = generic_inductive_set.the_set R
(λ t (l,r). is_Var l ∨ (∃ s. t ⊵ s ∧ is_Fun s ∧ match_tcap_below l R s)) (λ lr. {snd lr}) t lr"
(is "_ = generic_inductive_set.the_set R ?P ?Q t lr")
proof -
interpret generic_inductive_set R ?P ?Q .
show ?thesis
proof
assume "the_set t lr"
thus "U0 lr t"
by (induct rule: the_set.induct, auto intro: U0.intros)
next
assume "U0 lr t"
thus "the_set t lr"
proof (induct rule: U0.induct)
case match
thus ?case
by (intro non_rec, auto)
next
case lvar
thus ?case
by (intro non_rec, auto)
next
case rec
show ?case
by (rule rec_rec[OF rec(2) _ rec(4)], auto)
qed
qed
qed
end
definition usable_rules_reach_U0_impl :: "('f,'v)rules ⇒ ('f,'v)term ⇒ ('f,'v)rules" where
"usable_rules_reach_U0_impl R t = inductive_set_impl
R
(λt (l,r). is_Var l ∨ (∃ u ∈ set (supteq_list t). is_Fun u ∧ match_tcap_below_impl l R u))
(λ lr. [snd lr])
[t]"
definition usable_rules_reach_impl :: "('f,'v)rules ⇒ ('f,'v)term ⇒ ('f,'v)rules" where
"usable_rules_reach_impl R t ≡ let U0t = usable_rules_reach_U0_impl R t in
if (∀ (l,r) ∈ set U0t. vars_term r ⊆ vars_term l) then U0t else R"
lemma usable_rules_reach_impl[simp]: "set (usable_rules_reach_impl R t) = usable_rules_reach (set R) t"
proof -
interpret usable_rules_reachability "set R" .
have [simp]: "set (usable_rules_reach_U0_impl R t) = {lr. U0 lr t}"
unfolding U0_generic usable_rules_reach_U0_impl_def
by (rule inductive_set_impl_single, auto)
show ?thesis unfolding usable_rules_reach_impl_def Ur_def Let_def varcond_def
by (auto split: if_splits)
qed
end