40 (* pseudo reification : term -> fm *) |
40 (* pseudo reification : term -> fm *) |
41 fun fm_of_term vs t = |
41 fun fm_of_term vs t = |
42 case t of |
42 case t of |
43 Const("True",_) => T |
43 Const("True",_) => T |
44 | Const("False",_) => F |
44 | Const("False",_) => F |
45 | Const(@{const_name HOL.less},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2)) |
45 | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (num_of_term vs t1,num_of_term vs t2)) |
46 | Const(@{const_name HOL.less_eq},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2)) |
46 | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub (num_of_term vs t1,num_of_term vs t2)) |
47 | Const (@{const_name "MIR.rdvd"},_ )$ (Const("RealDef.real",_) $ (Const(@{const_name "Numeral.number_of"},_)$t1))$t2 => |
47 | Const (@{const_name "MIR.rdvd"},_ )$ (Const("RealDef.real",_) $ (Const(@{const_name "Numeral.number_of"},_)$t1))$t2 => |
48 Dvda (HOLogic.dest_numeral t1, num_of_term vs t2) |
48 Dvd (HOLogic.dest_numeral t1, num_of_term vs t2) |
49 | Const("op =",eqT)$t1$t2 => |
49 | Const("op =",eqT)$t1$t2 => |
50 if (domain_type eqT = @{typ real}) |
50 if (domain_type eqT = @{typ real}) |
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",_)$Abs(xn,xT,p) => |
57 | Const("Ex",_)$Abs(xn,xT,p) => |
58 E (fm_of_term (map (fn (v, n) => (v, Suc n)) vs) p) |
58 E (fm_of_term (map (fn (v, n) => (v, Suc n)) vs) p) |
59 | Const("All",_)$Abs(xn,xT,p) => |
59 | Const("All",_)$Abs(xn,xT,p) => |
60 A (fm_of_term (map (fn(v, n) => (v, Suc n)) vs) p) |
60 A (fm_of_term (map (fn(v, n) => (v, Suc 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); |
91 |
91 |
92 fun term_of_fm vs t = |
92 fun term_of_fm vs t = |
93 case t of |
93 case t of |
94 T => HOLogic.true_const |
94 T => HOLogic.true_const |
95 | F => HOLogic.false_const |
95 | F => HOLogic.false_const |
96 | Lta t => @{term "op <:: real => _"} $ term_of_num vs t $ rzero |
96 | Lt t => @{term "op <:: real => _"} $ term_of_num vs t $ rzero |
97 | Lea t => @{term "op <=:: real => _"} $ term_of_num vs t $ rzero |
97 | Le t => @{term "op <=:: real => _"} $ term_of_num vs t $ rzero |
98 | Gta t => @{term "op <:: real => _"}$ rzero $ term_of_num vs t |
98 | Gt t => @{term "op <:: real => _"}$ rzero $ term_of_num vs t |
99 | Gea t => @{term "op <=:: real => _"} $ rzero $ term_of_num vs t |
99 | Ge t => @{term "op <=:: real => _"} $ rzero $ term_of_num vs t |
100 | Eqa t => @{term "op = :: real => _"}$ term_of_num vs t $ rzero |
100 | Eq t => @{term "op = :: real => _"}$ term_of_num vs t $ rzero |
101 | NEq t => term_of_fm vs (Nota (Eqa t)) |
101 | NEq t => term_of_fm vs (Not (Eq t)) |
102 | NDvd (i,t) => term_of_fm vs (Nota (Dvda (i,t))) |
102 | NDvd (i,t) => term_of_fm vs (Not (Dvd (i,t))) |
103 | Dvda (i,t) => @{term "op rdvd"} $ term_of_num vs (C i) $ term_of_num vs t |
103 | Dvd (i,t) => @{term "op rdvd"} $ term_of_num vs (C i) $ term_of_num vs t |
104 | Nota t' => HOLogic.Not$(term_of_fm vs t') |
104 | Not t' => HOLogic.Not$(term_of_fm vs t') |
105 | And(t1,t2) => HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2 |
105 | And(t1,t2) => HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2 |
106 | Or(t1,t2) => HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2 |
106 | Or(t1,t2) => HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2 |
107 | Impa(t1,t2) => HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2 |
107 | Imp(t1,t2) => HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2 |
108 | Iffa(t1,t2) => HOLogic.mk_eq (term_of_fm vs t1, term_of_fm vs t2) |
108 | Iff(t1,t2) => HOLogic.mk_eq (term_of_fm vs t1, term_of_fm vs t2) |
109 | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!"; |
109 | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!"; |
110 |
110 |
111 (* The oracle *) |
111 (* The oracle *) |
112 |
112 |
113 fun mircfr_oracle thy t = |
113 fun mircfr_oracle thy t = |