moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
authorwenzelm
Sat Feb 28 14:52:21 2009 +0100 (2009-02-28)
changeset 301656ee87f67d9cd
parent 30164 9321f7b70450
child 30166 f47c812de07c
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
src/FOL/IFOL.thy
src/FOL/IsaMakefile
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/Pure/Isar/method.ML
src/Tools/intuitionistic.ML
     1.1 --- a/src/FOL/IFOL.thy	Sat Feb 28 14:42:54 2009 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Sat Feb 28 14:52:21 2009 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4    "~~/src/Tools/IsaPlanner/rw_inst.ML"
     1.5    "~~/src/Tools/eqsubst.ML"
     1.6    "~~/src/Provers/quantifier1.ML"
     1.7 +  "~~/src/Tools/intuitionistic.ML"
     1.8    "~~/src/Tools/project_rule.ML"
     1.9    "~~/src/Tools/atomize_elim.ML"
    1.10    ("fologic.ML")
    1.11 @@ -609,6 +610,8 @@
    1.12  
    1.13  subsection {* Intuitionistic Reasoning *}
    1.14  
    1.15 +setup {* Intuitionistic.method_setup "iprover" *}
    1.16 +
    1.17  lemma impE':
    1.18    assumes 1: "P --> Q"
    1.19      and 2: "Q ==> R"
     2.1 --- a/src/FOL/IsaMakefile	Sat Feb 28 14:42:54 2009 +0100
     2.2 +++ b/src/FOL/IsaMakefile	Sat Feb 28 14:52:21 2009 +0100
     2.3 @@ -34,10 +34,11 @@
     2.4    $(SRC)/Tools/IsaPlanner/rw_tools.ML					\
     2.5    $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML		\
     2.6    $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML			\
     2.7 -  $(SRC)/Tools/atomize_elim.ML $(SRC)/Tools/project_rule.ML		\
     2.8 -  $(SRC)/Provers/quantifier1.ML $(SRC)/Provers/splitter.ML FOL.thy	\
     2.9 -  IFOL.thy ROOT.ML blastdata.ML cladata.ML document/root.tex		\
    2.10 -  fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
    2.11 +  $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML		\
    2.12 +  $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
    2.13 +  $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML blastdata.ML	\
    2.14 +  cladata.ML document/root.tex fologic.ML hypsubstdata.ML intprover.ML	\
    2.15 +  simpdata.ML
    2.16  	@$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL
    2.17  
    2.18  
     3.1 --- a/src/HOL/HOL.thy	Sat Feb 28 14:42:54 2009 +0100
     3.2 +++ b/src/HOL/HOL.thy	Sat Feb 28 14:52:21 2009 +0100
     3.3 @@ -12,6 +12,7 @@
     3.4    "~~/src/Tools/IsaPlanner/isand.ML"
     3.5    "~~/src/Tools/IsaPlanner/rw_tools.ML"
     3.6    "~~/src/Tools/IsaPlanner/rw_inst.ML"
     3.7 +  "~~/src/Tools/intuitionistic.ML"
     3.8    "~~/src/Tools/project_rule.ML"
     3.9    "~~/src/Provers/hypsubst.ML"
    3.10    "~~/src/Provers/splitter.ML"
    3.11 @@ -39,6 +40,9 @@
    3.12    ("Tools/recfun_codegen.ML")
    3.13  begin
    3.14  
    3.15 +setup {* Intuitionistic.method_setup "iprover" *}
    3.16 +
    3.17 +
    3.18  subsection {* Primitive logic *}
    3.19  
    3.20  subsubsection {* Core syntax *}
     4.1 --- a/src/HOL/IsaMakefile	Sat Feb 28 14:42:54 2009 +0100
     4.2 +++ b/src/HOL/IsaMakefile	Sat Feb 28 14:52:21 2009 +0100
     4.3 @@ -100,6 +100,7 @@
     4.4    $(SRC)/Tools/coherent.ML \
     4.5    $(SRC)/Tools/eqsubst.ML \
     4.6    $(SRC)/Tools/induct.ML \
     4.7 +  $(SRC)/Tools/intuitionistic.ML \
     4.8    $(SRC)/Tools/induct_tacs.ML \
     4.9    $(SRC)/Tools/nbe.ML \
    4.10    $(SRC)/Tools/project_rule.ML \
     5.1 --- a/src/Pure/Isar/method.ML	Sat Feb 28 14:42:54 2009 +0100
     5.2 +++ b/src/Pure/Isar/method.ML	Sat Feb 28 14:52:21 2009 +0100
     5.3 @@ -49,7 +49,6 @@
     5.4    val erule: int -> thm list -> method
     5.5    val drule: int -> thm list -> method
     5.6    val frule: int -> thm list -> method
     5.7 -  val iprover_tac: Proof.context -> int option -> int -> tactic
     5.8    val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
     5.9    val tactic: string * Position.T -> Proof.context -> method
    5.10    val raw_tactic: string * Position.T -> Proof.context -> method
    5.11 @@ -296,55 +295,6 @@
    5.12      THEN Tactic.distinct_subgoals_tac;
    5.13  
    5.14  
    5.15 -(* iprover -- intuitionistic proof search *)
    5.16 -
    5.17 -local
    5.18 -
    5.19 -val remdups_tac = SUBGOAL (fn (g, i) =>
    5.20 -  let val prems = Logic.strip_assums_hyp g in
    5.21 -    REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
    5.22 -    (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
    5.23 -  end);
    5.24 -
    5.25 -fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
    5.26 -
    5.27 -val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist;
    5.28 -
    5.29 -fun safe_step_tac ctxt =
    5.30 -  ContextRules.Swrap ctxt
    5.31 -   (eq_assume_tac ORELSE'
    5.32 -    bires_tac true (ContextRules.netpair_bang ctxt));
    5.33 -
    5.34 -fun unsafe_step_tac ctxt =
    5.35 -  ContextRules.wrap ctxt
    5.36 -   (assume_tac APPEND'
    5.37 -    bires_tac false (ContextRules.netpair_bang ctxt) APPEND'
    5.38 -    bires_tac false (ContextRules.netpair ctxt));
    5.39 -
    5.40 -fun step_tac ctxt i =
    5.41 -  REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
    5.42 -  REMDUPS (unsafe_step_tac ctxt) i;
    5.43 -
    5.44 -fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) => if d > lim then no_tac else
    5.45 -  let
    5.46 -    val ps = Logic.strip_assums_hyp g;
    5.47 -    val c = Logic.strip_assums_concl g;
    5.48 -  in
    5.49 -    if member (fn ((ps1, c1), (ps2, c2)) =>
    5.50 -        c1 aconv c2 andalso
    5.51 -        length ps1 = length ps2 andalso
    5.52 -        gen_eq_set (op aconv) (ps1, ps2)) gs (ps, c) then no_tac
    5.53 -    else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
    5.54 -  end);
    5.55 -
    5.56 -in
    5.57 -
    5.58 -fun iprover_tac ctxt opt_lim =
    5.59 -  SELECT_GOAL (DEEPEN (2, the_default 20 opt_lim) (intprover_tac ctxt [] 0) 4 1);
    5.60 -
    5.61 -end;
    5.62 -
    5.63 -
    5.64  (* ML tactics *)
    5.65  
    5.66  structure TacticData = ProofDataFun
    5.67 @@ -511,39 +461,6 @@
    5.68  end;
    5.69  
    5.70  
    5.71 -(* iprover syntax *)
    5.72 -
    5.73 -local
    5.74 -
    5.75 -val introN = "intro";
    5.76 -val elimN = "elim";
    5.77 -val destN = "dest";
    5.78 -val ruleN = "rule";
    5.79 -
    5.80 -fun modifier name kind kind' att =
    5.81 -  Args.$$$ name |-- (kind >> K NONE || kind' |-- P.nat --| Args.colon >> SOME)
    5.82 -    >> (pair (I: Proof.context -> Proof.context) o att);
    5.83 -
    5.84 -val iprover_modifiers =
    5.85 - [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,
    5.86 -  modifier destN Args.colon (Scan.succeed ()) ContextRules.dest,
    5.87 -  modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang,
    5.88 -  modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim,
    5.89 -  modifier introN Args.bang_colon Args.bang ContextRules.intro_bang,
    5.90 -  modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
    5.91 -  Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
    5.92 -
    5.93 -in
    5.94 -
    5.95 -val iprover_meth =
    5.96 -  bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option P.nat))
    5.97 -    (fn n => fn prems => fn ctxt => METHOD (fn facts =>
    5.98 -      HEADGOAL (insert_tac (prems @ facts) THEN'
    5.99 -      ObjectLogic.atomize_prems_tac THEN' iprover_tac ctxt n)));
   5.100 -
   5.101 -end;
   5.102 -
   5.103 -
   5.104  (* tactic syntax *)
   5.105  
   5.106  fun nat_thms_args f = uncurry f oo
   5.107 @@ -599,7 +516,6 @@
   5.108      ("fold", thms_ctxt_args fold_meth, "fold definitions"),
   5.109      ("atomize", (atomize o fst) oo syntax (Args.mode "full"),
   5.110        "present local premises as object-level statements"),
   5.111 -    ("iprover", iprover_meth, "intuitionistic proof search"),
   5.112      ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
   5.113      ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
   5.114      ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"),
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/intuitionistic.ML	Sat Feb 28 14:52:21 2009 +0100
     6.3 @@ -0,0 +1,100 @@
     6.4 +(*  Title:      Tools/intuitionistic.ML
     6.5 +    Author:     Stefan Berghofer, TU Muenchen
     6.6 +
     6.7 +Simple intuitionistic proof search.
     6.8 +*)
     6.9 +
    6.10 +signature INTUITIONISTIC =
    6.11 +sig
    6.12 +  val prover_tac: Proof.context -> int option -> int -> tactic
    6.13 +  val method_setup: bstring -> theory -> theory
    6.14 +end;
    6.15 +
    6.16 +structure Intuitionistic: INTUITIONISTIC =
    6.17 +struct
    6.18 +
    6.19 +(* main tactic *)
    6.20 +
    6.21 +local
    6.22 +
    6.23 +val remdups_tac = SUBGOAL (fn (g, i) =>
    6.24 +  let val prems = Logic.strip_assums_hyp g in
    6.25 +    REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
    6.26 +    (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
    6.27 +  end);
    6.28 +
    6.29 +fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
    6.30 +
    6.31 +val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist;
    6.32 +
    6.33 +fun safe_step_tac ctxt =
    6.34 +  ContextRules.Swrap ctxt
    6.35 +   (eq_assume_tac ORELSE'
    6.36 +    bires_tac true (ContextRules.netpair_bang ctxt));
    6.37 +
    6.38 +fun unsafe_step_tac ctxt =
    6.39 +  ContextRules.wrap ctxt
    6.40 +   (assume_tac APPEND'
    6.41 +    bires_tac false (ContextRules.netpair_bang ctxt) APPEND'
    6.42 +    bires_tac false (ContextRules.netpair ctxt));
    6.43 +
    6.44 +fun step_tac ctxt i =
    6.45 +  REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
    6.46 +  REMDUPS (unsafe_step_tac ctxt) i;
    6.47 +
    6.48 +fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) => if d > lim then no_tac else
    6.49 +  let
    6.50 +    val ps = Logic.strip_assums_hyp g;
    6.51 +    val c = Logic.strip_assums_concl g;
    6.52 +  in
    6.53 +    if member (fn ((ps1, c1), (ps2, c2)) =>
    6.54 +        c1 aconv c2 andalso
    6.55 +        length ps1 = length ps2 andalso
    6.56 +        gen_eq_set (op aconv) (ps1, ps2)) gs (ps, c) then no_tac
    6.57 +    else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
    6.58 +  end);
    6.59 +
    6.60 +in
    6.61 +
    6.62 +fun prover_tac ctxt opt_lim =
    6.63 +  SELECT_GOAL (DEEPEN (2, the_default 20 opt_lim) (intprover_tac ctxt [] 0) 4 1);
    6.64 +
    6.65 +end;
    6.66 +
    6.67 +
    6.68 +(* method setup *)
    6.69 +
    6.70 +local
    6.71 +
    6.72 +val introN = "intro";
    6.73 +val elimN = "elim";
    6.74 +val destN = "dest";
    6.75 +val ruleN = "rule";
    6.76 +
    6.77 +fun modifier name kind kind' att =
    6.78 +  Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)
    6.79 +    >> (pair (I: Proof.context -> Proof.context) o att);
    6.80 +
    6.81 +val modifiers =
    6.82 + [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,
    6.83 +  modifier destN Args.colon (Scan.succeed ()) ContextRules.dest,
    6.84 +  modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang,
    6.85 +  modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim,
    6.86 +  modifier introN Args.bang_colon Args.bang ContextRules.intro_bang,
    6.87 +  modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
    6.88 +  Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
    6.89 +
    6.90 +val method =
    6.91 +  Method.bang_sectioned_args' modifiers (Scan.lift (Scan.option OuterParse.nat))
    6.92 +    (fn n => fn prems => fn ctxt => Method.METHOD (fn facts =>
    6.93 +      HEADGOAL (Method.insert_tac (prems @ facts) THEN'
    6.94 +      ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n)));
    6.95 +
    6.96 +in
    6.97 +
    6.98 +fun method_setup name = Method.add_method (name, method, "intuitionistic proof search");
    6.99 +
   6.100 +end;
   6.101 +
   6.102 +end;
   6.103 +