--- a/etc/isar-keywords-ZF.el Mon May 11 19:51:21 2009 +0200
+++ b/etc/isar-keywords-ZF.el Mon May 11 19:54:43 2009 +0200
@@ -18,7 +18,6 @@
"ML"
"ML_command"
"ML_prf"
- "ML_test"
"ML_val"
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
@@ -349,7 +348,6 @@
(defconst isar-keywords-theory-decl
'("ML"
- "ML_test"
"abbreviation"
"arities"
"attribute_setup"
--- a/etc/isar-keywords.el Mon May 11 19:51:21 2009 +0200
+++ b/etc/isar-keywords.el Mon May 11 19:54:43 2009 +0200
@@ -18,7 +18,6 @@
"ML"
"ML_command"
"ML_prf"
- "ML_test"
"ML_val"
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
@@ -64,6 +63,7 @@
"code_module"
"code_modulename"
"code_monad"
+ "code_pred"
"code_reserved"
"code_thms"
"code_type"
@@ -421,7 +421,6 @@
(defconst isar-keywords-theory-decl
'("ML"
- "ML_test"
"abbreviation"
"arities"
"atom_decl"
@@ -515,6 +514,7 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
+ "code_pred"
"corollary"
"cpodef"
"function"
--- a/lib/jedit/isabelle.xml Mon May 11 19:51:21 2009 +0200
+++ b/lib/jedit/isabelle.xml Mon May 11 19:54:43 2009 +0200
@@ -45,7 +45,6 @@
<OPERATOR>ML</OPERATOR>
<LABEL>ML_command</LABEL>
<OPERATOR>ML_prf</OPERATOR>
- <OPERATOR>ML_test</OPERATOR>
<LABEL>ML_val</LABEL>
<OPERATOR>abbreviation</OPERATOR>
<KEYWORD4>actions</KEYWORD4>
@@ -95,6 +94,7 @@
<OPERATOR>code_module</OPERATOR>
<OPERATOR>code_modulename</OPERATOR>
<OPERATOR>code_monad</OPERATOR>
+ <OPERATOR>code_pred</OPERATOR>
<OPERATOR>code_reserved</OPERATOR>
<LABEL>code_thms</LABEL>
<OPERATOR>code_type</OPERATOR>
--- a/src/HOL/Predicate.thy Mon May 11 19:51:21 2009 +0200
+++ b/src/HOL/Predicate.thy Mon May 11 19:54:43 2009 +0200
@@ -622,7 +622,10 @@
"pred_rec f P = f (eval P)"
by (cases P) simp
-text {* for evaluation of predicate enumerations *}
+inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x"
+
+lemma eq_is_eq: "eq x y \<equiv> (x = y)"
+ by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
ML {*
signature PREDICATE =
@@ -666,6 +669,12 @@
code_const Seq and Empty and Insert and Join
(Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)")
+text {* dummy setup for @{text code_pred} keyword *}
+
+ML {*
+OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
+ OuterKeyword.thy_goal (OuterParse.term_group >> (K (Proof.theorem_i NONE (K I) [[]])))
+*}
no_notation
inf (infixl "\<sqinter>" 70) and
@@ -678,6 +687,6 @@
hide (open) type pred seq
hide (open) const Pred eval single bind if_pred not_pred
- Empty Insert Join Seq member pred_of_seq "apply" adjunct
+ Empty Insert Join Seq member pred_of_seq "apply" adjunct eq
end
--- a/src/HOL/ex/Predicate_Compile.thy Mon May 11 19:51:21 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy Mon May 11 19:54:43 2009 +0200
@@ -7,6 +7,11 @@
setup {* Predicate_Compile.setup *}
+ML {*
+ OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
+ OuterKeyword.thy_goal (OuterParse.term_group >> Predicate_Compile.code_pred_cmd)
+*}
+
text {* Experimental code *}
@@ -83,4 +88,18 @@
ML_val {* Predicate.analyze_compr @{theory} @{term "{n. odd n}"} *}
+section {* Example for user interface *}
+
+inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+where
+ "append [] ys ys"
+| "append xs' ys zs' \<Longrightarrow> append (x#xs') ys (x#zs')"
+
+code_pred append
+ using assms by (rule append.cases)
+
+thm append_codegen
+thm append_cases
+
+
end
\ No newline at end of file
--- a/src/HOL/ex/predicate_compile.ML Mon May 11 19:51:21 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Mon May 11 19:54:43 2009 +0200
@@ -18,7 +18,12 @@
val modename_of: theory -> string -> mode -> string
val modes_of: theory -> string -> mode list
val setup : theory -> theory
+ val code_pred : string -> Proof.context -> Proof.state
+ val code_pred_cmd : string -> Proof.context -> Proof.state
+ val print_alternative_rules : theory -> theory
val do_proofs: bool ref
+ val pred_intros : theory -> string -> thm list
+ val get_nparams : theory -> string -> int
end;
structure Predicate_Compile: PREDICATE_COMPILE =
@@ -739,15 +744,15 @@
Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct
| _ => error "Trueprop_conv"
-fun preprocess_intro thy rule = Thm.transfer thy rule (*FIXME preprocessor
+fun preprocess_intro thy rule =
Conv.fconv_rule
(imp_prems_conv
- (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @ {thm Predicate.eq_is_eq})))))
- (Thm.transfer thy rule) *)
+ (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
+ (Thm.transfer thy rule)
-fun preprocess_elim thy nargs elimrule = (*FIXME preprocessor -- let
+fun preprocess_elim thy nargs elimrule = let
fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
- HOLogic.mk_Trueprop (Const (@ {const_name Predicate.eq}, T) $ lhs $ rhs)
+ HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
| replace_eqs t = t
fun preprocess_case t = let
val params = Logic.strip_params t
@@ -759,10 +764,10 @@
val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
in
Thm.equal_elim
- (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@ {thm eq_is_eq}])
+ (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm eq_is_eq}])
(cterm_of thy elimrule')))
elimrule
- end*) elimrule;
+ end;
(* returns true if t is an application of an datatype constructor *)
@@ -1354,6 +1359,57 @@
Attrib.setup @{binding code_ind_cases} (Scan.succeed code_ind_cases_attrib)
"adding alternative elimination rules for code generation of inductive predicates";
+(* generation of case rules from user-given introduction rules *)
+
+ fun mk_casesrule introrules nparams ctxt = let
+ val intros = map prop_of introrules
+ val (pred, (params, args)) = strip_intro_concl (hd intros) nparams
+ val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt
+ val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
+ val (argnames, ctxt2) = Variable.variant_fixes
+ (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt1
+ val argvs = map Free (argnames ~~ (map fastype_of args))
+ fun mk_case intro = let
+ val (_, (_, args)) = strip_intro_concl intro nparams
+ val prems = Logic.strip_imp_prems intro
+ val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
+ val frees = (fold o fold_aterms)
+ (fn t as Free _ =>
+ if member (op aconv) params t then I else insert (op aconv) t
+ | _ => I) (args @ prems) []
+ in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
+ val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
+ val cases = map mk_case intros
+ val (_, ctxt3) = ProofContext.add_assms_i Assumption.assume_export
+ [((Binding.name AutoBind.assmsN, []), map (fn t => (t, [])) (assm :: cases))]
+ ctxt2
+ in (pred, prop, ctxt3) end;
+
+(* setup for user interface *)
+
+ fun generic_code_pred prep_const raw_const lthy =
+ let
+ val thy = (ProofContext.theory_of lthy)
+ val const = prep_const thy raw_const
+ val nparams = get_nparams thy const
+ val intro_rules = pred_intros thy const
+ val (((tfrees, frees), fact), lthy') =
+ Variable.import_thms true intro_rules lthy;
+ val (pred, prop, lthy'') = mk_casesrule fact nparams lthy'
+ val (predname, _) = dest_Const pred
+ fun after_qed [[th]] lthy'' =
+ LocalTheory.note Thm.theoremK
+ ((Binding.name (Long_Name.base_name predname ^ "_cases"), (* FIXME: other suffix *)
+ [Attrib.internal (K (code_ind_cases_attrib))]) , [th]) lthy''
+ |> snd
+ |> LocalTheory.theory (create_def_equation predname)
+ in
+ Proof.theorem_i NONE after_qed [[(prop, [])]] lthy''
+ end;
+
+ val code_pred = generic_code_pred (K I);
+ val code_pred_cmd = generic_code_pred Code_Unit.read_const
+
end;
fun pred_compile name thy = Predicate_Compile.create_def_equation