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 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 equ_ds[rule_format]: "\pi1 pi2. (\a\ds pi1 pi2. nabla\a\t) \ (nabla\swap pi1 t\swap pi2 t)" apply(induct_tac t) apply(simp_all) (* Abst *) apply(rule allI)+ apply(rule impI) apply(case_tac "(swapas pi1 list)=(swapas pi2 list)") apply(simp) apply(rule equ_abst_aa) apply(drule_tac x="pi1" in spec) apply(drule_tac x="pi2" in spec) apply(subgoal_tac "(\a\ds pi1 pi2. 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) (* case pi1*list != pi2*list *) apply(rule equ_abst_ab) apply(force) (* second premise of abst-ab *) apply(drule_tac x="swapas ((rev pi2)@pi1) list" in bspec) apply(subgoal_tac "ds pi1 pi2 = ds [] ((rev pi2)@pi1)") (* B *) apply(simp add: ds_def del: atms_append) apply(rule conjI) apply(subgoal_tac "swapas ((rev pi2)@pi1) list \ list")(* C *) apply(rule swapas_pi_in_atms) apply(drule swapas_pi_ineq_a[THEN mp]) apply(simp) (* C *) apply(force dest!: swapas_rev_pi_b simp add: swapas_append) apply(clarify) apply(drule swapas_rev_pi_a) apply(simp add: swapas_append) apply(drule swapas_rev_pi_b) apply(simp) (* B *) apply(simp add: ds_rev ds_sym) apply(subgoal_tac "swapas (rev pi2 @ pi1) list \ list") apply(drule fresh_abst_ab_elim) apply(simp) apply(rule fresh_swap_right[THEN mp]) apply(simp add: swapas_append) apply(clarify) apply(simp add: swapas_append) apply(drule swapas_rev_pi_a) apply(simp) (* third premise of abst-ab *) apply(drule_tac x="pi1" in spec) apply(drule_tac x="(swapas pi1 list, swapas pi2 list)#pi2" in spec) apply(subgoal_tac "\a\ds pi1 ((swapas pi1 list, swapas pi2 list) # pi2). nabla \ a \ trm") (* D *) apply(force simp add: swap_append[THEN sym]) (* D *) apply(rule ballI) apply(drule_tac x="a" in bspec) apply(rule_tac b="list" in ds_swap) apply(simp) apply(case_tac "list=a") apply(simp) apply(simp only: ds_def mem_Collect_eq) apply(erule conjE) apply(simp) apply(force) (* Susp *) apply(rule allI)+ apply(rule impI) apply(rule equ_susp) apply(rule ballI) apply(subgoal_tac "swapas list1 c\ds pi1 pi2")(* 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 pi1 list) = (swapas pi2 list)") apply(force) apply(force dest!: ds_elem_pi1_pi2 fresh_atom_elim) (* Paar *) apply(force dest!: fresh_paar_elim) (* 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_pi1_pi2 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) \ ((\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) (* ADD PI *) apply(rule conjI) apply(rule allI) apply(rule impI) apply(ind_cases "nabla \ t1 \ t2") apply(simp_all) (* Abst-ab *) apply(rule equ_abst_ab) (* abst-ab first premise *) apply(clarify) apply(force dest: swapas_rev_pi_a) (* 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 equ_ds) apply(subgoal_tac "ds (pi @ [(a, b)]) ([(swapas pi a, swapas pi b)] @ pi) = {}")(* C *) apply(simp) (* C *) apply(force simp add: ds_def swapas_comm) (* A *) apply(simp add: swap_append) apply(best) (* Abst-aa *) apply(rule equ_abst_aa) apply(best) (* Unit *) apply(rule equ_unit) (* Atom *) apply(force) (* Susp *) apply(force simp only: ds_cancel_pi_front) (* Paar *) apply(rule equ_paar) apply(drule_tac x="depth t1a" in spec) apply(simp (asm_lr) only: Suc_max_left) apply(drule_tac x="depth s1" in spec) apply(simp (asm_lr) 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 (asm_lr)) apply(drule_tac x="swap [(a,b)] t2a" in spec) apply(drule equ_depth) apply(simp (no_asm_use)) apply(best) (* C *) apply(rule equ_ds[of _ "[]" _ _,simplified]) apply(force simp add: ds_def) (* B *) apply(simp only: swap_append) apply(drule_tac x="depth t1a" in spec) apply(simp (asm_lr)) apply(drule_tac x="t2a" in spec) apply(drule mp) apply(drule equ_depth)+ apply(simp) apply(best) (* 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 (asm_lr)) apply(drule_tac x="swap [(b, ba)] t2a" in spec) apply(drule mp) apply(force dest!: equ_depth) apply(best) (* B *) apply(rule equ_ds[of _ "[]" _ _,simplified]) apply(force simp add: ds_def) (* A *) apply(simp only: swap_append) apply(drule_tac x="depth t1a" in spec) apply(simp (asm_lr)) apply(drule_tac x="t2a" in spec) apply(drule mp) apply(force dest!: equ_depth) apply(best) (* abst-ab third premise *) apply(force intro!: fresh_swap_right[THEN mp]) (* 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(rule equ_ds) apply(subgoal_tac "ds ([(a, b)] @ [(b, ba)]) [(a, ba)] = {a,b}") (* C *) apply(simp) apply(erule disjE) 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") (* D *) apply(simp) apply(case_tac "b=a") apply(force) apply(force) (* D *) apply(rule fresh_swap_left[THEN mp]) apply(assumption) apply(simp) (* C *) apply(force simp add: ds_def) (* A *) apply(subgoal_tac "nabla\swap [(a,b)] t2a\swap [(a,b)] (swap [(b,ba)] t2b)") (* E *) 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]) (* E *) 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(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(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 end