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
Atoms.thy0100644000175000001440000000215107660505272011450 0ustar cu200users theory Atoms = Main + Swap + Terms: consts atms :: "(string \ string) list \ string set" primrec "atms [] = {}" "atms (x#xs) = (atms xs) \ {fst(x),snd(x)}" lemma [simp]: "atms (xs@ys) = atms xs \ atms ys" apply(induct_tac xs, auto) done lemma [simp]: "atms (rev pi) = atms pi" apply(induct_tac pi, simp_all) done lemma a_not_in_atms: "a\atms pi \ a = swapas pi a" apply(induct_tac pi, auto) done lemma swapas_pi_ineq_a: "swapas pi a \ a \ a\atms pi" and a_ineq_swapas_pi: "a \ swapas pi a \ a\atms pi" (* swapas_pi_ineq_a *) apply(case_tac "a\atms pi") apply(simp)+ apply(drule a_not_in_atms[THEN mp]) apply(simp) (* a_ineq_swapas_pi *) apply(case_tac "a\atms pi") apply(simp_all add: a_not_in_atms) done lemma swapas_pi_in_atms[THEN mp]: "a\atms pi \ swapas pi a\atms pi" apply(subgoal_tac "\pi1. (a\atms pi1) \ swapas pi a\(atms pi1 \ atms pi)") (* A *) apply(force) (* A *) apply(induct_tac pi) apply(auto) done endDisagreement.thy0100644000175000001440000000747607660505307013012 0ustar cu200users theory Disagreement = Main + Swap + Atoms: consts ds :: "(string \ string) list \ (string \ string) list \ string set" defs ds_def: "ds xs ys \ { a . a \ (atms xs \ atms ys) \ (swapas xs a \ swapas ys a) }" lemma ds_elem: "\swapas pi a\a\\a\ds [] pi" apply(simp add: ds_def) apply(auto simp add: swapas_pi_ineq_a) done lemma elem_ds: "\a\ds [] pi\\a\swapas pi a" apply(simp add: ds_def) done lemma ds_sym: "ds pi1 pi2 = ds pi2 pi1" apply(simp only: ds_def) apply(auto) done lemma ds_trans: "c\ds pi1 pi3\(c\ds pi1 pi2 \ c\ds pi2 pi3)" apply(auto) apply(simp only: ds_def) apply(auto) apply(drule a_not_in_atms[THEN mp])+ apply(simp) apply(drule a_not_in_atms[THEN mp]) apply(simp) apply(drule swapas_pi_ineq_a[THEN mp]) apply(assumption) done lemma ds_cancel_pi_left: "(c\ ds (pi1@pi) (pi2@pi)) \ (swapas pi c\ ds pi1 pi2)" apply(simp only: ds_def) apply(auto) apply(simp_all add: swapas_append) apply(rule a_ineq_swapas_pi[THEN mp], clarify, drule a_not_in_atms[THEN mp], simp)+ done lemma ds_cancel_pi_right: "(swapas pi c\ ds pi1 pi2) \ (c\ ds (pi1@pi) (pi2@pi))" apply(simp only: ds_def) apply(auto) apply(simp_all add: swapas_append) apply(rule a_ineq_swapas_pi[THEN mp],clarify, drule a_not_in_atms[THEN mp],drule a_not_in_atms[THEN mp],simp)+ done lemma ds_equality: "(ds [] pi)-{a,swapas pi a} = (ds [] ((a,swapas pi a)#pi))-{swapas pi a}" apply(simp only: ds_def) apply(auto) done lemma ds_7: "\b\ swapas pi b;a\ds [] ((b,swapas pi b)#pi)\\a\ds [] pi" apply(simp only: ds_def) apply(case_tac "b=a") apply(auto) apply(rule swapas_pi_in_atms) apply(drule a_ineq_swapas_pi[THEN mp]) apply(assumption) apply(drule sym) apply(drule swapas_rev_pi_a) apply(simp) apply(case_tac "swapas pi b = a") apply(auto) apply(drule sym) apply(drule swapas_rev_pi_a) apply(simp) done lemma ds_cancel_pi_front: "ds (pi@pi1) (pi@pi2) = ds pi1 pi2" apply(simp only: ds_def) apply(auto) apply(simp_all add: swapas_append) apply(rule swapas_pi_ineq_a[THEN mp], clarify, drule a_not_in_atms[THEN mp], simp)+ apply(drule swapas_rev_pi_a, simp)+ done lemma ds_rev_pi_pi: "ds ((rev pi1)@pi1) pi2 = ds [] pi2" apply(simp only: ds_def) apply(auto) apply(simp_all add: swapas_append) apply(drule a_ineq_swapas_pi[THEN mp], assumption)+ done lemma ds_rev: "ds [] ((rev pi1)@pi2) = ds pi1 pi2" apply(subgoal_tac "ds pi1 pi2 = ds ((rev pi1)@pi1) ((rev pi1)@pi2)") apply(simp add: ds_rev_pi_pi) apply(simp only: ds_cancel_pi_front) done lemma ds_acabbc: "\a\b;b\c;c\a\\ds [] [(a, c), (a, b), (b, c)] = {a, b}" apply(simp only: ds_def) apply(auto) done lemma ds_baab: "\a\b\\ds [] [(b, a), (a, b)] = {}" apply(simp only: ds_def) apply(auto) done lemma ds_abab: "\a\b\\ds [] [(a, b), (a, b)] = {}" apply(simp only: ds_def) apply(auto) done (* disagreement set as list *) consts flatten :: "(string \ string)list \ string list" primrec "flatten [] = []" "flatten (x#xs) = (fst x)#(snd x)#(flatten xs)" consts ds_list :: "(string \ string)list \ (string \ string)list \ string list" defs ds_list_def: "ds_list pi1 pi2 \ remdups ([x:(flatten (pi1@pi2)). x\ds pi1 pi2])" lemma set_flatten_eq_atms: "set (flatten pi) = atms pi" apply(induct_tac pi) apply(auto) done lemma ds_list_equ_ds: "set (ds_list pi1 pi2) = ds pi1 pi2" apply(auto) apply(simp add: ds_list_def) apply(simp add: ds_list_def) apply(simp add: set_flatten_eq_atms) apply(simp add: ds_def) done endEqu.thy0100644000175000001440000001203307660505332011114 0ustar cu200users theory Equ = Main + Terms + Fresh + PreEqu: lemma equ_refl: "nabla\t\t" apply(induct_tac t) apply(auto simp add: ds_def) done lemma equ_sym: "nabla\t1\t2 \ nabla\t2\t1" and equ_trans: "\nabla\t1\t2;nabla\t2\t3\ \ nabla\t1\t3" and equ_add_pi: "nabla\t1\t2 \ nabla\swap pi t1\swap pi t2" apply(insert big) apply(best)+ done lemma equ_dec_pi: "nabla\swap pi t1\swap pi t2\nabla\t1\t2" apply(drule_tac pi="(rev pi)" in equ_add_pi) apply(subgoal_tac "nabla\swap (rev pi) (swap pi t2)\t2") apply(drule_tac "t1.0"="swap (rev pi) (swap pi t1)" and "t2.0"="swap (rev pi) (swap pi t2)" and "t3.0"="t2" in equ_trans) apply(assumption) apply(subgoal_tac "nabla\t1\swap (rev pi) (swap pi t1)") apply(drule_tac "t1.0"="t1" and "t2.0"="swap (rev pi) (swap pi t1)" and "t3.0"="t2" in equ_trans) apply(assumption)+ apply(rule equ_sym) apply(rule rev_pi_pi_equ) apply(rule rev_pi_pi_equ) done lemma equ_involutive_left: "nabla\swap (rev pi) (swap pi t1)\t2 = nabla\t1\t2" apply(auto) apply(subgoal_tac "nabla \ t1\ swap (rev pi) (swap pi t1)") apply(drule_tac "t2.0"="swap (rev pi) (swap pi t1)" and "t1.0"="t1" and "t3.0"="t2" in equ_trans) apply(assumption)+ apply(rule equ_sym) apply(rule rev_pi_pi_equ) apply(subgoal_tac "nabla \ swap (rev pi) (swap pi t1)\t1") apply(drule_tac "t1.0"="swap (rev pi) (swap pi t1)" and "t2.0"="t1" and "t3.0"="t2" in equ_trans) apply(assumption)+ apply(rule rev_pi_pi_equ) done lemma equ_pi_to_left: "nabla\swap (rev pi) t1\t2 = nabla\t1\ swap pi t2" apply(auto) apply(rule_tac pi="rev pi" in equ_dec_pi) apply(rule equ_sym) apply(simp only: equ_involutive_left) apply(rule equ_sym) apply(assumption) apply(drule_tac pi="rev pi" in equ_add_pi) apply(drule equ_sym) apply(simp only: equ_involutive_left) apply(drule equ_sym) apply(assumption) done lemma equ_pi_to_right: "nabla\t1\swap (rev pi) t2 = nabla\swap pi t1\t2" apply(auto) apply(rule_tac pi="rev pi" in equ_dec_pi) apply(simp only: equ_involutive_left) apply(drule_tac pi="rev pi" in equ_add_pi) apply(simp only: equ_involutive_left) done lemma equ_involutive_right: "nabla\t1\swap (rev pi) (swap pi t2) = nabla\t1\t2" apply(simp only: swap_append[THEN sym]) apply(simp only: equ_pi_to_left[THEN sym]) apply(simp) apply(simp only: swap_append) apply(simp only: equ_involutive_left) done lemma equ_pi1_pi2_add: "(\a\ ds pi1 pi2. nabla\a\t)\(nabla\swap pi1 t \ swap pi2 t)" apply(simp only: equ_pi_to_right[THEN sym]) apply(simp only: swap_append[THEN sym]) apply(rule equ_pi_right[THEN spec, THEN mp]) apply(auto) apply(simp only: ds_rev) done lemma pi_right_equ: "(nabla\t \ swap pi t)\(\a\ ds [] pi. nabla\a\t)" apply(insert pi_right_equ_help) apply(best) done lemma equ_pi1_pi2_dec: "(nabla\swap pi1 t \ swap pi2 t)\(\a\ ds pi1 pi2. nabla\a\t)" apply(simp only: equ_pi_to_right[THEN sym]) apply(simp only: swap_append[THEN sym]) apply(drule pi_right_equ[THEN mp]) apply(simp only: ds_rev) done lemma equ_weak: "nabla1\t1\t2\(nabla1\nabla2)\t1\t2" apply(rule impI) apply(erule equ.induct) apply(auto simp add: fresh_weak) done (* no term can be equal to one of its proper subterm *) lemma psub_trm_not_equ: "\nabla t1. \ t2\psub_trms t1. (\(\ pi. (nabla\t1\swap pi t2)))" apply(rule allI)+ apply(induct_tac t1) apply(auto) (* Abst *) apply(simp add: equ_pi_to_left[THEN sym]) apply(ind_cases "nabla \ Abst (swapas (rev pi) list) (swap (rev pi) trm) \ t2") apply(simp_all) apply(drule abst_psub_trms) apply(drule_tac x="t2a" in bspec) apply(assumption) apply(simp add: equ_pi_to_left[THEN sym] swap_append[THEN sym]) apply(drule_tac x="rev (((swapas (rev pi) list, b) # rev pi))" in spec) apply(simp) apply(force dest!: abst_psub_trms) (* Paar *) apply(simp add: equ_pi_to_left[THEN sym]) apply(ind_cases "nabla \ Paar (swap (rev pi) trm1) (swap (rev pi) trm2) \ t2") apply(force dest!: paar_psub_trms) apply(simp add: equ_pi_to_left[THEN sym]) apply(ind_cases "nabla \ Paar (swap (rev pi) trm1) (swap (rev pi) trm2) \ t2") apply(force dest!: paar_psub_trms) (* Func *) apply(simp add: equ_pi_to_left[THEN sym]) apply(ind_cases "nabla \ Func list (swap (rev pi) trm) \ t2") apply(force dest!: func_psub_trms) done end Fresh.thy0100644000175000001440000000651607660505316011444 0ustar cu200users theory Fresh = Main + Swap + Terms + Disagreement: types fresh_envs = "(string \ string)set" consts fresh :: "(fresh_envs \ string \ trm) set" syntax "_fresh_judge" :: "fresh_envs \ string \ trm \ bool" (" _ \ _ \ _" [80,80,80] 80) translations "nabla \ a \ t" \ "(nabla,a,t) \ fresh" inductive fresh intros fresh_abst_ab[intro!]: "\(nabla\a\t); a\b\ \ (nabla\a\Abst b t)" fresh_abst_aa[intro!]: "(nabla\a\Abst a t)" fresh_unit[intro!]: "(nabla\a\Unit)" fresh_atom[intro!]: "a\b \ (nabla\a\Atom b)" fresh_susp[intro!]: "(swapas (rev pi) a,X)\nabla \ (nabla\a\Susp pi X)" fresh_paar[intro!]: "\(nabla\a\t1);(nabla\a\t2)\ \ (nabla\a\Paar t1 t2)" fresh_func[intro!]: "(nabla\a\t) \ (nabla\a\Func F t)" lemma fresh_atom_elim[elim!]: "(nabla\a\Atom b) \ a\b" apply(ind_cases "(nabla \a\Atom b)") apply(assumption) done lemma fresh_susp_elim[elim!]: "(nabla\a\Susp pi X) \ (swapas (rev pi) a,X)\nabla" apply(ind_cases "(nabla\a\Susp pi X)") apply(assumption) done lemma fresh_paar_elim[elim!]: "(nabla\a\Paar t1 t2) \ (nabla\a\t1)\(nabla \a\t2)" apply(ind_cases "(nabla\a\Paar t1 t2)") apply(force) done lemma fresh_func_elim[elim!]: "(nabla\a\Func F t) \ (nabla\a\t)" apply(ind_cases "nabla\a\Func F t") apply(assumption) done lemma fresh_abst_ab_elim[elim!]: "\nabla\a\Abst b t;a\b\ \ (nabla\a\t)" apply(ind_cases "nabla\a\Abst b t") apply(auto) done lemma fresh_swap_left: "(nabla\a\swap pi t) \ (nabla\swapas (rev pi) a\t)" apply(induct t) apply(simp_all) -- Abst apply(rule impI) apply(case_tac "swapas (rev pi) a = list") apply(force) apply(force dest!: fresh_abst_ab_elim) --Susp apply(force dest!: fresh_susp_elim simp add: swapas_append[THEN sym]) --Unit apply(force) --Atom apply(force dest!: fresh_atom_elim) --Paar apply(force dest!: fresh_paar_elim) -- Func apply(force dest!: fresh_func_elim) done lemma fresh_swap_right: "(nabla\swapas (rev pi) a\t) \ (nabla\a\swap pi t)" apply(induct t) apply(simp_all) -- Abst apply(rule impI) apply(case_tac "a = swapas pi list") apply(force) apply(force dest!: fresh_abst_ab_elim) --Susp apply(force dest!: fresh_susp_elim simp add: swapas_append[THEN sym]) --Unit apply(force) --Atom apply(force dest!: fresh_atom_elim) --Paar apply(force dest!: fresh_paar_elim) -- Func apply(force dest!: fresh_func_elim) done lemma fresh_weak: "nabla1\a\t\(nabla1\nabla2)\a\t" apply(rule impI) apply(erule fresh.induct) apply(auto) done end Mgu.thy0100644000175000001440000003526407660505352011127 0ustar cu200users 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_pi1_pi2_add) apply(drule conjunct2) apply(rule ballI) 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] subst_susp) 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 \ nabla1=nabla1 \ nabla3") (* A *) apply(simp) (* A *) apply(rule Un_commute) done lemma P1_to_P2_red_plus: "\P1 \(nabla,s)\P2\\ (nabla1,s1)\U P1 \ ((nabla1,s1)\U P2) \ (nabla1\subst (s1\s)\subst s1) \ (nabla1\(subst s1) nabla)" apply(erule red_plus.induct) (* sred *) apply(rule impI) apply(drule_tac "P2.0"="P2" and "s2.0"="s1a" in P1_to_P2_sred) apply(assumption) apply(force simp add: ext_subst_def) (* cred *) apply(rule impI) apply(drule_tac "P2.0"="P2" and "nabla2.0"="nabla1a" in P1_to_P2_cred) apply(assumption) apply(force intro!: equ_refl simp add: subst_equ_def) (* sred *) apply(rule impI) apply(drule_tac "P2.0"="P2" and "s2.0"="s1a" in P1_to_P2_sred) apply(assumption) apply(erule conjE)+ apply(rule conjI) apply(force) apply(rule conjI) apply(simp) apply(erule conjE)+ apply(rule_tac "s2.0"="((s1\s2)\s1a)" in subst_trans) apply(simp only: subst_assoc subst_equ_def) apply(rule ballI) apply(rule equ_refl) apply(rule_tac "s2.0"="(s1\s1a)" in subst_trans) apply(rule subst_cancel_right) apply(assumption) apply(assumption) apply(force) (* cred *) apply(rule impI) apply(drule_tac "P2.0"="P2" and "nabla2.0"="nabla1a" in P1_to_P2_cred) apply(auto simp add: ext_subst_def) done lemma P1_from_P2_red_plus: "\P1 \(nabla,s)\P2\\(nabla1,s1)\U P2\ nabla3\(subst s1)(nabla)\(nabla1\nabla3,(s1\s))\U P1" apply(erule red_plus.induct) (* sred *) apply(rule impI)+ apply(drule_tac "P1.0"="P1" and "s2.0"="s1a" in P1_from_P2_sred) apply(assumption) apply(force simp only: all_solutions_def equ_weak fresh_weak) (* cred *) apply(rule impI)+ apply(drule_tac "P1.0"="P1" and "nabla3.0"="nabla3" and "nabla2.0"="nabla1a" in P1_from_P2_cred) apply(assumption)+ apply(simp add: all_solutions_def) (* sred *) apply(rule impI)+ apply(simp) apply(drule_tac "P1.0"="P1" and "P2.0"="P2" and "s2.0"="s1a" in P1_from_P2_sred) apply(assumption) apply(simp add: all_solutions_def subst_assoc) (* cred *) apply(rule impI)+ apply(subgoal_tac "nabla3 \ (subst s1) nabla2") (* A *) apply(simp) apply(drule_tac "P1.0"="P1" and "P2.0"="P2" and "nabla2.0"="nabla1a" and "nabla3.0"="nabla3" in P1_from_P2_cred) apply(assumption) apply(simp) apply(simp add: ext_subst_def) apply(subgoal_tac "nabla1 \ nabla3 \ nabla3=nabla1 \ nabla3") (* B *) apply(simp) (* B *) apply(force) (* A *) apply(simp add: ext_subst_def) done (* if a problem reduces to the "ok"-problem then (nabla,s) is an idempotent mgu *) lemma mgu: "\P \(nabla,s)\([],[])\\ mgu P (nabla,s) \ idem (nabla,s)" apply(frule_tac "nabla3.2"="nabla" and "nabla2"="nabla" and "s1.2"="[]" and "nabla1.2"="{}" in P1_from_P2_red_plus[THEN mp,THEN mp]) apply(force simp add: all_solutions_def) apply(force simp add: ext_subst_def) apply(rule mgu_idem) apply(simp add: all_solutions_def) apply(rule ballI) apply(clarify) apply(drule_tac "nabla1.0"="a" and "s1.0"="b"in P1_to_P2_red_plus) apply(simp) done end PreEqu.thy0100644000175000001440000004634607660505324011602 0ustar cu200users theory PreEqu = Main + Swap + Terms + Disagreement + Fresh: consts equ :: "(fresh_envs \ trm \ trm) set" syntax "_equ_judge" :: "fresh_envs \ trm \ trm \ bool" (" _ \ _ \ _" [80,80,80] 80) translations "nabla \ t1 \ t2" \ "(nabla,t1,t2) \ equ" inductive equ intros equ_abst_ab[intro!]: "\a\b;(nabla \ a \ t2);(nabla \ t1 \ (swap [(a,b)] t2))\ \ (nabla \ Abst a t1 \ Abst b t2)" equ_abst_aa[intro!]: "(nabla \ t1 \ t2) \ (nabla \ Abst a t1 \ Abst a t2)" equ_unit[intro!]: "(nabla \ Unit \ Unit)" equ_atom[intro!]: "a=b\nabla \ Atom a \ Atom b" equ_susp[intro!]: "(\ c \ ds pi1 pi2. (c,X) \ nabla) \ (nabla \ Susp pi1 X \ Susp pi2 X)" equ_paar[intro!]: "\(nabla \ t1\t2);(nabla \ s1\s2)\ \ (nabla \ Paar t1 s1 \ Paar t2 s2)" equ_func[intro!]: "(nabla \ t1 \ t2) \ (nabla \ Func F t1 \ Func F t2)" lemma equ_atom_elim[elim!]: "nabla\Atom a \ Atom b \ a=b" apply(ind_cases "nabla \ Atom a \ Atom b", auto) done lemma equ_susp_elim[elim!]: "(nabla \ Susp pi1 X \ Susp pi2 X) \ (\ c \ ds pi1 pi2. (c,X)\ nabla)" apply(ind_cases "nabla \ Susp pi1 X \ Susp pi2 X", auto) done lemma equ_paar_elim[elim!]: "(nabla \ Paar s1 t1 \ Paar s2 t2) \ (nabla \ s1 \ s2)\(nabla \ t1 \ t2)" apply(ind_cases "nabla \ Paar s1 t1 \ Paar s2 t2", auto) done lemma equ_func_elim[elim!]: "(nabla \ Func F t1 \ Func F t2) \ (nabla \ t1 \ t2)" apply(ind_cases "nabla \ Func F t1 \ Func F t2", auto) done lemma equ_abst_aa_elim[elim!]: "(nabla \ Abst a t1 \ Abst a t2) \ (nabla \ t1 \ t2)" apply(ind_cases "nabla \ Abst a t1 \ Abst a t2", auto) done lemma equ_abst_ab_elim[elim!]: "\(nabla \ Abst a t1 \ Abst b t2);a\b\ \ (nabla \ t1 \ (swap [(a,b)] t2))\(nabla\a\t2)" apply(ind_cases "(nabla \ Abst a t1 \ Abst b t2)", auto) done lemma equ_atom_t[elim!]: "nabla\Atom a\t\equ_constr (Atom a,t)" apply(ind_cases "nabla\Atom a\t") apply(auto) done lemma equ_paar_t[elim!]: "nabla\Paar t1 t2\t\equ_constr (Paar t1 t2,t)" apply(ind_cases "nabla\Paar t1 t2\t") apply(auto) done lemma equ_abst_t[elim!]: "nabla\Abst a t1\t\equ_constr (Abst a t1,t)" apply(ind_cases "nabla\Abst a t1\t") apply(auto) done lemma equ_func_t[elim!]: "nabla\Func F t1\t\equ_constr (Func F t1,t)" apply(ind_cases "nabla\Func F t1\t") apply(auto) done lemma equ_unit_t[elim!]: "nabla\Unit\t\equ_constr (Unit,t)" apply(ind_cases "nabla\Unit\t") apply(auto) done lemma equ_depth: "nabla \ t1 \ t2 \ depth t1 = depth t2" apply(erule equ.induct) apply(simp_all) done lemma rev_pi_pi_equ: "(nabla\swap (rev pi) (swap pi t)\t)" apply(induct_tac t) apply(auto) (* Susp *) apply(drule_tac ds_cancel_pi_left[of _ "rev pi @ pi" _ "[]", THEN mp, simplified]) apply(simp only: ds_rev_pi_pi) apply(simp only: ds_def) apply(force) done lemma equ_pi_right: "\pi. (\a\ds [] pi. nabla\a\t) \ (nabla\t\swap pi t)" apply(induct_tac t) apply(simp_all) (* Abst *) apply(rule allI) apply(case_tac "(swapas pi list)=list") apply(simp) apply(rule impI) apply(rule equ_abst_aa) apply(drule_tac x="pi" in spec) apply(subgoal_tac "(\a\ds [] pi. nabla \ a \ trm)") (* A *) apply(force) (* A *) apply(rule ballI) apply(drule_tac x=a in bspec) apply(assumption) apply(case_tac "list\a") apply(force dest!: fresh_abst_ab_elim) apply(simp add: ds_def) apply(rule impI) apply(rule equ_abst_ab) apply(force) apply(drule_tac x="swapas (rev pi) list" in bspec) apply(simp add: ds_def) apply(rule conjI) apply(subgoal_tac "swapas (rev pi) list \ atms (rev pi)") (* B *) apply(simp) (* B *) apply(drule swapas_pi_ineq_a[THEN mp]) apply(rule swapas_pi_in_atms) apply(simp) apply(clarify) apply(drule swapas_rev_pi_b) apply(simp) apply(force dest!: fresh_abst_ab_elim swapas_rev_pi_b intro!: fresh_swap_right[THEN mp]) apply(drule_tac x="(list, swapas pi list)#pi" in spec) apply(subgoal_tac "(\a\ds [] ((list, swapas pi list) # pi). nabla \ a \ trm)")(* C *) apply(force simp add: swap_append[THEN sym]) (* C *) apply(rule ballI) apply(drule_tac x="a" in bspec) apply(rule_tac b="list" in ds_7) apply(force) apply(assumption) apply(case_tac "list=a") apply(simp) apply(simp only: ds_def mem_Collect_eq) apply(erule conjE) apply(subgoal_tac "a\swapas pi a") apply(simp) apply(force) apply(force dest!: fresh_abst_ab_elim) (* Susp *) apply(rule allI) apply(rule impI) apply(rule equ_susp) apply(rule ballI) apply(subgoal_tac "swapas list1 c\ds [] pi")(* A *) apply(force dest!: fresh_susp_elim) (* A *) apply(force intro!: ds_cancel_pi_left[THEN mp]) (* Unit *) apply(force) (* Atom *) apply(rule allI) apply(rule impI) apply(case_tac "(swapas pi list) = list") apply(force) apply(force dest!: ds_elem fresh_atom_elim) (* Paar *) apply(force dest!: fresh_paar_elim) (* Func *) apply(force) done lemma pi_comm: "nabla\(swap (pi@[(a,b)]) t)\(swap ([(swapas pi a, swapas pi b)]@pi) t)" apply(induct_tac t) apply(simp_all) (* Abst *) apply(force simp add: swapas_comm) (* Susp *) apply(rule equ_susp) apply(rule ballI) apply(simp only: ds_def) apply(simp only: mem_Collect_eq) apply(erule conjE) apply(subgoal_tac "swapas (pi@[(a,b)]) (swapas list1 c) = swapas ([(swapas pi a,swapas pi b)]@pi) (swapas list1 c)")(* A *) apply(simp add: swapas_append[THEN sym]) (* A *) apply(simp only: swapas_comm) (* Unit *) apply(rule equ_unit) (* Atom *) apply(force dest!: swapas_rev_pi_b swapas_rev_pi_a simp add: swapas_append) (* Paar *) apply(force) (* Func *) apply(force) done lemma equ_preserves_fresh: "(nabla \ t1\t2) \ (nabla \ a\t1) \ (nabla \ a\t2)" apply(erule equ.induct) apply(simp_all) (* Abst-ab *) apply(rule impI) apply(case_tac "aa=a") apply(force) apply(case_tac "b=a") apply(force) apply(force dest!: fresh_abst_ab_elim fresh_swap_left[THEN mp]) (* Abst-aa *) apply(case_tac "a=aa") apply(force) apply(force dest!: fresh_abst_ab_elim) (* Susp *) apply(rule impI) apply(drule fresh_susp_elim, rule fresh_susp) apply(case_tac "swapas (rev pi1) a = swapas (rev pi2) a") apply(simp) apply(drule_tac x="swapas (rev pi2) a" in bspec) apply(rule ds_cancel_pi_left[THEN mp]) apply(subgoal_tac "swapas (pi1@(rev pi2)) a \ a") (* A *) apply(force dest!: ds_elem simp add: ds_def swapas_append) (* A *) apply(force dest: swapas_rev_pi_a simp add: swapas_append) apply(assumption) (* Paar *) apply(force dest!: fresh_paar_elim) (* Func *) apply(force dest!: fresh_func_elim) done lemma big: "\t1 t2 t3. (n=depth t1) \ (((nabla\t1\t2)\(nabla\t2\t1))\ (\pi. (nabla\t1\t2)\(nabla\swap pi t1\swap pi t2))\ ((nabla\t1\t2)\(nabla\t2\t3)\(nabla\t1\t3)))" apply(induct_tac n rule: nat_less_induct) apply(rule allI)+apply(rule impI) apply(rule conjI) (* SYMMETRY *) apply(rule impI) apply(ind_cases "nabla \ t1 \ t2") apply(simp_all) (* Abst-ab *) apply(rule equ_abst_ab) apply(force) (* abst-ab first premise *) apply(rule_tac "t1.1"="swap [(a,b)] t2a" in equ_preserves_fresh[THEN mp]) apply(drule_tac x="depth t1a" in spec) apply(simp) apply(rule fresh_swap_right[THEN mp]) apply(simp) (* abst-ab second premise *) apply(subgoal_tac "nabla \ swap [(b, a)] t1a \ t2a") apply(drule_tac x="depth t1a" in spec) apply(simp) apply(subgoal_tac "nabla \ swap [(b,a)] t1a \ swap ([(b,a)]@[(a,b)]) t2a") (* A *) apply(subgoal_tac "nabla \ swap ([(b,a)]@[(a,b)]) t2a \ t2a") (* B *) apply(drule_tac x="depth t1a" in spec) apply(simp (no_asm_use)) apply(drule_tac x="swap [(b,a)] t1a" in spec) apply(simp (no_asm_use)) apply(drule_tac x="swap [(b,a),(a,b)] t2a" in spec) apply(force) (* B *) apply(subgoal_tac "nabla\t2a \ swap ([(b, a)] @ [(a, b)]) t2a") (* C *) apply(drule_tac x="depth t1a" in spec) apply(simp) apply(drule_tac x="t2a" in spec) apply(drule mp) apply(drule equ_depth) apply(force) apply(best) (* C *) apply(rule equ_pi_right[THEN spec,THEN mp]) apply(subgoal_tac "ds [] ([(b, a)] @ [(a, b)])={}") apply(simp) apply(simp add: ds_baab) (* A *) apply(force simp only: swap_append) (* Abst-aa *) apply(force) (* Unit *) apply(rule equ_unit) (* Atom *) apply(force) (* Susp *) apply(force simp only: ds_sym) (* Paar *) apply(rule equ_paar) apply(drule_tac x="depth t1a" in spec) apply(simp add: Suc_max_left) apply(drule_tac x="depth s1" in spec) apply(simp add: Suc_max_right) (* Func *) apply(best) (* ADD PI *) apply(rule conjI) apply(rule impI) apply(ind_cases "nabla \ t1 \ t2") apply(simp_all) (* Abst-ab *) apply(rule allI) apply(rule equ_abst_ab) (* abst-ab first premise *) apply(clarify) apply(drule swapas_rev_pi_a) apply(simp) (* abst-ab second premise *) apply(rule fresh_swap_right[THEN mp]) apply(simp) (* abst-ab third premise *) apply(subgoal_tac "nabla\swap pi t1a\swap (pi@[(a,b)]) t2a") (* A *) apply(subgoal_tac "nabla\swap (pi@[(a,b)]) t2a\swap ([(swapas pi a,swapas pi b)]@pi) t2a")(* B *) apply(drule_tac x="depth t1a" in spec) apply(simp (no_asm_use)) apply(drule_tac x="swap pi t1a" in spec) apply(simp (no_asm_use)) apply(drule_tac x="swap (pi@[(a,b)]) t2a" in spec) apply(drule conjunct2)+ apply(drule_tac x="swap ((swapas pi a, swapas pi b) # pi) t2a" in spec) apply(simp add: swap_append[THEN sym]) (* B *) apply(rule pi_comm) apply(force simp only: swap_append) (* A *) apply(force simp only: swap_append) (* Unit *) apply(rule equ_unit) (* Atom *) apply(force) (* Susp *) apply(force simp only: ds_cancel_pi_front) (* Paar *) apply(rule allI) apply(rule equ_paar) apply(drule_tac x="depth t1a" in spec) apply(simp only: Suc_max_left) apply(drule_tac x="depth s1" in spec) apply(simp only: Suc_max_right) (* Func *) apply(best) (* TRANSITIVITY *) apply(rule impI) apply(erule conjE) apply(ind_cases "nabla \ t1 \ t2") apply(simp_all) (* Abst-ab *) apply(ind_cases "nabla \ Abst b t2a \ t3") apply(simp) apply(case_tac "ba=a") apply(simp) apply(rule equ_abst_aa) apply(subgoal_tac "nabla\swap [(a,b)] t2a \ t2b") (* A *) apply(best) (* A *) apply(subgoal_tac "nabla\swap [(a,b)] t2a\ swap ([(a,b)]@[(b,a)]) t2b") (* B *) apply(subgoal_tac "nabla\swap ([(a,b)]@[(b,a)]) t2b \ t2b") (* C *) apply(drule_tac x="depth t1a" in spec) apply(simp) apply(drule_tac x="swap [(a,b)] t2a" in spec) apply(drule equ_depth) apply(simp (no_asm_use)) apply(best) (* C *) apply(subgoal_tac "nabla\t2b \ swap ([(a,b)]@[(b,a)]) t2b")(* D *) apply(drule_tac x="depth t1a" in spec) apply(simp) apply(drule_tac x="t2b" in spec) apply(drule mp) apply(force dest!: equ_depth) apply(best) (* D *) apply(rule equ_pi_right[THEN spec, THEN mp]) apply(simp add: ds_baab) (* B *) apply(drule_tac x="depth t1a" in spec) apply(simp) apply(drule_tac x="t2a" in spec) apply(drule equ_depth) apply(simp) apply(drule_tac x="swap [(b, a)] t2b" in spec) apply(drule conjunct2) apply(drule conjunct1) apply(simp) apply(drule_tac x="[(a,b)]" in spec) apply(simp add: swap_append[THEN sym]) (* Abst-ab *) apply(rule equ_abst_ab) (* abst-ab first premise *) apply(force) (* abst-ab second premise *) apply(rule_tac "t1.1"="swap [(b,ba)] t2a" in equ_preserves_fresh[THEN mp]) apply(subgoal_tac "nabla \ swap [(b,ba)] t2a \ swap ([(b,ba)]@[(b, ba)]) t2b") (* A *) apply(subgoal_tac "nabla\swap ([(b,ba)]@[(b,ba)]) t2b \ t2b") (* B *) apply(drule_tac x="depth t1a" in spec) apply(simp) apply(drule_tac x="swap [(b, ba)] t2a" in spec) apply(drule mp) apply(force dest!: equ_depth) apply(best) (* B *) apply(subgoal_tac "nabla\t2b \ swap ([(b,ba)] @ [(b,ba)]) t2b")--C apply(drule_tac x="depth t1a" in spec) apply(simp) apply(drule_tac x="t2b" in spec) apply(drule mp) apply(force dest!: equ_depth) apply(best) (* C *) apply(rule equ_pi_right[THEN spec, THEN mp]) apply(simp add: ds_abab) (* A *) apply(drule_tac x="depth t1a" in spec) apply(simp) apply(drule_tac x="t2a" in spec) apply(drule mp) apply(force dest!: equ_depth) apply(drule_tac x="swap [(b,ba)] t2b" in spec) apply(drule conjunct2) apply(drule conjunct1) apply(simp) apply(drule_tac x="[(b,ba)]" in spec) apply(simp add: swap_append[THEN sym]) (* abst-ab third premise *) apply(force intro!: fresh_swap_right[THEN mp]) (* very complex case *) apply(subgoal_tac "nabla\t1a \ swap ([(a,b)]@[(b,ba)]) t2b") (* A *) apply(subgoal_tac "nabla\swap ([(a,b)]@[(b,ba)]) t2b \ swap [(a,ba)] t2b") (* B *) apply(drule_tac x="depth t1a" in spec) apply(simp (no_asm_use)) apply(best) (* B *) apply(subgoal_tac "nabla\swap [(a, ba)] t2b \ swap [(a,b),(b,ba)] t2b") (* C *) apply(drule_tac x="depth t1a" in spec) apply(simp) apply(drule_tac x="swap [(a, ba)] t2b" in spec) apply(drule mp) apply(force dest!: equ_depth) apply(force) apply(subgoal_tac "nabla\swap [(a,ba)] t2b\ swap [(a,ba)] (swap [(a,ba),(a,b),(b,ba)] t2b)") (*D*) apply(subgoal_tac "nabla\swap (rev [(a,ba)]) (swap [(a,ba)] (swap [(a,b),(b,ba)] t2b)) \swap [(a,b),(b,ba)] t2b") (* E *) apply(simp add: swap_append[THEN sym]) apply(drule_tac x="depth t1a" in spec) apply(simp) apply(drule_tac x="swap [(a,ba)] t2b" in spec) apply(drule mp) apply(force dest!: equ_depth) apply(drule_tac x="swap [(a, ba), (a, ba), (a, b), (b, ba)] t2b" in spec) apply(drule conjunct2)+ apply(best) (* D *) apply(rule rev_pi_pi_equ) (* E *) apply(subgoal_tac "nabla\t2b\swap [(a, ba), (a, b), (b, ba)] t2b") (* F *) apply(drule_tac x="depth t1a" in spec) apply(simp) apply(drule_tac x="t2b" in spec) apply(drule mp) apply(force dest!: equ_depth) apply(best) (* F *) apply(rule equ_pi_right[THEN spec, THEN mp]) apply(subgoal_tac "ds [] [(a,ba),(a,b),(b,ba)]={a,b}") (* G *) apply(simp) apply(drule_tac "t1.1"="t2a" and "t2.1"="swap [(b, ba)] t2b" and a1="a" in equ_preserves_fresh[THEN mp]) apply(assumption) apply(subgoal_tac "nabla \ swapas (rev [(b,ba)]) a \ t2b") (* H *) apply(simp) apply(case_tac "b=a") apply(force) apply(force) (* H *) apply(rule fresh_swap_left[THEN mp]) apply(assumption) (* G *) apply(rule ds_acabbc) apply(assumption)+ (* A *) apply(subgoal_tac "nabla\swap [(a,b)] t2a\swap [(a,b)] (swap [(b,ba)] t2b)") (* I *) apply(drule_tac x="depth t1a" in spec) apply(simp (no_asm_use)) apply(drule_tac x="t1a" in spec) apply(simp (no_asm_use)) apply(drule_tac x="swap [(a,b)] t2a" in spec) apply(drule conjunct2)+ apply(drule_tac x="swap [(a, b)] (swap [(b, ba)] t2b)" in spec) apply(force simp add: swap_append[THEN sym]) (* I *) apply(drule_tac x="depth t1a" in spec) apply(simp (no_asm_use)) apply(drule_tac x="t2a" in spec) apply(drule mp) apply(force dest!: equ_depth) apply(drule_tac x="swap [(b,ba)] t2b" in spec) apply(best) (* Abst-ab *) apply(simp) apply(rule equ_abst_ab) apply(assumption) apply(drule_tac "t1.1"="t2a" and "t2.1"="t2b" and a1="a" in equ_preserves_fresh[THEN mp]) apply(assumption)+ apply(subgoal_tac "nabla\swap [(a, b)] t2a\swap [(a, b)] t2b") (* A *) apply(best) (* A *) apply(drule_tac x="depth t1a" in spec) apply(simp (no_asm_use)) apply(drule_tac x="t2a" in spec) apply(drule mp) apply(force dest!: equ_depth) apply(drule_tac x="t2b" in spec) apply(best) (* Abst *) apply(ind_cases "nabla \ Abst a t2a \ t3") apply(best) apply(best) (* Susp *) apply(ind_cases "nabla \ Susp pi2 X \ t3") apply(simp) apply(rule equ_susp) apply(rule ballI) apply(drule_tac "pi2.1"="pi2" in ds_trans[THEN mp]) apply(force) (* Paar *) apply(ind_cases "nabla \ Paar t2a s2 \ t3") apply(simp) apply(rule equ_paar) apply(drule_tac x="depth t1a" in spec) apply(simp (no_asm_use) add: Suc_max_left) apply(best) apply(drule_tac x="depth s1" in spec) apply(simp (no_asm_use) add: Suc_max_right) apply(best) (* Func *) apply(ind_cases "nabla \ Func F t2a \ t3") apply(best) done lemma pi_right_equ_help: "\t. (n=depth t) \ (\pi. nabla\t\swap pi t\(\a\ ds [] pi. nabla\a\t))" apply(induct_tac n rule: nat_less_induct) apply(rule allI)+ apply(rule impI) apply(rule allI)+ apply(rule impI) apply(ind_cases "nabla \ t \ swap pi t") apply(simp_all) (* Abst-ab *) apply(rule ballI) apply(case_tac "aa=a") apply(force) apply(rule fresh_abst_ab) apply(case_tac "aa=swapas (rev pi) a") apply(simp) apply(drule fresh_swap_left[THEN mp]) apply(assumption) apply(drule_tac x="depth t1" in spec) apply(simp) apply(drule_tac x="t1" in spec) apply(simp add: swap_append[THEN sym]) apply(drule_tac x="[(a, swapas pi a)] @ pi" in spec) apply(simp) apply(case_tac "aa=swapas pi a") apply(simp) apply(drule_tac x="swapas pi a" in bspec) apply(simp (no_asm) only: ds_def) apply(simp only: mem_Collect_eq) apply(rule conjI) apply(simp) apply(simp) apply(rule impI) apply(clarify) apply(drule sym) apply(drule swapas_rev_pi_a) apply(force) apply(assumption) apply(drule_tac x="aa" in bspec) apply(subgoal_tac "\A. aa\A-{swapas pi a} \ aa\swapas pi a \aa\A") (* A *) apply(drule_tac x="ds [] ((a,swapas pi a) # pi)" in spec) apply(simp add: ds_equality[THEN sym]) (* A *) apply(force) apply(assumption)+ (* Abst-aa *) apply(rule ballI) apply(case_tac "aa=a") apply(force) apply(best) (* Unit *) apply(force) (* Atom *) apply(force simp add: ds_def) (* Susp *) apply(rule ballI) apply(rule fresh_susp) apply(drule_tac x="swapas (rev pi1) a" in bspec) apply(rule ds_cancel_pi_right[of _ _ "[]" _, simplified, THEN mp]) apply(simp) apply(assumption) (* Paar *) apply(rule ballI) apply(rule fresh_paar) apply(drule_tac x="depth t1" in spec) apply(force simp add: Suc_max_left) apply(drule_tac x="depth s1" in spec) apply(force simp add: Suc_max_right) (* Func *) apply(best) done end Substs.thy0100644000175000001440000003300407660505342011647 0ustar cu200users theory Substs = Main + Terms + PreEqu + Equ: (* substitutions *) types substs = "(string \ trm)list" consts look_up :: "string \ substs \ trm" primrec "look_up X [] = Susp [] X" "look_up X (x#xs) = (if (X = fst x) then (snd x) else look_up X xs)" consts subst :: "substs \ trm \ trm" primrec subst_unit: "subst s (Unit) = Unit" subst_susp: "subst s (Susp pi X) = swap pi (look_up X s)" subst_atom: "subst s (Atom a) = Atom a" subst_abst: "subst s (Abst a t) = Abst a (subst s t)" subst_paar: "subst s (Paar t1 t2) = Paar (subst s t1) (subst s t2)" subst_func: "subst s (Func F t) = Func F (subst s t)" declare subst_susp [simp del] (* composition of substitutions (adapted from Martin Coen) *) consts alist_rec :: "substs \ substs \ (string\trm\substs\substs\substs) \ substs" primrec "alist_rec [] c d = c" "alist_rec (p#al) c d = d (fst p) (snd p) al (alist_rec al c d)" consts "\" :: "substs \ substs \ substs" (infixl 81) defs comp_def: "s1 \ s2 \ alist_rec s2 s1 (\ x y xs g. (x,subst s1 y)#g)" (* domain of substitutions *) consts domn :: "(trm \ trm) \ string set" defs domn_def: "domn s \ {X. (s (Susp [] X)) \ (Susp [] X)}" (* how substitutions extend freshness environments *) consts ext_subst :: "fresh_envs \ (trm \ trm) \ fresh_envs \ bool" (" _ \ _ _ " [80,80,80] 80) defs ext_subst_def: "nabla1 \ s (nabla2) \ (\(a,X)\nabla2. nabla1\a\ s (Susp [] X))" (* alpha-equality for substitutions *) consts subst_equ :: "fresh_envs \ (trm\trm) \ (trm\trm) \ bool" (" _ \ _ \ _" [80,80,80] 80) defs subst_equ_def: "nabla\ s1 \ s2 \ \X\(domn s1\domn s2). (nabla \ s1 (Susp [] X) \ s2 (Susp [] X))" lemma not_in_domn: "X\(domn s)\ (s (Susp [] X)) = (Susp [] X)" apply(auto simp only: domn_def) done lemma subst_swap_comm: "subst s (swap pi t) = swap pi (subst s t)" apply(induct_tac t) apply(auto simp add: swap_append subst_susp) done lemma subst_not_occurs: "\(occurs X t) \ subst [(X,t2)] t = t" apply(induct t) apply(auto simp add: subst_susp) done lemma [simp]: "subst [] t = t" apply(induct_tac t, auto simp add: subst_susp) done lemma [simp]: "subst (s\[]) = subst s" apply(auto simp add: comp_def) done lemma [simp]: "subst ([]\s) = subst s" apply(rule ext) apply(induct_tac x) apply(auto) apply(induct_tac s rule: alist_rec.induct) apply(auto simp add: comp_def subst_susp) done lemma subst_comp_expand: "subst (s1\s2) t = subst s1 (subst s2 t)" apply(induct_tac t) apply(auto) apply(induct_tac s2 rule: alist_rec.induct) apply(auto simp add: comp_def subst_susp subst_swap_comm) done lemma subst_assoc: "subst (s1\(s2\s3))=subst ((s1\s2)\s3)" apply(rule ext) apply(induct_tac x) apply(auto) apply(simp add: subst_comp_expand) done lemma fresh_subst: "nabla1\a\t \ nabla2\(subst s) nabla1 \ nabla2\a \ subst s t" apply(erule fresh.induct) apply(auto) (* Susp *) apply(simp add: ext_subst_def subst_susp) apply(drule_tac x="(swapas (rev pi) a, X)" in bspec) apply(assumption) apply(simp) apply(rule fresh_swap_right[THEN mp]) apply(assumption) done lemma equ_subst: "nabla1\t1\t2 \ nabla2\ (subst s) nabla1 \ nabla2\(subst s t1)\(subst s t2)" apply(erule equ.induct) apply(auto) apply(rule_tac "nabla1.1"="nabla" in fresh_subst[THEN mp]) apply(assumption)+ apply(simp add: subst_swap_comm) (* Susp *) apply(force intro!: equ_pi1_pi2_add simp add: ext_subst_def subst_susp) done lemma susp_subst_equ: "\nabla\subst s (Susp pi X)\subst s t\\ nabla\ subst (s\[(X,swap (rev pi) t)])\subst s" apply(simp only: subst_equ_def) apply(case_tac "pi=[]") apply(simp add: subst_susp comp_def) apply(force intro: equ_sym equ_refl) apply(subgoal_tac "domn (subst (s\[(X,swap (rev pi) t)]))=domn(subst s)\{X}")(* A *) apply(simp) apply(rule conjI) apply(simp add: subst_comp_expand) apply(simp add: subst_susp) apply(simp only: subst_swap_comm) apply(simp only: equ_pi_to_left) apply(rule equ_sym) apply(assumption) apply(rule ballI) apply(simp only: subst_comp_expand) apply(simp add: subst_susp) apply(force intro: equ_sym equ_refl simp add: subst_swap_comm equ_pi_to_left) (* A *) apply(simp only: domn_def) apply(auto) apply(simp add: subst_comp_expand) apply(simp add: subst_susp subst_swap_comm) apply(simp only: subst_comp_expand) apply(simp add: subst_susp subst_swap_comm) apply(force dest!: swap_empty[THEN mp]) apply(simp only: subst_comp_expand) apply(simp only: subst_susp) apply(auto) apply(case_tac "x=X") apply(force dest!: swap_empty[THEN mp] simp add: subst_swap_comm) apply(simp add: subst_susp) done lemma subst_equ_a: "\nabla\(subst s1)\(subst s2)\ \ \t2. nabla\(subst s2 t1)\t2 \ nabla\(subst s1 t1)\t2" apply(rule allI) apply(induct t1) (* Abst-ab *) apply(rule impI) apply(simp) apply(ind_cases "nabla \ Abst list (subst s1 trm) \ t2") apply(best) (* Abst-aa *) apply(force) (* Susp *) apply(rule impI) apply(simp only: subst_equ_def) apply(case_tac "list2\domn (subst s1) \ domn (subst s2)") apply(drule_tac x="list2" in bspec) apply(assumption) apply(simp) apply(subgoal_tac "nabla \ subst s2 (Susp [] list2) \ swap (rev list1) t2")(* A *) apply(drule_tac "t1.0"="subst s1 (Susp [] list2)" and "t2.0"="subst s2 (Susp [] list2)" and "t3.0"="swap (rev list1) t2" in equ_trans) apply(assumption) apply(simp only: equ_pi_to_right) apply(simp add: subst_swap_comm[THEN sym]) (* A *) apply(simp only: equ_pi_to_right) apply(simp add: subst_swap_comm[THEN sym]) apply(simp) apply(erule conjE) apply(drule not_in_domn)+ apply(subgoal_tac "subst s1 (Susp list1 list2)=swap list1 (subst s1 (Susp [] list2))") (* B *) apply(subgoal_tac "subst s2 (Susp list1 list2)=swap list1 (subst s2 (Susp [] list2))") (* C *) apply(simp) (* B / C *) apply(simp (no_asm) add: subst_swap_comm[THEN sym]) apply(simp (no_asm) add: subst_swap_comm[THEN sym]) (* Unit *) apply(force) (* Atom *) apply(force) (* Paar *) apply(rule impI) apply(simp) apply(ind_cases "nabla \ Paar (subst sigma1 trm1) (subst sigma1 trm2) \ t2") apply(best) (* Func *) apply(rule impI) apply(simp) apply(ind_cases "nabla \ Func list (subst sigma1 trm) \ t2") apply(best) done lemma subst_change_equ: "\nabla\subst s1\subst s2\\(nabla\subst s2 t1\subst s2 t2)\(nabla\subst s1 t1\subst s1 t2)" apply(rule impI) apply(frule_tac "t1.0"="t1" in subst_equ_a) apply(drule_tac x="subst s2 t2" in spec) apply(simp) apply(drule equ_sym) apply(drule equ_sym) apply(drule_tac "t1.0"="t2" in subst_equ_a) apply(drule_tac x="subst s1 t1" in spec) apply(rule equ_sym) apply(simp) done lemma subst_change_fresh: "\nabla\subst s1\subst s2\ \ nabla\a\subst s2 t \ nabla\a\subst s1 t" apply(induct t) (* Abst *) apply(simp) apply(rule impI) apply(case_tac "a=list") apply(force) apply(force dest!: fresh_abst_ab_elim) (* Susp *) apply(rule impI) apply(subgoal_tac "subst s1 (Susp list1 list2)= swap list1 (subst s1 (Susp [] list2))")(* A *) apply(subgoal_tac "subst s2 (Susp list1 list2)= swap list1 (subst s2 (Susp [] list2))")(* B *) apply(simp add: subst_equ_def) apply(case_tac "list2\domn (subst s1) \ domn (subst s2)") apply(drule_tac x="list2" in bspec) apply(assumption) apply(rule fresh_swap_right[THEN mp]) apply(rule_tac "t1.1"=" subst s2 (Susp [] list2)" in equ_preserves_fresh[THEN mp]) apply(rule equ_sym) apply(simp) apply(rule fresh_swap_left[THEN mp]) apply(simp) apply(simp) apply(erule conjE) apply(drule not_in_domn)+ apply(simp add: subst_swap_comm) (* A / B *) apply(simp (no_asm) add: subst_swap_comm[THEN sym]) apply(simp (no_asm) add: subst_swap_comm[THEN sym]) (* Unit *) apply(force) (* Atom *) apply(force) (* Paar *) apply(force dest!: fresh_paar_elim) (* Func *) apply(force dest!: fresh_func_elim) done lemma subst_sym: "nabla\subst s1\subst s2 \ nabla\subst s2\ subst s1" apply(auto dest!: equ_sym simp add: subst_equ_def) done lemma subst_equ_to_trm: "nabla\subst s1\subst s2 \ nabla\subst s1 t\subst s2 t" apply(induct_tac t) apply(auto simp add: subst_equ_def) apply(case_tac "list2\domn (subst s1) \ domn (subst s2)") apply(simp only: subst_susp) apply(simp only: equ_pi_to_left[THEN sym]) apply(simp only: equ_involutive_left) apply(simp) apply(erule conjE) apply(drule not_in_domn)+ apply(subgoal_tac "subst s1 (Susp list1 list2)=swap list1 (subst s1 (Susp [] list2))")(* A *) apply(subgoal_tac "subst s2 (Susp list1 list2)=swap list1 (subst s2 (Susp [] list2))")(* B *) apply(simp) apply(rule equ_refl) (* A / B *) apply(simp (no_asm) add: subst_swap_comm[THEN sym])+ done lemma subst_cancel_right: "\nabla\(subst s1)\(subst s2)\ \ nabla\(subst (s1\s))\(subst (s2\s))" apply(simp (no_asm) only: subst_equ_def) apply(force intro: subst_equ_to_trm simp add: subst_comp_expand) done lemma subst_trans: "\nabla\subst s1\subst s2; nabla\subst s2\subst s3\ \ nabla\subst s1\subst s3" apply(simp add: subst_equ_def) apply(auto) apply(case_tac "X \domn (subst s2)") apply(drule_tac x="X" in bspec) apply(force) apply(drule_tac x="X" in bspec) apply(force) apply(rule_tac "t2.0"="subst s2 (Susp [] X)" in equ_trans) apply(assumption)+ apply(case_tac "X \domn (subst s3)") apply(drule_tac x="X" in bspec) apply(force) apply(drule_tac x="X" in bspec) apply(force) apply(rule_tac "t2.0"="subst s2 (Susp [] X)" in equ_trans) apply(assumption)+ apply(drule not_in_domn)+ apply(drule_tac x="X" in bspec) apply(force) apply(simp) apply(case_tac "X \domn (subst s1)") apply(drule_tac x="X" in bspec) apply(force) apply(drule_tac x="X" in bspec) apply(force) apply(rule_tac "t2.0"="subst s2 (Susp [] X)" in equ_trans) apply(assumption)+ apply(case_tac "X \domn (subst s2)") apply(drule_tac x="X" in bspec) apply(force) apply(drule_tac x="X" in bspec) apply(force) apply(rule_tac "t2.0"="subst s2 (Susp [] X)" in equ_trans) apply(assumption)+ apply(drule not_in_domn)+ apply(simp) apply(rotate_tac 1) apply(drule_tac x="X" in bspec) apply(force) apply(simp) done (* if occurs holds, then one subterm is equal to (subst s (Susp pi X)) *) lemma occurs_sub_trm_equ: "occurs X t1 \ (\t2\sub_trms (subst s t1). (\pi.(nabla\subst s (Susp pi1 X)\(swap pi t2))))" apply(induct_tac t1) apply(auto) (* Susp *) apply(simp only: subst_susp) apply(rule_tac x="swap list1 (look_up X s)" in bexI) apply(rule_tac x="pi1@(rev list1)" in exI) apply(simp add: swap_append) apply(simp add: equ_pi_to_left[THEN sym]) apply(simp only: equ_involutive_left) apply(rule equ_refl) apply(simp) done (* occurs implies that the problem is not solvable *) lemma occurs_not_solvable: "\occurs X t;psub_trms t\{}\ \ \(\ nabla s. nabla\(subst s (Susp pi X))\(subst s t))" apply(simp) apply(insert psub_trm_not_equ) apply(rule allI)+ apply(clarify) apply(case_tac t) apply(simp_all) (* Abst *) apply(drule equ_sym) apply(drule_tac x="nabla" in spec) apply(drule_tac x="Abst list (subst s trm)" in spec) apply(force dest: occurs_sub_trm_equ[THEN mp] equ_trans) (* Paar *) apply(drule equ_sym) apply(drule_tac x="nabla" in spec) apply(drule_tac x="Paar (subst s trm1) (subst s trm2)" in spec) apply(case_tac "occurs X trm1") apply(simp) apply(drule_tac nabla1="nabla" and s1="s" and "pi1.1"="pi" in occurs_sub_trm_equ[THEN mp]) apply(clarify) apply(drule_tac x="t2" in bspec) apply(force) apply(auto dest: equ_trans) apply(drule_tac nabla1="nabla" and s1="s" and "pi1.1"="pi" in occurs_sub_trm_equ[THEN mp]) apply(clarify) apply(drule_tac x="t2" in bspec) apply(force) apply(auto dest: equ_trans) (* Func *) apply(drule equ_sym) apply(drule_tac x="nabla" in spec) apply(drule_tac x="Func list (subst s trm)" in spec) apply(force dest: occurs_sub_trm_equ[THEN mp] equ_trans) done (* terms with different term-constructors are not unifyable *) lemma not_unifyable: "\(equ_constr (t1,t2)) \ \(\nabla s. nabla\subst s t1\subst s t2)" apply(case_tac t1) apply(simp_all) apply(case_tac t2) apply(simp_all) apply(auto dest!: equ_abst_t) apply(case_tac t2) apply(simp_all) apply(case_tac t2) apply(simp_all) apply(auto dest!: equ_unit_t) apply(case_tac t2) apply(simp_all) apply(auto dest!: equ_atom_t) apply(case_tac t2) apply(simp_all) apply(auto dest!: equ_paar_t) apply(case_tac t2) apply(simp_all) apply(auto dest!: equ_func_t) done end Swap.thy0100644000175000001440000000222107660505260011272 0ustar cu200users theory Swap = Main: consts swapa :: "(string \ string) \ string \ string" swapas :: "(string \ string)list \ string \ string" primrec "swapa (b,c) a = (if b = a then c else (if c = a then b else a))" primrec "swapas [] a = a" "swapas (x#pi) a = swapa x (swapas pi a)" lemma [simp]: "swapas [(a,a)] b=b" apply(auto) done lemma swapas_append: "swapas (pi1@pi2) a = swapas pi1 (swapas pi2 a)" apply(induct_tac pi1, auto) done lemma [simp]: "swapas (rev pi) (swapas pi a) = a" apply(induct_tac pi) apply(simp_all add: swapas_append, auto) done lemma swapas_rev_pi_a: "swapas pi a = b \ swapas (rev pi) b = a" apply(auto) done lemma [simp]: "swapas pi (swapas (rev pi) a) = a" apply(rule swapas_rev_pi_a[of "(rev pi)" _ _,simplified]) apply(simp) done lemma swapas_rev_pi_b: "swapas (rev pi) a = b \ swapas pi b = a" apply(auto) done lemma swapas_comm: "(swapas (pi@[(a,b)]) c) = (swapas ([(swapas pi a,swapas pi b)]@pi) c)" apply(auto) apply(simp_all only: swapas_append) apply(auto) apply(drule swapas_rev_pi_a, simp)+ done endTermination.thy0100644000175000001440000001455007660505360012662 0ustar cu200users theory Termination = Main + Terms + Fresh + Equ + Substs + Mgu: (* set of variables *) consts vars_trm :: "trm \ string set" vars_eprobs :: "eprobs \ (string set)" primrec "vars_trm (Unit) = {}" "vars_trm (Atom a) = {}" "vars_trm (Susp pi X) = {X}" "vars_trm (Paar t1 t2) = (vars_trm t1)\(vars_trm t2)" "vars_trm (Abst a t) = vars_trm t" "vars_trm (Func F t) = vars_trm t" primrec "vars_eprobs [] = {}" "vars_eprobs (x#xs) = (vars_trm (snd x))\(vars_trm (fst x))\(vars_eprobs xs)" lemma[simp]: "vars_trm (swap pi t) = vars_trm t" apply(induct_tac t) apply(auto) done consts size_trm :: "trm \ nat" size_fprobs :: "fprobs \ nat" size_eprobs :: "eprobs \ nat" size_probs :: "probs \ nat" primrec "size_trm (Unit) = 1" "size_trm (Atom a) = 1" "size_trm (Susp pi X) = 1" "size_trm (Abst a t) = 1 + size_trm t" "size_trm (Func F t) = 1 + size_trm t" "size_trm (Paar t t') = 1 + (size_trm t) + (size_trm t')" primrec "size_fprobs [] = 0" "size_fprobs (x#xs) = (size_trm (snd x))+(size_fprobs xs)" primrec "size_eprobs [] = 0" "size_eprobs (x#xs) = (size_trm (fst x))+(size_trm (snd x))+(size_eprobs xs)" lemma[simp]: "size_trm (swap pi t) = size_trm t" apply(induct_tac t) apply(auto) done syntax "_measure_relation" :: "(nat\nat\nat) \ (nat\nat\nat) \ bool" ("_ \ _" [80,80] 80) translations "n1 \ n2" \ "(n1,n2) \ (less_than<*lex*>less_than<*lex*>less_than)" consts rank :: "probs \ (nat\nat\nat)" primrec "rank (eprobs,fprobs) = (card (vars_eprobs eprobs),size_eprobs eprobs,size_fprobs fprobs)" lemma[simp]: "finite (vars_trm t)" apply(induct t) apply(auto) done lemma[simp]: "finite (vars_eprobs P)" apply(induct_tac P) apply(auto) done lemma union_comm: "A\(B\C)=(A\B)\C" apply(auto) done lemma card_union: "\finite A; finite B\\(card B < card (A\B)) \ (card B = card (A\B))" apply(auto) apply(rule psubset_card_mono) apply(auto) done lemma card_insert: "\finite B\\(card B < card (insert X B)) \ (card B = card (insert X B))" apply(auto) apply(rule psubset_card_mono) apply(auto) done lemma subseteq_card: "\A\B; finite B\\(card A \ card B)" apply(drule_tac A="A" in card_mono) apply(auto simp add: le_eq_less_or_eq) done lemma not_occurs_trm: "\occurs X t \ X\ vars_trm t" apply(induct_tac t) apply(auto) done lemma not_occurs_subst: "\occurs X t1\ X\ vars_trm (subst [(X,swap pi2 t1)] t2)" apply(induct_tac t2) apply(auto simp add: subst_susp not_occurs_trm) done lemma not_occurs_list: "\occurs X t \ X\ vars_eprobs (apply_subst_eprobs [(X, swap pi t)] xs)" apply(induct_tac xs) apply(simp) apply(case_tac a) apply(auto simp add: not_occurs_subst) done lemma vars_equ: "\occurs X t1 \ occurs X t2\ vars_trm (subst [(X, swap pi t1)] t2)=(vars_trm t1\vars_trm t2)-{X}" apply(induct_tac t2) apply(force) apply(case_tac "X=list2") apply(simp add: subst_susp not_occurs_trm) apply(simp) apply(simp) apply(simp) apply(simp) apply(rule conjI) apply(case_tac "occurs X trm2") apply(force) apply(force dest: not_occurs_trm[THEN mp] simp add: subst_not_occurs) apply(force dest: not_occurs_trm[THEN mp] simp add: subst_not_occurs) apply(force) done lemma vars_subseteq: "\occurs X t \ vars_eprobs (apply_subst_eprobs [(X, swap pi t)] xs) \ (vars_trm t \ vars_eprobs xs)" apply(induct_tac xs) apply(simp) apply(rule impI) apply(simp) apply(case_tac "occurs X (fst a)") apply(case_tac "occurs X (snd a)") apply(simp add: vars_equ[THEN mp]) apply(force) apply(simp add: subst_not_occurs) apply(force simp add: vars_equ) apply(case_tac "occurs X (snd a)") apply(simp add: vars_equ[THEN mp]) apply(force simp add: subst_not_occurs) apply(force simp add: subst_not_occurs) done lemma vars_decrease: "\occurs X t\ card (vars_eprobs (apply_subst_eprobs [(X, swap pi t)] xs)) vars_eprobs xs))" apply(rule impI) apply(case_tac "X\(vars_trm t \ vars_eprobs xs)") (* first case *) apply(subgoal_tac "insert X (vars_trm t \ vars_eprobs xs) = (vars_trm t \ vars_eprobs xs)") (*A*) apply(simp) apply(frule_tac pi1="pi" and xs1="xs" in vars_subseteq[THEN mp]) apply(frule_tac pi1="pi" and xs1="xs" in not_occurs_list[THEN mp]) apply(subgoal_tac "vars_eprobs (apply_subst_eprobs [(X, swap pi t)] xs) \ vars_trm t \ vars_eprobs xs") (* B *) apply(simp add: psubset_card_mono) (* B *) apply(force) (* A *) apply(force) (* second case *) apply(subgoal_tac "finite (vars_trm t \ vars_eprobs xs)") apply(drule_tac x="X" in card_insert_disjoint) apply(simp) apply(simp) apply(frule_tac pi1="pi" and xs1="xs" in vars_subseteq[THEN mp]) apply(auto dest: subseteq_card) done lemma rank_cred: "\P1\(nabla)\P2\\(rank P2) \ (rank P1)" apply(ind_cases "P1 \ nabla \ P2") apply(simp_all add: lex_prod_def) done lemma rank_sred: "\P1\(s)\P2\\(rank P2) \ (rank P1)" apply(ind_cases "P1 \ s \ P2") apply(simp_all add: lex_prod_def union_comm) apply(subgoal_tac "vars_trm s1\vars_trm t1\vars_trm s2\vars_trm t2\vars_eprobs xs = vars_trm s1\vars_trm s2\vars_trm t1\vars_trm t2\vars_eprobs xs") (*A*) apply(simp) (* A *) apply(force) (* Susp-Susp case *) apply(simp add: card_insert) (* variable elimination cases *) apply(simp_all add: apply_subst_def vars_decrease) done lemma rank_trans: "\rank P1 \ rank P2; rank P2 \ rank P3\\rank P1 \ rank P3" apply(simp add: lex_prod_def) apply(auto) done (* all reduction are well-founded under \ *) lemma rank_red_plus: "\P1\(s,nabla)\P2\\(rank P2) \ (rank P1)" apply(erule red_plus.induct) apply(auto dest: rank_sred rank_cred rank_trans) done end Terms.thy0100644000175000001440000001016307660505301011452 0ustar cu200users theory Terms = Main + Swap: (* terms *) datatype trm = Abst string trm | Susp "(string \ string)list" string | Unit | Atom string | Paar trm trm | Func string trm (* swapping operation on terms *) consts swap :: "(string \ string)list \ trm \ trm" primrec "swap pi (Unit) = Unit" "swap pi (Atom a) = Atom (swapas pi a)" "swap pi (Susp pi' X) = Susp (pi@pi') X" "swap pi (Abst a t) = Abst (swapas pi a) (swap pi t)" "swap pi (Paar t1 t2) = Paar (swap pi t1) (swap pi t2)" "swap pi (Func F t) = Func F (swap pi t)" lemma [simp]: "swap [] t = t" apply(induct_tac t) apply(auto) done lemma swap_append[rule_format]: "\pi1 pi2. swap (pi1@pi2) t = swap pi1 (swap pi2 t)" apply(induct_tac t, auto) apply(induct_tac pi1,auto) apply(induct_tac pi1,auto) done lemma swap_empty: "swap pi t=Susp [] X\ pi=[]" apply(induct_tac t) apply(auto) done (* depth of terms *) consts depth :: "trm \ nat" primrec "depth (Unit) = 1" "depth (Atom a) = 1" "depth (Susp pi X) = 1" "depth (Abst a t) = 1 + depth t" "depth (Func F t) = 1 + depth t" "depth (Paar t t') = 1 + (max (depth t) (depth t'))" lemma Suc_max_left: "Suc(max x y) = z \ x < z" and Suc_max_right: "Suc(max x y) = z \ y < z" apply(auto) apply(simp_all only: max_Suc_Suc[THEN sym] less_max_iff_disj) apply(simp_all) done lemma [simp]: "depth (swap pi t) = depth t" apply(induct_tac t,auto) done (* function that compares the top-most term constructor *) consts equ_constr :: "(trm\trm) \ bool" recdef equ_constr "measure (\(t1,t2). 1)" "equ_constr (Atom a1,Atom a2) = (if a1=a2 then True else False)" "equ_constr (Susp pi1 X1,t1) = True" "equ_constr (t1,Susp pi1 X1) = True" "equ_constr (Unit,Unit) = True" "equ_constr (Abst a1 t1,Abst a2 t2) = True" "equ_constr (Paar t1 s1,Paar t2 s2) = True" "equ_constr (Func F1 t1,Func F2 t2) = (if F1=F2 then True else False)" "equ_constr (t1,t2) = False" (* occurs predicate *) consts occurs :: "string \ trm \ bool" primrec "occurs X (Unit) = False" "occurs X (Atom a) = False" "occurs X (Susp pi Y) = (if X=Y then True else False)" "occurs X (Abst a t) = occurs X t" "occurs X (Paar t1 t2) = (if (occurs X t1) then True else (occurs X t2))" "occurs X (Func F t) = occurs X t" (* subterms and proper subterms *) consts sub_trms :: "trm \ trm set" primrec "sub_trms (Unit) = {Unit}" "sub_trms (Atom a) = {Atom a}" "sub_trms (Susp pi Y) = {Susp pi Y}" "sub_trms (Abst a t) = {Abst a t}\sub_trms t" "sub_trms (Paar t1 t2) = {Paar t1 t2}\sub_trms t1 \sub_trms t2" "sub_trms (Func F t) = {Func F t}\sub_trms t" consts psub_trms :: "trm \ trm set" primrec "psub_trms (Unit) = {}" "psub_trms (Atom a) = {}" "psub_trms (Susp pi X) = {}" "psub_trms (Paar t1 t2) = sub_trms t1 \ sub_trms t2" "psub_trms (Abst a t) = sub_trms t" "psub_trms (Func F t) = sub_trms t" lemma psub_sub_trms[rule_format]: "\t1 . t1 \ psub_trms t2 \ t1 \ sub_trms t2" apply(induct t2) apply(auto) done lemma[simp]: "t\ sub_trms t" apply(induct t) apply(auto) done lemma[simp]: "sub_trms t\{}" apply(induct t) apply(auto) done lemma abst_psub_trms[rule_format]: "\ t1. Abst a t1 \ sub_trms t2 \ t1 \ psub_trms t2" apply(induct_tac t2) apply(auto) apply(best dest!: psub_sub_trms)+ done lemma func_psub_trms[rule_format]: "\ t1. Func F t1 \ sub_trms t2 \ t1 \ psub_trms t2" apply(induct_tac t2) apply(auto) apply(best dest!: psub_sub_trms)+ done lemma paar_psub_trms[rule_format]: "\ t1. Paar t1 t2 \ sub_trms t3\(t1 \ psub_trms t3 \ t2 \ psub_trms t3)" apply(induct_tac t3) apply(auto) apply(best dest!: psub_sub_trms)+ done endUnification.thy0100644000175000001440000004023507660505367012647 0ustar cu200users theory Unification = Main + Terms + Fresh + Equ + Substs + Mgu + Termination: (* problems to which no reduction applies *) consts stuck :: "probs set" defs stuck_def: "stuck \ { P1. \(\P2 nabla s. P1 \(nabla,s)\P2)}" (* all problems which are stuck and have no unifier *) consts fail :: "probs set" inductive fail intros susp_abst[intro!]: "occurs X (Abst a t) \ (Susp pi X\?Abst a t#xs,ys)\fail" susp_func[intro!]: "occurs X (Func F t) \ (Susp pi X\?Func F t#xs,ys)\fail" susp_paar[intro!]: "occurs X (Paar t1 t2) \ (Susp pi X\?Paar t1 t2#xs,ys)\fail" abst_susp[intro!]: "occurs X (Abst a t) \ (Abst a t\?Susp pi X#xs,ys)\fail" func_susp[intro!]: "occurs X (Func F t) \ (Func F t\?Susp pi X#xs,ys)\fail" paar_susp[intro!]: "occurs X (Paar t1 t2) \ (Paar t1 t2\?Susp pi X#xs,ys)\fail" fresh_fail[intro!]: "([],a\? Atom a#ys)\fail" constr_fail[intro!]: "\(equ_constr (t1,t2)) \ (t1\?t2#xs,ys)\fail" (* the results that are interesting are the stuck ones *) consts results :: "probs \ probs set" defs results_def: "results P1 \ if P1\stuck then {P1} else {P2. \nabla s. P1\(nabla,s)\P2 \ P2\stuck}" (* a "failed" problem has no unifier *) lemma fail_then_empty: "(P1\fail) \ (U P1={})" apply(erule fail.cases) apply(simp_all (no_asm) add: all_solutions_def) apply(drule_tac pi="pi" and t="(Abst a t)" in occurs_not_solvable) apply(simp) apply(force) apply(drule_tac pi="pi" and t="(Func F t)" in occurs_not_solvable) apply(simp) apply(force) apply(drule_tac pi="pi" and t="(Paar t1 t2)" in occurs_not_solvable) apply(simp) apply(force) apply(drule_tac pi="pi" and t="(Abst a t)" in occurs_not_solvable) apply(simp) apply(force dest: equ_sym) apply(drule_tac pi="pi" and t="(Func F t)" in occurs_not_solvable) apply(simp) apply(force dest: equ_sym) apply(drule_tac pi="pi" and t="(Paar t1 t2)" in occurs_not_solvable) apply(simp) apply(force dest: equ_sym) apply(simp) apply(rule allI,rule impI) apply(ind_cases "aa \ a \ Atom a") apply(drule not_unifyable[THEN mp]) apply(force) done (* the only stuck problems are the "failed" problems and the empty problem *) lemma stuck_equiv: "stuck = {([],[])}\fail" apply(subgoal_tac "([],[])\stuck") apply(subgoal_tac "\P\fail. P\stuck") apply(subgoal_tac "\P\stuck. P=([],[]) \ P\fail") apply(force) apply(rule ballI) apply(thin_tac "([], []) \ stuck") apply(thin_tac "\P\fail. P \ stuck") apply(simp add: stuck_def) apply(clarify) apply(case_tac a) apply(simp) apply(case_tac b) apply(simp) apply(simp) apply(case_tac aa) apply(simp) apply(case_tac ba) apply(simp_all) apply(case_tac "ab=lista") apply(force) apply(force) apply(force) apply(force) apply(force) apply(force) apply(force) apply(case_tac aa) apply(simp) apply(case_tac ab) apply(simp_all) apply(case_tac ba) apply(simp_all) apply(case_tac "lista=listb") apply(force) apply(force) apply(case_tac "occurs list2 (Abst lista trm)") apply(drule_tac a="lista" and t="trm" and pi="list1" and xs="list" and ys="b" in abst_susp) apply(simp) apply(simp) apply(drule_tac x="fst (apply_subst [(list2,swap (rev list1) (Abst lista trm))] (list,b))" in spec) apply(drule_tac x="snd (apply_subst [(list2,swap (rev list1) (Abst lista trm))] (list,b))" in spec) apply(drule_tac x="{}" in spec) apply(drule_tac x="[(list2, swap (rev list1) (Abst lista trm))]" in spec) apply(simp only: surjective_pairing[THEN sym]) apply(force) apply(force) apply(force) apply(force) apply(force) apply(case_tac ba) apply(simp_all) apply(case_tac "occurs list2 (Abst lista trm)") apply(drule_tac a="lista" and t="trm" and pi="list1" and xs="list" and ys="b" in susp_abst) apply(simp) apply(drule_tac x="fst (apply_subst [(list2,swap (rev list1) (Abst lista trm))] (list,b))" in spec) apply(drule_tac x="snd (apply_subst [(list2,swap (rev list1) (Abst lista trm))] (list,b))" in spec) apply(drule_tac x="{}" in spec) apply(drule_tac x="[(list2, swap (rev list1) (Abst lista trm))]" in spec) apply(simp only: surjective_pairing[THEN sym]) apply(force) apply(case_tac "list2=list2a") apply(force) apply(case_tac "occurs list2 (Susp list1a list2a)") apply(simp) apply(drule_tac x="fst (apply_subst [(list2,swap (rev list1) (Susp list1a list2a))] (list,b))" in spec) apply(drule_tac x="snd (apply_subst [(list2,swap (rev list1) (Susp list1a list2a))] (list,b))" in spec) apply(drule_tac x="{}" in spec) apply(drule_tac x="[(list2, swap (rev list1) (Susp list1a list2a))]" in spec) apply(simp only: surjective_pairing[THEN sym]) apply(force) apply(case_tac "occurs list2 Unit") apply(simp) apply(drule_tac x="fst (apply_subst [(list2,swap (rev list1) Unit)] (list,b))" in spec) apply(drule_tac x="snd (apply_subst [(list2,swap (rev list1) Unit)] (list,b))" in spec) apply(drule_tac x="{}" in spec) apply(drule_tac x="[(list2, swap (rev list1) Unit)]" in spec) apply(simp only: surjective_pairing[THEN sym]) apply(force) apply(case_tac "occurs list2 (Atom lista)") apply(simp) apply(drule_tac x="fst (apply_subst [(list2,swap (rev list1) (Atom lista))] (list,b))" in spec) apply(drule_tac x="snd (apply_subst [(list2,swap (rev list1) (Atom lista))] (list,b))" in spec) apply(drule_tac x="{}" in spec) apply(drule_tac x="[(list2, swap (rev list1) (Atom lista))]" in spec) apply(simp only: surjective_pairing[THEN sym]) apply(force) apply(case_tac "occurs list2 (Paar trm1 trm2)") apply(drule_tac "t1.0"="trm1" and "t2.0"="trm2" and pi="list1" and xs="list" and ys="b" in susp_paar) apply(simp) apply(drule_tac x="fst (apply_subst [(list2,swap (rev list1) (Paar trm1 trm2))] (list,b))" in spec) apply(drule_tac x="snd (apply_subst [(list2,swap (rev list1) (Paar trm1 trm2))] (list,b))" in spec) apply(drule_tac x="{}" in spec) apply(drule_tac x="[(list2, swap (rev list1) (Paar trm1 trm2))]" in spec) apply(simp only: surjective_pairing[THEN sym]) apply(force) apply(case_tac "occurs list2 (Func lista trm)") apply(drule_tac F="lista" and "t"="trm" and pi="list1" and xs="list" and ys="b" in susp_func) apply(force) apply(drule_tac x="fst (apply_subst [(list2,swap (rev list1) (Func lista trm))] (list,b))" in spec) apply(drule_tac x="snd (apply_subst [(list2,swap (rev list1) (Func lista trm))] (list,b))" in spec) apply(drule_tac x="{}" in spec) apply(drule_tac x="[(list2, swap (rev list1) (Func lista trm))]" in spec) apply(simp only: surjective_pairing[THEN sym]) apply(force) apply(case_tac ba) apply(simp_all) apply(force) apply(case_tac "occurs list2 Unit") apply(simp) apply(drule_tac x="fst (apply_subst [(list2,swap (rev list1) Unit)] (list,b))" in spec) apply(drule_tac x="snd (apply_subst [(list2,swap (rev list1) Unit)] (list,b))" in spec) apply(drule_tac x="{}" in spec) apply(drule_tac x="[(list2, swap (rev list1) Unit)]" in spec) apply(simp only: surjective_pairing[THEN sym]) apply(force) apply(force) apply(force) apply(force) apply(force) apply(case_tac ba) apply(simp_all) apply(force) apply(case_tac "occurs list2 (Atom lista)") apply(simp) apply(drule_tac x="fst (apply_subst [(list2,swap (rev list1) (Atom lista))] (list,b))" in spec) apply(drule_tac x="snd (apply_subst [(list2,swap (rev list1) (Atom lista))] (list,b))" in spec) apply(drule_tac x="{}" in spec) apply(drule_tac x="[(list2, swap (rev list1) (Atom lista))]" in spec) apply(simp only: surjective_pairing[THEN sym]) apply(force) apply(force) apply(case_tac "lista=listb") apply(force) apply(force) apply(force) apply(force) apply(case_tac ba) apply(simp_all) apply(force) apply(case_tac "occurs list2 (Paar trm1 trm2)") apply(drule_tac "t1.0"="trm1" and "t2.0"="trm2" and pi="list1" and xs="list" and ys="b" in paar_susp) apply(simp) apply(drule_tac x="fst (apply_subst [(list2,swap (rev list1) (Paar trm1 trm2))] (list,b))" in spec) apply(drule_tac x="snd (apply_subst [(list2,swap (rev list1) (Paar trm1 trm2))] (list,b))" in spec) apply(drule_tac x="{}" in spec) apply(drule_tac x="[(list2, swap (rev list1) (Paar trm1 trm2))]" in spec) apply(simp only: surjective_pairing[THEN sym]) apply(force) apply(force) apply(force) apply(force) apply(force) apply(case_tac ba) apply(simp_all) apply(force) apply(case_tac "occurs list2 (Func lista trm)") apply(drule_tac F="lista" and "t"="trm" and pi="list1" and xs="list" and ys="b" in func_susp) apply(force) apply(drule_tac x="fst (apply_subst [(list2,swap (rev list1) (Func lista trm))] (list,b))" in spec) apply(drule_tac x="snd (apply_subst [(list2,swap (rev list1) (Func lista trm))] (list,b))" in spec) apply(drule_tac x="{}" in spec) apply(drule_tac x="[(list2, swap (rev list1) (Func lista trm))]" in spec) apply(simp only: surjective_pairing[THEN sym]) apply(force) apply(force) apply(force) apply(force) apply(case_tac "lista=listb") apply(simp) apply(force) apply(force) apply(rule ballI) apply(thin_tac "([], []) \ stuck") apply(simp add: stuck_def) apply(clarify) apply(ind_cases "((a, b), (nabla, s), aa, ba) \ red_plus") apply(ind_cases "((a, b), s, aa, ba) \ s_red") apply(simp_all) apply(ind_cases "((Unit, Unit) # aa, b) \ fail") apply(ind_cases "((Paar t1 t2, Paar s1 s2) # xs, b) \ fail") apply(simp) apply(ind_cases "((Func F t1, Func F t2) # xs, b) \ fail") apply(simp) apply(ind_cases "((Abst ab t1, Abst ab t2) # xs, b) \ fail") apply(simp) apply(ind_cases "((Abst ab t1, Abst bb t2) # xs, b) \ fail") apply(simp) apply(ind_cases "((Atom ab, Atom ab) # aa, b) \ fail") apply(simp) apply(ind_cases "((Susp pi1 X, Susp pi2 X) # aa, b) \ fail") apply(simp) apply(simp add: apply_subst_def) apply(clarify) apply(ind_cases "((Susp pi X, t) # xs, b) \ fail") apply(simp_all) apply(case_tac t) apply(simp_all) apply(ind_cases "((t, Susp pi X) # xs, b) \ fail") apply(simp_all) apply(case_tac t) apply(simp_all) apply(ind_cases "((a, b), nabla, aa, ba) \ c_red") apply(simp_all) apply(ind_cases "([], (ab, Unit) # ba) \ fail") apply(ind_cases "([], (ab, Paar t1 t2) # xs) \ fail") apply(ind_cases "([], (ab, Func F t) # xs) \ fail") apply(ind_cases "([], (ab, Abst ab t) # ba) \ fail") apply(ind_cases "([], (ab, Abst bb t) # xs) \ fail") apply(ind_cases "([], (ab, Atom bb) # ba) \ fail") apply(simp) apply(ind_cases "([], (ab, Susp pi X) # ba) \ fail") apply(ind_cases "(a, b) \ s1 \ P2") apply(simp_all) apply(ind_cases "((Unit, Unit) # xs, b) \ fail") apply(ind_cases "((Paar t1 t2, Paar s1 s2) # xs, b) \ fail") apply(simp) apply(ind_cases "((Func F t1, Func F t2) # xs, b) \ fail") apply(simp) apply(ind_cases "((Abst ab t1, Abst ab t2) # xs, b) \ fail") apply(simp) apply(ind_cases "((Abst ab t1, Abst bb t2) # xs, b) \ fail") apply(simp) apply(ind_cases "((Atom ab, Atom ab) # aa, b) \ fail") apply(simp) apply(ind_cases "((Susp pi1 X, Susp pi2 X) # aa, b) \ fail") apply(simp) apply(ind_cases "((Susp pi X, t) # xs, b) \ fail") apply(simp add: apply_subst_def)+ apply(case_tac t) apply(simp_all) apply(ind_cases "((t, Susp pi X) # xs, b) \ fail") apply(simp add: apply_subst_def) apply(simp) apply(simp) apply(case_tac t) apply(simp_all) apply(ind_cases "(a, b) \ nabla1 \ P2") apply(simp_all) apply(ind_cases "([], (ab, Unit) # ba) \ fail") apply(ind_cases "([], (ab, Paar t1 t2) # xs) \ fail") apply(ind_cases "([], (ab, Func F t) # xs) \ fail") apply(ind_cases "([], (ab, Abst ab t) # ba) \ fail") apply(ind_cases "([], (ab, Abst bb t) # xs) \ fail") apply(ind_cases "([], (ab, Atom bb) # ba) \ fail") apply(simp) apply(ind_cases "([], (ab, Susp pi X) # ba) \ fail") apply(simp add: stuck_def) apply(rule allI)+ apply(clarify) apply(ind_cases "(([], []), (nabla, s), a, b) \ red_plus") apply(ind_cases "(([], []), s, a, b) \ s_red") apply(ind_cases "(([], []), nabla, a, b) \ c_red") apply(ind_cases "([], []) \ s1 \ P2") apply(ind_cases "([], []) \ nabla1 \ P2") done lemma u_empty_sred: "P1\s\P2 \ U P2 ={} \ U P1={}" apply(rule impI) apply(ind_cases "P1 \ s \ P2") apply(rule impI, simp add: all_solutions_def) apply(rule impI, simp add: all_solutions_def) apply(fast dest!: equ_paar_elim) apply(rule impI, simp add: all_solutions_def) apply(fast dest!: equ_func_elim) apply(rule impI, simp add: all_solutions_def) apply(fast dest!: equ_abst_aa_elim) apply(rule impI, simp add: all_solutions_def) apply(force dest!: equ_abst_ab_elim simp add: subst_swap_comm[THEN sym]) apply(rule impI, simp add: all_solutions_def) apply(rule impI, simp add: all_solutions_def) apply(simp add: ds_list_equ_ds) apply(rule allI)+ apply(rule impI) apply(drule_tac x="a" in spec) apply(drule_tac x="b" in spec) apply(erule disjE) apply(force) apply(simp add: subst_susp) apply(drule equ_pi1_pi2_dec) apply(force simp add: subst_susp) apply(auto) apply(simp add: all_solutions_def) apply(simp_all add: apply_subst_def) apply(simp only: map_equ map_fresh) apply(auto) apply(drule_tac x="a" in spec) apply(drule_tac x="b" in spec) apply(drule susp_subst_equ) apply(auto) apply(drule_tac x="(aa,ba)" in bspec) apply(assumption) apply(simp) apply(drule_tac "t1.0"="aa" and "t2.0"="ba" in subst_change_equ) apply(simp add: subst_comp_expand) apply(drule_tac x="(aa,ba)" in bspec) apply(assumption) apply(simp) apply(drule_tac a="aa" and "t"="ba" in subst_change_fresh) apply(simp add: subst_comp_expand) apply(simp only: map_equ map_fresh) apply(simp add: all_solutions_def) apply(auto) apply(drule_tac x="a" in spec) apply(drule_tac x="b" in spec) apply(drule equ_sym) apply(drule susp_subst_equ) apply(auto) apply(drule_tac x="(aa,ba)" in bspec) apply(assumption) apply(simp) apply(drule_tac "t1.0"="aa" and "t2.0"="ba" in subst_change_equ) apply(simp add: subst_comp_expand) apply(drule_tac x="(aa,ba)" in bspec) apply(assumption) apply(simp) apply(drule_tac a="aa" and "t"="ba" in subst_change_fresh) apply(simp add: subst_comp_expand) done lemma u_empty_cred: "P1\nabla\P2 \ U P2 ={} \ U P1={}" apply(rule impI) apply(ind_cases "P1 \nabla\P2") apply(rule impI, simp add: all_solutions_def) apply(rule impI, simp add: all_solutions_def) apply(fast dest!: fresh_paar_elim) apply(rule impI, simp add: all_solutions_def) apply(fast dest!: fresh_func_elim) apply(rule impI, simp add: all_solutions_def) apply(rule impI, simp add: all_solutions_def) apply(force dest!: fresh_abst_ab_elim) apply(rule impI, simp add: all_solutions_def) apply(rule impI, simp add: all_solutions_def) done lemma u_empty_red_plus: "P1\(nabla,s)\P2 \ U P2 ={} \ U P1={}" apply(rule impI) apply(erule red_plus.induct) apply(drule u_empty_sred[THEN mp], assumption) apply(drule u_empty_cred[THEN mp], assumption) apply(drule u_empty_sred[THEN mp], force) apply(drule u_empty_cred[THEN mp], force) done (* all problems that cannot be solved produce "failed" problems only *) lemma empty_then_fail: "U P1={} \ (\P\results P1. P\fail)" apply(simp add: results_def) apply(rule conjI) apply(rule impI) apply(rule impI) apply(simp add: stuck_equiv) apply(erule disjE) apply(subgoal_tac "({},[])\U ([],[])") apply(simp) apply(simp add: all_solutions_def) apply(assumption) apply(rule impI)+ apply(rule allI)+ apply(rule impI) apply(erule conjE) apply(simp add: stuck_equiv) apply(auto) apply(subgoal_tac "({},[])\U ([],[])") apply(drule_tac "nabla3.0"="nabla" and "nabla1.0"="{}" and "s1.0"="[]" in P1_from_P2_red_plus) apply(simp add: ext_subst_def) apply(auto) apply(simp add: all_solutions_def) done (* if a problem can be solved then no "failed" problem is produced *) lemma not_empty_then_not_fail: "U P1\{} \ \(\P\results P1. P\fail)" apply(rule impI) apply(simp) apply(rule ballI) apply(clarify) apply(simp add: results_def) apply(case_tac "P1\stuck") apply(simp_all) apply(drule fail_then_empty) apply(simp) apply(drule fail_then_empty) apply(erule conjE) apply(clarify) apply(drule u_empty_red_plus[THEN mp]) apply(simp) done end ROOT.ML0100644000175000001440000000031207660505417010652 0ustar cu200usersuse_thy "Swap"; use_thy "Terms"; use_thy "Atoms"; use_thy "Disagreement"; use_thy "Fresh"; use_thy "PreEqu"; use_thy "Equ"; use_thy "Substs"; use_thy "Mgu"; use_thy "Termination"; use_thy "Unification";