src/HOL/HOL.thy
changeset 58826 2ed2eaabe3df
parent 58775 9cd64a66a765
child 58830 e05c620eceeb
     1.1 --- a/src/HOL/HOL.thy	Wed Oct 29 17:01:44 2014 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Oct 29 19:01:49 2014 +0100
     1.3 @@ -27,18 +27,12 @@
     1.4  ML_file "~~/src/Tools/eqsubst.ML"
     1.5  ML_file "~~/src/Provers/quantifier1.ML"
     1.6  ML_file "~~/src/Tools/atomize_elim.ML"
     1.7 -ML_file "~~/src/Tools/induct.ML"
     1.8  ML_file "~~/src/Tools/cong_tac.ML"
     1.9 -ML_file "~~/src/Tools/intuitionistic.ML"
    1.10 +ML_file "~~/src/Tools/intuitionistic.ML" setup \<open>Intuitionistic.method_setup @{binding iprover}\<close>
    1.11  ML_file "~~/src/Tools/project_rule.ML"
    1.12  ML_file "~~/src/Tools/subtyping.ML"
    1.13  ML_file "~~/src/Tools/case_product.ML"
    1.14  
    1.15 -setup {*
    1.16 -  Intuitionistic.method_setup @{binding iprover}
    1.17 -  #> Subtyping.setup
    1.18 -  #> Case_Product.setup
    1.19 -*}
    1.20  
    1.21  ML \<open>Plugin_Name.declare_setup @{binding extraction}\<close>
    1.22  
    1.23 @@ -231,7 +225,7 @@
    1.24  lemma trans_sym [Pure.elim?]: "r = s ==> t = s ==> r = t"
    1.25    by (rule trans [OF _ sym])
    1.26  
    1.27 -lemma meta_eq_to_obj_eq: 
    1.28 +lemma meta_eq_to_obj_eq:
    1.29    assumes meq: "A == B"
    1.30    shows "A = B"
    1.31    by (unfold meq) (rule refl)
    1.32 @@ -847,26 +841,23 @@
    1.33    val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
    1.34  );
    1.35  
    1.36 -structure Basic_Classical: BASIC_CLASSICAL = Classical; 
    1.37 +structure Basic_Classical: BASIC_CLASSICAL = Classical;
    1.38  open Basic_Classical;
    1.39  *}
    1.40  
    1.41 -setup Classical.setup
    1.42 -
    1.43  setup {*
    1.44 -let
    1.45 -  fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
    1.46 -    | non_bool_eq _ = false;
    1.47 -  fun hyp_subst_tac' ctxt =
    1.48 -    SUBGOAL (fn (goal, i) =>
    1.49 -      if Term.exists_Const non_bool_eq goal
    1.50 -      then Hypsubst.hyp_subst_tac ctxt i
    1.51 -      else no_tac);
    1.52 -in
    1.53 -  Hypsubst.hypsubst_setup
    1.54    (*prevent substitution on bool*)
    1.55 -  #> Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
    1.56 -end
    1.57 +  let
    1.58 +    fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
    1.59 +      | non_bool_eq _ = false;
    1.60 +    fun hyp_subst_tac' ctxt =
    1.61 +      SUBGOAL (fn (goal, i) =>
    1.62 +        if Term.exists_Const non_bool_eq goal
    1.63 +        then Hypsubst.hyp_subst_tac ctxt i
    1.64 +        else no_tac);
    1.65 +  in
    1.66 +    Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
    1.67 +  end
    1.68  *}
    1.69  
    1.70  declare iffI [intro!]
    1.71 @@ -932,8 +923,6 @@
    1.72    val blast_tac = Blast.blast_tac;
    1.73  *}
    1.74  
    1.75 -setup Blast.setup
    1.76 -
    1.77  
    1.78  subsubsection {* Simplifier *}
    1.79  
    1.80 @@ -1197,18 +1186,14 @@
    1.81  ML_file "Tools/simpdata.ML"
    1.82  ML {* open Simpdata *}
    1.83  
    1.84 -setup {* map_theory_simpset (put_simpset HOL_basic_ss) *}
    1.85 +setup {*
    1.86 +  map_theory_simpset (put_simpset HOL_basic_ss) #>
    1.87 +  Simplifier.method_setup Splitter.split_modifiers
    1.88 +*}
    1.89  
    1.90  simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
    1.91  simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}
    1.92  
    1.93 -setup {*
    1.94 -  Simplifier.method_setup Splitter.split_modifiers
    1.95 -  #> Splitter.setup
    1.96 -  #> clasimp_setup
    1.97 -  #> EqSubst.setup
    1.98 -*}
    1.99 -
   1.100  text {* Simproc for proving @{text "(y = x) == False"} from premise @{text "~(x = y)"}: *}
   1.101  
   1.102  simproc_setup neq ("x = y") = {* fn _ =>
   1.103 @@ -1467,6 +1452,7 @@
   1.104  
   1.105  text {* Method setup. *}
   1.106  
   1.107 +ML_file "~~/src/Tools/induct.ML"
   1.108  ML {*
   1.109  structure Induct = Induct
   1.110  (
   1.111 @@ -1484,7 +1470,6 @@
   1.112  ML_file "~~/src/Tools/induction.ML"
   1.113  
   1.114  setup {*
   1.115 -  Induct.setup #> Induction.setup #>
   1.116    Context.theory_map (Induct.map_simpset (fn ss => ss
   1.117      addsimprocs
   1.118        [Simplifier.simproc_global @{theory} "swap_induct_false"
   1.119 @@ -1558,13 +1543,12 @@
   1.120  lemma [induct_simp]: "induct_implies induct_true P == P"
   1.121    by (simp add: induct_implies_def induct_true_def)
   1.122  
   1.123 -lemma [induct_simp]: "(x = x) = True" 
   1.124 +lemma [induct_simp]: "(x = x) = True"
   1.125    by (rule simp_thms)
   1.126  
   1.127  hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
   1.128  
   1.129  ML_file "~~/src/Tools/induct_tacs.ML"
   1.130 -setup Induct_Tacs.setup
   1.131  
   1.132  
   1.133  subsubsection {* Coherent logic *}
   1.134 @@ -1640,8 +1624,8 @@
   1.135  lemmas eq_sym_conv = eq_commute
   1.136  
   1.137  lemma nnf_simps:
   1.138 -  "(\<not>(P \<and> Q)) = (\<not> P \<or> \<not> Q)" "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)" 
   1.139 -  "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))" 
   1.140 +  "(\<not>(P \<and> Q)) = (\<not> P \<or> \<not> Q)" "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
   1.141 +  "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))"
   1.142    "(\<not> \<not>(P)) = P"
   1.143  by blast+
   1.144  
   1.145 @@ -1737,10 +1721,11 @@
   1.146    by (fact arg_cong)
   1.147  
   1.148  setup {*
   1.149 -  Code_Preproc.map_pre (put_simpset HOL_basic_ss)
   1.150 -  #> Code_Preproc.map_post (put_simpset HOL_basic_ss)
   1.151 -  #> Code_Simp.map_ss (put_simpset HOL_basic_ss
   1.152 -    #> Simplifier.add_cong @{thm conj_left_cong} #> Simplifier.add_cong @{thm disj_left_cong})
   1.153 +  Code_Preproc.map_pre (put_simpset HOL_basic_ss) #>
   1.154 +  Code_Preproc.map_post (put_simpset HOL_basic_ss) #>
   1.155 +  Code_Simp.map_ss (put_simpset HOL_basic_ss #>
   1.156 +  Simplifier.add_cong @{thm conj_left_cong} #>
   1.157 +  Simplifier.add_cong @{thm disj_left_cong})
   1.158  *}
   1.159  
   1.160  
   1.161 @@ -1799,7 +1784,7 @@
   1.162  text {* More about @{typ prop} *}
   1.163  
   1.164  lemma [code nbe]:
   1.165 -  shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q" 
   1.166 +  shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
   1.167      and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
   1.168      and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" by (auto intro!: equal_intr_rule)
   1.169  
   1.170 @@ -1828,9 +1813,7 @@
   1.171    "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
   1.172    by (simp add: equal)
   1.173  
   1.174 -setup {*
   1.175 -  Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
   1.176 -*}
   1.177 +setup {* Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"}) *}
   1.178  
   1.179  lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
   1.180  proof
   1.181 @@ -1843,14 +1826,10 @@
   1.182    show "PROP ?ofclass" proof
   1.183    qed (simp add: `PROP ?equal`)
   1.184  qed
   1.185 -  
   1.186 -setup {*
   1.187 -  Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"})
   1.188 -*}
   1.189  
   1.190 -setup {*
   1.191 -  Nbe.add_const_alias @{thm equal_alias_cert}
   1.192 -*}
   1.193 +setup {* Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"}) *}
   1.194 +
   1.195 +setup {* Nbe.add_const_alias @{thm equal_alias_cert} *}
   1.196  
   1.197  text {* Cases *}
   1.198  
   1.199 @@ -1860,8 +1839,8 @@
   1.200    using assms by simp_all
   1.201  
   1.202  setup {*
   1.203 -  Code.add_case @{thm Let_case_cert}
   1.204 -  #> Code.add_undefined @{const_name undefined}
   1.205 +  Code.add_case @{thm Let_case_cert} #>
   1.206 +  Code.add_undefined @{const_name undefined}
   1.207  *}
   1.208  
   1.209  declare [[code abort: undefined]]
   1.210 @@ -1877,7 +1856,7 @@
   1.211  | constant True \<rightharpoonup>
   1.212      (SML) "true" and (OCaml) "true" and (Haskell) "True" and (Scala) "true"
   1.213  | constant False \<rightharpoonup>
   1.214 -    (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false" 
   1.215 +    (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false"
   1.216  
   1.217  code_reserved SML
   1.218    bool true false
   1.219 @@ -1936,13 +1915,13 @@
   1.220  subsubsection {* Evaluation and normalization by evaluation *}
   1.221  
   1.222  method_setup eval = {*
   1.223 -let
   1.224 -  fun eval_tac ctxt =
   1.225 -    let val conv = Code_Runtime.dynamic_holds_conv ctxt
   1.226 -    in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
   1.227 -in
   1.228 -  Scan.succeed (SIMPLE_METHOD' o eval_tac)
   1.229 -end
   1.230 +  let
   1.231 +    fun eval_tac ctxt =
   1.232 +      let val conv = Code_Runtime.dynamic_holds_conv ctxt
   1.233 +      in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
   1.234 +  in
   1.235 +    Scan.succeed (SIMPLE_METHOD' o eval_tac)
   1.236 +  end
   1.237  *} "solve goal by evaluation"
   1.238  
   1.239  method_setup normalization = {*
   1.240 @@ -1989,23 +1968,23 @@
   1.241  subsection {* Legacy tactics and ML bindings *}
   1.242  
   1.243  ML {*
   1.244 -(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
   1.245 -local
   1.246 -  fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t
   1.247 -    | wrong_prem (Bound _) = true
   1.248 -    | wrong_prem _ = false;
   1.249 -  val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
   1.250 -in
   1.251 -  fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
   1.252 -  fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
   1.253 -end;
   1.254 +  (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
   1.255 +  local
   1.256 +    fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t
   1.257 +      | wrong_prem (Bound _) = true
   1.258 +      | wrong_prem _ = false;
   1.259 +    val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
   1.260 +  in
   1.261 +    fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
   1.262 +    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
   1.263 +  end;
   1.264  
   1.265 -local
   1.266 -  val nnf_ss =
   1.267 -    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms simp_thms nnf_simps});
   1.268 -in
   1.269 -  fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
   1.270 -end
   1.271 +  local
   1.272 +    val nnf_ss =
   1.273 +      simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms simp_thms nnf_simps});
   1.274 +  in
   1.275 +    fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
   1.276 +  end
   1.277  *}
   1.278  
   1.279  hide_const (open) eq equal