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