(* Substitution on pi terms. *) Goalw [NIL_def] "NIL[x//i] = NIL"; by Auto_tac; qed "SUBST_NIL"; Goalw [PAR_def] "(PAR p q)[x//i] = PAR p[x//i] q[x//i]"; by Auto_tac; qed "SUBST_PAR"; Goalw [REP_def] "(REP p)[x//i] = REP p[x//i]"; by Auto_tac; qed "SUBST_REP"; Goalw [NEW_def] "(NEW n ts p)[x//i] = NEW n ts p[x+n // i+n]"; by Auto_tac; qed "SUBST_NEW"; Goalw [IN_def] "(IN x n ts p)[y//i] = IN (substv x y i) n ts p[y+n // i+n]"; by Auto_tac; qed "SUBST_IN"; Goalw [OUT_def] "(OUT x n ys p)[z//i] = \ \ OUT (substv x z i) n (map (%a. substv a z i) ys) p[z//i]"; by Auto_tac; qed "SUBST_OUT"; Addsimps [SUBST_NIL,SUBST_PAR,SUBST_REP,SUBST_NEW,SUBST_IN,SUBST_OUT]; (* Distinctness of constructors for PI *) Goalw [NIL_def,PAR_def] "NIL ~= PAR p q"; by Auto_tac; qed "NIL_not_PAR"; bind_thm("PAR_not_NIL",NIL_not_PAR RS not_sym); Goalw [NIL_def,REP_def] "NIL ~= REP p"; by Auto_tac; qed "NIL_not_REP"; bind_thm("REP_not_NIL",NIL_not_REP RS not_sym); Goalw [NIL_def,NEW_def] "NIL ~= NEW n ts p"; by Auto_tac; qed "NIL_not_NEW"; bind_thm("NEW_not_NIL",NIL_not_NEW RS not_sym); Goalw [NIL_def,IN_def] "NIL ~= IN x n ts p"; by Auto_tac; qed "NIL_not_IN"; bind_thm("IN_not_NIL",NIL_not_IN RS not_sym); Goalw [NIL_def,OUT_def] "NIL ~= OUT x n xs p"; by Auto_tac; qed "NIL_not_OUT"; bind_thm("OUT_not_NIL",NIL_not_OUT RS not_sym); Goalw [PAR_def,REP_def] "PAR p q ~= REP r"; by Auto_tac; qed "PAR_not_REP"; bind_thm("REP_not_PAR",PAR_not_REP RS not_sym); Goalw [PAR_def,NEW_def] "PAR p q ~= NEW n ts r"; by Auto_tac; qed "PAR_not_NEW"; bind_thm("NEW_not_PAR",PAR_not_NEW RS not_sym); Goalw [PAR_def,IN_def] "PAR p q ~= IN x n ts r"; by Auto_tac; qed "PAR_not_IN"; bind_thm("IN_not_PAR",PAR_not_IN RS not_sym); Goalw [PAR_def,OUT_def] "PAR p q ~= OUT x n xs r"; by Auto_tac; qed "PAR_not_OUT"; bind_thm("OUT_not_PAR",PAR_not_OUT RS not_sym); Goalw [REP_def,NEW_def] "REP p ~= NEW n ts q"; by Auto_tac; qed "REP_not_NEW"; bind_thm("NEW_not_REP",REP_not_NEW RS not_sym); Goalw [REP_def,IN_def] "REP p ~= IN x n ts q"; by Auto_tac; qed "REP_not_IN"; bind_thm("IN_not_REP",REP_not_IN RS not_sym); Goalw [REP_def,OUT_def] "REP p ~= OUT x n xs q"; by Auto_tac; qed "REP_not_OUT"; bind_thm("OUT_not_REP",REP_not_OUT RS not_sym); Goalw [NEW_def,IN_def] "NEW m ts p ~= IN y n us q"; by Auto_tac; qed "NEW_not_IN"; bind_thm("IN_not_NEW",NEW_not_IN RS not_sym); Goalw [NEW_def,OUT_def] "NEW m ts p ~= OUT y n xs q"; by Auto_tac; qed "NEW_not_OUT"; bind_thm("OUT_not_NEW",NEW_not_OUT RS not_sym); Goalw [IN_def,OUT_def] "IN x m ts p ~= OUT y n ys q"; by Auto_tac; qed "IN_not_OUT"; bind_thm("OUT_not_IN",IN_not_OUT RS not_sym); Addsimps [NIL_not_PAR,PAR_not_NIL,NIL_not_REP,REP_not_NIL,NIL_not_NEW,NEW_not_NIL, NIL_not_IN, IN_not_NIL, NIL_not_OUT,OUT_not_NIL,PAR_not_REP,REP_not_PAR, PAR_not_NEW,NEW_not_PAR,PAR_not_IN, IN_not_PAR, PAR_not_OUT,OUT_not_PAR, REP_not_NEW,NEW_not_REP,REP_not_IN, IN_not_REP, REP_not_OUT,OUT_not_REP, NEW_not_IN, IN_not_NEW, NEW_not_OUT,OUT_not_NEW,IN_not_OUT, OUT_not_IN]; (* Injectivity of constructors for PI *) Goalw [PAR_def] "(PAR p q = PAR pp qq) = (p = pp & q = qq)"; by Auto_tac; qed "PAR_PAR_eq"; Goalw [REP_def] "(REP p = REP q) = (p = q)"; by Auto_tac; qed "REP_REP_eq"; Goalw [NEW_def] "NEW m ts p = NEW n us q = (m = n & ts = us & p = q)"; by Auto_tac; qed "NEW_NEW_eq"; Goalw [OUT_def] "(OUT x m xs p = OUT y n ys q) = (x = y & m = n & xs = ys & p = q)"; by Auto_tac; qed "OUT_OUT_eq"; Goalw [IN_def] "IN x m ts p = IN y n us q = (x = y & m = n & ts = us & p = q)"; by Auto_tac; qed "IN_IN_eq"; Addsimps [PAR_PAR_eq,REP_REP_eq,OUT_OUT_eq,NEW_NEW_eq,IN_IN_eq]; (* Typing rules for pi terms are derived rules for meta terms. *) Goalw [NIL_def] "unlimited G ==> (G , NIL) : TYPEDMETA"; by(Asm_full_simp_tac 1); by(eresolve_tac [TYPEDMETA.conI] 1); qed "NIL_TYPEDMETA"; Goalw [PAR_def] "[| (G , p) : TYPEDMETA ; (H , q) : TYPEDMETA ; canaddenv G H |] ==> \ \ (addenv G H , PAR p q) : TYPEDMETA"; by(Asm_full_simp_tac 1); by(resolve_tac [TYPEDMETA.appI] 1); by(eresolve_tac [TYPEDMETA_app_con_I] 1); by(assume_tac 1); by(asm_simp_tac (simpset() addsimps [canaddenv_sym]) 1); by(asm_simp_tac (simpset() addsimps [canaddenv_sym,addenv_comm]) 1); qed "PAR_TYPEDMETA"; Goalw [REP_def] "[| unlimited G ; (G , p) : TYPEDMETA |] ==> (G , REP p) : TYPEDMETA"; by(Asm_full_simp_tac 1); by(eresolve_tac [TYPEDMETA_app_con_I] 1); qed "REP_TYPEDMETA"; Goalw [NEW_def] "[| (ts @ G , p) : TYPEDMETA ; length ts = n ; balanced ts |] ==> \ \ (G , NEW n ts p) : TYPEDMETA"; by(Asm_full_simp_tac 1); by(resolve_tac [TYPEDMETA_app_con_I] 1); by(resolve_tac [TYPEDMETA_ABS_I] 1); by(eresolve_tac [TYPEDMETA_app_con_I] 1); by(assume_tac 1); qed "NEW_TYPEDMETA"; Goalw [IN_def] "[| (ts @ G , p) : TYPEDMETA ; length ts = n ; index x = i ; i < length G ; \ \ tag x = Neg ; \ \ canaddtypetoenv G i (LinV (| pos = Zero, neg = One (LChan ts) |)) |] ==> \ \ (addtypetoenv G i (LinV (| pos = Zero, neg = One (LChan ts) |)) , \ \ IN x n ts p) : TYPEDMETA"; by(Asm_full_simp_tac 1); by(resolve_tac [TYPEDMETA.appI] 1); by(resolve_tac [TYPEDMETA_app_con_I] 1); by(resolve_tac [TYPEDMETA_var_I] 1); by(resolve_tac [unlimited_skeleton] 1); by(assume_tac 3); by(asm_full_simp_tac (simpset() addsimps [length_skeleton]) 1); by(eresolve_tac [canaddtypetoenv_skeleton] 1); by(assume_tac 2); by(asm_full_simp_tac (simpset() addsimps [tvocc_def]) 1); by(resolve_tac [refl] 1); by(resolve_tac [TYPEDMETA_ABS_I] 1); by(eresolve_tac [TYPEDMETA_app_con_I] 1); by(assume_tac 1); by(simp_tac (simpset() addsimps [canaddenv_sym]) 1); by(resolve_tac [canaddenv_addtypetoenv_skeleton] 1); by(Asm_full_simp_tac 1); by(cond_rewrite_right_tac addenv_comm 1); by(resolve_tac [addenv_addtypetoenv_skeleton RS sym] 1); by(Asm_full_simp_tac 1); by(simp_tac (simpset() addsimps [canaddenv_sym]) 1); by(resolve_tac [canaddenv_addtypetoenv_skeleton] 1); by(Asm_full_simp_tac 1); qed "LIN_TYPEDMETA"; Goalw [IN_def] "[| (ts @ G , p) : TYPEDMETA ; length ts = n ; index x = i ; i < length G ; \ \ tag x = Both ; \ \ canaddtypetoenv G i (NLinV (NLChan ts)) |] ==> \ \ (addtypetoenv G i (NLinV (NLChan ts)) , IN x n ts p) : TYPEDMETA"; by(Asm_full_simp_tac 1); by(resolve_tac [TYPEDMETA.appI] 1); by(resolve_tac [TYPEDMETA_app_con_I] 1); by(resolve_tac [TYPEDMETA_var_I] 1); by(resolve_tac [unlimited_skeleton] 1); by(assume_tac 3); by(asm_full_simp_tac (simpset() addsimps [length_skeleton]) 1); by(eresolve_tac [canaddtypetoenv_skeleton] 1); by(assume_tac 2); by(asm_full_simp_tac (simpset() addsimps [tvocc_def]) 1); by(resolve_tac [refl] 1); by(resolve_tac [TYPEDMETA_ABS_I] 1); by(eresolve_tac [TYPEDMETA_app_con_I] 1); by(assume_tac 1); by(simp_tac (simpset() addsimps [canaddenv_sym]) 1); by(resolve_tac [canaddenv_addtypetoenv_skeleton] 1); by(Asm_full_simp_tac 1); by(cond_rewrite_right_tac addenv_comm 1); by(resolve_tac [addenv_addtypetoenv_skeleton RS sym] 1); by(Asm_full_simp_tac 1); by(simp_tac (simpset() addsimps [canaddenv_sym]) 1); by(resolve_tac [canaddenv_addtypetoenv_skeleton] 1); by(Asm_full_simp_tac 1); qed "NLIN_TYPEDMETA"; Goalw [OUT_def] "[| (G , p) : TYPEDMETA ; length xs = n ; index x = j ; tag x = Pos ; \ \ map index xs = js ; allless js (length G) ; j < length G ; \ \ map tag xs = tgs ; tvoccs ts tgs ; \ \ canaddtoenv G (j#js) ((LinV (| pos = One (LChan ts), neg = Zero |)) # ts) \ \ |] ==> \ \ (addtypetoenv (addtoenv G js ts) \ \ j (LinV (| pos = One (LChan ts), neg = Zero |)), \ \ OUT x n xs p) : TYPEDMETA"; by(resolve_tac [TYPEDMETA_app_varlist_I] 1); by(eresolve_tac [TYPEDMETA_app_con_I] 1); by(assume_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [tvocc_def]) 1); by(Asm_full_simp_tac 1); qed "LOUT_TYPEDMETA"; Goalw [OUT_def] "[| (G , p) : TYPEDMETA ; length xs = n ; index x = j ; tag x = Both ; \ \ map index xs = js ; allless js (length G) ; j < length G ; \ \ map tag xs = tgs ; tvoccs ts tgs ; \ \ canaddtoenv G (j # js) ((NLinV (NLChan ts)) # ts) |] ==> \ \ (addtypetoenv (addtoenv G js ts) j (NLinV (NLChan ts)) , \ \ OUT x n xs p) : TYPEDMETA"; by(resolve_tac [TYPEDMETA_app_varlist_I] 1); by(eresolve_tac [TYPEDMETA_app_con_I] 1); by(assume_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [tvocc_def]) 1); by(Asm_full_simp_tac 1); qed "NLOUT_TYPEDMETA"; val TYPEDMETA_derivs = [NIL_TYPEDMETA,PAR_TYPEDMETA,REP_TYPEDMETA,NEW_TYPEDMETA, LIN_TYPEDMETA,NLIN_TYPEDMETA,LOUT_TYPEDMETA,NLOUT_TYPEDMETA]; fun nth n xs = if n = 1 then hd xs else nth (n-1) (tl xs); Goalw [TYPEDREL_def] "G |- p ==> (G , p) : TYPEDMETA"; by(eresolve_tac [TYPED.induct] 1); by(ALLGOALS (fn n => (resolve_tac [nth n TYPEDMETA_derivs] n))); by Auto_tac; qed "TYPED_TYPEDMETA"; Goal "[| G |- p ; length G = length H ; \ \ unlimited G ; canaddenv G H ; H |- p |] \ \ ==> unlimited H"; by(dresolve_tac [TYPED_TYPEDMETA] 1); by(dresolve_tac [TYPED_TYPEDMETA] 1); by(resolve_tac [TYPEDMETA_canaddenv_unlimited] 1); by Auto_tac; qed "TYPED_canaddenv_unlimited"; Goal "[| G |- p ; lift m n q = p ; m + n <= length G |] ==> \ \ unlimited (midenv m n G)"; by(dresolve_tac [TYPED_TYPEDMETA] 1); by(resolve_tac [TYPEDMETA_lift_unlimited_midenv] 1); by Auto_tac; qed "TYPED_lift_unlimited_midenv"; Goal "[| ts @ G |- lift 0 n p ; n = length ts |] ==> \ \ unlimited ts"; by(dresolve_tac [TYPED_lift_unlimited_midenv] 1); by Auto_tac; by(rewrite_goals_tac [midenv_def]); by Auto_tac; qed "TYPED_lift_unlimited"; (* Single variable substitution. *) Goal "[| unlimited G; oksubst x i G |] ==> (substenv x i G, NIL) : TYPED"; by(resolve_tac [TYPED.nilI] 1); by Auto_tac; qed "NIL_TYPED_subst"; Goal "[| (substenv y j G, p) : TYPED ; (substenv y j H, q) : TYPED ; \ \ canaddenv G H ; oksubst y j (addenv G H); \ \ oksubst y j G ; oksubst y j H |] ==> \ \ (substenv y j (addenv G H), PAR p q) : TYPED"; by(auto_tac (claset() addIs [TYPED.parI], simpset())); qed "PAR_TYPED_subst"; Goal "[| unlimited G ; (substenv y j G, p) : TYPED ; oksubst y j G |] ==> \ \ (substenv y j G, REP p) : TYPED"; by(auto_tac (claset() addIs [TYPED.repI], simpset())); qed "REP_TYPED_subst"; Goal "[| (ts @ substenv y j G, p) : TYPED ; \ \ length ts = n ; balanced ts ; oksubst y j G |] ==> \ \ (substenv y j G, NEW n ts p) : TYPED"; by(auto_tac (claset() addIs [TYPED.newI], simpset())); qed "NEW_TYPED_subst"; Goal "[| (ts @ substenv y j G, p) : TYPED ; \ \ length ts = n ; index x = i ; i < length G ; \ \ tag x = Neg ; \ \ canaddtypetoenv G i (LinV (| pos = Zero, neg = One (LChan ts)|)) ; \ \ oksubst y j G ; \ \ oksubst y j (addtypetoenv G i (LinV (| pos=Zero, neg= One (LChan ts)|)))|]==> \ \ (substenv y j (addtypetoenv G i (LinV (| pos=Zero, neg= One (LChan ts)|))), \ \ IN (substv x y j) n ts p) : TYPED"; by(auto_tac (claset() addIs [TYPED.linI], simpset() addsimps [substv_def,canaddtypetoenv_substenv])); qed "LIN_TYPED_subst"; Goal "[| (ts @ substenv y j G, p) : TYPED ; \ \ length ts = n ; index x = i ; i < length G ; \ \ tag x = Both ; \ \ canaddtypetoenv G i (NLinV (NLChan ts)) ; \ \ oksubst y j G ; \ \ oksubst y j (addtypetoenv G i (NLinV (NLChan ts))) |] ==> \ \ (substenv y j (addtypetoenv G i (NLinV (NLChan ts))), \ \ IN (substv x y j) n ts p) : TYPED"; by(auto_tac (claset() addIs [TYPED.nlinI], simpset() addsimps [substv_def,canaddtypetoenv_substenv])); qed "NLIN_TYPED_subst"; Goal "[| (substenv y k G, p) : TYPED; \ \ length xs = n; index x = j; tag x = Pos; map index xs = js; \ \ allless js (length G); j < length G; map tag xs = tgs; \ \ tvoccs ts tgs; \ \ canaddtypetoenv (addtoenv G js ts) j \ \ (LinV (| pos = One (LChan ts), neg = Zero |)) ; \ \ canaddtoenv G js ts ; \ \ oksubst y k (addtypetoenv (addtoenv G js ts) j \ \ (LinV (| pos = One (LChan ts), neg = Zero |))) ; \ \ oksubst y k (addtoenv G js ts) ; \ \ oksubst y k G |] ==> \ \ (substenv y k \ \ (addtypetoenv (addtoenv G js ts) j \ \ (LinV (| pos = One (LChan ts), neg = Zero |))), \ \ OUT (substv x y k) n (map (%a. substv a y k) xs) p) : TYPED"; by(auto_tac (claset(), simpset() addsimps [addtoenv_substenv])); by(resolve_tac [TYPED.loutI] 1); by(auto_tac (claset(), simpset() addsimps [map_index_substv,map_tag_substv,allless_map_substvar_2])); by(auto_tac (claset(),simpset() addsimps [substv_def])); by(auto_tac (claset(), simpset() addsimps [addtoenv_substenv RS sym, canaddtypetoenv_substenv,canaddtoenv_substenv])); qed "LOUT_TYPED_subst"; Goal "[| (substenv y k G, p) : TYPED; \ \ length xs = n; index x = j; tag x = Both; map index xs = js; \ \ allless js (length G); j < length G; map tag xs = tgs; \ \ tvoccs ts tgs; \ \ canaddtypetoenv (addtoenv G js ts) j (NLinV (NLChan ts)); \ \ canaddtoenv G js ts ; \ \ oksubst y k (addtypetoenv (addtoenv G js ts) j \ \ (NLinV (NLChan ts))) ; \ \ oksubst y k (addtoenv G js ts) ; \ \ oksubst y k G |] ==> \ \ (substenv y k \ \ (addtypetoenv (addtoenv G js ts) j \ \ (NLinV (NLChan ts))), \ \ OUT (substv x y k) n (map (%a. substv a y k) xs) p) : TYPED"; by(auto_tac (claset(), simpset() addsimps [addtoenv_substenv])); by(resolve_tac [TYPED.nloutI] 1); by(auto_tac (claset(), simpset() addsimps [map_index_substv,map_tag_substv,allless_map_substvar_2])); by(auto_tac (claset(),simpset() addsimps [substv_def])); by(auto_tac (claset(), simpset() addsimps [addtoenv_substenv RS sym, canaddtypetoenv_substenv,canaddtoenv_substenv])); qed "NLOUT_TYPED_subst"; val TYPED_subst_cases = [NIL_TYPED_subst,PAR_TYPED_subst,REP_TYPED_subst, NEW_TYPED_subst,LIN_TYPED_subst,NLIN_TYPED_subst, LOUT_TYPED_subst,NLOUT_TYPED_subst]; Goalw [TYPEDREL_def] "G |- p ==> \ \ !x i. oksubst x i G --> \ \ (substenv x i G) |- p[x//i]"; by(eresolve_tac [TYPED.induct] 1); by(ALLGOALS strip_tac); by(ALLGOALS Simp_tac); by(ALLGOALS (fn n => (TRY (eresolve_tac [oksubst_addenv_elim] n)))); by(ALLGOALS (fn n => (TRY (assume_tac n)))); by(ALLGOALS (fn n => (TRY (eresolve_tac [oksubst_addtypetoenv_elim] n)))); by(ALLGOALS (fn n => (TRY (assume_tac n)))); by(ALLGOALS (fn n => (TRY (eresolve_tac [oksubst_addtoenv_elim] n)))); by(ALLGOALS (fn n => (TRY (assume_tac n)))); by(ALLGOALS (fn n => (resolve_tac [nth n TYPED_subst_cases] n))); by Auto_tac; qed "TYPED_subst_lemma"; Goal "[| G |- p ; oksubst x i G |] ==> substenv x i G |- p[x//i]"; by(dresolve_tac [TYPED_subst_lemma] 1); by Auto_tac; qed "TYPED_subst"; Goal "[| t # G |- p ; canaddtypetoenv G x t |] ==> \ \ addtypetoenv G x t |- p[Suc x//0]"; by(dres_inst_tac [("i","0"),("x","Suc x")] TYPED_subst 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def,oksubst_def,typeof_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def,substenv_def,typeof_def]) 1); qed "TYPED_subst_0"; (* General substitution. *) Goalw [oksub_def,subenv_def,SUB_def] "!p ts G. (ts @ G |- p) & canaddtoenv G xs ts \ \ --> (addtoenv G xs ts) |- SUB p (map (%a. a + length ts) xs)"; by(induct_tac "xs" 1); by(ALLGOALS strip_tac); by(ALLGOALS (exhaust_tac "ts")); by(auto_tac (claset(),simpset() addsimps sub.rules)); by(forward_tac [canaddtypetoenv_addtoenv_comm] 1); by(Asm_full_simp_tac 1); by(forward_tac [canaddtypetoenv_addtoenv_comm_canaddtoenv] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [addtypetoenv_addtoenv_comm]) 1); by(dresolve_tac [TYPED_subst_0] 1); by(resolve_tac [canaddtypetoenv_append] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [addtypetoenv_append RS sym]) 1); by(asm_full_simp_tac (simpset() addsimps [map_newpos_map]) 1); QED "TYPED_SUB"; Goal "[| ts @ G |- p ; canaddtoenv G (map index xs) ts ; length ts = n |] \ \ ==> (addtoenv G (map index xs) ts) |- SUB p (map (%a. index a + n) xs)"; by(auto_tac (claset() addDs [TYPED_SUB],simpset() addsimps [map_index_map])); qed "TYPED_SUB_1"; (* Lifting theorems. *) val lift_tac = REPEAT ((dresolve_tac meta_lifts 1) THEN Auto_tac); Goalw [NIL_def] "lift m n p = NIL ==> p = NIL"; by lift_tac; qed "NIL_lift"; Goalw [PAR_def] "lift m n p = PAR q r ==> \ \ (? qq rr. p = PAR qq rr & q = lift m n qq & r = lift m n rr)"; by lift_tac; qed "PAR_lift"; Goalw [REP_def] "lift m n p = REP q ==> \ \ (? qq. p = REP qq & q = lift m n qq)"; by lift_tac; qed "REP_lift"; Goalw [NEW_def] "lift m n p = NEW r ts q ==> \ \ (? qq. q = lift (m + r) n qq & p = NEW r ts qq)"; by lift_tac; qed "NEW_lift"; Goalw [IN_def] "lift m n p = IN x r ts q ==> \ \ (? qq xx. q = lift (m + r) n qq & x = liftv m n xx & \ \ p = IN xx r ts qq)"; by lift_tac; qed "IN_lift"; Goalw [OUT_def] "lift m n p = OUT x r xs q ==> \ \ (? qq xx xxs. p = OUT xx r xxs qq & q = lift m n qq & \ \ x = liftv m n xx & xs = map (liftv m n) xxs)"; by lift_tac; qed "OUT_lift"; val lifts = [NIL_lift,PAR_lift,REP_lift,NEW_lift,IN_lift,OUT_lift]; Goalw [NIL_def] "lift m n NIL = NIL"; by Auto_tac; qed "lift_NIL"; Goalw [PAR_def] "lift m n (PAR p q) = PAR (lift m n p) (lift m n q)"; by Auto_tac; qed "lift_PAR"; Goalw [REP_def] "lift m n (REP p) = REP (lift m n p)"; by Auto_tac; qed "lift_REP"; Goalw [NEW_def] "lift m n (NEW r ts p) = NEW r ts (lift (m + r) n p)"; by Auto_tac; qed "lift_NEW"; Goalw [IN_def] "lift m n (IN x r ts p) = IN (liftv m n x) r ts (lift (m + r) n p)"; by Auto_tac; qed "lift_IN"; Goalw [OUT_def] "lift m n (OUT x r xs p) = \ \ OUT (liftv m n x) r (map (liftv m n) xs) (lift m n p)"; by Auto_tac; qed "lift_OUT"; Addsimps [lift_NIL,lift_PAR,lift_REP,lift_NEW,lift_IN,lift_OUT]; Goal "[| unlimited G; m + n <= length G |] ==> (remove n m G, NIL) : TYPED"; by(auto_tac (claset() addIs [TYPED.nilI], simpset() addsimps [unlimited_remove])); qed "NIL_TYPED_lift"; Goal "[| (remove n m G, p) : TYPED ; (remove n m H, q) : TYPED ; \ \ canaddenv G H ; m + n <= length (addenv G H); \ \ m + n <= length G ; m + n <= length H |] ==> \ \ (remove n m (addenv G H), PAR p q) : TYPED"; by(auto_tac (claset() addIs [TYPED.parI], simpset() addsimps [remove_addenv,canaddenv_remove])); qed "PAR_TYPED_lift"; Goal "[| unlimited G ; (remove n m G, p) : TYPED ; m + n <= length G |] ==> \ \ (remove n m G, REP p) : TYPED"; by(auto_tac (claset() addIs [TYPED.repI], simpset() addsimps [unlimited_remove])); qed "REP_TYPED_lift"; Goal "[| (ts @ remove n m G, p) : TYPED ; \ \ length ts = a ; balanced ts ; m + n <= length G |] ==> \ \ (remove n m G, NEW a ts p) : TYPED"; by(auto_tac (claset() addIs [TYPED.newI], simpset())); qed "NEW_TYPED_lift"; Goal "[| (ts @ remove n m G, p) : TYPED ; \ \ length ts = a ; index x = i ; liftvar m n i < length G ; \ \ tag x = Neg ; \ \ canaddtypetoenv G (liftvar m n i) \ \ (LinV (| pos = Zero, neg = One (LChan ts)|)) ; \ \ m + n <= length G ; \ \ m + n <= length (addtypetoenv G (liftvar m n i) \ \ (LinV (| pos=Zero, neg= One (LChan ts)|))) \ \ |]==> \ \ (remove n m (addtypetoenv G (liftvar m n i) \ \ (LinV (| pos=Zero, neg= One (LChan ts)|))), \ \ IN x a ts p) : TYPED"; by(auto_tac (claset() addIs [TYPED.linI], simpset() addsimps [remove_addtypetoenv,canaddtypetoenv_def])); qed "LIN_TYPED_lift"; Goal "[| (ts @ remove n m G, p) : TYPED ; \ \ length ts = a ; index x = i ; liftvar m n i < length G ; \ \ tag x = Both ; \ \ canaddtypetoenv G (liftvar m n i) (NLinV (NLChan ts)) ; \ \ m + n <= length G ; \ \ m + n <= length (addtypetoenv G (liftvar m n i) \ \ (NLinV (NLChan ts))) \ \ |]==> \ \ (remove n m (addtypetoenv G (liftvar m n i) \ \ (NLinV (NLChan ts))), \ \ IN x a ts p) : TYPED"; by(auto_tac (claset() addIs [TYPED.nlinI], simpset() addsimps [remove_addtypetoenv,canaddtypetoenv_def])); qed "NLIN_TYPED_lift"; Goal "[| (remove n m G, p) : TYPED; \ \ length xs = a; index x = j; tag x = Pos; map index xs = js; \ \ allless (map (liftvar m n) js) (length G); \ \ liftvar m n j < length G; map tag xs = tgs; \ \ tvoccs ts tgs; \ \ canaddtypetoenv (addtoenv G (map (liftvar m n) js) ts) (liftvar m n j) \ \ (LinV (| pos = One (LChan ts), neg = Zero |)) ; \ \ canaddtoenv G (map (liftvar m n) js) ts ; \ \ m + n <= length (addtypetoenv (addtoenv G (map (liftvar m n) js) ts) \ \ (liftvar m n j) \ \ (LinV (| pos = One (LChan ts), neg = Zero |))) ; \ \ m + n <= length (addtoenv G (map (liftvar m n) js) ts) ; \ \ m + n <= length G |] ==> \ \ (remove n m \ \ (addtypetoenv (addtoenv G (map (liftvar m n) js) ts) \ \ (liftvar m n j) \ \ (LinV (| pos = One (LChan ts), neg = Zero |))), \ \ OUT x a xs p) : TYPED"; by(asm_full_simp_tac (simpset() addsimps [remove_addtypetoenv]) 1); by(asm_full_simp_tac (simpset() addsimps [remove_addtoenv]) 1); by(resolve_tac [TYPED.loutI] 1); by(auto_tac (claset(), simpset() addsimps [remove_addtoenv RS sym,canaddtypetoenv_liftvar_remove, canaddtoenv_liftvar_remove])); qed "LOUT_TYPED_lift"; Goal "[| (remove n m G, p) : TYPED; \ \ length xs = a; index x = j; tag x = Both; map index xs = js; \ \ allless (map (liftvar m n) js) (length G); \ \ liftvar m n j < length G; map tag xs = tgs; \ \ tvoccs ts tgs; \ \ canaddtypetoenv (addtoenv G (map (liftvar m n) js) ts) (liftvar m n j) \ \ (NLinV (NLChan ts)) ; \ \ canaddtoenv G (map (liftvar m n) js) ts ; \ \ m + n <= length (addtypetoenv (addtoenv G (map (liftvar m n) js) ts) \ \ (liftvar m n j) \ \ (NLinV (NLChan ts))) ; \ \ m + n <= length (addtoenv G (map (liftvar m n) js) ts) ; \ \ m + n <= length G |] ==> \ \ (remove n m \ \ (addtypetoenv (addtoenv G (map (liftvar m n) js) ts) \ \ (liftvar m n j) \ \ (NLinV (NLChan ts))), \ \ OUT x a xs p) : TYPED"; by(asm_full_simp_tac (simpset() addsimps [remove_addtypetoenv]) 1); by(asm_full_simp_tac (simpset() addsimps [remove_addtoenv]) 1); by(resolve_tac [TYPED.nloutI] 1); by(auto_tac (claset(), simpset() addsimps [remove_addtoenv RS sym,canaddtypetoenv_liftvar_remove, canaddtoenv_liftvar_remove])); qed "NLOUT_TYPED_lift"; val TYPED_lift_cases = [NIL_TYPED_lift,PAR_TYPED_lift,REP_TYPED_lift,NEW_TYPED_lift, LIN_TYPED_lift,NLIN_TYPED_lift,LOUT_TYPED_lift,NLOUT_TYPED_lift]; Goalw [TYPEDREL_def] "G |- p ==> !q m. lift m n q = p & m + n <= length G \ \ --> remove n m G |- q"; by(eresolve_tac [TYPED.induct] 1); by(ALLGOALS strip_tac); by(ALLGOALS (eresolve_tac [conjE])); by(ALLGOALS (dresolve_tac lifts)); by(auto_tac (claset(),simpset() addsimps [map_index_liftv,map_tag_liftv])); by(auto_tac (claset(),simpset() addsimps [liftv_def])); by(ALLGOALS (fn n => (TRY (eresolve_tac [length_addenv_leq_elim] n)))); by(ALLGOALS (fn n => (TRY (assume_tac n)))); by(ALLGOALS (fn n => (resolve_tac [nth n TYPED_lift_cases] n))); by Auto_tac; qed "TYPED_lift_lemma"; Goal "[| G |- p ; lift m n q = p ; m + n <= length G |] ==> \ \ remove n m G |- q"; by(dresolve_tac [TYPED_lift_lemma] 1); by Auto_tac; qed "TYPED_lift"; Goal "ts @ G |- lift 0 (length ts) q ==> G |- q"; by(dresolve_tac [TYPED_lift] 1); by Auto_tac; qed "TYPED_lift_0"; Goal "[| unlimited G ; m <= length G ; length ts = n ; unlimited ts |] ==> \ \ (ins ts m G, NIL) : TYPED"; by(resolve_tac [TYPED.nilI] 1); by(auto_tac(claset(),simpset() addsimps [unlimited_ins])); qed "NIL_lift_TYPED"; Goal "[| (ins ts m G, p) : TYPED ; (ins ts m H, q) : TYPED ; \ \ canaddenv G H ; m <= length (addenv G H); \ \ m <= length G ; m <= length H ; length ts = n ; unlimited ts |] ==> \ \ (ins ts m (addenv G H), PAR p q) : TYPED"; by(auto_tac (claset() addIs [TYPED.parI], simpset() addsimps [addenv_ins,canaddenv_ins])); qed "PAR_lift_TYPED"; Goal "[| unlimited G ; (ins ts m G, p) : TYPED ; m <= length G ; \ \ length ts = n ; unlimited ts |] ==> \ \ (ins ts m G, REP p) : TYPED"; by(auto_tac (claset() addIs [TYPED.repI], simpset() addsimps [unlimited_ins])); qed "REP_lift_TYPED"; Goal "[| (ts @ ins us m G, p) : TYPED ; length us = n ; unlimited us ; \ \ length ts = a ; balanced ts ; m <= length G |] ==> \ \ (ins us m G, NEW a ts p) : TYPED"; by(auto_tac (claset() addIs [TYPED.newI], simpset())); qed "NEW_lift_TYPED"; Goal "[| (ts @ ins us m G, p) : TYPED ; length us = n ; unlimited us ; \ \ length ts = a ; index x = i ; i < length G ; \ \ tag x = Neg ; \ \ canaddtypetoenv G i (LinV (| pos = Zero, neg = One (LChan ts)|)) ; \ \ m <= length G ; \ \ m <= length (addtypetoenv G i (LinV (| pos=Zero, neg= One (LChan ts)|)))|]==> \ \ (ins us m (addtypetoenv G i (LinV (| pos=Zero, neg= One (LChan ts)|))), \ \ IN (liftv m n x) a ts p) : TYPED"; by(auto_tac (claset() addIs [TYPED.linI], simpset() addsimps [liftv_def,canaddtypetoenv_ins,addtypetoenv_ins])); qed "LIN_lift_TYPED"; Goal "[| (ts @ ins us m G, p) : TYPED ; length us = n ; unlimited us ; \ \ length ts = a ; index x = i ; i < length G ; \ \ tag x = Both ; \ \ canaddtypetoenv G i (NLinV (NLChan ts)) ; \ \ m <= length G ; \ \ m <= length (addtypetoenv G i (NLinV (NLChan ts))) |]==> \ \ (ins us m (addtypetoenv G i (NLinV (NLChan ts))), \ \ IN (liftv m n x) a ts p) : TYPED"; by(auto_tac (claset() addIs [TYPED.nlinI], simpset() addsimps [liftv_def,canaddtypetoenv_ins,addtypetoenv_ins])); qed "NLIN_lift_TYPED"; Goal "[| (ins us m G, p) : TYPED; \ \ length xs = a; index x = j; tag x = Pos; map index xs = js; \ \ allless js (length G); j < length G; map tag xs = tgs; \ \ tvoccs ts tgs; length us = n ; unlimited us ; \ \ canaddtypetoenv (addtoenv G js ts) j \ \ (LinV (| pos = One (LChan ts), neg = Zero |)) ; \ \ canaddtoenv G js ts ; \ \ m <= length (addtypetoenv (addtoenv G js ts) j \ \ (LinV (| pos = One (LChan ts), neg = Zero |))) ; \ \ m <= length (addtoenv G js ts) ; \ \ m <= length G |] ==> \ \ (ins us m \ \ (addtypetoenv (addtoenv G js ts) j \ \ (LinV (| pos = One (LChan ts), neg = Zero |))), \ \ OUT (liftv m n x) a (map (liftv m n) xs) p) : TYPED"; by(auto_tac (claset(), simpset() addsimps [addtoenv_ins,addtypetoenv_ins])); by(resolve_tac [TYPED.loutI] 1); by(auto_tac (claset(), simpset() addsimps [map_index_liftv,map_tag_liftv])); by(auto_tac (claset(),simpset() addsimps [liftv_def])); by(auto_tac (claset(), simpset() addsimps [addtoenv_ins RS sym, canaddtypetoenv_ins,canaddtoenv_ins])); qed "LOUT_lift_TYPED"; Goal "[| (ins us m G, p) : TYPED; \ \ length xs = a; index x = j; tag x = Both; map index xs = js; \ \ allless js (length G); j < length G; map tag xs = tgs; \ \ tvoccs ts tgs; length us = n ; unlimited us ; \ \ canaddtypetoenv (addtoenv G js ts) j \ \ (NLinV (NLChan ts)) ; \ \ canaddtoenv G js ts ; \ \ m <= length (addtypetoenv (addtoenv G js ts) j \ \ (NLinV (NLChan ts))) ; \ \ m <= length (addtoenv G js ts) ; \ \ m <= length G |] ==> \ \ (ins us m \ \ (addtypetoenv (addtoenv G js ts) j \ \ (NLinV (NLChan ts))), \ \ OUT (liftv m n x) a (map (liftv m n) xs) p) : TYPED"; by(auto_tac (claset(), simpset() addsimps [addtoenv_ins,addtypetoenv_ins])); by(resolve_tac [TYPED.nloutI] 1); by(auto_tac (claset(), simpset() addsimps [map_index_liftv,map_tag_liftv])); by(auto_tac (claset(),simpset() addsimps [liftv_def])); by(auto_tac (claset(), simpset() addsimps [addtoenv_ins RS sym, canaddtypetoenv_ins,canaddtoenv_ins])); qed "NLOUT_lift_TYPED"; val lift_TYPED_cases = [NIL_lift_TYPED,PAR_lift_TYPED,REP_lift_TYPED, NEW_lift_TYPED,LIN_lift_TYPED,NLIN_lift_TYPED, LOUT_lift_TYPED,NLOUT_lift_TYPED]; Goalw [TYPEDREL_def] "G |- p ==> \ \ !m. (length ts = n & m <= length G & unlimited ts --> \ \ ins ts m G |- lift m n p)"; by(eresolve_tac [TYPED.induct] 1); by(ALLGOALS strip_tac); by(ALLGOALS (fn n => (REPEAT (eresolve_tac [conjE] n)))); by(ALLGOALS Simp_tac); by(ALLGOALS (fn n => (TRY (eresolve_tac [length_addenv_leq_elim] n)))); by(ALLGOALS (fn n => (TRY (assume_tac n)))); by(ALLGOALS (fn n => (resolve_tac [nth n lift_TYPED_cases] n))); by Auto_tac; qed "lift_TYPED_lemma"; Goal "[| G |- p ; length ts = n ; unlimited ts ; m <= length G |] ==> \ \ ins ts m G |- lift m n p"; by(dresolve_tac [lift_TYPED_lemma] 1); by Auto_tac; qed "lift_TYPED"; Goal "[| G |- p ; unlimited ts ; length ts = n |] ==> ts @ G |- lift 0 n p"; by(dres_inst_tac [("m","0")] lift_TYPED 1); by Auto_tac; qed "lift_TYPED_0"; Goal "[| unlimited G ; canaddenv G H ; unlimited H |] ==> \ \ (addenv G H, NIL) : TYPED"; by(auto_tac (claset() addIs [TYPED.nilI], simpset() addsimps [unlimited_addenv])); qed "NIL_addenv_TYPED"; Goal "[| (addenv G I, p) : TYPED ; (addenv H I, q) : TYPED ; \ \ canaddenv G H ; canaddenv (addenv G H) I ; \ \ canaddenv G I ; canaddenv H I ; unlimited I |] ==> \ \ (addenv (addenv G H) I, PAR p q) : TYPED"; by(auto_tac (claset() addIs [TYPED.parI], simpset() addsimps [canaddenv_unlimited_addenv RS sym,canaddenv_unlimited_canaddenv])); qed "PAR_addenv_TYPED"; Goal "[| unlimited G ; (addenv G H, p) : TYPED ; canaddenv G H ; \ \ unlimited H |] ==> \ \ (addenv G H, REP p) : TYPED"; by(auto_tac (claset() addIs [TYPED.repI], simpset() addsimps [unlimited_addenv])); qed "REP_addenv_TYPED"; Goal "[| (addenv (ts @ G) ((skeleton ts) @ H), p) : TYPED ; \ \ length ts = n ; unlimited H ; \ \ balanced ts ; canaddenv G H |] ==> \ \ (addenv G H, NEW n ts p) : TYPED"; by(resolve_tac [TYPED.newI] 1); by(asm_full_simp_tac (simpset() addsimps [addenv_append_skeleton]) 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); qed "NEW_addenv_TYPED"; Goal "[| (addenv (ts @ G) ((skeleton ts) @ H), p) : TYPED ; \ \ unlimited H ; \ \ length ts = n ; index x = i ; i < length G ; \ \ tag x = Neg ; \ \ canaddtypetoenv G i (LinV (| pos = Zero, neg = One (LChan ts)|)) ; \ \ canaddenv G H ; \ \ canaddenv (addtypetoenv G i (LinV (| pos=Zero, neg= One (LChan ts)|))) \ \ H |]==> \ \ (addenv (addtypetoenv G i (LinV (| pos=Zero, neg= One (LChan ts)|))) H, \ \ IN x n ts p) : TYPED"; by(asm_full_simp_tac (simpset() addsimps [unlimited_addtypetoenv_addenv RS sym]) 1); by(resolve_tac [TYPED.linI] 1); by(asm_full_simp_tac (simpset() addsimps [addenv_append_skeleton]) 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [unlimited_canaddtypetoenv_addenv]) 1); qed "LIN_addenv_TYPED"; Goal "[| (addenv (ts @ G) ((skeleton ts) @ H), p) : TYPED ; \ \ unlimited H ; \ \ length ts = n ; index x = i ; i < length G ; \ \ tag x = Both ; \ \ canaddtypetoenv G i (NLinV (NLChan ts)) ; \ \ canaddenv G H ; \ \ canaddenv (addtypetoenv G i (NLinV (NLChan ts))) \ \ H |]==> \ \ (addenv (addtypetoenv G i (NLinV (NLChan ts))) H, \ \ IN x n ts p) : TYPED"; by(asm_full_simp_tac (simpset() addsimps [unlimited_addtypetoenv_addenv RS sym]) 1); by(resolve_tac [TYPED.nlinI] 1); by(asm_full_simp_tac (simpset() addsimps [addenv_append_skeleton]) 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [unlimited_canaddtypetoenv_addenv]) 1); qed "NLIN_addenv_TYPED"; Goal "[| (addenv G H, p) : TYPED; \ \ length xs = n; index x = j; tag x = Pos; map index xs = js; \ \ allless js (length G); j < length G; map tag xs = tgs; \ \ tvoccs ts tgs; unlimited H ; \ \ canaddtypetoenv (addtoenv G js ts) j \ \ (LinV (| pos = One (LChan ts), neg = Zero |)) ; \ \ canaddtoenv G js ts ; \ \ canaddenv (addtypetoenv (addtoenv G js ts) j \ \ (LinV (| pos = One (LChan ts), neg = Zero |))) H ; \ \ canaddenv (addtoenv G js ts) H ; \ \ canaddenv G H |] ==> \ \ (addenv \ \ (addtypetoenv (addtoenv G js ts) j \ \ (LinV (| pos = One (LChan ts), neg = Zero |))) H, \ \ OUT x n xs p) : TYPED"; by(asm_full_simp_tac (simpset() addsimps [unlimited_addtypetoenv_addenv RS sym]) 1); by(asm_full_simp_tac (simpset() addsimps [unlimited_addtoenv_addenv RS sym]) 1); by(resolve_tac [TYPED.loutI] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [unlimited_addtoenv_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [unlimited_canaddtypetoenv_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [unlimited_canaddtoenv_addenv]) 1); qed "LOUT_addenv_TYPED"; Goal "[| (addenv G H, p) : TYPED; \ \ length xs = n; index x = j; tag x = Both; map index xs = js; \ \ allless js (length G); j < length G; map tag xs = tgs; \ \ tvoccs ts tgs; unlimited H ; \ \ canaddtypetoenv (addtoenv G js ts) j \ \ (NLinV (NLChan ts)) ; \ \ canaddtoenv G js ts ; \ \ canaddenv (addtypetoenv (addtoenv G js ts) j \ \ (NLinV (NLChan ts))) H ; \ \ canaddenv (addtoenv G js ts) H ; \ \ canaddenv G H |] ==> \ \ (addenv \ \ (addtypetoenv (addtoenv G js ts) j \ \ (NLinV (NLChan ts))) H, \ \ OUT x n xs p) : TYPED"; by(asm_full_simp_tac (simpset() addsimps [unlimited_addtypetoenv_addenv RS sym]) 1); by(asm_full_simp_tac (simpset() addsimps [unlimited_addtoenv_addenv RS sym]) 1); by(resolve_tac [TYPED.nloutI] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [unlimited_addtoenv_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [unlimited_canaddtypetoenv_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [unlimited_canaddtoenv_addenv]) 1); qed "NLOUT_addenv_TYPED"; val addenv_TYPED_cases = [NIL_addenv_TYPED,PAR_addenv_TYPED,REP_addenv_TYPED, NEW_addenv_TYPED,LIN_addenv_TYPED,NLIN_addenv_TYPED, LOUT_addenv_TYPED,NLOUT_addenv_TYPED]; Goalw [TYPEDREL_def] "G |- p ==> \ \ !H. (unlimited H & canaddenv G H --> addenv G H |- p)"; by(eresolve_tac [TYPED.induct] 1); by(ALLGOALS strip_tac); by(ALLGOALS (eresolve_tac [conjE])); by(ALLGOALS (fn n => (TRY (eresolve_tac [canaddenv_addenv_elim] n)))); by(ALLGOALS (fn n => (TRY (assume_tac n)))); by(ALLGOALS (fn n => (TRY (eresolve_tac [canaddenv_addtypetoenv_elim] n)))); by(ALLGOALS (fn n => (TRY (assume_tac n)))); by(ALLGOALS (fn n => (TRY (eresolve_tac [canaddenv_addtoenv_elim] n)))); by(ALLGOALS (fn n => (TRY (assume_tac n)))); by(ALLGOALS (fn n => (resolve_tac [nth n addenv_TYPED_cases] n))); by(auto_tac (claset(), simpset() addsimps [unlimited_skeleton,unlimited_append, canaddenv_append_skeleton])); qed "addenv_TYPED_lemma"; Goal "[| G |- p ; unlimited H ; canaddenv G H |] ==> addenv G H |- p"; by(dresolve_tac [addenv_TYPED_lemma] 1); by Auto_tac; qed "addenv_TYPED"; Goal "[| G = H ; (G , p) : TYPED |] ==> (H , p) : TYPED"; by Auto_tac; qed "TYPED_cong"; val SCONG_tac = (eresolve_tac [TYPED.elim] 1) THEN (auto_tac (claset() addIs TYPED.intrs,simpset())); val SCONG_tac = Auto_tac THEN (eresolve_tac [TYPED.elim] 1) THEN (auto_tac (claset() addIs TYPED.intrs,simpset())) THEN (eresolve_tac [TYPED.elim] 1) THEN (auto_tac (claset() addIs TYPED.intrs,simpset())); (* Cases for SCONG_TYPED *) Goal "p = q ==> ((G, p) : TYPED) = ((G, q) : TYPED)"; by Auto_tac; qed "SCONG_refl_TYPED"; Goal "[| (p, q) : SCONG ; !G. ((G, p) : TYPED) = ((G, q) : TYPED) |] \ \ ==> ((G, q) : TYPED) = ((G, p) : TYPED)"; by Auto_tac; qed "SCONG_symm_TYPED"; Goal "[| (p, q) : SCONG ; !G. ((G, p) : TYPED) = ((G, q) : TYPED) ; \ \ (q, r) : SCONG ; !G. ((G, q) : TYPED) = ((G, r) : TYPED) |] \ \ ==> ((G, p) : TYPED) = ((G, r) : TYPED) "; by Auto_tac; qed "SCONG_trans_TYPED"; Goal "((G, NIL) : TYPED) = ((G, NIL) : TYPED)"; by Auto_tac; qed "SCONG_nilC_TYPED"; Goal "[| (p1, p2) : SCONG ; !G. ((G, p1) : TYPED) = ((G, p2) : TYPED) ; \ \ (q1, q2) : SCONG ; !G. ((G, q1) : TYPED) = ((G, q2) : TYPED) |] \ \ ==> ((G, PAR p1 q1) : TYPED) = ((G, PAR p2 q2) : TYPED)"; by SCONG_tac; qed "SCONG_parC_TYPED"; Goal "[| (p, q) : SCONG ; !G. ((G, p) : TYPED) = ((G, q) : TYPED) |] \ \ ==> ((G, REP p) : TYPED) = ((G, REP q) : TYPED)"; by SCONG_tac; qed "SCONG_repC_TYPED"; Goal "[| (p, q) : SCONG ; !G. ((G, p) : TYPED) = ((G, q) : TYPED) |] \ \ ==> ((G, NEW n ts p) : TYPED) = ((G, NEW n ts q) : TYPED)"; by SCONG_tac; qed "SCONG_newC_TYPED"; Goal "[| (p, q) : SCONG ; !G. ((G, p) : TYPED) = ((G, q) : TYPED) |] \ \ ==> ((G, IN x n ts p) : TYPED) = ((G, IN x n ts q) : TYPED)"; by SCONG_tac; qed "SCONG_inC_TYPED"; Goal "[| (p, q) : SCONG ; !G. ((G, p) : TYPED) = ((G, q) : TYPED) |] \ \ ==> ((G, OUT x n xs p) : TYPED) = ((G, OUT x n xs q) : TYPED)"; by SCONG_tac; qed "SCONG_outC_TYPED"; Goal "((G, PAR p q) : TYPED) = ((G, PAR q p) : TYPED)"; by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(forward_tac [addenv_comm] 1); by(Asm_simp_tac 1); by(resolve_tac TYPED.intrs 1); by(assume_tac 1); by(assume_tac 1); by(asm_full_simp_tac (simpset() addsimps [canaddenv_sym]) 1); by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(forward_tac [addenv_comm] 1); by(Asm_simp_tac 1); by(resolve_tac TYPED.intrs 1); by(assume_tac 1); by(assume_tac 1); by(asm_full_simp_tac (simpset() addsimps [canaddenv_sym]) 1); qed "SCONG_par_comm_TYPED"; Goal "((G, PAR p (PAR q r)) : TYPED) = ((G, PAR (PAR p q) r) : TYPED)"; by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(rotate_tac 1 1); by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(forward_tac [rotate_prems 1 addenv_assoc_r] 1); by(Asm_full_simp_tac 1); by(Asm_simp_tac 1); by(resolve_tac TYPED.intrs 1); by(resolve_tac TYPED.intrs 1); by(assume_tac 1); by(assume_tac 1); by(eresolve_tac [addenv_assoc_r_canaddenv_1] 1); by(assume_tac 1); by(assume_tac 1); by(eresolve_tac [addenv_assoc_r_canaddenv_2] 1); by(assume_tac 1); by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(forward_tac [rotate_prems 1 addenv_assoc_l] 1); by(Asm_full_simp_tac 1); by(Asm_simp_tac 1); by(resolve_tac TYPED.intrs 1); by(assume_tac 1); by(resolve_tac TYPED.intrs 1); by(assume_tac 1); by(assume_tac 1); by(eresolve_tac [addenv_assoc_l_canaddenv_1] 1); by(assume_tac 1); by(eresolve_tac [addenv_assoc_l_canaddenv_2] 1); by(assume_tac 1); qed "SCONG_par_assoc_TYPED"; Goal "((G, PAR p NIL) : TYPED) = ((G, p) : TYPED)"; by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(rotate_tac 1 1); by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(eresolve_tac [rewrite_rule [TYPEDREL_def] addenv_TYPED] 1); by(assume_tac 1); by(assume_tac 1); by(resolve_tac [TYPED_cong] 1); by(resolve_tac [addenv_skeleton_id] 1); by(eresolve_tac TYPED.intrs 1); by(resolve_tac TYPED.intrs 1); by(resolve_tac [unlimited_skeleton] 1); by(resolve_tac [canaddenv_skeleton] 1); qed "SCONG_par_nil_TYPED"; Goal "((G, REP NIL) : TYPED) = ((G, NIL) : TYPED)"; by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(resolve_tac TYPED.intrs 1); by(assume_tac 1); by(eresolve_tac TYPED.intrs 1); qed "SCONG_rep_nil_TYPED"; Goal "((G, REP p) : TYPED) = ((G, PAR p (REP p)) : TYPED)"; by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(resolve_tac [TYPED_cong] 1); by(eresolve_tac [unlimited_addenv_idem] 1); by(resolve_tac TYPED.intrs 1); by(assume_tac 1); by(eresolve_tac TYPED.intrs 1); by(assume_tac 1); by(asm_full_simp_tac (simpset() addsimps [unlimited_canaddenv]) 1); by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(rotate_tac 1 1); by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(rotate_tac 3 1); by(forward_tac [rewrite_rule [TYPEDREL_def] TYPED_canaddenv_unlimited] 1); by(eresolve_tac [canaddenv_length RS sym] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [canaddenv_sym]) 1); by(Asm_full_simp_tac 1); by(resolve_tac TYPED.intrs 1); by(resolve_tac [unlimited_addenv] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(forward_tac [unlimited_canaddenv_eq] 1); by(eresolve_tac [canaddenv_sym_1] 2); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [unlimited_addenv_idem]) 1); qed "SCONG_rep_def_TYPED"; Goal "length us = m ==> \ \ ((G, NEW n ts (NEW m us p)) : TYPED) = \ \ ((G, NEW (m + n) (us @ ts) p) : TYPED)"; by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(resolve_tac TYPED.intrs 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [balanced_append]) 1); by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(resolve_tac TYPED.intrs 1); by(resolve_tac TYPED.intrs 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(eresolve_tac [balanced_append_elim_1] 1); by(Asm_full_simp_tac 1); by(eresolve_tac [balanced_append_elim_2] 1); qed "SCONG_new_merge_TYPED"; Goal "((G, NEW n ts (PAR (lift 0 n p) q)) : TYPED) = \ \ ((G,PAR p (NEW n ts q)) : TYPED)"; by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(dresolve_tac [addenv_append_ex] 1); by(assume_tac 1); by(REPEAT (eresolve_tac [exE] 1)); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(forward_tac [rewrite_rule [TYPEDREL_def] TYPED_lift_unlimited] 1); by(Asm_full_simp_tac 1); by(resolve_tac TYPED.intrs 1); by(Asm_full_simp_tac 3); by(eresolve_tac [rewrite_rule [TYPEDREL_def] TYPED_lift_0] 1); by(resolve_tac TYPED.intrs 1); by(REPEAT (eresolve_tac [conjE] 1)); by(forward_tac [unlimited_addenv_id] 1); by(assume_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(Asm_full_simp_tac 1); by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(rotate_tac 1 1); by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(resolve_tac TYPED.intrs 1); by(resolve_tac [TYPED_cong] 1); by(resolve_tac [addenv_append_skeleton_1 RS sym] 1); by(assume_tac 1); by(resolve_tac TYPED.intrs 1); by(eresolve_tac [rewrite_rule [TYPEDREL_def] lift_TYPED_0] 1); by(resolve_tac [unlimited_skeleton] 1); by(resolve_tac [length_skeleton] 1); by(assume_tac 1); by(eresolve_tac [canaddenv_sym_1 RS canaddenv_append_skeleton RS canaddenv_sym_1] 1); by Auto_tac; qed "SCONG_new_par_TYPED"; val SCONG_TYPED_cases = [SCONG_refl_TYPED,SCONG_symm_TYPED,SCONG_trans_TYPED, SCONG_nilC_TYPED,SCONG_parC_TYPED,SCONG_repC_TYPED, SCONG_newC_TYPED,SCONG_inC_TYPED,SCONG_outC_TYPED, SCONG_par_comm_TYPED,SCONG_par_assoc_TYPED,SCONG_par_nil_TYPED, SCONG_rep_nil_TYPED,SCONG_rep_def_TYPED,SCONG_new_merge_TYPED, SCONG_new_par_TYPED]; Goalw [TYPEDREL_def,SCONGREL_def] "p === q ==> !G. ((G |- p) = (G |- q))"; by(eresolve_tac [SCONG.induct] 1); by(ALLGOALS strip_tac); by(ALLGOALS (fn n => (resolve_tac [nth n SCONG_TYPED_cases] n))); by Auto_tac; qed "SCONG_TYPED"; Goal "length ts = n ==> \ \ usechan x (ts @ G) = (usechan x ts) @ (usechan (newch n x) G)"; by(exhaust_tac "x" 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [usetype_append_less,usetype_append_notless]) 1); qed "usechan_append"; Goal "length (usechan x G) = length G"; by(exhaust_tac "x" 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [length_usetype]) 1); qed "length_usechan"; Goal "balanced ts ==> balanced (usechan x ts)"; by(exhaust_tac "x" 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [balanced_usetype]) 1); qed "balanced_usechan"; Goal "newch n x = Ch y ==> x = Ch (y + n)"; by(exhaust_tac "x" 1); by Auto_tac; by(case_tac "nat < n" 1); by Auto_tac; qed "newch_Ch"; Goal "[| (G, PAR (OUT x m xs p) (IN y n ts q)) : TYPED ; \ \ index x = i |] ==> i < length G"; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by(auto_tac (claset(),simpset() addsimps [length_addenv])); qed "RED_length_comm"; Goalw [TYPEDREL_def] "(p, x, q) : RED ==> \ \ !G y. ((G |- p) & x = Ch y --> y < length G)"; by(eresolve_tac [RED.induct] 1); by(ALLGOALS strip_tac); by(ALLGOALS (fn n => REPEAT (eresolve_tac [conjE] n))); by(eresolve_tac [RED_length_comm] 1); by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(dresolve_tac [newch_Ch] 1); by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(dresolve_tac [SCONG_TYPED] 1); by(asm_full_simp_tac (simpset() addsimps [TYPEDREL_def]) 1); qed "RED_length_lemma"; Goal "[| (p, x, q) : RED ; G |- p ; x = Ch y |] ==> y < length G"; by(dresolve_tac [RED_length_lemma] 1); by Auto_tac; qed "RED_length"; Goal "[| (G, PAR (OUT x m xs p) (IN y n ts q)) : TYPED ; \ \ index x = index y ; index x = i |] \ \ ==> cmp (typeof i G)"; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(ALLGOALS (eresolve_tac [TYPED.elim])); by Auto_tac; by(asm_full_simp_tac (simpset() addsimps [typeof_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(resolve_tac [cmp_addt_pos_neg] 1); by(forward_tac [canaddenv_canaddt] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(forward_tac [canaddenv_canaddt] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(forward_tac [rotate_prems ~1 canaddt_addt_addt_2] 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddt_def]) 1); by(forward_tac [canaddenv_canaddt] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(forward_tac [rotate_prems ~1 canaddt_addt_addt_2] 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddt_def]) 1); by(rotate_tac 2 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(resolve_tac [cmp_addt] 1); by(forward_tac [canaddenv_canaddt] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(resolve_tac [cmp_fn] 1); by(resolve_tac [addt_comm] 2); by(resolve_tac [cmp_addt] 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def,canaddt_sym]) 1); by(asm_full_simp_tac (simpset() addsimps [cmp_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def,canaddt_sym]) 1); qed "RED_cmp_comm"; Goalw [TYPEDREL_def] "(p, x, q) : RED ==> \ \ !G y. ((G |- p) & x = Ch y --> cmp (typeof y G))"; by(eresolve_tac [RED.induct] 1); by(ALLGOALS strip_tac); by(ALLGOALS (fn n => REPEAT (eresolve_tac [conjE] n))); by(eresolve_tac [RED_cmp_comm] 1); by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(dresolve_tac [newch_Ch] 1); by(resolve_tac [cmp_fn] 1); by(resolve_tac [typeof_append] 2); by(Blast_tac 1); by(dresolve_tac [rewrite_rule [TYPEDREL_def] RED_length] 1); by(assume_tac 1); by(assume_tac 1); by(Asm_full_simp_tac 1); by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(dresolve_tac [rewrite_rule [TYPEDREL_def] RED_length] 1); by(assume_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addenv]) 1); by(resolve_tac [cmp_addt] 1); by(asm_full_simp_tac (simpset() addsimps [canaddenv_canaddt]) 1); by(Asm_full_simp_tac 1); by(dresolve_tac [rewrite_rule [TYPEDREL_def] SCONG_TYPED] 1); by(Asm_full_simp_tac 1); qed "RED_cmp_lemma"; Goal "[| (p, x, q) : RED ; G |- p ; x = Ch y |] ==> cmp (typeof y G)"; by(dresolve_tac [RED_cmp_lemma] 1); by Auto_tac; qed "RED_cmp"; Goal "[| balchan (newch n x) G ; length ts = n ; balanced ts ; \ \ !y. (x = Ch y --> y < length (ts @ G)) |] \ \ ==> balchan x (ts @ G)"; by(exhaust_tac "x" 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(case_tac "nat < n" 1); by(asm_full_simp_tac (simpset() addsimps [typeof_append_2]) 1); by(asm_full_simp_tac (simpset() addsimps [bal_typeof]) 1); by(Asm_full_simp_tac 1); by(resolve_tac [bal_fn] 1); by(assume_tac 1); by(cond_rewrite_left_tac (typeof_append_1 RS sym) 1); by(assume_tac 2); by(arith_tac 1); by(Asm_full_simp_tac 1); qed "balchan_append"; Goal "G = H ==> usetype x G = usetype x H"; by Auto_tac; qed "usetype_cong"; Goal "[| (G, PAR (OUT x m xs p) (IN y n ts q)) : TYPED ; \ \ index x = index y ; balchan (Ch (index x)) G |] ==> \ \ (usechan (Ch (index x)) G, \ \ PAR p (SUB q (map (%a. index a + n) xs))) : TYPED"; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(ALLGOALS (eresolve_tac [TYPED.elim])); by Auto_tac; by(rotate_tac 2 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(forward_tac [bal_addt_pos_neg] 1); by(forward_tac [canaddenv_canaddt] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(resolve_tac [rotate_prems 1 TYPED_cong] 1); by(resolve_tac TYPED.intrs 1); by(Asm_full_simp_tac 1); by(resolve_tac [rewrite_rule [TYPEDREL_def] TYPED_SUB_1] 1); by(Asm_full_simp_tac 1); by(resolve_tac [canaddenv_addtypetoenv_addtoenv_addtypetoenv_shift] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(dresolve_tac [rotate_prems 1 canaddenv_addtypetoenv_canaddenv] 1); by(Asm_full_simp_tac 1); by(dresolve_tac [rotate_prems 1 canaddenv_addtypetoenv_canaddenv_1] 1); by(Asm_full_simp_tac 1); by(resolve_tac [canaddenv_addtoenv_shift_canaddenv] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(resolve_tac [sym] 1); by(cond_rewrite_left_tac usetype_cong 1); by(resolve_tac [addenv_addtypetoenv_addtypetoenv] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(simp_tac (simpset() addsimps [addt_def,addocc_def]) 1); by(cond_rewrite_left_tac usetype_addtypetoenv 1); by(forward_tac [canaddenv_addtypetoenv_addtypetoenv_canaddenv_lemma] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [addt_def,addocc_def]) 1); by(asm_full_simp_tac (simpset() addsimps [cmp_def]) 1); by(Asm_full_simp_tac 1); by(resolve_tac [addenv_addtoenv_shift] 1); by(resolve_tac [canaddenv_addtypetoenv_addtypetoenv_canaddenv] 1); by(assume_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(forward_tac [canaddenv_addtypetoenv_addtypetoenv_canaddenv_lemma] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [canaddt_def]) 1); by(forward_tac [canaddenv_addtypetoenv_addtypetoenv_canaddenv_lemma] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [canaddt_def]) 1); by(forward_tac [canaddenv_addtypetoenv_addtypetoenv_canaddenv_lemma] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [canaddt_def]) 1); by(resolve_tac [rotate_prems 1 TYPED_cong] 1); by(resolve_tac TYPED.intrs 1); by(Asm_full_simp_tac 1); by(resolve_tac [rewrite_rule [TYPEDREL_def] TYPED_SUB_1] 1); by(Asm_full_simp_tac 1); by(resolve_tac [canaddenv_addtypetoenv_addtoenv_addtypetoenv_shift] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(dresolve_tac [rotate_prems 1 canaddenv_addtypetoenv_canaddenv] 1); by(Asm_full_simp_tac 1); by(dresolve_tac [rotate_prems 1 canaddenv_addtypetoenv_canaddenv_1] 1); by(Asm_full_simp_tac 1); by(resolve_tac [canaddenv_addtoenv_shift_canaddenv] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(resolve_tac [sym] 1); by(cond_rewrite_left_tac usetype_cong 1); by(resolve_tac [addenv_addtypetoenv_addtypetoenv] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(simp_tac (simpset() addsimps [addt_def]) 1); by(cond_rewrite_left_tac usetype_addtypetoenv 1); by(forward_tac [canaddenv_addtypetoenv_addtypetoenv_canaddenv_lemma] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [addt_def]) 1); by(asm_full_simp_tac (simpset() addsimps [cmp_def]) 1); by(Asm_full_simp_tac 1); by(resolve_tac [addenv_addtoenv_shift] 1); by(resolve_tac [canaddenv_addtypetoenv_addtypetoenv_canaddenv] 1); by(assume_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); qed "subj_red_comm"; Goalw [TYPEDREL_def] "(p, x, q) : RED ==> \ \ !G y. ((G |- p) & balchan x G --> usechan x G |- q)"; by(eresolve_tac [RED.induct] 1); by(ALLGOALS strip_tac); by(ALLGOALS (fn n => REPEAT (eresolve_tac [conjE] n))); by(resolve_tac [subj_red_comm] 1); by Auto_tac; by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(dresolve_tac [rewrite_rule [TYPEDREL_def] RED_length_lemma] 1); by(resolve_tac TYPED.intrs 1); by(asm_full_simp_tac (simpset() addsimps [usechan_append RS sym]) 1); by(dresolve_tac [balchan_append] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(strip_tac 1); by(Blast_tac 1); by(Blast_tac 1); by(asm_full_simp_tac (simpset() addsimps [length_usechan]) 1); by(asm_full_simp_tac (simpset() addsimps [balanced_usechan]) 1); by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(forward_tac [rewrite_rule [TYPEDREL_def] RED_length_lemma] 1); by(exhaust_tac "x" 1); by(Asm_full_simp_tac 1); by(resolve_tac TYPED.intrs 1); by(Blast_tac 1); by(assume_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(forward_tac [bal_fn] 1); by(resolve_tac [typeof_addenv] 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(forward_tac [rotate_prems 1 addt_cmp_bal] 1); by(resolve_tac [rewrite_rule [TYPEDREL_def] RED_cmp] 1); by(assume_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [canaddenv_canaddt]) 1); by(asm_full_simp_tac (simpset() addsimps [usetype_addenv]) 1); by(resolve_tac TYPED.intrs 1); by(Blast_tac 1); by(Asm_full_simp_tac 3); by(resolve_tac [usetype_canaddenv] 2); by(Asm_full_simp_tac 2); by(Blast_tac 2); by(forward_tac [rotate_prems 1 cmp_canaddenv_usetype_eq] 1); by(Blast_tac 1); by(resolve_tac [rewrite_rule [TYPEDREL_def] RED_cmp] 1); by(assume_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(dresolve_tac [rewrite_rule [TYPEDREL_def] SCONG_TYPED] 1); by(dresolve_tac [rewrite_rule [TYPEDREL_def] SCONG_TYPED] 1); by(Asm_full_simp_tac 1); qed "subj_red_lemma"; Goal "[| G |- p ; (p, x, q) : RED ; balchan x G |] ==> usechan x G |- q"; by(dresolve_tac [subj_red_lemma] 1); by Auto_tac; qed "subj_red_lemma_1"; Goal "!x. balanced G & x < length G --> balanced (usetype x G)"; by(induct_tac "G" 1); by Auto_tac; by(exhaust_tac "x" 1); by(auto_tac (claset(),simpset() addsimps [typeof_def,bal_skel])); QED "balanced_usetype"; Goal "[| G |- p ; (p, x, q) : RED ; balanced G |] ==> usechan x G |- q"; by(resolve_tac [subj_red_lemma_1] 1); by Auto_tac; by(exhaust_tac "x" 1); by(auto_tac (claset() addEs [bal_typeof,RED_length], simpset())); qed "subj_red"; (* Proved 5.6.2000 *) (* Now prove theorems about the lack of immediate communication errors or misuse of capabilities in well-typed processes. *) Goalw [canaddt_def,addt_def] "[| canaddt t (LinV (| pos = One a , neg = Zero |)) ; \ \ canaddt u (LinV (| pos = Zero , neg = One b |)) ; \ \ canaddt (addt t (LinV (| pos = One a , neg = Zero |))) \ \ (addt u (LinV (| pos = Zero , neg = One b |))) |] ==> \ \ ? v. (addt (addt t (LinV (| pos = One a , neg = Zero |))) \ \ (addt u (LinV (| pos = Zero , neg = One b |))) = LinV v \ \ & pos v ~= Zero & neg v ~= Zero)"; by(exhaust_tac "t" 1); by(ALLGOALS (exhaust_tac "u")); by(ALLGOALS Asm_full_simp_tac); by(record_split_tac 1); by(asm_full_simp_tac (simpset() addsimps [addocc_def]) 1); qed "addt_LinV_LinV"; Goalw [canaddt_def,addt_def] "[| canaddt t (NLinV a) ; \ \ canaddt u (NLinV b) ; \ \ canaddt (addt t (NLinV a)) \ \ (addt u (NLinV b)) |] ==> \ \ ? v. (addt (addt t (NLinV a)) \ \ (addt u (NLinV b))) = NLinV v"; by(exhaust_tac "t" 1); by(ALLGOALS (exhaust_tac "u")); by(ALLGOALS Asm_full_simp_tac); qed "addt_NLinV_NLinV"; Goalw [addt_def,canaddt_def] "[| canaddt t (addt u (NLinV v)) ; canaddt u (NLinV v) ; \ \ addt t (addt u (NLinV v)) = LinV w |] ==> False"; by(exhaust_tac "t" 1); by(ALLGOALS (exhaust_tac "u")); by Auto_tac; qed "addt_NLinV_LinV_False"; Goalw [addt_def,canaddt_def] "[| canaddt (addt t (LinV u)) v ; canaddt t (LinV u) ; pos u ~= Zero |] ==> \ \ ? w. (addt (addt t (LinV u)) v = LinV w & pos w ~= Zero)"; by(exhaust_tac "t" 1); by(ALLGOALS (exhaust_tac "v")); by(auto_tac (claset(),simpset() addsimps [addocc_def])); qed "addt_LinV_pos"; Goalw [addt_def,canaddt_def] "[| canaddt (addt t (LinV u)) v ; canaddt t (LinV u) ; neg u ~= Zero |] ==> \ \ ? w. (addt (addt t (LinV u)) v = LinV w & neg w ~= Zero)"; by(exhaust_tac "t" 1); by(ALLGOALS (exhaust_tac "v")); by(auto_tac (claset(),simpset() addsimps [addocc_def])); qed "addt_LinV_neg"; Goalw [addt_def,canaddt_def] "[| canaddt (addt t (NLinV u)) v ; canaddt t (NLinV u) |] ==> \ \ ? w. (addt (addt t (NLinV u)) v = NLinV w)"; by(exhaust_tac "t" 1); by(ALLGOALS (exhaust_tac "v")); by(auto_tac (claset(),simpset() addsimps [addocc_def])); qed "addt_NLinV"; Goal "[| (G , (PAR (OUT x m xs p) (IN y n ts q))) : TYPED ; \ \ index x = index y ; bal (typeof (index x) G) |] ==> \ \ (m = n) & \ \ ((? t. (typeof (index x) G = NLinV t)) | \ \ (? u. ((typeof (index x) G = LinV u) & (pos u ~= Zero) & (neg u ~= Zero))))"; by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(rotate_tac ~16 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addenv,typeof_addtypetoenv]) 1); by(forward_tac [bal_addt_pos_neg] 1); by(forward_tac [canaddenv_canaddt] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(Asm_full_simp_tac 1); by(resolve_tac [conjI] 1); by(dresolve_tac [tvoccs_length] 1); by(Force_tac 1); by(resolve_tac [disjI2] 1); by(resolve_tac [addt_LinV_LinV] 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(forward_tac [canaddenv_canaddt] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(forward_tac [canaddenv_canaddt] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(dresolve_tac [rotate_prems ~1 canaddt_addt_addt_2] 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddt_def]) 1); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(forward_tac [canaddenv_canaddt] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(dresolve_tac [rotate_prems ~1 canaddt_addt_addt_2] 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddt_def]) 1); by(forward_tac [canaddenv_canaddt] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(dresolve_tac [rotate_prems ~1 canaddt_addt_addt_2] 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddt_def]) 1); by(resolve_tac [conjI] 1); by(dresolve_tac [tvoccs_length] 1); by(Force_tac 1); by(resolve_tac [disjI1] 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(resolve_tac [addt_NLinV_NLinV] 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(forward_tac [canaddenv_canaddt] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); qed "TYPED_comm_safe_lemma"; Goal "[| (G , PAR (PAR (OUT x m xs p) (IN y n ts q)) r) : TYPED ; \ \ index x = index y ; bal (typeof (index x) G) |] ==> \ \ (m = n) & \ \ ((? t. (typeof (index x) G = NLinV t)) | \ \ (? u. ((typeof (index x) G = LinV u) & (pos u ~= Zero) & (neg u ~= Zero))))"; by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(dresolve_tac [bal_fn] 1); by(resolve_tac [typeof_addenv] 1); by(Asm_full_simp_tac 1); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(rotate_tac ~2 1); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(forward_tac [canaddenv_length] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(forward_tac [canaddenv_length] 1); by(Asm_full_simp_tac 1); by(forward_tac [rotate_prems 1 RED_cmp_comm] 1); by(Asm_full_simp_tac 1); by(Force_tac 1); by(forward_tac [rotate_prems 1 addt_cmp_bal] 1); by(Asm_full_simp_tac 1); by(forward_tac [canaddenv_canaddt] 1); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(rotate_tac ~2 1); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(forward_tac [canaddenv_length] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(forward_tac [canaddenv_length] 1); by(Asm_full_simp_tac 1); by(forward_tac [rotate_prems ~2 TYPED_comm_safe_lemma] 1); by(Asm_full_simp_tac 1); by(Force_tac 1); by(resolve_tac [conjI] 1); by(Asm_full_simp_tac 1); by(REPEAT (eresolve_tac [conjE] 1)); by(eresolve_tac [disjE] 1); by(eresolve_tac [exE] 1); by(resolve_tac [disjI1] 1); by(resolve_tac [exI] 1); by(cond_rewrite_left_tac typeof_addenv 1); by(Asm_full_simp_tac 1); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(rotate_tac ~2 1); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(forward_tac [canaddenv_length] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(forward_tac [canaddenv_length] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [addt_def]) 1); by(eresolve_tac [exE] 1); by(resolve_tac [disjI2] 1); by(resolve_tac [exI] 1); by(resolve_tac [conjI] 1); by(cond_rewrite_left_tac typeof_addenv 1); by(Asm_full_simp_tac 1); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(rotate_tac ~2 1); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(forward_tac [canaddenv_length] 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [length_addenv]) 1); by(forward_tac [canaddenv_length] 1); by(Asm_full_simp_tac 1); by(resolve_tac [cmp_addt_eq] 1); by(Asm_full_simp_tac 2); by(Asm_full_simp_tac 2); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(rotate_tac ~2 1); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(dres_inst_tac [("xa","H"),("x","i")] canaddenv_canaddt 1); by(asm_full_simp_tac (simpset() addsimps [length_addenv_2]) 1); by(Asm_full_simp_tac 1); by(forward_tac [canaddenv_length] 1); by(Asm_full_simp_tac 1); by(rotate_tac ~4 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(REPEAT (eresolve_tac [conjE] 1)); by(forward_tac [rotate_prems ~1 addt_NLinV_LinV_False] 1); by(dres_inst_tac [("x","i")] canaddenv_canaddt 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by Auto_tac; qed "TYPED_comm_safe"; Goal "[| (G , PAR (OUT x m xs p) q) : TYPED ; \ \ bal (typeof (index x) G) |] ==> \ \ ((? t. (typeof (index x) G = NLinV t)) | \ \ (? u. ((typeof (index x) G = LinV u) & (pos u ~= Zero))))"; by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(resolve_tac [disjI2] 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(resolve_tac [addt_LinV_pos] 1); by(dres_inst_tac [("x","j")] canaddenv_canaddt 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(Asm_full_simp_tac 1); by(resolve_tac [disjI1] 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(resolve_tac [addt_NLinV] 1); by(dres_inst_tac [("x","j")] canaddenv_canaddt 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); qed "TYPED_out_safe"; Goal "[| (G , PAR (IN x n ts p) q) : TYPED ; \ \ bal (typeof (index x) G) |] ==> \ \ ((? t. (typeof (index x) G = NLinV t)) | \ \ (? u. ((typeof (index x) G = LinV u) & (neg u ~= Zero))))"; by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(resolve_tac [disjI2] 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(resolve_tac [addt_LinV_neg] 1); by(dres_inst_tac [("x","i")] canaddenv_canaddt 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(Asm_full_simp_tac 1); by(resolve_tac [disjI1] 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(resolve_tac [addt_NLinV] 1); by(dres_inst_tac [("x","i")] canaddenv_canaddt 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); qed "TYPED_in_safe"; Goal "[| (G , PAR (OUT x m xs p) (OUT x n ys q)) : TYPED ; \ \ bal (typeof (index x) G) |] ==> \ \ (? t. (typeof (index x) G = NLinV t))"; by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(dres_inst_tac [("x","index x")] canaddenv_canaddt 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(dresolve_tac [rotate_prems ~1 canaddt_addt_addt_2] 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddt_def]) 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(resolve_tac [addt_NLinV] 1); by(dres_inst_tac [("x","index x")] canaddenv_canaddt 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); qed "TYPED_out_out_safe"; Goal "[| (G , PAR (IN x m ts p) (IN x n us q)) : TYPED ; \ \ bal (typeof (index x) G) |] ==> \ \ (? t. (typeof (index x) G = NLinV t))"; by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(eresolve_tac [TYPED.elim] 1); by(ALLGOALS Asm_full_simp_tac); by(eresolve_tac [TYPED.elim] 1); by Auto_tac; by(dres_inst_tac [("x","index x")] canaddenv_canaddt 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(dresolve_tac [rotate_prems ~1 canaddt_addt_addt_2] 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddt_def]) 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addenv]) 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(resolve_tac [addt_NLinV] 1); by(dres_inst_tac [("x","index x")] canaddenv_canaddt 1); by(Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [typeof_addtypetoenv]) 1); by(asm_full_simp_tac (simpset() addsimps [canaddtypetoenv_def]) 1); qed "TYPED_in_in_safe";