10 open UTerm; |
10 open UTerm; |
11 |
11 |
12 |
12 |
13 (**** vars_of lemmas ****) |
13 (**** vars_of lemmas ****) |
14 |
14 |
15 goal UTerm.thy "(v : vars_of(Var(w))) = (w=v)"; |
15 Goal "(v : vars_of(Var(w))) = (w=v)"; |
16 by (Simp_tac 1); |
16 by (Simp_tac 1); |
17 by (fast_tac HOL_cs 1); |
17 by (fast_tac HOL_cs 1); |
18 qed "vars_var_iff"; |
18 qed "vars_var_iff"; |
19 |
19 |
20 goal UTerm.thy "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)"; |
20 Goal "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)"; |
21 by (induct_tac "t" 1); |
21 by (induct_tac "t" 1); |
22 by (ALLGOALS Simp_tac); |
22 by (ALLGOALS Simp_tac); |
23 by (fast_tac HOL_cs 1); |
23 by (fast_tac HOL_cs 1); |
24 qed "vars_iff_occseq"; |
24 qed "vars_iff_occseq"; |
25 |
25 |
26 |
26 |
27 (* Not used, but perhaps useful in other proofs *) |
27 (* Not used, but perhaps useful in other proofs *) |
28 goal UTerm.thy "M<:N --> vars_of(M) <= vars_of(N)"; |
28 Goal "M<:N --> vars_of(M) <= vars_of(N)"; |
29 by (induct_tac "N" 1); |
29 by (induct_tac "N" 1); |
30 by (ALLGOALS Asm_simp_tac); |
30 by (ALLGOALS Asm_simp_tac); |
31 by (fast_tac set_cs 1); |
31 by (fast_tac set_cs 1); |
32 val occs_vars_subset = result(); |
32 val occs_vars_subset = result(); |
33 |
33 |
34 |
34 |
35 goal UTerm.thy "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)"; |
35 Goal "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)"; |
36 by (Blast_tac 1); |
36 by (Blast_tac 1); |
37 val monotone_vars_of = result(); |
37 val monotone_vars_of = result(); |
38 |
38 |
39 goal UTerm.thy "finite(vars_of M)"; |
39 Goal "finite(vars_of M)"; |
40 by (induct_tac"M" 1); |
40 by (induct_tac"M" 1); |
41 by (ALLGOALS Simp_tac); |
41 by (ALLGOALS Simp_tac); |
42 by (forward_tac [finite_UnI] 1); |
42 by (forward_tac [finite_UnI] 1); |
43 by (assume_tac 1); |
43 by (assume_tac 1); |
44 by (Asm_simp_tac 1); |
44 by (Asm_simp_tac 1); |