14 of Free(xn,xT) => (case AList.lookup (op aconv) vs t |
14 of Free(xn,xT) => (case AList.lookup (op aconv) vs t |
15 of NONE => error "Variable not found in the list!" |
15 of NONE => error "Variable not found in the list!" |
16 | SOME n => Bound n) |
16 | SOME n => Bound n) |
17 | @{term "0::int"} => C 0 |
17 | @{term "0::int"} => C 0 |
18 | @{term "1::int"} => C 1 |
18 | @{term "1::int"} => C 1 |
19 | Term.Bound i => Bound (nat i) |
19 | Term.Bound i => Bound 0 |
20 | Const(@{const_name "HOL.uminus"},_)$t' => Neg (i_of_term vs t') |
20 | Const(@{const_name "HOL.uminus"},_)$t' => Neg (i_of_term vs t') |
21 | Const(@{const_name "HOL.plus"},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2) |
21 | Const(@{const_name "HOL.plus"},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2) |
22 | Const(@{const_name "HOL.minus"},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2) |
22 | Const(@{const_name "HOL.minus"},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2) |
23 | Const(@{const_name "HOL.times"},_)$t1$t2 => (Mul (HOLogic.dest_number t1 |> snd,i_of_term vs t2) |
23 | Const(@{const_name "HOL.times"},_)$t1$t2 => (Mul (HOLogic.dest_number t1 |> snd,i_of_term vs t2) |
24 handle TERM _ => |
24 handle TERM _ => |
40 | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2) |
40 | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2) |
41 | Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2) |
41 | Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2) |
42 | Const("Not",_)$t' => Not(qf_of_term ps vs t') |
42 | Const("Not",_)$t' => Not(qf_of_term ps vs t') |
43 | Const("Ex",_)$Abs(xn,xT,p) => |
43 | Const("Ex",_)$Abs(xn,xT,p) => |
44 let val (xn',p') = variant_abs (xn,xT,p) |
44 let val (xn',p') = variant_abs (xn,xT,p) |
45 val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs) |
45 val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1 + n)) vs) |
46 in E (qf_of_term ps vs' p') |
46 in E (qf_of_term ps vs' p') |
47 end |
47 end |
48 | Const("All",_)$Abs(xn,xT,p) => |
48 | Const("All",_)$Abs(xn,xT,p) => |
49 let val (xn',p') = variant_abs (xn,xT,p) |
49 let val (xn',p') = variant_abs (xn,xT,p) |
50 val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs) |
50 val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1 + n)) vs) |
51 in A (qf_of_term ps vs' p') |
51 in A (qf_of_term ps vs' p') |
52 end |
52 end |
53 | _ =>(case AList.lookup (op aconv) ps t of |
53 | _ =>(case AList.lookup (op aconv) ps t of |
54 NONE => error "qf_of_term ps : unknown term!" |
54 NONE => error "qf_of_term ps : unknown term!" |
55 | SOME n => Closed n); |
55 | SOME n => Closed n); |
75 fun start_vs t = |
75 fun start_vs t = |
76 let |
76 let |
77 val fs = term_frees t |
77 val fs = term_frees t |
78 val ps = term_bools [] t |
78 val ps = term_bools [] t |
79 in |
79 in |
80 (fs ~~ (map nat (0 upto (length fs - 1))), |
80 (fs ~~ (0 upto (length fs - 1)), ps ~~ (0 upto (length ps - 1))) |
81 ps ~~ (map nat (0 upto (length ps - 1)))) |
|
82 end; |
81 end; |
83 |
82 |
84 fun term_of_i vs t = case t |
83 fun term_of_i vs t = case t |
85 of C i => HOLogic.mk_number HOLogic.intT i |
84 of C i => HOLogic.mk_number HOLogic.intT i |
86 | Bound n => (fst o the) (find_first (fn (_, m) => m = n) vs) |
85 | Bound n => (fst o the) (find_first (fn (_, m) => m = n) vs) |