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 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