Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
theory Mgu = Main + Terms + Fresh + Equ + Substs:
(* unification problems *)
syntax
"_equ_prob" :: "trm \ trm \ (trm\trm)" ("_ \? _" [81,81] 81)
"_fresh_prob" :: "string \ trm \ (string\trm)" ("_ \? _" [81,81] 81)
translations
"t1 \? t2" \ "(t1,t2)"
" a \? t" \ "(a,t)"
(* all solutions for a unification problem *)
types
eprobs = "(trm\trm)list"
fprobs = "(string\trm)list"
probs = "eprobs \ fprobs"
unifiers = "fresh_envs \ substs"
consts
U :: "probs \ (unifiers set)"
defs all_solutions_def :
"U P \ {(nabla,s).
(\ (t1,t2)\set (fst P). nabla \ subst s t1 \ subst s t2) \
(\ (a,t)\set (snd P). nabla \ a \ subst s t) }"
(* most general unifier *)
consts
mgu :: "probs \ unifiers \ bool"
defs
mgu_def:"mgu P unif \ \ (nabla,s1)\ U P. (\ s2. (nabla\(subst s2) (fst unif)) \
(nabla\subst (s2 \(snd unif)) \ subst s1))"
(* idempotency of a unifier *)
consts
idem :: "unifiers \ bool"
defs
idem_def: "idem unif \ (fst unif)\ subst ((snd unif)\(snd unif)) \ subst (snd unif)"
(* application of a substitution to a problem *)
consts
apply_subst :: "substs \ probs \ probs"
apply_subst_eprobs :: "substs \ eprobs \ eprobs"
apply_subst_fprobs :: "substs \ fprobs \ fprobs"
primrec
"apply_subst_eprobs s [] = []"
"apply_subst_eprobs s (x#xs) = (subst s (fst x) \? subst s (snd x))#(apply_subst_eprobs s xs)"
primrec
"apply_subst_fprobs s [] = []"
"apply_subst_fprobs s (x#xs) = ((fst x) \? subst s (snd x))#(apply_subst_fprobs s xs)"
defs apply_subst_def:
"apply_subst s P \ (apply_subst_eprobs s (fst P),apply_subst_fprobs s (snd P))"
lemma map_equ:
"apply_subst_eprobs s P = map (\(t1,t2). (subst s t1 \? subst s t2)) P"
apply(induct_tac P)
apply(auto)
done
lemma map_fresh:
"apply_subst_fprobs s P = map (\(a,t). (a \? subst s t)) P"
apply(induct_tac P)
apply(auto)
done
(* equality reductions *)
consts
s_red :: "(probs \ substs \ probs) set"
syntax
"_s_red" :: "probs \ substs \ probs \ bool" ("_ \ _ \ _ " [80,80,80] 80)
translations "P1 \sigma\ P2" \ "(P1,sigma,P2)\s_red"
inductive s_red
intros
unit_sred[intro!]: "((Unit\?Unit)#xs,ys) \[]\ (xs,ys)"
paar_sred[intro!]: "((Paar t1 t2\?Paar s1 s2)#xs,ys) \[]\ ((t1\?s1)#(t2\?s2)#xs,ys)"
func_sred[intro!]: "((Func F t1\?Func F t2)#xs,ys) \[]\ ((t1\?t2)#xs,ys)"
abst_aa_sred[intro!]: "((Abst a t1\?Abst a t2)#xs,ys) \[]\ ((t1\?t2)#xs,ys)"
abst_ab_sred[intro!]: "a\b\
((Abst a t1\?Abst b t2)#xs,ys) \[]\ ((t1\?swap [(a,b)] t2)#xs,(a\?t2)#ys)"
atom_sred[intro!]: "((Atom a\?Atom a)#xs,ys) \[]\ (xs,ys)"
susp_sred[intro!]: "((Susp pi1 X\?Susp pi2 X)#xs,ys)
\[]\ (xs,(map (\a. a\? Susp [] X) (ds_list pi1 pi2))@ys)"
var_1_sred[intro!]: "\(occurs X t)\((Susp pi X\?t)#xs,ys)
\[(X,swap (rev pi) t)]\ apply_subst [(X,swap (rev pi) t)] (xs,ys)"
var_2_sred[intro!]: "\(occurs X t)\((t\?Susp pi X)#xs,ys)
\[(X,swap (rev pi) t)]\ apply_subst [(X,swap (rev pi) t)] (xs,ys)"
(* freshness reductions *)
consts
c_red :: "(probs \ fresh_envs \ probs) set"
syntax
"_c_red" :: "probs \ fresh_envs \ probs \ bool" ("_ \ _ \ _ " [80,80,80] 80)
translations "P1 \nabla\ P2" \ "(P1,nabla,P2)\c_red"
inductive c_red
intros
unit_cred[intro!]: "([],(a \? Unit)#xs) \{}\ ([],xs)"
paar_cred[intro!]: "([],(a \? Paar t1 t2)#xs) \{}\ ([],(a\?t1)#(a\?t2)#xs)"
func_cred[intro!]: "([],(a \? Func F t)#xs) \{}\ ([],(a\?t)#xs)"
abst_aa_cred[intro!]: "([],(a \? Abst a t)#xs) \{}\ ([],xs)"
abst_ab_cred[intro!]: "a\b\([],(a \? Abst b t)#xs) \{}\ ([],(a\?t)#xs)"
atom_cred[intro!]: "a\b\([],(a \? Atom b)#xs) \{}\ ([],xs)"
susp_cred[intro!]: "([],(a \? Susp pi X)#xs) \{((swapas (rev pi) a),X)}\ ([],xs)"
(* unification reduction sequence *)
consts
red_plus :: "(probs \ unifiers \ probs) set"
syntax
red_plus :: "probs \ unifiers \ probs \ bool" ("_ \ _ \ _ " [80,80,80] 80)
translations "P1 \(nabla,s)\ P2" \ "(P1,(nabla,s),P2)\red_plus"
inductive red_plus
intros
sred_single[intro!]: "\P1\s1\P2\\P1\({},s1)\P2"
cred_single[intro!]: "\P1\nabla1\P2\\P1\(nabla1,[])\P2"
sred_step[intro!]: "\P1\s1\P2;P2\(nabla2,s2)\P3\\P1\(nabla2,(s2\s1))\P3"
cred_step[intro!]: "\P1\nabla1\P2;P2\(nabla2,[])\P3\\P1\(nabla2\nabla1,[])\P3"
lemma mgu_idem:
"\(nabla1,s1)\U P;
\(nabla2,s2)\U P. nabla2\(subst s2) nabla1 \ nabla2\subst(s2\s1)\subst s2\\
mgu P (nabla1,s1) \ idem (nabla1,s1)"
apply(rule conjI)
(* mgu *)
apply(force simp add: mgu_def)
(* idem *)
apply(force simp add: idem_def)
done
lemma problem_subst_comm:
"((nabla,s2)\U (apply_subst s1 P)) = ((nabla,(s2\s1))\U P)"
apply(simp add: all_solutions_def subst_comp_expand apply_subst_def)
apply(induct_tac P)
apply(simp)
apply(induct_tac a)
apply(simp)
apply(induct_tac b)
apply(auto)
done
lemma P1_to_P2_sred:
"\(nabla1,s1)\U P1; P1 \s2\ P2 \\((nabla1,s1)\U P2) \ (nabla1\subst (s1\s2)\subst s1)"
apply(ind_cases "P1 \s2\ P2")
apply(simp_all)
(* Unit *)
apply(force intro!: equ_refl simp add: all_solutions_def ext_subst_def subst_equ_def subst_susp)
(* Paar *)
apply(simp add: all_solutions_def ext_subst_def subst_equ_def subst_susp)
apply(force intro!: equ_refl dest!: equ_paar_elim)
(* Func *)
apply(simp add: all_solutions_def ext_subst_def subst_equ_def subst_susp)
apply(force intro!: equ_refl dest!: equ_func_elim)
(* Abst.aa *)
apply(simp add: all_solutions_def ext_subst_def subst_equ_def subst_susp)
apply(force intro!: equ_refl dest!: equ_abst_aa_elim)
(* Abst.ab *)
apply(simp add: all_solutions_def ext_subst_def subst_equ_def subst_susp)
apply(force intro!: equ_refl dest!: equ_abst_ab_elim simp add: subst_swap_comm)
(* Atom *)
apply(simp add: all_solutions_def ext_subst_def subst_equ_def subst_susp)
apply(force intro!: equ_refl)
(* Susp *)
apply(rule conjI)
apply(simp add: all_solutions_def ds_list_equ_ds subst_susp)
apply(erule conjE)+
apply(drule equ_pi1_pi2_dec)
apply(force simp add: subst_susp)
apply(force intro!: equ_refl simp add: subst_equ_def subst_susp)
(* Var 1 *)
apply(rule conjI)
apply(drule_tac "t2.1"="swap (rev pi) t" in subst_not_occurs[THEN mp])
apply(simp only: problem_subst_comm)
apply(simp add: all_solutions_def ext_subst_def subst_equ_def)
apply(force dest!: susp_subst_equ simp add: subst_change_equ subst_change_fresh)
apply(force intro!: susp_subst_equ simp add: all_solutions_def)
(* Var 2 *)
apply(rule conjI)
apply(drule_tac "t2.1"="swap (rev pi) t" in subst_not_occurs[THEN mp])
apply(simp only: problem_subst_comm)
apply(simp add: all_solutions_def ext_subst_def subst_equ_def)
apply(erule conjE)+
apply(drule equ_sym)
apply(force dest!: susp_subst_equ simp add: subst_change_equ subst_change_fresh)
apply(rule susp_subst_equ)
apply(rule equ_sym)
apply(simp add: all_solutions_def)
done
lemma P1_from_P2_sred:
"\(nabla1,s1)\U P2; P1\s2\P2\\(nabla1,s1\s2)\U P1"
apply(ind_cases "P1 \s2\ P2")
(* Susp Paar Func Abst-aa *)
apply(simp add: all_solutions_def, force)
apply(simp add: all_solutions_def, force)
apply(simp add: all_solutions_def, force)
apply(simp add: all_solutions_def, force)
(* Abst-ab *)
apply(simp only: all_solutions_def)
apply(force simp add: subst_swap_comm)
(* Atom *)
apply(simp only: all_solutions_def, force)
(* Susp *)
apply(simp add: all_solutions_def ds_list_equ_ds)
apply(subgoal_tac "subst s1 (Susp pi1 X) = swap pi1 (subst s1 (Susp [] X))") (* A *)
apply(subgoal_tac "subst s1 (Susp pi2 X) = swap pi2 (subst s1 (Susp [] X))") (* B *)
apply(simp add: subst_susp subst_swap_comm)
apply(rule equ_ds)
apply(drule conjunct2)
apply(drule_tac x="(a,Susp [] X)" in bspec)
apply(simp)
apply(force simp add: subst_susp)
(* A / B *)
apply(simp add: subst_swap_comm[THEN sym])
apply(simp add: subst_swap_comm[THEN sym])
(* Var 1 *)
apply(simp only: problem_subst_comm)
apply(simp add: all_solutions_def subst_comp_expand)
apply(subgoal_tac "subst [(X, swap (rev pi) t)] t = t") (* A *)
apply(simp add: subst_susp subst_swap_comm)
apply(simp only: equ_pi_to_right[THEN sym])
apply(simp only: equ_involutive_right)
apply(rule equ_refl)
(* A *)
apply(force intro!: subst_not_occurs[THEN mp])
(* Var 2 *)
apply(simp only: problem_subst_comm)
apply(simp add: all_solutions_def subst_comp_expand)
apply(subgoal_tac "subst [(X, swap (rev pi) t)] t = t") (* B *)
apply(simp add: subst_susp subst_swap_comm)
apply(simp only: equ_pi_to_left[THEN sym])
apply(simp only: equ_involutive_left)
apply(rule equ_refl)
(* B *)
apply(force intro!: subst_not_occurs[THEN mp])
done
lemma P1_to_P2_cred:
"\(nabla1,s1)\U P1; P1 \nabla2\ P2 \\((nabla1,s1)\U P2) \ (nabla1\(subst s1) nabla2)"
apply(ind_cases " P1\nabla2\P2")
apply(simp_all)
apply(auto simp add: ext_subst_def all_solutions_def)
apply(rule fresh_swap_left[THEN mp])
apply(simp add: subst_swap_comm[THEN sym])
done
lemma P1_from_P2_cred:
"\(nabla1,s1)\U P2; P1 \nabla2\ P2; nabla3\(subst s1) nabla2\\(nabla1\nabla3,s1)\U P1"
apply(ind_cases "P1 \nabla2\ P2")
apply(simp_all)
apply(auto simp add: ext_subst_def all_solutions_def fresh_weak)
apply(simp add: subst_susp)
apply(rule fresh_swap_right[THEN mp])
apply(drule_tac "nabla2.1"="nabla1" in fresh_weak[THEN mp])
apply(subgoal_tac "nabla3 \