# HG changeset patch # User haftmann # Date 1284571250 -7200 # Node ID 84647a469fda2a782b12fed961d991d3240d1b28 # Parent 0cf524fad3f57e541f40dd1b9615ea1e24eab29d# Parent 9969401e1fb86c5d201ecbd98247a125e20a980b merged diff -r 0cf524fad3f5 -r 84647a469fda src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Sep 15 17:05:18 2010 +0200 +++ b/src/HOL/HOL.thy Wed Sep 15 19:20:50 2010 +0200 @@ -1802,21 +1802,10 @@ subsubsection {* Generic code generator foundation *} -text {* Datatypes *} +text {* Datatype @{typ bool} *} code_datatype True False -code_datatype "TYPE('a\{})" - -code_datatype "prop" Trueprop - -text {* Code equations *} - -lemma [code]: - shows "(True \ PROP Q) \ PROP Q" - and "(PROP Q \ True) \ Trueprop True" - and "(P \ R) \ Trueprop (P \ R)" by (auto intro!: equal_intr_rule) - lemma [code]: shows "False \ P \ False" and "True \ P \ P" @@ -1835,6 +1824,23 @@ and "(P \ False) \ \ P" and "(P \ True) \ True" by simp_all +text {* More about @{typ prop} *} + +lemma [code nbe]: + shows "(True \ PROP Q) \ PROP Q" + and "(PROP Q \ True) \ Trueprop True" + and "(P \ R) \ Trueprop (P \ R)" by (auto intro!: equal_intr_rule) + +lemma Trueprop_code [code]: + "Trueprop True \ Code_Generator.holds" + by (auto intro!: equal_intr_rule holds) + +declare Trueprop_code [symmetric, code_post] + +text {* Equality *} + +declare simp_thms(6) [code nbe] + instantiation itself :: (type) equal begin @@ -1850,10 +1856,6 @@ "equal TYPE('a) TYPE('a) \ True" by (simp add: equal) -text {* Equality *} - -declare simp_thms(6) [code nbe] - setup {* Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\type \ 'a \ bool"}) *} diff -r 0cf524fad3f5 -r 84647a469fda src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Wed Sep 15 17:05:18 2010 +0200 +++ b/src/Tools/Code/code_runtime.ML Wed Sep 15 19:20:50 2010 +0200 @@ -10,6 +10,8 @@ val value: string option -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a + val code_reflect: (string * string list) list -> string list -> string -> string option + -> theory -> theory val setup: theory -> theory end; @@ -20,6 +22,8 @@ val target = "Eval"; +val truth_struct = "Code_Truth"; + fun value some_target cookie postproc thy t args = let val ctxt = ProofContext.init_global thy; @@ -184,7 +188,7 @@ |> process result module_name some_file end; -val code_reflect = gen_code_reflect Code_Target.cert_tyco Code.check_const; +val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I); val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const; diff -r 0cf524fad3f5 -r 84647a469fda src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Wed Sep 15 17:05:18 2010 +0200 +++ b/src/Tools/Code_Generator.thy Wed Sep 15 19:20:50 2010 +0200 @@ -37,4 +37,33 @@ #> Quickcheck.setup *} +code_datatype "TYPE('a\{})" + +definition holds :: "prop" where + "holds \ ((\x::prop. x) \ (\x. x))" + +lemma holds: "PROP holds" + by (unfold holds_def) (rule reflexive) + +code_datatype holds + +lemma implies_code [code]: + "(PROP holds \ PROP P) \ PROP P" + "(PROP P \ PROP holds) \ PROP holds" +proof - + show "(PROP holds \ PROP P) \ PROP P" + proof + assume "PROP holds \ PROP P" + then show "PROP P" using holds . + next + assume "PROP P" + then show "PROP P" . + qed +next + show "(PROP P \ PROP holds) \ PROP holds" + by rule (rule holds)+ +qed + +hide_const (open) holds + end