theory Term_Impl
imports
Term_More
Certification_Monads.Check_Monad
Deriving.Compare_Order_Instances
Auxx.Shows_Literal
begin
derive compare_order "term"
definition showsl_pos :: "pos ⇒ showsl" where
"showsl_pos = showsl_list_gen (λ i. showsl (Suc i)) (STR ''empty'') (STR '''') (STR ''.'') (STR '''')"
subsection ‹@{text "showl"} Instance for Terms.›
fun showsl_term' :: "('f ⇒ showsl) ⇒ ('v ⇒ showsl) ⇒ ('f, 'v) term ⇒ showsl"
where
"showsl_term' fun var (Var x) = var x" |
"showsl_term' fun var (Fun f ts) =
fun f ∘ showsl_list_gen id (STR '''') (STR ''('') (STR '', '') (STR '')'') (map (showsl_term' fun var) ts)"
abbreviation showsl_nat_var :: "nat ⇒ showsl"
where
"showsl_nat_var i ≡ showsl_lit (STR ''x'') ∘ showsl i"
abbreviation showsl_nat_term :: "('f::showl, nat) term ⇒ showsl"
where
"showsl_nat_term ≡ showsl_term' showsl showsl_nat_var"
instantiation "term" :: (showl,showl)showl
begin
definition "showsl (t :: ('a,'b)term) = showsl_term' showsl showsl t"
definition "showsl_list (xs :: ('a,'b)term list) = default_showsl_list showsl xs"
instance ..
end
subsection ‹@{text "showl"} Instance for Contexts›
fun showsl_ctxt' :: "('f ⇒ showsl) ⇒ ('v ⇒ showsl) ⇒ ('f, 'v) ctxt ⇒ showsl" where
"showsl_ctxt' fun var (Hole) = showsl_lit (STR ''[]'')"
| "showsl_ctxt' fun var (More f ss1 D ss2) = (
fun f ∘ showsl (STR ''('') ∘
showsl_list_gen (showsl_term' fun var) (STR '''') (STR '''') (STR '', '') (STR '', '') ss1 ∘
showsl_ctxt' fun var D ∘
showsl_list_gen (showsl_term' fun var) (STR '')'') (STR '', '') (STR '', '') (STR '')'') ss2
)"
instantiation ctxt :: (showl,showl)showl
begin
definition "showsl (t :: ('a,'b)ctxt) = showsl_ctxt' showsl showsl t"
definition "showsl_list (xs :: ('a,'b)ctxt list) = default_showsl_list showsl xs"
instance ..
end
fun poss_list :: "('f, 'v) term ⇒ pos list"
where
"poss_list (Var x) = [[]]" |
"poss_list (Fun f ss) = ([] # concat (map (λ (i, ps).
map ((#) i) ps) (zip [0 ..< length ss] (map poss_list ss))))"
lemma poss_list_sound [simp]:
"set (poss_list s) = poss s"
proof (induct s)
case (Fun f ss)
let ?z = "zip [0..<length ss] (map poss_list ss)"
have len: "length ?z = length ss" by auto
have "(⋃a∈set ?z.
set (case_prod (λi. map ((#) i)) a)) =
{i # p |i p. i < length ss ∧ p ∈ poss (ss ! i)}" (is "?l = ?r")
proof (rule set_eqI)
fix ip
show "(ip ∈ ?l) = (ip ∈ ?r)"
proof
assume "ip ∈ ?l"
from this obtain ipI where
z: "ipI ∈ set ?z" and
ip: "ip ∈ set (case_prod (λ i. map ((#) i)) ipI)"
by auto
from z obtain i where i: "i < length ?z" and zi: "?z ! i = ipI"
by (force simp: set_conv_nth)
with ip Fun show "ip ∈ ?r" by auto
next
assume "ip ∈ ?r"
from this obtain i p where i: "i < length ss" and "p ∈ poss (ss ! i)"
and ip: "ip = i # p" by auto
with Fun have p: "p ∈ set (poss_list (ss ! i))" and iz: "i < length ?z" by auto
from i have id: "?z ! i = (i, poss_list (ss ! i))" (is "_ = ?ipI") by auto
from iz have "?z ! i ∈ set ?z" by (rule nth_mem)
with id have inZ: "?ipI ∈ set ?z" by auto
from p have "i # p ∈ set (case_prod (λ i. map ((#) i)) ?ipI)" by auto
with inZ ip show "ip ∈ ?l" by force
qed
qed
with Fun show ?case by simp
qed simp
declare poss_list.simps [simp del]
context
begin
private fun in_poss :: "pos ⇒ ('f, 'v) term ⇒ bool"
where
"in_poss [] _ ⟷ True" |
"in_poss (Cons i p) (Fun f ts) ⟷ i < length ts ∧ in_poss p (ts ! i)" |
"in_poss (Cons i p) (Var _) ⟷ False"
lemma [code_unfold]:
"p ∈ poss t = in_poss p t" by (induct rule: in_poss.induct) auto
end
text ‹Resolve problems with recursive dependencies in generated code.›
lemma [code]:
shows "HOL.eq (Var x) (Var y) ⟷ HOL.eq x y"
and "HOL.eq (Fun f ts) (Fun g us) ⟷ HOL.eq f g ∧ list_all2 HOL.eq ts us"
by (simp_all add: list_all2_eq [symmetric])
subsection ‹Useful abstractions›
text ‹Given that we perform the same operations on terms in order to get
a list of the variables and a list of the functions, we define functions
that run through the term and perform these actions.›
context
begin
private fun contains_var_term :: "'v ⇒ ('f, 'v) term ⇒ bool" where
"contains_var_term x (Var y) = (x = y)"
| "contains_var_term x (Fun _ ts) = Bex (set ts) (contains_var_term x)"
lemma contains_var_term_sound[simp]:
"contains_var_term x t ⟷ x ∈ vars_term t"
by (induct t) auto
lemma [code_unfold]: "x ∈ vars_term t = contains_var_term x t" by simp
end
lemma linear_vars_term_list:
assumes "linear_term t"
shows "length (filter ((=) x) (vars_term_list t)) ≤ 1"
using assms
proof (induct t)
case (Var y)
show ?case by (auto simp: vars_term_list.simps)
next
case (Fun f ss)
show ?case
proof (rule ccontr)
assume "¬ ?thesis"
from this [unfolded vars_term_list.simps]
have len: "2 ≤ length (filter ((=) x) (concat (map vars_term_list ss)))" (is "_ ≤ length ?xs") by auto
from len obtain y ys where xs: "?xs = y # ys" by (cases ?xs, auto)
from len[unfolded xs] obtain z zs where ys: "ys = z # zs" by (cases ys, auto)
from xs[unfolded ys] have "{y,z} ⊆ set ?xs" by auto
from this[unfolded set_filter] have "y = x" and "z = x" by auto
from xs[unfolded ys this] have xs: "?xs = x # x # zs" by auto
{
fix s
assume s: "s ∈ set ss"
with Fun(2)[unfolded linear_term.simps]
have "linear_term s" by auto
note Fun(1)[OF s this]
}
from this Fun(2)[unfolded linear_term.simps] xs
show False
proof (induct ss)
case Nil then show ?case by simp
next
case (Cons s ss) note oCons = this
from Cons(3) have part: "is_partition (map vars_term ss) ∧ (∀ s ∈ set ss. linear_term s)" and lin: "linear_term s" using is_partition_Cons by auto
from Cons(1)[OF _ part] Cons(2)
have ind: "filter ((=) x) (concat (map vars_term_list ss)) ≠ x # x # zs" by auto
show ?case
proof (cases "filter ((=) x) (vars_term_list s)")
case Nil
with Cons(4) ind show False by auto
next
case (Cons y ys)
let ?s = "filter ((=) x) (vars_term_list s)"
let ?ss = "filter ((=) x) (concat (map vars_term_list ss))"
from Cons oCons(4) have "?s = x # ys" by auto
with oCons(2)[of s] have sx: "?s = [x]"
by auto
with oCons(4) have ssx: "?ss = x # zs" by auto
from sx have "x ∈ set ?s" by auto
from this[unfolded set_filter set_vars_term_list]
have sx: "x ∈ vars_term s" by auto
from ssx have "x ∈ set ?ss" by auto
from this[unfolded set_filter set_vars_term_list]
obtain t where tx: "x ∈ vars_term t" and t: "t ∈ set ss" by auto
from t[unfolded set_conv_nth] obtain i where i: "i < length ss" and
t: "t = ss ! i" by auto
from oCons(3)[THEN conjunct1, unfolded is_partition_def, THEN spec[of _ "Suc i"], THEN mp, THEN spec[of _ 0]] i tx[unfolded t] sx
show False by auto
qed
qed
qed
qed
fun supteq_list :: "('f, 'v) term ⇒ ('f, 'v) term list"
where
"supteq_list (Var x) = [Var x]" |
"supteq_list (Fun f ts) = Fun f ts # concat (map supteq_list ts)"
fun supt_list :: "('f, 'v) term ⇒ ('f, 'v) term list"
where
"supt_list (Var x) = []" |
"supt_list (Fun f ts) = concat (map supteq_list ts)"
lemma supteq_list [simp]:
"set (supteq_list t) = {s. t ⊵ s}"
proof (rule set_eqI, simp)
fix s
show "s ∈ set(supteq_list t) = (t ⊵ s)"
proof (induct t, simp add: supteq_var_imp_eq)
case (Fun f ss)
show ?case
proof (cases "Fun f ss = s", (auto)[1])
case False
show ?thesis
proof
assume "Fun f ss ⊵ s"
with False have sup: "Fun f ss ⊳ s" using supteq_supt_conv by auto
obtain C where "C ≠ □" and "Fun f ss = C⟨s⟩" using sup by auto
then obtain b D a where "Fun f ss = Fun f (b @ D⟨s⟩ # a)" by (cases C, auto)
then have D: "D⟨s⟩ ∈ set ss" by auto
with Fun[OF D] ctxt_imp_supteq[of D s] obtain t where "t ∈ set ss" and "s ∈ set (supteq_list t)" by auto
then show "s ∈ set (supteq_list (Fun f ss))" by auto
next
assume "s ∈ set (supteq_list (Fun f ss))"
with False obtain t where t: "t ∈ set ss" and "s ∈ set (supteq_list t)" by auto
with Fun[OF t] have "t ⊵ s" by auto
with t show "Fun f ss ⊵ s" by auto
qed
qed
qed
qed
lemma supt_list_sound [simp]:
"set (supt_list t) = {s. t ⊳ s}"
by (cases t) auto
fun supt_impl :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool"
where
"supt_impl (Var x) t ⟷ False" |
"supt_impl (Fun f ss) t ⟷ t ∈ set ss ∨ Bex (set ss) (λs. supt_impl s t)"
lemma supt_impl [code_unfold]:
"s ⊳ t ⟷ supt_impl s t"
proof
assume "s ⊳ t" then show "supt_impl s t"
proof (induct s)
case (Var x) then show ?case by auto
next
case (Fun f ss) then show ?case
proof (cases "t ∈ set ss")
case True then show ?thesis by (simp)
next
case False
assume "⋀s. ⟦s ∈ set ss; s ⊳ t⟧ ⟹ supt_impl s t"
and "Fun f ss ⊳ t" and "t ∉ set ss"
moreover from ‹Fun f ss ⊳ t› obtain s where "s ∈ set ss" and "s ⊳ t"
by (cases rule: supt.cases) (simp_all add: ‹t ∉ set ss›)
ultimately have "supt_impl s t" by simp
with ‹s ∈ set ss› show ?thesis by auto
qed
qed
next
assume "supt_impl s t"
then show "s ⊳ t"
proof (induct s)
case (Var x) then show ?case by simp
next
case (Fun f ss)
then have "t ∈ set ss ∨ (∃s∈set ss. supt_impl s t)" by simp
then show ?case
proof
assume "t ∈ set ss" then show ?case by (auto intro: supt.intros)
next
assume "∃s∈set ss. supt_impl s t"
then obtain s where "s ∈ set ss" and "supt_impl s t" by auto
with Fun have "s ⊳ t" by auto
with ‹s ∈ set ss› show ?thesis by (auto intro: supt.intros)
qed
qed
qed
lemma supteq_impl[code_unfold]: "s ⊵ t ⟷ s = t ∨ supt_impl s t"
unfolding supteq_supt_set_conv
by (auto simp: supt_impl)
fun
linear_term_impl :: "'v set ⇒ ('f, 'v) term ⇒ ('v set) option"
where
"linear_term_impl xs (Var x) = (if x ∈ xs then None else Some (insert x xs))" |
"linear_term_impl xs (Fun _ []) = Some xs" |
"linear_term_impl xs (Fun f (t # ts)) = (case linear_term_impl xs t of
None ⇒ None
| Some ys ⇒ linear_term_impl ys (Fun f ts))"
lemma [code]: "linear_term t = (linear_term_impl {} t ≠ None)"
proof -
{
note [simp] = is_partition_Nil is_partition_Cons
fix xs ys
let ?P = "λ ys xs t. (linear_term_impl xs t = None ⟶ (xs ∩ vars_term t ≠ {} ∨ ¬ linear_term t)) ∧
(linear_term_impl xs t = Some ys ⟶ (ys = (xs ∪ vars_term t)) ∧ xs ∩ vars_term t = {} ∧ linear_term t)"
have "?P ys xs t"
proof (induct rule: linear_term_impl.induct[of "λ xs t. ∀ ys. ?P ys xs t", rule_format])
case (3 xs f t ts zs)
show ?case
proof (cases "linear_term_impl xs t")
case None
with 3 show ?thesis by auto
next
case (Some ys)
note some = this
with 3 have rec1: "ys = xs ∪ vars_term t ∧ xs ∩ vars_term t = {} ∧ linear_term t" by auto
show ?thesis
proof (cases "linear_term_impl ys (Fun f ts)")
case None
with rec1 Some have res: "linear_term_impl xs (Fun f (t # ts)) = None" by simp
from None 3(2) Some have rec2: "ys ∩ vars_term (Fun f ts) ≠ {} ∨ ¬ linear_term (Fun f ts)" by simp
then have "xs ∩ vars_term (Fun f (t # ts)) ≠ {} ∨ ¬ linear_term (Fun f (t # ts))"
proof
assume "ys ∩ vars_term (Fun f ts) ≠ {}"
then obtain x where x1: "x ∈ ys" and x2: "x ∈ vars_term (Fun f ts)" by auto
show ?thesis
proof (cases "x ∈ xs")
case True
with x2 show ?thesis by auto
next
case False
with x1 rec1 have "x ∈ vars_term t" by auto
with x2 have "¬ linear_term (Fun f (t # ts))" by auto
then show ?thesis ..
qed
next
assume "¬ linear_term (Fun f ts)" then have "¬ linear_term (Fun f (t # ts))" by auto
then show ?thesis ..
qed
with res show ?thesis by auto
next
case (Some us)
with some have res: "linear_term_impl xs (Fun f (t # ts)) = Some us" by auto
{
assume us: "us = zs"
from Some[simplified us] 3(2) some
have rec2: "zs = ys ∪ vars_term (Fun f ts) ∧ ys ∩ vars_term (Fun f ts) = {} ∧ linear_term (Fun f ts)" by auto
from rec1 rec2
have part1: "zs = xs ∪ vars_term (Fun f (t # ts)) ∧ xs ∩ vars_term (Fun f (t # ts)) = {}" (is ?part1) by auto
from rec1 rec2 have "vars_term t ∩ vars_term (Fun f ts) = {}" and "linear_term t" and "linear_term (Fun f ts)" by auto
then have "linear_term (Fun f (t # ts))" (is ?part2) by auto
with part1 have "?part1 ∧ ?part2" ..
}
with res show ?thesis by auto
qed
qed
qed auto
} note main = this
from main[of "{}"] show ?thesis by (cases "linear_term_impl {} t", auto)
qed
definition check_no_var :: "('f::showl, 'v::showl) term ⇒ showsl check" where
"check_no_var t ≡ check (is_Fun t) (showsl (STR ''variable found⏎''))"
lemma check_no_var_sound[simp]:
"isOK (check_no_var t) ⟷ is_Fun t"
unfolding check_no_var_def by simp
definition
check_supt :: "('f::showl, 'v::showl) term ⇒ ('f, 'v) term ⇒ showsl check"
where
"check_supt s t ≡ check (s ⊳ t) (showsl t ∘ showsl (STR '' is not a proper subterm of '') ∘ showsl s)"
definition
check_supteq :: "('f::showl, 'v::showl) term ⇒ ('f, 'v) term ⇒ showsl check"
where
"check_supteq s t ≡ check (s ⊵ t) (showsl t ∘ showsl (STR '' is not a subterm of '') ∘ showsl s)"
lemma isOK_check_supt [simp]:
"isOK (check_supt s t) ⟷ s ⊳ t"
by (auto simp: check_supt_def)
lemma isOK_check_supteq [simp]:
"isOK (check_supteq s t) ⟷ s ⊵ t"
by (auto simp: check_supteq_def)
subsection ‹Additional Functions on Terms›
fun with_arity :: "('f, 'v) term ⇒ ('f × nat, 'v) term" where
"with_arity (Var x) = Var x"
| "with_arity (Fun f ts) = Fun (f, length ts) (map with_arity ts)"
fun add_vars_term :: "('f, 'v) term ⇒ 'v list ⇒ 'v list"
where
"add_vars_term (Var x) xs = x # xs" |
"add_vars_term (Fun _ ts) xs = foldr add_vars_term ts xs"
fun add_funs_term :: "('f, 'v) term ⇒ 'f list ⇒ 'f list"
where
"add_funs_term (Var _) fs = fs" |
"add_funs_term (Fun f ts) fs = f # foldr add_funs_term ts fs"
fun add_funas_term :: "('f, 'v) term ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
"add_funas_term (Var _) fs = fs" |
"add_funas_term (Fun f ts) fs = (f, length ts) # foldr add_funas_term ts fs"
definition add_funas_args_term :: "('f, 'v) term ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
"add_funas_args_term t fs = foldr add_funas_term (args t) fs"
lemma add_vars_term_vars_term_list_conv [simp]:
"add_vars_term t xs = vars_term_list t @ xs"
proof (induct t arbitrary: xs)
case (Fun f ts)
then show ?case by (induct ts) (simp_all add: vars_term_list.simps)
qed (simp add: vars_term_list.simps)
lemma add_funs_term_funs_term_list_conv [simp]:
"add_funs_term t fs = funs_term_list t @ fs"
proof (induct t arbitrary: fs)
case (Fun f ts)
then show ?case by (induct ts) (simp_all add: funs_term_list.simps)
qed (simp add: funs_term_list.simps)
lemma add_funas_term_funas_term_list_conv [simp]:
"add_funas_term t fs = funas_term_list t @ fs"
proof (induct t arbitrary: fs)
case (Fun f ts)
then show ?case by (induct ts) (simp_all add: funas_term_list.simps)
qed (simp add: funas_term_list.simps)
lemma add_vars_term_vars_term_list_abs_conv [simp]:
"add_vars_term = (@) ∘ vars_term_list"
by (intro ext) simp
lemma add_funs_term_funs_term_list_abs_conv [simp]:
"add_funs_term = (@) ∘ funs_term_list"
by (intro ext) simp
lemma add_funas_term_funas_term_list_abs_conv [simp]:
"add_funas_term = (@) ∘ funas_term_list"
by (intro ext) simp
lemma add_funas_args_term_funas_args_term_list_conv [simp]:
"add_funas_args_term t fs = funas_args_term_list t @ fs"
by (simp add: add_funas_args_term_def funas_args_term_list_def concat_conv_foldr foldr_map)
fun insert_vars_term :: "('f, 'v) term ⇒ 'v list ⇒ 'v list"
where
"insert_vars_term (Var x) xs = List.insert x xs" |
"insert_vars_term (Fun f ts) xs = foldr insert_vars_term ts xs"
fun insert_funs_term :: "('f, 'v) term ⇒ 'f list ⇒ 'f list"
where
"insert_funs_term (Var x) fs = fs" |
"insert_funs_term (Fun f ts) fs = List.insert f (foldr insert_funs_term ts fs)"
fun insert_funas_term :: "('f, 'v) term ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
"insert_funas_term (Var x) fs = fs" |
"insert_funas_term (Fun f ts) fs = List.insert (f, length ts) (foldr insert_funas_term ts fs)"
definition insert_funas_args_term :: "('f, 'v) term ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
"insert_funas_args_term t fs = foldr insert_funas_term (args t) fs"
lemma set_insert_vars_term_vars_term [simp]:
"set (insert_vars_term t xs) = vars_term t ∪ set xs"
proof (induct t arbitrary: xs)
case (Fun f ts)
then show ?case by (induct ts) auto
qed simp
lemma set_insert_funs_term_funs_term [simp]:
"set (insert_funs_term t fs) = funs_term t ∪ set fs"
proof (induct t arbitrary: fs)
case (Fun f ts)
then show ?case by (induct ts) auto
qed simp
lemma set_insert_funas_term_funas_term [simp]:
"set (insert_funas_term t fs) = funas_term t ∪ set fs"
proof (induct t arbitrary: fs)
case (Fun f ts)
then have "set (foldr insert_funas_term ts fs) = ⋃ (funas_term ` set ts) ∪ set fs"
by (induct ts) auto
then show ?case by simp
qed simp
lemma set_insert_funas_args_term [simp]:
"set (insert_funas_args_term t fs) = ⋃ (funas_term ` set (args t)) ∪ set fs"
proof (induct t arbitrary: fs)
case (Fun f ts)
then show ?case by (induct ts) (auto simp: insert_funas_args_term_def)
qed (simp add: insert_funas_args_term_def)
text ‹Implementations of corresponding set-based functions.›
abbreviation "vars_term_impl t ≡ insert_vars_term t []"
abbreviation "funs_term_impl t ≡ insert_funs_term t []"
abbreviation "funas_term_impl t ≡ insert_funas_term t []"
lemma [code]:
"vars_term_list t = add_vars_term t []"
"funs_term_list t = add_funs_term t []"
by simp_all
lemma with_arity_term_fold [code]:
"with_arity = Term_More.fold Var (λf ts. Fun (f, length ts) ts)"
proof
fix t :: "('f, 'v) term"
show "with_arity t = Term_More.fold Var (λf ts. Fun (f, length ts) ts) t"
by (induct t) simp_all
qed
fun flatten_term_enum :: "('f list, 'v) term ⇒ ('f, 'v) term list"
where
"flatten_term_enum (Var x) = [Var x]" |
"flatten_term_enum (Fun fs ts) =
(let
lts = map flatten_term_enum ts;
ss = concat_lists lts
in concat (map (λ f. map (Fun f) ss) fs))"
lemma flatten_term_enum:
"set (flatten_term_enum t) = {u. instance_term u (map_funs_term set t)}"
proof (induct t)
case (Var x)
show ?case (is "_ = ?R")
proof -
{
fix t
assume "t ∈ ?R"
then have "t = Var x" by (cases t, auto)
}
then show ?thesis by auto
qed
next
case (Fun fs ts)
show ?case (is "?L = ?R")
proof -
{
fix i
assume "i < length ts"
then have "ts ! i ∈ set ts" by auto
note Fun[OF this]
} note ind = this
have idL: "?L = {Fun g ss | g ss. g ∈ set fs ∧ length ss = length ts ∧ (∀i<length ts. ss ! i ∈ set (flatten_term_enum (ts ! i)))}" (is "_ = ?M1") by auto
let ?R1 = "{Fun f ss | f ss. f ∈ set fs ∧ length ss = length ts ∧ (∀ i<length ss. instance_term (ss ! i) (map_funs_term set (ts ! i)))}"
{
fix u
assume "u ∈ ?R"
then have "u ∈ ?R1" by (cases u, auto)
}
then have idR: "?R = ?R1" by auto
show ?case unfolding idL idR using ind by auto
qed
qed
definition mk_subst_domain :: "('f, 'v) substL ⇒ ('v × ('f, 'v) term) list" where
"mk_subst_domain σ ≡
let τ = mk_subst Var σ in
(filter (λ(x, t). Var x ≠ t) (map (λ x. (x, τ x)) (remdups (map fst σ))))"
lemma mk_subst_domain:
"set (mk_subst_domain σ) = (λ x. (x, mk_subst Var σ x)) ` subst_domain (mk_subst Var σ)"
(is "?I = ?R")
proof -
have "?I ⊆ ?R" unfolding mk_subst_domain_def Let_def subst_domain_def by auto
moreover
{
fix xt
assume mem: "xt ∈ ?R"
obtain x t where xt: "xt = (x, t)" by force
from mem [unfolded xt]
have x: "x ∈ subst_domain (mk_subst Var σ)" and t: "t = mk_subst Var σ x" by auto
then have "mk_subst Var σ x ≠ Var x" unfolding subst_domain_def by simp
with t have l: "map_of σ x = Some t" and tx: "t ≠ Var x"
unfolding mk_subst_def by (cases "map_of σ x", auto)
from map_of_SomeD[OF l] l t tx have "(x,t) ∈ ?I" unfolding mk_subst_domain_def Let_def
by force
then have "xt ∈ ?I" unfolding xt .
}
ultimately show ?thesis by blast
qed
lemma finite_mk_subst: "finite (subst_domain (mk_subst Var σ))"
proof -
have "subst_domain (mk_subst Var σ) = fst ` set (mk_subst_domain σ)"
unfolding mk_subst_domain Let_def by force
moreover have "finite ..."
using finite_set by auto
ultimately show ?thesis by simp
qed
definition subst_eq :: "('f, 'v) substL ⇒ ('f, 'v) substL ⇒ bool" where
"subst_eq σ τ = (let σ' = mk_subst_domain σ; τ' = mk_subst_domain τ in set σ' = set τ')"
lemma subst_eq [simp]:
"subst_eq σ τ = (mk_subst Var σ = mk_subst Var τ)"
proof -
let ?σ = "mk_subst Var σ"
let ?τ = "mk_subst Var τ"
{
assume id: "((λ x. (x, ?σ x)) ` subst_domain ?σ) = ((λ x. (x, ?τ x)) ` subst_domain ?τ)" (is "?l = ?r")
from arg_cong[OF id, of "(`) fst"] have idd: "subst_domain ?σ = subst_domain ?τ" by force
have "?σ = ?τ"
proof (rule ext)
fix x
show "?σ x = ?τ x"
proof (cases "x ∈ subst_domain ?σ")
case False
then show ?thesis using idd unfolding subst_domain_def by auto
next
case True
with idd have x: "(x,?σ x) ∈ ?l" "(x,?τ x) ∈ ?r" by auto
with id have x: "(x,?τ x) ∈ ?l" "(x,?σ x) ∈ ?l" by auto
then show ?thesis by auto
qed
qed
}
then show ?thesis
unfolding subst_eq_def Let_def
unfolding mk_subst_domain by auto
qed
definition range_vars_impl :: "('f, 'v) substL ⇒ 'v list"
where
"range_vars_impl σ =
(let σ' = mk_subst_domain σ in
concat (map (vars_term_list o snd) σ'))"
definition vars_subst_impl :: "('f, 'v) substL ⇒ 'v list"
where
"vars_subst_impl σ =
(let σ' = mk_subst_domain σ in
map fst σ' @ concat (map (vars_term_list o snd) σ'))"
lemma vars_subst_impl [simp]:
"set (vars_subst_impl σ) = vars_subst (mk_subst Var σ)"
unfolding vars_subst_def vars_subst_impl_def Let_def
by (auto simp: mk_subst_domain, force)
lemma range_vars_impl [simp]:
"set (range_vars_impl σ) = range_vars (mk_subst Var σ)"
unfolding range_vars_def range_vars_impl_def Let_def
by (auto simp: mk_subst_domain)
lemma mk_subst_one [simp]: "mk_subst Var [(x, t)] = subst x t"
unfolding mk_subst_def subst_def by auto
lemma fst_image [simp]: "fst ` (λ x. (x,g x)) ` a = a" by force
definition
subst_compose_impl :: "('f, 'v) substL ⇒ ('f, 'v) substL ⇒ ('f, 'v) substL"
where
"subst_compose_impl σ τ ≡
let
σ' = mk_subst_domain σ;
τ' = mk_subst_domain τ;
dσ = map fst σ'
in map (λ (x, t). (x, t ⋅ mk_subst Var τ')) σ' @ filter (λ (x, t). x ∉ set dσ) τ'"
lemma mk_subst_mk_subst_domain [simp]:
"mk_subst Var (mk_subst_domain σ) = mk_subst Var σ"
proof (intro ext)
fix x
{
assume x: "x ∉ subst_domain (mk_subst Var σ)"
then have σ: "mk_subst Var σ x = Var x" unfolding subst_domain_def by auto
from x have "x ∉ fst ` set (mk_subst_domain σ)" unfolding mk_subst_domain by auto
then have look: "map_of (mk_subst_domain σ) x = None" by (cases "map_of (mk_subst_domain σ) x", insert map_of_SomeD[of "mk_subst_domain σ" x], force+)
then have "mk_subst Var (mk_subst_domain σ) x = mk_subst Var σ x" unfolding σ
unfolding mk_subst_def by auto
} note ndom = this
{
assume "x ∈ subst_domain (mk_subst Var σ)"
then have "x ∈ fst ` set (mk_subst_domain σ)" unfolding mk_subst_domain by auto
then obtain t where look: "map_of (mk_subst_domain σ) x = Some t" by (cases "map_of (mk_subst_domain σ) x", (force simp: map_of_eq_None_iff)+)
from map_of_SomeD[OF look, unfolded mk_subst_domain] have t: "t = mk_subst Var σ x" by auto
from look t have res: "mk_subst Var (mk_subst_domain σ) x = mk_subst Var σ x" unfolding mk_subst_def by auto
} note dom = this
from ndom dom
show "mk_subst Var (mk_subst_domain σ) x = mk_subst Var σ x" by auto
qed
lemma subst_compose_impl [simp]:
"mk_subst Var (subst_compose_impl σ τ) = mk_subst Var σ ∘⇩s mk_subst Var τ" (is "?l = ?r")
proof (rule ext)
fix x
let ?σ = "mk_subst Var σ"
let ?τ = "mk_subst Var τ"
let ?s = "map (λ (x, t). (x, t ⋅ mk_subst Var (mk_subst_domain τ))) (mk_subst_domain σ)"
let ?t = "[(x,t) ← mk_subst_domain τ. x ∉ set (map fst (mk_subst_domain σ))]"
note d = subst_compose_impl_def[unfolded Let_def]
show "?l x = ?r x"
proof (cases "x ∈ subst_domain (mk_subst Var σ)")
case True
then have "?σ x ≠ Var x" unfolding subst_domain_def by auto
then obtain t where look: "map_of σ x = Some t" and σ: "?σ x = t"
unfolding mk_subst_def by (cases "map_of σ x", auto)
from σ have r: "?r x = t ⋅ ?τ" unfolding subst_compose_def by simp
from True have "x ∈ subst_domain (mk_subst Var (mk_subst_domain σ))"
by simp
from σ True have mem: "(x,t ⋅ ?τ) ∈ set ?s" by (auto simp: mk_subst_domain)
with map_of_eq_None_iff[of "?s" x]
obtain u where look2: "map_of ?s x = Some u"
by (cases "map_of ?s x", force+)
from map_of_SomeD[OF this] σ have u: "u = t ⋅ ?τ"
by (auto simp: mk_subst_domain)
note look2 = map_of_append_Some[OF look2, of ?t]
have l: "?l x = t ⋅ ?τ" unfolding d mk_subst_def[of Var "?s @ ?t"] look2 u
by simp
from l r show ?thesis by simp
next
case False
then have σ: "?σ x = Var x" unfolding subst_domain_def by auto
from σ have r: "?r x = ?τ x" unfolding subst_compose_def by simp
from False have "x ∉ subst_domain (mk_subst Var (mk_subst_domain σ))"
by simp
from False have mem: "⋀ y. (x,y) ∉ set ?s" by (auto simp: mk_subst_domain)
with map_of_SomeD[of ?s x] have look2: "map_of ?s x = None"
by (cases "map_of ?s x", auto)
note look2 = map_of_append_None[OF look2, of ?t]
have l: "?l x = (case map_of ?t x of None ⇒ Var x | Some t ⇒ t)" unfolding d mk_subst_def[of Var "?s @ ?t"] look2 by simp
also have "... = ?τ x"
proof (cases "x ∈ subst_domain ?τ")
case True
then have "?τ x ≠ Var x" unfolding subst_domain_def by auto
then obtain t where look: "map_of τ x = Some t" and τ: "?τ x = t"
unfolding mk_subst_def by (cases "map_of τ x", auto)
from True have "x ∈ subst_domain (mk_subst Var (mk_subst_domain τ))"
by simp
from τ True have mem: "(x,?τ x) ∈ set ?t" using False by (auto simp: mk_subst_domain)
with map_of_eq_None_iff[of ?t x] obtain u where look2: "map_of ?t x = Some u"
by (cases "map_of ?t x", force+)
from map_of_SomeD[OF this] τ have u: "u = ?τ x"
by (auto simp: mk_subst_domain)
show ?thesis using look2 u by simp
next
case False
then have τ: "?τ x = Var x" unfolding subst_domain_def by auto
from False have "x ∉ subst_domain (mk_subst Var (mk_subst_domain τ))"
by simp
from False have mem: "⋀ y. (x,y) ∉ set ?t" by (auto simp: mk_subst_domain)
with map_of_SomeD[of ?t x] have look2: "map_of ?t x = None"
by (cases "map_of ?t x", auto)
show ?thesis unfolding τ look2 by simp
qed
finally show ?thesis unfolding r by simp
qed
qed
fun subst_power_impl :: "('f, 'v) substL ⇒ nat ⇒ ('f, 'v) substL" where
"subst_power_impl σ 0 = []"
| "subst_power_impl σ (Suc n) = subst_compose_impl σ (subst_power_impl σ n)"
lemma subst_power_impl [simp]:
"mk_subst Var (subst_power_impl σ n) = (mk_subst Var σ)^^n"
by (induct n, auto)
definition commutes_impl :: "('f, 'v) substL ⇒ ('f, 'v) substL ⇒ bool" where
"commutes_impl σ μ ≡ subst_eq (subst_compose_impl σ μ) (subst_compose_impl μ σ)"
lemma commutes_impl [simp]:
"commutes_impl σ μ = ((mk_subst Var σ ∘⇩s mk_subst Var μ) = (mk_subst Var μ ∘⇩s mk_subst Var σ))"
unfolding commutes_impl_def by simp
definition
subst_compose'_impl :: "('f, 'v) substL ⇒ ('f, 'v) subst ⇒ ('f, 'v) substL"
where
"subst_compose'_impl σ ρ ≡ map (λ (x, s). (x, s ⋅ ρ)) (mk_subst_domain σ)"
lemma subst_compose'_impl [simp]:
"mk_subst Var (subst_compose'_impl σ ρ) = subst_compose' (mk_subst Var σ) ρ" (is "?l = ?r")
proof (rule ext)
fix x
note d = subst_compose'_def subst_compose'_impl_def
let ?σ = "mk_subst Var σ"
let ?s = "subst_compose'_impl σ ρ"
show "?l x = ?r x"
proof (cases "x ∈ subst_domain (mk_subst Var σ)")
case True
then have r: "?r x = ?σ x ⋅ ρ" unfolding d by simp
from True have "(x, ?σ x) ∈ set (mk_subst_domain σ)" unfolding mk_subst_domain by auto
then have "(x, ?σ x ⋅ ρ) ∈ set ?s" unfolding d by auto
with map_of_eq_None_iff[of ?s x] obtain u where look: "map_of ?s x = Some u"
by (cases "map_of ?s x", force+)
from map_of_SomeD[OF this] have u: "u = ?σ x ⋅ ρ" unfolding d using mk_subst_domain[of σ] by auto
then have l: "?l x = ?σ x ⋅ ρ" using look u unfolding mk_subst_def by auto
from l r show ?thesis by simp
next
case False
then have r: "?r x = Var x" unfolding d by simp
from False have "⋀ y. (x,y) ∉ set ?s" unfolding d
by (auto simp: mk_subst_domain)
with map_of_SomeD[of ?s x] have look: "map_of ?s x = None"
by (cases "map_of ?s x", auto)
then have l: "?l x = Var x" unfolding mk_subst_def by simp
from l r show ?thesis by simp
qed
qed
definition
subst_replace_impl :: "('f, 'v) substL ⇒ 'v ⇒ ('f, 'v) term ⇒ ('f, 'v) substL"
where
"subst_replace_impl σ x t ≡ (x, t) # filter (λ (y, t). y ≠ x) σ"
lemma subst_replace_impl [simp]:
"mk_subst Var (subst_replace_impl σ x t) = (λ y. if x = y then t else mk_subst Var σ y)" (is "?l = ?r")
proof (rule ext)
fix y
note d = subst_replace_impl_def
show "?l y = ?r y"
proof (cases "y = x")
case True
then show ?thesis unfolding d mk_subst_def by auto
next
case False
let ?σ = "mk_subst Var σ"
from False have r: "?r y = ?σ y" by auto
from False have l: "?l y = mk_subst Var ([(y, t)←σ . y ≠ x]) y" unfolding mk_subst_def d
by simp
also have "... = ?σ y" unfolding mk_subst_def
using map_of_filter[of "λ y. y ≠ x" y σ, OF False] by simp
finally show ?thesis using r by simp
qed
qed
lemma mk_subst_domain_distinct: "distinct (map fst (mk_subst_domain σ))"
unfolding mk_subst_domain_def Let_def distinct_map
by (rule conjI[OF distinct_filter], auto simp: distinct_map inj_on_def)
definition is_renaming_impl :: "('f,'v) substL ⇒ bool" where
"is_renaming_impl σ ≡
let σ' = map snd (mk_subst_domain σ) in
(∀ t ∈ set σ'. is_Var t) ∧ distinct σ'"
lemma is_renaming_impl [simp]:
"is_renaming_impl σ = is_renaming (mk_subst Var σ)" (is "?l = ?r")
proof -
let ?σ = "mk_subst Var σ"
let ?d = "mk_subst_domain σ"
let ?m = "map snd ?d"
let ?k = "map fst ?d"
have "?l = ((∀ t ∈ set ?m. is_Var t) ∧ distinct ?m)" unfolding is_renaming_impl_def Let_def by auto
also have "(∀ t ∈ set ?m. is_Var t) = (∀ x. is_Var (?σ x))"
by (force simp: mk_subst_domain subst_domain_def)
also have "distinct ?m = inj_on ?σ (subst_domain ?σ)"
proof
assume inj: "inj_on ?σ (subst_domain ?σ)"
show "distinct ?m" unfolding distinct_conv_nth
proof (intro allI impI)
fix i j
assume i: "i < length ?m" and j: "j < length ?m" and ij: "i ≠ j"
obtain x t where di: "?d ! i = (x,t)" by (cases "?d ! i", auto)
obtain y s where dj: "?d ! j = (y,s)" by (cases "?d ! j", auto)
from di i have mi: "?m ! i = t" and ki: "?k ! i = x" by auto
from dj j have mj: "?m ! j = s" and kj: "?k ! j = y" by auto
from di i have xt: "(x,t) ∈ set ?d" unfolding set_conv_nth by force
from dj j have ys: "(y,s) ∈ set ?d" unfolding set_conv_nth by force
from xt ys have d: "x ∈ subst_domain ?σ" "y ∈ subst_domain ?σ" unfolding mk_subst_domain by auto
have dist: "distinct ?k" by (rule mk_subst_domain_distinct)
from ij i j have xy: "x ≠ y" unfolding ki[symmetric] kj[symmetric]
using dist[unfolded distinct_conv_nth] by auto
from xt ys have m: "?σ x = t" "?σ y = s" unfolding mk_subst_domain by auto
from inj[unfolded inj_on_def, rule_format, OF d]
show "?m ! i ≠ ?m ! j" unfolding m mi mj using xy by auto
qed
next
assume dist: "distinct ?m"
show "inj_on ?σ (subst_domain ?σ)" unfolding inj_on_def
proof (intro ballI impI)
fix x y
assume x: "x ∈ subst_domain ?σ" and y: "y ∈ subst_domain ?σ"
and id: "?σ x = ?σ y"
from x y have x: "(x,?σ x) ∈ set ?d" and y: "(y,?σ y) ∈ set ?d"
unfolding mk_subst_domain by auto
from x obtain i where di: "?d ! i = (x,?σ x)" and i: "i < length ?d" unfolding set_conv_nth by auto
from y obtain j where dj: "?d ! j = (y,?σ y)" and j: "j < length ?d" unfolding set_conv_nth by auto
from di i have mi: "?m ! i = ?σ x" by simp
from dj j have mj: "?m ! j = ?σ x" unfolding id by simp
from mi mj have id: "?m ! i = ?m ! j" by simp
from dist[unfolded distinct_conv_nth] i j id have id: "i = j" by auto
with di dj
show "x = y" by auto
qed
qed
finally
show ?thesis unfolding is_renaming_def by simp
qed
definition is_inverse_renaming_impl :: "('f, 'v) substL ⇒ ('f, 'v) substL" where
"is_inverse_renaming_impl σ ≡
let σ' = mk_subst_domain σ in
map (λ (x, y). (the_Var y, Var x)) σ'"
lemma is_inverse_renaming_impl [simp]:
fixes σ :: "('f, 'v) substL"
assumes var: "is_renaming (mk_subst Var σ)"
shows "mk_subst Var (is_inverse_renaming_impl σ) = is_inverse_renaming (mk_subst Var σ)" (is "?l = ?r")
proof (rule ext)
fix x
let ?σ = "mk_subst Var σ"
let ?σ' = "mk_subst_domain σ"
let ?m = "map (λ (x, y). (the_Var y, Var x :: ('f, 'v) term)) ?σ'"
let ?ran = "subst_range ?σ"
note d = is_inverse_renaming_impl_def is_inverse_renaming_def
{
fix t
assume "(x,t) ∈ set ?m"
then obtain u z where id: "(x,t) = (the_Var u,Var z)" and mem: "(z,u) ∈ set ?σ'" by auto
from var[unfolded is_renaming_def] mem obtain zz where u: "u = Var zz"
unfolding mk_subst_domain by auto
from id[unfolded u] have id: "zz = x" "t = Var z" by auto
with mem u have "(z,Var x) ∈ set ?σ'" by auto
then have "?σ z = Var x" "z ∈ subst_domain ?σ" unfolding mk_subst_domain by auto
with id have "∃ z. t = Var z ∧ ?σ z = Var x ∧ z ∈ subst_domain ?σ" by auto
} note one = this
have "?l x = mk_subst Var ?m x" unfolding d by simp
also have "... = ?r x"
proof (cases "Var x ∈ ?ran")
case False
{
fix t
assume "(x,t) ∈ set ?m"
from one[OF this] obtain z where t: "t = Var z" and z: "?σ z = Var x"
and dom: "z ∈ subst_domain ?σ" by auto
from z dom False have False by force
}
from this[OF map_of_SomeD[of ?m x]] have look: "map_of ?m x = None"
by (cases "map_of ?m x", auto)
then have "mk_subst Var ?m x = Var x" unfolding mk_subst_def by auto
also have "... = ?r x" using False unfolding d by simp
finally show ?thesis .
next
case True
then obtain y where y: "y ∈ subst_domain ?σ" and x: "?σ y = Var x" by auto
then have "(y,Var x) ∈ set ?σ'" unfolding mk_subst_domain by auto
then have "(x,Var y) ∈ set ?m" by force
then obtain u where look: "map_of ?m x = Some u" using map_of_eq_None_iff[of ?m x]
by (cases "map_of ?m x", force+)
from map_of_SomeD[OF this] have xu: "(x,u) ∈ set ?m" by auto
from one[OF this] obtain z where u: "u = Var z" and z: "?σ z = Var x" and dom: "z ∈ subst_domain ?σ" by auto
have "mk_subst Var ?m x = Var z" unfolding mk_subst_def look u by simp
also have "... = ?r x" using is_renaming_inverse_domain[OF var dom] z by auto
finally show ?thesis .
qed
finally show "?l x = ?r x" .
qed
definition
mk_subst_case :: "'v list ⇒ ('f, 'v) subst ⇒ ('f, 'v) substL ⇒ ('f, 'v) substL"
where
"mk_subst_case xs σ τ = subst_compose_impl (map (λ x. (x, σ x)) xs) τ"
lemma mk_subst_case [simp]:
"mk_subst Var (mk_subst_case xs σ τ) =
(λ x. if x ∈ set xs then σ x ⋅ mk_subst Var τ else mk_subst Var τ x)"
proof -
let ?m = "map (λ x. (x, σ x)) xs"
have id: "mk_subst Var ?m = (λ x. if x ∈ set xs then σ x else Var x)" (is "?l = ?r")
proof (rule ext)
fix x
show "?l x = ?r x"
proof (cases "x ∈ set xs")
case True
then have "(x,σ x) ∈ set ?m" by auto
with map_of_eq_None_iff[of ?m x] obtain u where look: "map_of ?m x = Some u" by auto
from map_of_SomeD[OF look] have u: "u = σ x" by auto
show ?thesis unfolding mk_subst_def look u using True by auto
next
case False
with map_of_SomeD[of ?m x]
have look: "map_of ?m x = None" by (cases "map_of ?m x", auto)
show ?thesis unfolding mk_subst_def look using False by auto
qed
qed
show ?thesis unfolding mk_subst_case_def subst_compose_impl id
unfolding subst_compose_def by auto
qed
definition check_linear_term :: "('f :: showl, 'v :: showl) term ⇒ showsl check"
where
"check_linear_term s = check (linear_term s)
(showsl (STR ''the term '') ∘ showsl s ∘ showsl (STR '' is not linear⏎''))"
lemma check_linear_term [simp]:
"isOK (check_linear_term s) = linear_term s"
by (simp add: check_linear_term_def)
definition check_ground_term :: "('f :: showl, 'v :: showl) term ⇒ showsl check"
where
"check_ground_term s = check (ground s)
(showsl (STR ''the term '') ∘ showsl s ∘ showsl (STR '' is not a ground term⏎''))"
lemma check_ground_term [simp]:
"isOK (check_ground_term s) ⟷ ground s"
by (simp add: check_ground_term_def)
end