# HG changeset patch # User wenzelm # Date 1235829141 -3600 # Node ID 6ee87f67d9cdb4e410cf9bb7f8590b213573d870 # Parent 9321f7b70450e394dbe770aecea9557949186817 moved generic intuitionistic prover to src/Tools/intuitionistic.ML; diff -r 9321f7b70450 -r 6ee87f67d9cd src/FOL/IFOL.thy --- 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" diff -r 9321f7b70450 -r 6ee87f67d9cd src/FOL/IsaMakefile --- 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 diff -r 9321f7b70450 -r 6ee87f67d9cd src/HOL/HOL.thy --- 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 *} diff -r 9321f7b70450 -r 6ee87f67d9cd src/HOL/IsaMakefile --- 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 \ diff -r 9321f7b70450 -r 6ee87f67d9cd src/Pure/Isar/method.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)"), 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; +