diff -r 9321f7b70450 -r 6ee87f67d9cd src/Tools/intuitionistic.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/intuitionistic.ML Sat Feb 28 14:52:21 2009 +0100 @@ -0,0 +1,100 @@ +(* Title: Tools/intuitionistic.ML + Author: Stefan Berghofer, TU Muenchen + +Simple intuitionistic proof search. +*) + +signature INTUITIONISTIC = +sig + val prover_tac: Proof.context -> int option -> int -> tactic + val method_setup: bstring -> theory -> theory +end; + +structure Intuitionistic: INTUITIONISTIC = +struct + +(* main tactic *) + +local + +val remdups_tac = SUBGOAL (fn (g, i) => + let val prems = Logic.strip_assums_hyp g in + REPEAT_DETERM_N (length prems - length (distinct op aconv prems)) + (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i) + end); + +fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac; + +val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist; + +fun safe_step_tac ctxt = + ContextRules.Swrap ctxt + (eq_assume_tac ORELSE' + bires_tac true (ContextRules.netpair_bang ctxt)); + +fun unsafe_step_tac ctxt = + ContextRules.wrap ctxt + (assume_tac APPEND' + bires_tac false (ContextRules.netpair_bang ctxt) APPEND' + bires_tac false (ContextRules.netpair ctxt)); + +fun step_tac ctxt i = + REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE + REMDUPS (unsafe_step_tac ctxt) i; + +fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) => if d > lim then no_tac else + let + val ps = Logic.strip_assums_hyp g; + val c = Logic.strip_assums_concl g; + in + if member (fn ((ps1, c1), (ps2, c2)) => + c1 aconv c2 andalso + length ps1 = length ps2 andalso + gen_eq_set (op aconv) (ps1, ps2)) gs (ps, c) then no_tac + else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i + end); + +in + +fun prover_tac ctxt opt_lim = + SELECT_GOAL (DEEPEN (2, the_default 20 opt_lim) (intprover_tac ctxt [] 0) 4 1); + +end; + + +(* method setup *) + +local + +val introN = "intro"; +val elimN = "elim"; +val destN = "dest"; +val ruleN = "rule"; + +fun modifier name kind kind' att = + Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME) + >> (pair (I: Proof.context -> Proof.context) o att); + +val modifiers = + [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang, + modifier destN Args.colon (Scan.succeed ()) ContextRules.dest, + modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang, + modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim, + modifier introN Args.bang_colon Args.bang ContextRules.intro_bang, + modifier introN Args.colon (Scan.succeed ()) ContextRules.intro, + Args.del -- Args.colon >> K (I, ContextRules.rule_del)]; + +val method = + Method.bang_sectioned_args' modifiers (Scan.lift (Scan.option OuterParse.nat)) + (fn n => fn prems => fn ctxt => Method.METHOD (fn facts => + HEADGOAL (Method.insert_tac (prems @ facts) THEN' + ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n))); + +in + +fun method_setup name = Method.add_method (name, method, "intuitionistic proof search"); + +end; + +end; +