# HG changeset patch # User haftmann # Date 1291623905 -3600 # Node ID fb2d3ccda5a785e275c4233ae16e897d116e946d # Parent a6fcd305f7dcc79afccd55d4971359021a902937 moved bootstrap of type_lifting to Fun diff -r a6fcd305f7dc -r fb2d3ccda5a7 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Mon Dec 06 09:19:10 2010 +0100 +++ b/src/HOL/Datatype.thy Mon Dec 06 09:25:05 2010 +0100 @@ -13,6 +13,12 @@ ("Tools/Datatype/datatype_realizer.ML") begin +subsection {* Prelude: lifting over function space *} + +type_lifting map_fun + by (simp_all add: fun_eq_iff) + + subsection {* The datatype universe *} typedef (Node) diff -r a6fcd305f7dc -r fb2d3ccda5a7 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Mon Dec 06 09:19:10 2010 +0100 +++ b/src/HOL/Fun.thy Mon Dec 06 09:25:05 2010 +0100 @@ -7,6 +7,7 @@ theory Fun imports Complete_Lattice +uses ("Tools/type_lifting.ML") begin text{*As a simplification rule, it replaces all function equalities by @@ -126,9 +127,6 @@ "map_fun f g h x = g (h (f x))" by (simp add: map_fun_def) -type_lifting map_fun - by (simp_all add: fun_eq_iff) - subsection {* Injectivity and Bijectivity *} @@ -774,7 +772,9 @@ thus False by best qed -subsection {* Proof tool setup *} +subsection {* Setup *} + +subsubsection {* Proof tools *} text {* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *} @@ -809,7 +809,7 @@ *} -subsection {* Code generator setup *} +subsubsection {* Code generator *} types_code "fun" ("(_ ->/ _)") @@ -840,4 +840,9 @@ code_const "id" (Haskell "id") + +subsubsection {* Functorial structure of types *} + +use "Tools/type_lifting.ML" + end diff -r a6fcd305f7dc -r fb2d3ccda5a7 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Mon Dec 06 09:19:10 2010 +0100 +++ b/src/HOL/HOL.thy Mon Dec 06 09:25:05 2010 +0100 @@ -32,7 +32,6 @@ "Tools/async_manager.ML" "Tools/try.ML" ("Tools/cnf_funcs.ML") - ("Tools/type_lifting.ML") "~~/src/Tools/subtyping.ML" begin @@ -714,7 +713,6 @@ and [Pure.elim?] = iffD1 iffD2 impE use "Tools/hologic.ML" -use "Tools/type_lifting.ML" subsubsection {* Atomizing meta-level connectives *} diff -r a6fcd305f7dc -r fb2d3ccda5a7 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Dec 06 09:19:10 2010 +0100 +++ b/src/HOL/IsaMakefile Mon Dec 06 09:25:05 2010 +0100 @@ -147,7 +147,6 @@ $(SRC)/Tools/solve_direct.ML \ $(SRC)/Tools/value.ML \ HOL.thy \ - Tools/type_lifting.ML \ Tools/hologic.ML \ Tools/recfun_codegen.ML \ Tools/simpdata.ML @@ -243,6 +242,7 @@ Tools/split_rule.ML \ Tools/try.ML \ Tools/typedef.ML \ + Tools/type_lifting.ML \ Transitive_Closure.thy \ Typedef.thy \ Wellfounded.thy