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 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(simp add: swapas_append)+ 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, auto) done lemma[simp]: "t\sub_trms t" apply(induct t, auto) done lemma[simp]: "sub_trms t\{}" apply(induct t, 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 end