42 (* pseudo reification : term -> fm *) |
42 (* pseudo reification : term -> fm *) |
43 fun fm_of_term vs t = |
43 fun fm_of_term vs t = |
44 case t of |
44 case t of |
45 Const("True",_) => T |
45 Const("True",_) => T |
46 | Const("False",_) => F |
46 | Const("False",_) => F |
47 | Const(@{const_name HOL.less},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2)) |
47 | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (num_of_term vs t1,num_of_term vs t2)) |
48 | Const(@{const_name HOL.less_eq},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2)) |
48 | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub (num_of_term vs t1,num_of_term vs t2)) |
49 | Const("op =",eqT)$t1$t2 => |
49 | Const("op =",eqT)$t1$t2 => |
50 if (domain_type eqT = rT) |
50 if (domain_type eqT = rT) |
51 then Eqa (Sub (num_of_term vs t1,num_of_term vs t2)) |
51 then Eq (Sub (num_of_term vs t1,num_of_term vs t2)) |
52 else Iffa(fm_of_term vs t1,fm_of_term vs t2) |
52 else Iff(fm_of_term vs t1,fm_of_term vs t2) |
53 | Const("op &",_)$t1$t2 => And(fm_of_term vs t1,fm_of_term vs t2) |
53 | Const("op &",_)$t1$t2 => And(fm_of_term vs t1,fm_of_term vs t2) |
54 | Const("op |",_)$t1$t2 => Or(fm_of_term vs t1,fm_of_term vs t2) |
54 | Const("op |",_)$t1$t2 => Or(fm_of_term vs t1,fm_of_term vs t2) |
55 | Const("op -->",_)$t1$t2 => Impa(fm_of_term vs t1,fm_of_term vs t2) |
55 | Const("op -->",_)$t1$t2 => Imp(fm_of_term vs t1,fm_of_term vs t2) |
56 | Const("Not",_)$t' => Nota(fm_of_term vs t') |
56 | Const("Not",_)$t' => Not(fm_of_term vs t') |
57 | Const("Ex",_)$Term.Abs(xn,xT,p) => |
57 | Const("Ex",_)$Term.Abs(xn,xT,p) => |
58 E(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p) |
58 E(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p) |
59 | Const("All",_)$Term.Abs(xn,xT,p) => |
59 | Const("All",_)$Term.Abs(xn,xT,p) => |
60 A(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p) |
60 A(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p) |
61 | _ => error ("fm_of_term : unknown term!" ^ (Display.raw_string_of_term t)); |
61 | _ => error ("fm_of_term : unknown term!" ^ (Display.raw_string_of_term t)); |
89 |
89 |
90 fun term_of_fm vs t = |
90 fun term_of_fm vs t = |
91 case t of |
91 case t of |
92 T => HOLogic.true_const |
92 T => HOLogic.true_const |
93 | F => HOLogic.false_const |
93 | F => HOLogic.false_const |
94 | Lta t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$ |
94 | Lt t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$ |
95 (term_of_num vs t)$ rzero |
95 (term_of_num vs t)$ rzero |
96 | Lea t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$ |
96 | Le t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$ |
97 (term_of_num vs t)$ rzero |
97 (term_of_num vs t)$ rzero |
98 | Gta t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$ |
98 | Gt t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$ |
99 rzero $(term_of_num vs t) |
99 rzero $(term_of_num vs t) |
100 | Gea t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$ |
100 | Ge t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$ |
101 rzero $(term_of_num vs t) |
101 rzero $(term_of_num vs t) |
102 | Eqa t => Const("op =",[rT,rT] ---> bT)$ |
102 | Eq t => Const("op =",[rT,rT] ---> bT)$ |
103 (term_of_num vs t)$ rzero |
103 (term_of_num vs t)$ rzero |
104 | NEq t => term_of_fm vs (Nota (Eqa t)) |
104 | NEq t => term_of_fm vs (Not (Eq t)) |
105 | Nota t' => HOLogic.Not$(term_of_fm vs t') |
105 | Not t' => HOLogic.Not$(term_of_fm vs t') |
106 | And(t1,t2) => HOLogic.conj$(term_of_fm vs t1)$(term_of_fm vs t2) |
106 | And(t1,t2) => HOLogic.conj$(term_of_fm vs t1)$(term_of_fm vs t2) |
107 | Or(t1,t2) => HOLogic.disj$(term_of_fm vs t1)$(term_of_fm vs t2) |
107 | Or(t1,t2) => HOLogic.disj$(term_of_fm vs t1)$(term_of_fm vs t2) |
108 | Impa(t1,t2) => HOLogic.imp$(term_of_fm vs t1)$(term_of_fm vs t2) |
108 | Imp(t1,t2) => HOLogic.imp$(term_of_fm vs t1)$(term_of_fm vs t2) |
109 | Iffa(t1,t2) => (HOLogic.eq_const bT)$(term_of_fm vs t1)$ |
109 | Iff(t1,t2) => (HOLogic.eq_const bT)$(term_of_fm vs t1)$ |
110 (term_of_fm vs t2) |
110 (term_of_fm vs t2) |
111 | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!"; |
111 | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!"; |
112 |
112 |
113 (* The oracle *) |
113 (* The oracle *) |
114 |
114 |