modernized functor names;
authorwenzelm
Sat May 14 11:42:43 2011 +0200 (2011-05-14)
changeset 427994e33894aec6d
parent 42798 02c88bdabe75
child 42800 df2dc9406287
modernized functor names;
tuned;
src/FOL/FOL.thy
src/FOL/IFOL.thy
src/FOL/IsaMakefile
src/FOL/hypsubstdata.ML
src/FOLP/FOLP.thy
src/FOLP/IFOLP.thy
src/FOLP/classical.ML
src/FOLP/hypsubst.ML
src/HOL/HOL.thy
src/Provers/classical.ML
src/Provers/hypsubst.ML
     1.1 --- a/src/FOL/FOL.thy	Sat May 14 00:32:16 2011 +0200
     1.2 +++ b/src/FOL/FOL.thy	Sat May 14 11:42:43 2011 +0200
     1.3 @@ -167,7 +167,7 @@
     1.4  section {* Classical Reasoner *}
     1.5  
     1.6  ML {*
     1.7 -structure Cla = ClassicalFun
     1.8 +structure Cla = Classical
     1.9  (
    1.10    val imp_elim = @{thm imp_elim}
    1.11    val not_elim = @{thm notE}
     2.1 --- a/src/FOL/IFOL.thy	Sat May 14 00:32:16 2011 +0200
     2.2 +++ b/src/FOL/IFOL.thy	Sat May 14 11:42:43 2011 +0200
     2.3 @@ -19,7 +19,6 @@
     2.4    "~~/src/Tools/project_rule.ML"
     2.5    "~~/src/Tools/atomize_elim.ML"
     2.6    ("fologic.ML")
     2.7 -  ("hypsubstdata.ML")
     2.8    ("intprover.ML")
     2.9  begin
    2.10  
    2.11 @@ -592,7 +591,23 @@
    2.12  
    2.13  lemma thin_refl: "[|x=x; PROP W|] ==> PROP W" .
    2.14  
    2.15 -use "hypsubstdata.ML"
    2.16 +ML {*
    2.17 +structure Hypsubst = Hypsubst
    2.18 +(
    2.19 +  val dest_eq = FOLogic.dest_eq
    2.20 +  val dest_Trueprop = FOLogic.dest_Trueprop
    2.21 +  val dest_imp = FOLogic.dest_imp
    2.22 +  val eq_reflection = @{thm eq_reflection}
    2.23 +  val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
    2.24 +  val imp_intr = @{thm impI}
    2.25 +  val rev_mp = @{thm rev_mp}
    2.26 +  val subst = @{thm subst}
    2.27 +  val sym = @{thm sym}
    2.28 +  val thin_refl = @{thm thin_refl}
    2.29 +);
    2.30 +open Hypsubst;
    2.31 +*}
    2.32 +
    2.33  setup hypsubst_setup
    2.34  use "intprover.ML"
    2.35  
     3.1 --- a/src/FOL/IsaMakefile	Sat May 14 00:32:16 2011 +0200
     3.2 +++ b/src/FOL/IsaMakefile	Sat May 14 11:42:43 2011 +0200
     3.3 @@ -36,8 +36,7 @@
     3.4    $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML		\
     3.5    $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
     3.6    $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML			\
     3.7 -  document/root.tex fologic.ML hypsubstdata.ML intprover.ML		\
     3.8 -  simpdata.ML
     3.9 +  document/root.tex fologic.ML intprover.ML simpdata.ML
    3.10  	@$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL
    3.11  
    3.12  
     4.1 --- a/src/FOL/hypsubstdata.ML	Sat May 14 00:32:16 2011 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,19 +0,0 @@
     4.4 -
     4.5 -(** Applying HypsubstFun to generate hyp_subst_tac **)
     4.6 -structure Hypsubst_Data =
     4.7 -struct
     4.8 -  structure Simplifier = Simplifier
     4.9 -  val dest_eq = FOLogic.dest_eq
    4.10 -  val dest_Trueprop = FOLogic.dest_Trueprop
    4.11 -  val dest_imp = FOLogic.dest_imp
    4.12 -  val eq_reflection = @{thm eq_reflection}
    4.13 -  val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
    4.14 -  val imp_intr = @{thm impI}
    4.15 -  val rev_mp = @{thm rev_mp}
    4.16 -  val subst = @{thm subst}
    4.17 -  val sym = @{thm sym}
    4.18 -  val thin_refl = @{thm thin_refl}
    4.19 -end;
    4.20 -
    4.21 -structure Hypsubst = HypsubstFun(Hypsubst_Data);
    4.22 -open Hypsubst;
     5.1 --- a/src/FOLP/FOLP.thy	Sat May 14 00:32:16 2011 +0200
     5.2 +++ b/src/FOLP/FOLP.thy	Sat May 14 11:42:43 2011 +0200
     5.3 @@ -103,17 +103,14 @@
     5.4  use "simp.ML"           (* Patched 'cos matching won't instantiate proof *)
     5.5  
     5.6  ML {*
     5.7 -(*** Applying ClassicalFun to create a classical prover ***)
     5.8 -structure Classical_Data =
     5.9 -struct
    5.10 +structure Cla = Classical
    5.11 +(
    5.12    val sizef = size_of_thm
    5.13    val mp = @{thm mp}
    5.14    val not_elim = @{thm notE}
    5.15    val swap = @{thm swap}
    5.16    val hyp_subst_tacs = [hyp_subst_tac]
    5.17 -end;
    5.18 -
    5.19 -structure Cla = ClassicalFun(Classical_Data);
    5.20 +);
    5.21  open Cla;
    5.22  
    5.23  (*Propositional rules
     6.1 --- a/src/FOLP/IFOLP.thy	Sat May 14 00:32:16 2011 +0200
     6.2 +++ b/src/FOLP/IFOLP.thy	Sat May 14 11:42:43 2011 +0200
     6.3 @@ -587,11 +587,8 @@
     6.4  use "hypsubst.ML"
     6.5  
     6.6  ML {*
     6.7 -
     6.8 -(*** Applying HypsubstFun to generate hyp_subst_tac ***)
     6.9 -
    6.10 -structure Hypsubst_Data =
    6.11 -struct
    6.12 +structure Hypsubst = Hypsubst
    6.13 +(
    6.14    (*Take apart an equality judgement; otherwise raise Match!*)
    6.15    fun dest_eq (Const (@{const_name Proof}, _) $
    6.16      (Const (@{const_name eq}, _)  $ t $ u) $ _) = (t, u);
    6.17 @@ -605,9 +602,7 @@
    6.18    val subst = @{thm subst}
    6.19    val sym = @{thm sym}
    6.20    val thin_refl = @{thm thin_refl}
    6.21 -end;
    6.22 -
    6.23 -structure Hypsubst = HypsubstFun(Hypsubst_Data);
    6.24 +);
    6.25  open Hypsubst;
    6.26  *}
    6.27  
     7.1 --- a/src/FOLP/classical.ML	Sat May 14 00:32:16 2011 +0200
     7.2 +++ b/src/FOLP/classical.ML	Sat May 14 11:42:43 2011 +0200
     7.3 @@ -60,7 +60,7 @@
     7.4    end;
     7.5  
     7.6  
     7.7 -functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
     7.8 +functor Classical(Data: CLASSICAL_DATA): CLASSICAL = 
     7.9  struct
    7.10  
    7.11  local open Data in
     8.1 --- a/src/FOLP/hypsubst.ML	Sat May 14 00:32:16 2011 +0200
     8.2 +++ b/src/FOLP/hypsubst.ML	Sat May 14 11:42:43 2011 +0200
     8.3 @@ -26,7 +26,7 @@
     8.4    val inspect_pair        : bool -> term * term -> thm
     8.5    end;
     8.6  
     8.7 -functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
     8.8 +functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
     8.9  struct
    8.10  
    8.11  local open Data in
     9.1 --- a/src/HOL/HOL.thy	Sat May 14 00:32:16 2011 +0200
     9.2 +++ b/src/HOL/HOL.thy	Sat May 14 11:42:43 2011 +0200
     9.3 @@ -826,9 +826,8 @@
     9.4    "\<And>X. \<lbrakk> x=x; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
     9.5  
     9.6  ML {*
     9.7 -structure Hypsubst = HypsubstFun(
     9.8 -struct
     9.9 -  structure Simplifier = Simplifier
    9.10 +structure Hypsubst = Hypsubst
    9.11 +(
    9.12    val dest_eq = HOLogic.dest_eq
    9.13    val dest_Trueprop = HOLogic.dest_Trueprop
    9.14    val dest_imp = HOLogic.dest_imp
    9.15 @@ -839,18 +838,18 @@
    9.16    val subst = @{thm subst}
    9.17    val sym = @{thm sym}
    9.18    val thin_refl = @{thm thin_refl};
    9.19 -end);
    9.20 +);
    9.21  open Hypsubst;
    9.22  
    9.23 -structure Classical = ClassicalFun(
    9.24 -struct
    9.25 +structure Classical = Classical
    9.26 +(
    9.27    val imp_elim = @{thm imp_elim}
    9.28    val not_elim = @{thm notE}
    9.29    val swap = @{thm swap}
    9.30    val classical = @{thm classical}
    9.31    val sizef = Drule.size_of_thm
    9.32    val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
    9.33 -end);
    9.34 +);
    9.35  
    9.36  structure Basic_Classical: BASIC_CLASSICAL = Classical; 
    9.37  open Basic_Classical;
    10.1 --- a/src/Provers/classical.ML	Sat May 14 00:32:16 2011 +0200
    10.2 +++ b/src/Provers/classical.ML	Sat May 14 11:42:43 2011 +0200
    10.3 @@ -131,7 +131,7 @@
    10.4  end;
    10.5  
    10.6  
    10.7 -functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL =
    10.8 +functor Classical(Data: CLASSICAL_DATA): CLASSICAL =
    10.9  struct
   10.10  
   10.11  (** classical elimination rules **)
    11.1 --- a/src/Provers/hypsubst.ML	Sat May 14 00:32:16 2011 +0200
    11.2 +++ b/src/Provers/hypsubst.ML	Sat May 14 11:42:43 2011 +0200
    11.3 @@ -53,7 +53,7 @@
    11.4    val hypsubst_setup         : theory -> theory
    11.5  end;
    11.6  
    11.7 -functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
    11.8 +functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
    11.9  struct
   11.10  
   11.11  exception EQ_VAR;