equal
deleted
inserted
replaced
4 |
4 |
5 signature MIR_TAC = |
5 signature MIR_TAC = |
6 sig |
6 sig |
7 val trace: bool Unsynchronized.ref |
7 val trace: bool Unsynchronized.ref |
8 val mir_tac: Proof.context -> bool -> int -> tactic |
8 val mir_tac: Proof.context -> bool -> int -> tactic |
9 val setup: theory -> theory |
|
10 end |
9 end |
11 |
10 |
12 structure Mir_Tac = |
11 structure Mir_Tac = |
13 struct |
12 struct |
14 |
13 |
141 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) |
140 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) |
142 end |
141 end |
143 | _ => (pre_thm, assm_tac i) |
142 | _ => (pre_thm, assm_tac i) |
144 in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end); |
143 in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end); |
145 |
144 |
146 val setup = |
|
147 Method.setup @{binding mir} |
|
148 let |
|
149 val parse_flag = Args.$$$ "no_quantify" >> K (K false) |
|
150 in |
|
151 Scan.lift (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >> |
|
152 curry (Library.foldl op |>) true) >> |
|
153 (fn q => fn ctxt => SIMPLE_METHOD' (mir_tac ctxt q)) |
|
154 end |
|
155 "decision procedure for MIR arithmetic"; |
|
156 |
|
157 end |
145 end |