equal
deleted
inserted
replaced
15 |
15 |
16 |
16 |
17 subsection {* Properties of @{text IT} *} |
17 subsection {* Properties of @{text IT} *} |
18 |
18 |
19 lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> lift t i \<in> IT" |
19 lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> lift t i \<in> IT" |
20 apply (induct fixing: i set: IT) |
20 apply (induct arbitrary: i set: IT) |
21 apply (simp (no_asm)) |
21 apply (simp (no_asm)) |
22 apply (rule conjI) |
22 apply (rule conjI) |
23 apply |
23 apply |
24 (rule impI, |
24 (rule impI, |
25 rule IT.Var, |
25 rule IT.Var, |
36 |
36 |
37 lemma lifts_IT: "ts \<in> lists IT \<Longrightarrow> map (\<lambda>t. lift t 0) ts \<in> lists IT" |
37 lemma lifts_IT: "ts \<in> lists IT \<Longrightarrow> map (\<lambda>t. lift t 0) ts \<in> lists IT" |
38 by (induct ts) auto |
38 by (induct ts) auto |
39 |
39 |
40 lemma subst_Var_IT: "r \<in> IT \<Longrightarrow> r[Var i/j] \<in> IT" |
40 lemma subst_Var_IT: "r \<in> IT \<Longrightarrow> r[Var i/j] \<in> IT" |
41 apply (induct fixing: i j set: IT) |
41 apply (induct arbitrary: i j set: IT) |
42 txt {* Case @{term Var}: *} |
42 txt {* Case @{term Var}: *} |
43 apply (simp (no_asm) add: subst_Var) |
43 apply (simp (no_asm) add: subst_Var) |
44 apply |
44 apply |
45 ((rule conjI impI)+, |
45 ((rule conjI impI)+, |
46 rule IT.Var, |
46 rule IT.Var, |