1open HolKernel boolLib bossLib Parse stringTheory ramanaLib bagTheory commonUnifTheory;
2
3val _ = new_theory "term";
4
5val _ = Hol_datatype`
6  term = Var of num
7       | Pair of term => term
8       | Const of 'a`;
9
10val pair_count_def = RWDefine`
11(pair_count (Var v) = 0) /\
12(pair_count (Const c) = 0) /\
13(pair_count (Pair t1 t2) = 1 + pair_count t1 + pair_count t2)`;
14
15val vars_def = RWDefine`
16  (vars (Var x) = {x}) /\
17  (vars (Pair t1 t2) = vars t1 UNION vars t2) /\
18  (vars (Const _) = {})`;
19
20val FINITE_vars = RWstore_thm(
21"FINITE_vars",
22`FINITE (vars t)`,
23Induct_on `t` THEN SRW_TAC [][]);
24
25val varb_def = RWDefine`
26  (varb (Var s) = {| s |}) /\
27  (varb (Pair t1 t2) = BAG_UNION (varb t1) (varb t2)) /\
28  (varb (Const c) = {||})`;
29
30val FINITE_varb = RWstore_thm(
31  "FINITE_varb",
32  `FINITE_BAG (varb t)`,
33  Induct_on `t` THEN SRW_TAC [][]);
34
35val IN_varb_vars = RWstore_thm(
36  "IN_varb_vars",
37  `BAG_IN e (varb t) <=> e IN vars t`,
38  Induct_on `t` THEN SRW_TAC [][]);
39
40val _ = export_theory ();
41