# HG changeset patch
# User haftmann
# Date 1496671185 -7200
# Node ID 59bf29d2b3a142d5a00a14401c337cb2492fdf26
# Parent  f10bbfe07c412420eee613cac58af23bb24f39bf
modernized (code) setup for enumeration predicates

diff -r f10bbfe07c41 -r 59bf29d2b3a1 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon Jun 05 15:59:45 2017 +0200
+++ b/src/HOL/Predicate.thy	Mon Jun 05 15:59:45 2017 +0200
@@ -10,14 +10,7 @@
 
 subsection \<open>The type of predicate enumerations (a monad)\<close>
 
-datatype (plugins only: code extraction) (dead 'a) pred = Pred "'a \<Rightarrow> bool"
-
-primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where
-  eval_pred: "eval (Pred f) = f"
-
-lemma Pred_eval [simp]:
-  "Pred (eval x) = x"
-  by (cases x) simp
+datatype (plugins only: extraction) (dead 'a) pred = Pred (eval: "'a \<Rightarrow> bool")
 
 lemma pred_eqI:
   "(\<And>w. eval P w \<longleftrightarrow> eval Q w) \<Longrightarrow> P = Q"
@@ -339,7 +332,7 @@
   unfolding if_pred_eq by (cases b) (auto elim: botE)
 
 lemma not_predI: "\<not> P \<Longrightarrow> eval (not_pred (Pred (\<lambda>u. P))) ()"
-  unfolding not_pred_eq eval_pred by (auto intro: singleI)
+  unfolding not_pred_eq by (auto intro: singleI)
 
 lemma not_predI': "\<not> eval P () \<Longrightarrow> eval (not_pred P) ()"
   unfolding not_pred_eq by (auto intro: singleI)
@@ -529,18 +522,27 @@
   by (cases "f ()")
     (simp_all add: Seq_def single_less_eq_eval contained_less_eq)
 
-lemma eq_pred_code [code]:
-  fixes P Q :: "'a pred"
-  shows "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
-  by (auto simp add: equal)
+instantiation pred :: (type) equal
+begin
+
+definition equal_pred
+  where [simp]: "HOL.equal P Q \<longleftrightarrow> P = (Q :: 'a pred)"
+
+instance by standard simp
+
+end
+    
+lemma [code]:
+  "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P" for P Q :: "'a pred"
+  by auto
 
 lemma [code nbe]:
-  "HOL.equal (x :: 'a pred) x \<longleftrightarrow> True"
+  "HOL.equal P P \<longleftrightarrow> True" for P :: "'a pred"
   by (fact equal_refl)
 
 lemma [code]:
   "case_pred f P = f (eval P)"
-  by (cases P) simp
+  by (fact pred.case_eq_if)
 
 lemma [code]:
   "rec_pred f P = f (eval P)"
diff -r f10bbfe07c41 -r 59bf29d2b3a1 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jun 05 15:59:45 2017 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jun 05 15:59:45 2017 +0200
@@ -1085,7 +1085,7 @@
                      HOLogic.mk_tuple outargs))
     val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
     val simprules =
-      [defthm, @{thm eval_pred},
+      [defthm, @{thm pred.sel},
         @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm prod.collapse}]
     val unfolddef_tac =
       Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simprules) 1
@@ -1347,7 +1347,7 @@
               (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
             val def = Core_Data.predfun_definition_of ctxt predname full_mode
             val tac = fn _ => Simplifier.simp_tac
-              (put_simpset HOL_basic_ss ctxt addsimps [def, @{thm holds_eq}, @{thm eval_pred}]) 1
+              (put_simpset HOL_basic_ss ctxt addsimps [def, @{thm holds_eq}, @{thm pred.sel}]) 1
             val eq = Goal.prove ctxt arg_names [] eq_term tac
           in
             (pred, result_thms @ [eq])
diff -r f10bbfe07c41 -r 59bf29d2b3a1 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Mon Jun 05 15:59:45 2017 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Mon Jun 05 15:59:45 2017 +0200
@@ -61,7 +61,7 @@
     val f_tac =
       (case f of
         Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps
-           [@{thm eval_pred}, Core_Data.predfun_definition_of ctxt name mode,
+           [@{thm pred.sel}, Core_Data.predfun_definition_of ctxt name mode,
            @{thm case_prod_eta}, @{thm case_prod_beta}, @{thm fst_conv},
            @{thm snd_conv}, @{thm prod.collapse}, @{thm Product_Type.split_conv}]) 1
       | Free _ =>
@@ -180,7 +180,7 @@
         preds
   in
     simp_tac (put_simpset HOL_basic_ss ctxt
-      addsimps (@{thms HOL.simp_thms eval_pred} @ defs)) 1
+      addsimps (@{thms HOL.simp_thms pred.sel} @ defs)) 1
     (* need better control here! *)
   end
 
@@ -339,7 +339,7 @@
     val f_tac =
       (case f of
         Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
-           [@{thm eval_pred}, Core_Data.predfun_definition_of ctxt name mode,
+           [@{thm pred.sel}, Core_Data.predfun_definition_of ctxt name mode,
             @{thm Product_Type.split_conv}]) 1
       | Free _ => all_tac
       | _ => error "prove_param2: illegal parameter term")
@@ -383,7 +383,7 @@
         preds
   in
     (* only simplify the one assumption *)
-    full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1
+    full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm pred.sel} :: defs) 1
     (* need better control here! *)
     THEN trace_tac ctxt options "after sidecond2 simplification"
   end