--- a/src/FOL/IFOL.thy Sat Feb 28 14:42:54 2009 +0100
+++ b/src/FOL/IFOL.thy Sat Feb 28 14:52:21 2009 +0100
@@ -15,6 +15,7 @@
"~~/src/Tools/IsaPlanner/rw_inst.ML"
"~~/src/Tools/eqsubst.ML"
"~~/src/Provers/quantifier1.ML"
+ "~~/src/Tools/intuitionistic.ML"
"~~/src/Tools/project_rule.ML"
"~~/src/Tools/atomize_elim.ML"
("fologic.ML")
@@ -609,6 +610,8 @@
subsection {* Intuitionistic Reasoning *}
+setup {* Intuitionistic.method_setup "iprover" *}
+
lemma impE':
assumes 1: "P --> Q"
and 2: "Q ==> R"
--- a/src/FOL/IsaMakefile Sat Feb 28 14:42:54 2009 +0100
+++ b/src/FOL/IsaMakefile Sat Feb 28 14:52:21 2009 +0100
@@ -34,10 +34,11 @@
$(SRC)/Tools/IsaPlanner/rw_tools.ML \
$(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \
$(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \
- $(SRC)/Tools/atomize_elim.ML $(SRC)/Tools/project_rule.ML \
- $(SRC)/Provers/quantifier1.ML $(SRC)/Provers/splitter.ML FOL.thy \
- IFOL.thy ROOT.ML blastdata.ML cladata.ML document/root.tex \
- fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
+ $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \
+ $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML \
+ $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML blastdata.ML \
+ cladata.ML document/root.tex fologic.ML hypsubstdata.ML intprover.ML \
+ simpdata.ML
@$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL
--- a/src/HOL/HOL.thy Sat Feb 28 14:42:54 2009 +0100
+++ b/src/HOL/HOL.thy Sat Feb 28 14:52:21 2009 +0100
@@ -12,6 +12,7 @@
"~~/src/Tools/IsaPlanner/isand.ML"
"~~/src/Tools/IsaPlanner/rw_tools.ML"
"~~/src/Tools/IsaPlanner/rw_inst.ML"
+ "~~/src/Tools/intuitionistic.ML"
"~~/src/Tools/project_rule.ML"
"~~/src/Provers/hypsubst.ML"
"~~/src/Provers/splitter.ML"
@@ -39,6 +40,9 @@
("Tools/recfun_codegen.ML")
begin
+setup {* Intuitionistic.method_setup "iprover" *}
+
+
subsection {* Primitive logic *}
subsubsection {* Core syntax *}
--- a/src/HOL/IsaMakefile Sat Feb 28 14:42:54 2009 +0100
+++ b/src/HOL/IsaMakefile Sat Feb 28 14:52:21 2009 +0100
@@ -100,6 +100,7 @@
$(SRC)/Tools/coherent.ML \
$(SRC)/Tools/eqsubst.ML \
$(SRC)/Tools/induct.ML \
+ $(SRC)/Tools/intuitionistic.ML \
$(SRC)/Tools/induct_tacs.ML \
$(SRC)/Tools/nbe.ML \
$(SRC)/Tools/project_rule.ML \
--- a/src/Pure/Isar/method.ML Sat Feb 28 14:42:54 2009 +0100
+++ b/src/Pure/Isar/method.ML Sat Feb 28 14:52:21 2009 +0100
@@ -49,7 +49,6 @@
val erule: int -> thm list -> method
val drule: int -> thm list -> method
val frule: int -> thm list -> method
- val iprover_tac: Proof.context -> int option -> int -> tactic
val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
val tactic: string * Position.T -> Proof.context -> method
val raw_tactic: string * Position.T -> Proof.context -> method
@@ -296,55 +295,6 @@
THEN Tactic.distinct_subgoals_tac;
-(* iprover -- intuitionistic proof search *)
-
-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 iprover_tac ctxt opt_lim =
- SELECT_GOAL (DEEPEN (2, the_default 20 opt_lim) (intprover_tac ctxt [] 0) 4 1);
-
-end;
-
-
(* ML tactics *)
structure TacticData = ProofDataFun
@@ -511,39 +461,6 @@
end;
-(* iprover syntax *)
-
-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' |-- P.nat --| Args.colon >> SOME)
- >> (pair (I: Proof.context -> Proof.context) o att);
-
-val iprover_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)];
-
-in
-
-val iprover_meth =
- bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option P.nat))
- (fn n => fn prems => fn ctxt => METHOD (fn facts =>
- HEADGOAL (insert_tac (prems @ facts) THEN'
- ObjectLogic.atomize_prems_tac THEN' iprover_tac ctxt n)));
-
-end;
-
-
(* tactic syntax *)
fun nat_thms_args f = uncurry f oo
@@ -599,7 +516,6 @@
("fold", thms_ctxt_args fold_meth, "fold definitions"),
("atomize", (atomize o fst) oo syntax (Args.mode "full"),
"present local premises as object-level statements"),
- ("iprover", iprover_meth, "intuitionistic proof search"),
("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"),
--- /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;
+