equal
deleted
inserted
replaced
1 (* Title: HOL/Decision_Procs/mir_tac.ML |
1 (* Title: HOL/Decision_Procs/mir_tac.ML |
2 Author: Amine Chaieb, TU Muenchen |
2 Author: Amine Chaieb, TU Muenchen |
3 *) |
3 *) |
|
4 |
|
5 signature MIR_TAC = |
|
6 sig |
|
7 val trace: bool ref |
|
8 val mir_tac: Proof.context -> bool -> int -> tactic |
|
9 val setup: theory -> theory |
|
10 end |
4 |
11 |
5 structure Mir_Tac = |
12 structure Mir_Tac = |
6 struct |
13 struct |
7 |
14 |
8 val trace = ref false; |
15 val trace = ref false; |
80 (* object implication to meta---*) |
87 (* object implication to meta---*) |
81 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp; |
88 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp; |
82 |
89 |
83 |
90 |
84 fun mir_tac ctxt q i = |
91 fun mir_tac ctxt q i = |
85 (ObjectLogic.atomize_prems_tac i) |
92 ObjectLogic.atomize_prems_tac i |
86 THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i) |
93 THEN simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i |
87 THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i)) |
94 THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i) |
88 THEN (fn st => |
95 THEN (fn st => |
89 let |
96 let |
90 val g = List.nth (prems_of st, i - 1) |
97 val g = List.nth (prems_of st, i - 1) |
91 val thy = ProofContext.theory_of ctxt |
98 val thy = ProofContext.theory_of ctxt |
92 (* Transform the term*) |
99 (* Transform the term*) |
141 | _ => (pre_thm, assm_tac i) |
148 | _ => (pre_thm, assm_tac i) |
142 in (rtac (((mp_step nh) o (spec_step np)) th) i |
149 in (rtac (((mp_step nh) o (spec_step np)) th) i |
143 THEN tac) st |
150 THEN tac) st |
144 end handle Subscript => no_tac st); |
151 end handle Subscript => no_tac st); |
145 |
152 |
146 fun mir_args meth = |
|
147 let val parse_flag = |
|
148 Args.$$$ "no_quantify" >> (K (K false)); |
|
149 in |
|
150 Method.simple_args |
|
151 (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >> |
|
152 curry (Library.foldl op |>) true) |
|
153 (fn q => fn ctxt => meth ctxt q) |
|
154 end; |
|
155 |
|
156 fun mir_method ctxt q = SIMPLE_METHOD' (mir_tac ctxt q); |
|
157 |
|
158 val setup = |
153 val setup = |
159 Method.add_method ("mir", |
154 Method.setup @{binding mir} |
160 mir_args mir_method, |
155 let |
161 "decision procedure for MIR arithmetic"); |
156 val parse_flag = Args.$$$ "no_quantify" >> K (K false) |
162 |
157 in |
|
158 Scan.lift (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >> |
|
159 curry (Library.foldl op |>) true) >> |
|
160 (fn q => fn ctxt => SIMPLE_METHOD' (mir_tac ctxt q)) |
|
161 end |
|
162 "decision procedure for MIR arithmetic"; |
163 |
163 |
164 end |
164 end |