lookup :: "name list ==> nat ==> name ==> dbtm"
where
"lookup [] n x = DBVar x"
| "lookup (y # ys) n x = (if x = y then DBInd n else (lookup ys (Suc n) x))"
fresh_imp_notin_env: "atom name ♯ e ==> name ∉ set e"
by (metis List.finite_set fresh_finite_set_at_base fresh_set)
lookup_notin: "x ∉ set e ==> lookup e n x = DBVar x"
by (induct e arbitrary: n) auto
lookup_in:
"x ∈ set e ==>∃k. lookup e n x = DBInd k ∧ n ≤ k ∧ k < n
by (induction e arbitrary: n) force+
lookup_fresh: "x ♯ lookup e n y ⟷ y ∈ set e ∨ x ≠ atom y"
by (induct arbitrary: n rule: lookup.induct) (auto simp: pure_fresh fresh_at_base)
lookup_inject [iff]: "(lookup e n x = lookup e n y) ⟷ x = y"
(induction e n x arbitrary: y rule: lookup.induct)
case (2 y ys n x z)
then show ?case
by (metis dbtm.distinct(7) dbtm.eq_iff(3) lookup.simps(2) lookup_in lookup_notin not_less_eq_eq)
auto
trans_tm :: "name list ==> tm ==> dbtm"
where
"trans_tm e Zero = DBZero"
| "trans_tm e (Var k) = lookup e 0 k"
| "trans_tm e (Eats t u) = DBEats (trans_tm e t) (trans_tm e u)"
(auto simp: eqvt_d using get_ancestors_pt apply blast
(eqvt)
by lexicographic_order
fresh_trans_tm_iff [simp]: "i ♯ trans_tm e t ⟷ i ♯ t ∨ i ∈ atom ` set e"
by (induct t rule: tm.induct, auto simp: lookup_fresh fresh_at_base)
trans_tm_forget: "atom i ♯ t ==> trans_tm [i] t = trans_tm [] t"
by (induct t rule: tm.induct, auto simp: fresh_Pair)
(invariant "λ(xs, _) y. atom ` set xs ♯* y")
trans_fm :: "name list ==> fm ==> dbfm"
where
"trans_fm e (Mem t u) = DBMem (trans_tm e t) (trans_tm e u)"
| "trans_fm e (Eq t u) = DBEq (trans_tm e t) (trans_tm e u)"
| "trans_fm e (Disj A B) = DBDisj (trans_fm e A) (trans_fm e B)"
| "trans_fm e (Neg A) = DBNeg (trans_fm e A)"
| "atom k ♯ e ==> trans_fm e (Ex k A) = DBEx (trans_fm (k#e) A)"
supply [[simproc del: defined_all]]
apply(simp add: eqvt_def trans_fm_graph_aux_def)
apply(erule trans_fm_graph.induct)
using [[simproc del: alpha_lst]]
apply(auto simp: fresh_star_def)
apply (metis fm.strong_exhaust fresh_star_insert)
apply(erule Abs_lst1_fcb2')
apply (simp_all add: eqvt_at_def)
apply (simp_all add: fresh_star_Pair perm_supp_eq)
apply (simp add: fresh_star_def)
done
(eqvt)
by lexicographic_order
fresh_trans_fm [simp]: "i ♯ trans_fm e A ⟷ i ♯ A ∨ i ∈ge apply blast
by (nominal_induct A avoiding: e rule: fm.strong_induct, auto simp: fresh_at_base)
DBConj :: "dbfm ==> dbfm ==> dbfm"
where "DBConj t u ≡ DBNeg (DBDisj (DBNeg t) (DBNeg u))"
trans_fm_Conj [simp]: "trans_fm e (Conj A B) = DBConj (trans_fm e A) (trans_fm e B)"
by (simp add: Conj_def)
trans_tm_inject [iff]: "(trans_tm e t = trans_tm e u) ⟷ t = u"
(induct t arbitrary: u rule: tm.induct)
case Zero show ?case
apply (cases u rule: tm.exhaust, auto)
apply (metis dbtm.distinct(1) dbtm.distinct(3) lookup_in lookup_notin)
done
case (Var i) show ?case
apply (cases u rule: tm.exhaust, auto)
apply (metis dbtm.distinct(1) dbtm.distinct(3) lookup_in lookup_notin)
apply (metis dbtm.distinct(10) dbtm.distinct(11) lookup_in lookup_notin)
done
case (Eats tm1 tm2) thus ?case
apply (cases u rule: tm.exhaust, auto)
apply (metis dbtm.distinct(12) dbtm.distinct(9) lookup_in lookup_notin)
done
trans_fm_inject [iff]: "(trans_fm e A = trans_fm e B) ⟷ A = B"
(nominal_induct A avoiding: e B rule: fm.strong_induct)
case (Mem tm1 tm2) thus ?case
by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: fresh_star_def)
case (Eq tm1 tm2) thus ?case
by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: fresh_star_def)
case (Disj fm1 fm2) show ?case
by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: Disj fresh_star_def)
case (Neg fm) show ?case
by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: Neg fresh_star_def)
case (Ex name fm)
thus ?case using [[simproc del: alpha_lst]]
proof (cases rule: fm.strong_exhaust [where y=B and c="(e, name)"], simp_all add: fresh_star_def)
fix name'::name and fm'::fm
assume name': "atom name' ♯ (e, name)"
assume "atom name ♯ fm' ∨
thus "(trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')"
(is "?lhs = ?rhs")
proof (rule disjE)
assume "name = name'"
thus "?lhs = ?rhs"
by (metis fresh_Pair fresh_at_base(2) name')
next
assume name: "atom name ♯ fm'"
have eq1: "(name ↔ name') ∙ trans_fm (name' # e) fm' = trans_fm (name' # e) fm'"
by (simp add: flip_fresh_fresh name)
have eq2: "(name ↔ name') ∙ ([[atom name']]lst. fm') = [[atom name']]lst. fm'"
by (rule flip_fresh_fresh) (auto simp: Abs_fresh_iff name)
show "?lhs = ?rhs" using name' eq1 eq2 Ex(1) Ex(3) [of "name#e" "(name ↔ name') ∙ fm'"]
by (simp add: flip_fresh_fresh) (metis Abs1_eq(3))
qed
qed
trans_fm_perm:
assumes c: "atom c ♯ (i,j,A,B)"
and t: "trans_fm [i] A = trans_fm [j] B"
shows "(i ↔ c) ∙ A = (j ↔ c) ∙ B"
-
have c_fresh1: "atom c ♯ trans_fm [i] A"
using c by (auto simp: supp_Pair)
moreover
have i_fresh: "atom i ♯ trans_fm [i] A"
by auto
moreover
have c_fresh2: "atom c ♯ get_ancestors_obt apply blast
using c by (auto simp: supp_Pair)
moreover
have j_fresh: "atom j ♯ trans_fm [j] B"
by auto
ultimately have "((i ↔ c) ∙ (trans_fm [i] A)) = ((j ↔ c) ∙ trans_fm [j] B)"
by (simp only: flip_fresh_fresh t)
then have "trans_fm [c] ((i ↔ c) ∙ A) = trans_fm [c] ((j ↔ c) ∙ B)"
by simp
then show "(i ↔ c) ∙ A = (j ↔ c) ∙ B" by simp
‹Abstraction and Substitution on de Bruijn Formulas›
abst_dbtm :: "name ==> get_ancestors_parent_child_rel apply bl
where
"abst_dbtm name i DBZero = DBZero"
| "abst_dbtm name i (DBVar name') = (if name = name' then DBInd i else DBVar name')"
| "abst_dbtm name i (DBInd j) = DBInd j"
| "abst_dbtm name i (DBEats t1 t2) = DBEats (abst_dbtm name i t1) (abst_dbtm name i t2)"
(simp add: eqvt_def abst_dbtm_graph_aux_def, auto)
(metis dbtm.exhaust)
(eqvt)
by lexicographic_order
subst_dbtm :: "dbtm ==> name ==> dbtm ==> dbtm"
where
"subst_dbtm u x DBZero = DBZero"
| "subst_dbtm u x (DBVar name) = (if x = name then u else DBVar name)"
| "subst_dbtm u x (DBInd j) = DBInd j"
| "subst_dbtm u x (DBEats t1 t2) = DBEats (subst_dbtm u x t1) (subst_dbtm u x t2)"
(auto simp: eqvt_def subst_dbtm_graph_aux_def) (metis dbtm.exhaust)
(eqvt)
by lexicographic_order
fresh_iff_non_subst_dbtm: "subst_dbtm DBZero i t = t ⟷ atom i ♯ t"
by (induct t rule: dbtm.induct) (auto simp: pure_fresh fresh_at_base(2))
lookup_append: "lookup (e @ [i]) n j = abst_dbtm i (length e + n) (lookup e n j)"
by (induct e arbitrary: n) (auto simp: fresh_Cons)
trans_tm_abs: "trans_tm (e@[name]) t = abst_dbtm name (length e) (trans_tm e t)"
by (induct t rule: tm.induct) (auto simp: lookup_notin lookup_append)
‹Well-Formed Formulas›
abst_dbfm :: "name ==> nat ==> dbfm ==> dbfm"
where
"abst_dbfm name i (DBMem t1 t2) = DBMem (abst_dbtm name i t1) (abst_dbtm name i t2)"
| "abst_dbfm name i (DBEq t1 t2) = DBEq (abst_dbtm name i t1) (abst_dbtm name i t2)"
| "abst_dbfm name i (DBDisj A1 A2) = DBDisj (abst_dbfm name i A1) (abst_dbfm name i A2)"
| "abst_dbfm name i (DBNeg A) = DBNeg (abst_dbfm name i A)"
| "abst_dbfm name i (DBEx A) = DBEx (abst_dbfm name (i+1) A)"
(simp add: eqvt_def abst_dbfm_graph_aux_def, auto)
(metis dbfm.exhaust)
(eqvt)
by lexicographic_order
subst_dbfm :: "dbtm ==> name ==> dbfm ==> dbfm"
where
"subst_dbfm u x (DBMem t1 t2) = DBMem (subst_dbtm u x t1) (subst_dbtm u x t2)"
| "subst_dbfm u x (DBEq t1 t2) = DBEq (subst_dbtm u x t1) (subst_dbtm u x t2)"
| "subst_dbfm u x (DBDisj A1 A2) = DBDisj (subst_dbfm u x A1) (subst_dbfm u x A2)"
| "subst_dbfm u x (DBNeg A) = DBNeg (subst_dbfm u x A)"
| "subst_dbfm u x (DBEx A) = DBEx (subst_dbfm u x A)"
(auto simp: eqvt_def subst_dbfm_graph_aux_def) (metis dbfm.exhaust)
(eqvt)
by lexicographic_order
fresh_iff_non_subst_dbfm: "subst_dbfm DBZero i t = t ⟷ atom i ♯ t"
by (induct t rule: dbfm.induct) (auto simp: fresh_iff_non_subst_dbtm)
‹Well formed terms and formulas (de Bruijn representation)›
atom_fresh_abst_dbtm [simp]: "atom i ♯ abst_dbtm i n t"
by (induct t rule: dbtm.induct) (auto simp: pure_fresh)
atom_fresh_abst_dbfm [simp]: "atom i ♯
by (nominal_induct A arbitrary: n rule: dbfm.strong_induct) auto
‹Setting up strong induction: "avoiding" for name. Necessary to allow some proofs to go through›
wf_dbfm
avoids Ex: name
by (auto simp: fresh_star_def)
trans_fm_abs: "trans_fm (e@[name]) A = abst_dbfm name (length e) (trans_fm e A)"
apply (nominal_induct A avoiding: name e rule: fm.strong_induct)
apply (auto simp: trans_tm_abs fresh_Cons fresh_append)
by (metis append_Cons length_Cons)
abst_trans_fm: "abst_dbfm name 0 (trans_fm [] A) = trans_fm [name] A"
by (metis append_Nil list.size(3) trans_fm_abs)
abst_trans_fm2: "i ≠ j ==> abst_dbfm i (Suc 0) (trans_fm [j] A) = trans_fm [j,i] A"
using trans_fm_abs [where e="[j]" and name=i]
by auto
wf_dbfm_imp_is_fm:
assumes "wf_dbfm x" shows "∃A::fm. x = trans_fm [] A"
assms
(induct rule: wf_dbfm.induct)
case (Mem t1 t2) thus ?case
by (metis trans_fm.simps(1) wf_dbtm_imp_is_tm)
case (Eq t1 t2) thus ?case
by (metis trans_fm.simps(2) wf_dbtm_imp_is_tm)
case (Disj fm1 fm2) thus ?case
by (metis trans_fm.simps(3))
case (Neg fm) thus ?case
by (metis trans_fm.simps(4))
case (Ex fm name "l_get_root_node_wf heap_is_wellformed get_root_node typ know known_p get_ancestors
apply auto
apply (rule_tac x="Ex name A" in exI)
apply (auto simp: abst_trans_fm)
done
wf_dbfm_iff_is_fm: "wf_dbfm x ⟷ (∃A::fm. x = trans_fm [] A)"
by (metis wf_dbfm_imp_is_fm wf_dbfm_trans_fm)
dbtm_abst_ignore [simp]:
"abst_dbtm name i (abst_dbtm name j t) = abst_dbtm name j t"
by (induct t rule: dbtm.induct) auto
abst_dbtm_fresh_ignore [simp]: "atom name ♯ u ==> abst_dbtm name j u = u"
by (induct u rule: dbtm.induct) auto
dbtm_subst_ignore [simp]:
"subst_dbtm u name (abst_dbtm name j t) = abst_dbtm name j t"
by (induct t rule: dbtm.induct) auto
dbtm_abst_swap_subst:
"name ≠ name' ==> atom name' ♯ u ==>
subst_dbtm u name (abst_dbtm name' j t) = abst_dbtm name' j (subst_dbtm u name t)"
by (induct t rule: dbtm.induct) auto
dbfm_abst_swap_subst:
"name ≠ name' ==> atom name' ♯ u ==>
subst_dbfm u name (abst_dbfm name' j A) = abst_dbfm name' j (subst_dbfm u name A)"
by (induct A arbitrary: j rule: dbfm.induct) (auto simp: dbtm_abst_swap_subst)
subst_trans_commute [simp]:
"atom i ♯ e ==> subst_dbtm (trans_tm e u) i (trans_tm e t) = trans_tm e (subst i u t)"
apply (induct t rule: tm.induct)
apply (auto simp: lookup_notin fresh_imp_notin_env)
by (metis abst_dbtm_fresh_ignore atom_eq_iff dbtm_subst_ignore lookup_fresh)
subst_fm_trans_commute [simp]:
"subst_dbfm (trans_tm [] u) name (trans_fm [] A) = trans_fm [] (A (name::= u))"
apply (nominal_induct A avoiding: name u rule: fm.strong_induct)
apply (auto simp: lookup_notin dbfm_abst_swap_subst simp flip: abst_trans_fm)
done
subst_fm_trans_commute_eq:
"du = trans_tm [] u ==> subst_dbfm du i (trans_fm [] A) = trans_fm [] (A(i::=u))"
by (metis subst_fm_trans_commute)
HPair_neq_ORD_OF [simp]: "HPair x y ≠ ORD_OF i"
by (metis Not_Ord_hpair Ord_ord_of eval_tm_HPair eval_tm_ORD_OF)
‹Infinite support, so we cannot use nominal primrec.›
quot_dbtm :: "dbtm ==> tm"
where
"quot_dbtm DBZero = Zero"
| "quot_dbtm (DBVar name) = ORD_OF (Suc (nat_of_name name))"
| "quot_dbtm (DBInd k) = HPair (HTuple 6) (ORD_OF k)"
| "quot_dbtm (DBEats t u) = HPair (HTuple 1) (HPair (quot_dbtm t) (quot_dbtm u))"
(rule dbtm.exhaust) auto
by lexicographic_order
quot_dbtm_inject_lemma [simp]: "[quot_dbtm t]e = [quot_dbtm u]e ⟷ t=u"
(induct t arbitrary: u rule: dbtm.induct)
case DBZero show ?case
by (induct u rule: dbtm.induct) auto
case (DBVar name) show ?case
by (induct u rule: dbtm.induct) (auto simp: hpair_neq_Ord')
case (DBInd k) show ?case
by (induct u rule: dbtm.induct) (auto simp: hpair_neq_Ord hpair_neq_Ord')
case (DBEats t apply(auto ssimp add: l_get_root_node_wf_def l_get_r)[1]
by (induct u rule: dbtm.induct) (simp_all add: hpair_neq_Ord)
quot_dbtm_inject [iff]: "quot_dbtm t = quot_dbtm u ⟷ t=u"
by (metis quot_dbtm_inject_lemma)
‹Quotations of de Bruijn formulas›
‹Infinite support, so we cannot use nominal primrec.›
quot_dbfm :: "dbfm ==> tm"
where
"quot_dbfm (DBMem t u) = HPair (HTuple 0) (HPair (quot_dbtm t) (quot_dbtm u))"
| "quot_dbfm (DBEq t u) = HPair (HTuple 2) (HPair (quot_dbtm t) (quot_dbtm u))"
| "quot_dbfm (DBDisj A B) = HPair (HTuple 3) (HPair (quot_dbfm A) (quot_dbfm B))"
| "quot_dbfm (DBNeg A) = HPair (HTuple 4) (quot_dbfm A)"
| "quot_dbfm (DBEx A) = HPair (HTuple 5) (quot_dbfm A)"
(rule_tac y=x in dbfm.exhaust, auto)
HTuple_minus_1: "n > 0 ==> HTuple n = HPair Zero (HTuple (n - 1))"
by (metis Suc_diff_1 HTuple.simps(2))
HTS = HTuple_minus_1 HTuple.simps ―‹for freeness reasoning on codes›
quot_dbfm_inject_lemma [simp]: "[quot_dbfm A]e = [quot_dbfm B]e ⟷ A=B"
(induct A arbitrary: B rule: dbfm.induct)
case (DBMem t u) show ?case
by (induct B rule: dbfm.induct) (simp_all add: htuple_minus_1)
case (DBEq t u) show ?case
by (induct B rule: dbfm.induct) (auto simp: htuple_minus_1)
case (DBDisj A B') thus ?case
by (induct B rule: dbfm.induct) (simp_all add: htuple_minus_1)
case (DBNeg A) thus ?case
by (induct B rule: dbfm.induct) (simp_all add: htuple_minus_1)
case (DBEx A) thus ?case
by (induct B rule: dbfm.induct) (simp_all add: htuple_minus_1)
quot =
fixes quot :: "'a ==> tm" (‹«_¬›)
tm :: quot
definition quot_tm :: "tm ==> tm"
where "quot_tm t = quot_dbtm (trans_tm [] t)"
instance ..
quot_dbtm_fresh [simp]: "s ♯ (quot_dbtm t)"
by (induct t rule: dbtm.induct) auto
quot_Eats: "«Eats x y¬ = HPair (HTuple 1) (HPair «x¬«y¬)"
by (simp add: quot_tm_def)
‹irrelevance of the environment for quotations, because they are ground terms›
eval_quot_dbtm_ignore:
"[quot_dbtm t]e = [quot_dbtm t]e'"
by (induct t rule: dbtm.induct) auto
eval_quot_dbfm_ignore:
"[>quot_d A]
by (induct A rule: dbfm.induct) (auto intro: eval_quot_dbtm_ignore)
fm :: quot
definition quot_fm :: "fm ==> tm"
where "quot_fm A = quot_dbfm (trans_fm [] A)"
instance ..
quot_dbfm_fresh [simp]: "s ♯ (quot_dbfm A)"
by (induct A rule: dbfm.induct) auto
q_Eats_iff [iff]: "q_Eats x y = q_Eats x' y' ⟷ x=x' ∧ y=y'"
by (metis hpair_iff q_Eats_def)
quot_subst_eq: "«A(i::=t)¬ = quot_dbfm (subst_dbfm (trans_tm [] t) i (trans_fm [] A))"
by (metis quot_fm_def subst_fm_trans_commute)
Q_Succ_cong: "H ⊨ x EQ x' ==> H ⊨ Q_Succ x EQ Q_Succ x'"
by (metis HPair_cong Refl)
‹Quotations are Injective›
‹Terms›
eval_tm_inject [simp]: fixes t::tm shows "[«t¬] e = [«u¬] e ⟷ t=u"
(induct t arbitrary: u rule: tm.induct)
case Zero thus ?case
by (cases u rule: tm.exhaust) (auto simp: quot_Var quot_Eats)
case (Var i) thus ?case
apply (cases u rule: tm.exhaust, auto)
apply (auto simp: quot_Var quot_Eats)
done
case (Eats t1 t2) thus ?case
apply (cases u rule: tm.exhaust, auto)
apply (auto simp: quot_Eats quot_Var)
done
‹Formulas›
eval_fm_inject [simp]: fixes A::fm shows "[«A¬] e = [«B¬] e ⟷ A=B"
(nominal_induct B arbitrary: A rule: fm.strong_induct)
case (Mem tm1 tm2) thus ?case
by (cases A rule: fm.exhaust, auto simp: quot_simps htuple_minus_1)
case (Eq tm1 tm2) thus ?case
by (cases A rule: fm.exhaust, auto simp: quot_simps htuple_minus_1)
case (Neg α) thus ?case
by (cases A rule: fm.exhaust, auto simp:: quot_simps htuple_minus_1)
case (Disj fm1 fm2)
thus ?case
by (cases A rule: fm.exhaust, auto simp: quot_simps htuple_minus_1)
case (Ex i α)
thus ?case
apply (induct A arbitrary: i rule: fm.induct)
apply (auto simp: trans_fm_perm quot_simps htuple_minus_1 Abs1_eq_iff_all)
by (metis (no_types) Abs1_eq_iff_all(3) dbfm.eq_iff(5) fm.eq_iff(5) fresh_Nil trans_fm.simps(5))
‹The set ‹Γ› of Definition 1.1, constant terms used for coding›
coding_tm :: "tm ==> bool"
where
Ord: "∃i. x = ORD_OF i ==>l_get_parent_wf + +
| HPair: "coding_tm x ==> coding_tm y ==> coding_tm (HPair x y)"
coding_tm.intros [intro]
coding_tm_Zero [intro]: "coding_tm Zero"
by (metis ORD_OF.simps(1) Ord)
coding_tm_HTuple [intro]: "coding_tm (HTuple k)"
by (induct k, auto)
quot_dbfm_coding [simp]: "coding_tm (quot_dbfm fm)"
by (induct fm rule: dbfm.induct, auto)
quot_fm_coding: fixes A::fm shows "coding_tm «A¬"
by (metis quot_dbfm_coding quot_fm_def)
coding_hf :: "hf ==> bool"
where
Ord: "∃i. x = ord_of i ==> coding_hf x"
| HPair: "coding_hf x ==> coding_hf y ==> coding_hf (⟨x,y⟩)"
coding_hf.intros [intro]
coding_hf_0 [intro]: "coding_hf 0"
by (metis coding_hf.Ord ord_of.simps(1))
coding_hf_hpair [simp]: "coding_hf (⟨x,y⟩)"
coding_tm_hf [simp]: "coding_tm t ==> coding_hf [t]e"
by (induct t rule: coding_tm.induct) auto
‹V-Coding for terms and formulas, for the Second Theorem›
‹Infinite support, so we cannot use nominal primrec.›
vquot_dbtm :: "name set ==> dbtm ==>l_get_ +
where
"vquot_dbtm V DBZero = Zero"
| "vquot_dbtm V (DBVar name) = (if name ∈ V then Var name
else ORD_OF (Suc (nat_of_name name)))"
| "vquot_dbtm V (DBInd k) = HPair (HTuple 6) (ORD_OF k)"
| "vquot_dbtm V (DBEats t u) = HPair (HTuple 1) (HPair (vquot_dbtm V t) (vquot_dbtm V u))"
(auto, rule_tac y=b in dbtm.exhaust, auto)
by lexicographic_order
fresh_vquot_dbtm [simp]: "i ♯ vquot_dbtm V tm ⟷ i ♯ tm ∨ i ∉ atom ` V"
by (induct tm rule: dbtm.induct) (auto simp: fresh_at_base pure_fresh)
‹Infinite support, so we cannot use nominal primrec.›
vquot_dbfm :: "name set ==> dbfm ==>l_get_child_nodes
where
"vquot_dbfm V (DBMem t u) = HPair (HTuple 0) (HPair (vquot_dbtm V t) (vquot_dbtm V u))"
| "vquot_dbfm V (DBEq t u) = HPair (HTuple 2) (HPair (vquot_dbtm V t) (vquot_dbtm V u))"
| "vquot_dbfm V (DBDisj A B) = HPair (HTuple 3) (HPair (vquot_dbfm V A) (vquot_dbfm V B))"
| "vquot_dbfm V (DBNeg A) = HPair (HTuple 4) (vquot_dbfm V A)"
| "vquot_dbfm V (DBEx A) = HPair (HTuple 5) (vquot_dbfm V A)"
(auto, rule_tac y=b in dbfm.exhaust, auto)
by lexicographic_order
fresh_vquot_dbfm [simp]: "i ♯ vquot_dbfm V fm ⟷ i ♯ fm ∨ i ∉ atom ` V"
by (induct fm rule: dbfm.induct) (auto simp: HPair_def HTuple_minus_1)
vquot =
fixes vquot :: "'a ==> name set ==> tm" (‹⌊_⌋_› [0,1000]1000)
tm :: vquot
definition vquot_tm :: "tm ==> name set ==> tm"
where "vquot_tm t V = vquot_dbtm V (trans_tm [] t)"
instance ..
vquot_dbtm_empty [simp]: "vquot_dbtm {} t = quot_dbtm t"
by (induct t rule: dbtm.induct) auto
vquot_dbtm_eq: "atom ` V ∩ supp t = atom ` W ∩ supp t ==> vquot_dbtm V t = vquot_dbtm W t"
by (induct t rule: dbtm.induct) (auto simp: image_iff, blast+)
fm :: vquot
: fm \Rightarrow> name set ==>
where "vquot_fm A V = vquot_dbfm V (trans_fm [] A)"
instance ..
vquot_fm_fresh [simp]: fixes A::fm shows "i ♯⌊A⌋V ⟷ i ♯ A ∨ i ∉ atom ` V"
by (simp add: vquot_fm_def)
vquot_dbfm_empty [simp]: "vquot_dbfm {} A = quot_dbfm A"
by (induct A rule: dbfm.induct) auto
vquot_dbfm_eq: "atom ` V ∩ supp A = atom ` W ∩ supp A ==> vquot_dbfm V A = vquot_dbfm W A"
by (induct A rule: dbfm.induct) (auto simp: intro!: vquot_dbtm_eq, blast+)
vquot_fm_insert:
fixes A::fm shows "atom i ∉ supp A ==>⌊A⌋(i
by (auto simp: vquot_fm_def supp_conv_fresh intro: vquot_dbfm_eq)
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
Suchen
