tuned
authorhaftmann
Fri Oct 19 19:45:31 2007 +0200 (2007-10-19)
changeset 251031ee419a5a30f
parent 25102 db3e412c4cb1
child 25104 26b9a7db3386
tuned
src/HOL/Orderings.thy
src/Pure/Isar/class.ML
src/Tools/code/code_funcgr.ML
     1.1 --- a/src/HOL/Orderings.thy	Fri Oct 19 19:45:29 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Oct 19 19:45:31 2007 +0200
     1.3 @@ -114,7 +114,7 @@
     1.4  text {* Reverse order *}
     1.5  
     1.6  lemma order_reverse:
     1.7 -  "order (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x)"
     1.8 +  "order (op \<ge>) (op >)"
     1.9  by unfold_locales
    1.10     (simp add: less_le, auto intro: antisym order_trans)
    1.11  
    1.12 @@ -187,7 +187,7 @@
    1.13  text {* Reverse order *}
    1.14  
    1.15  lemma linorder_reverse:
    1.16 -  "linorder (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x)"
    1.17 +  "linorder (op \<ge>) (op >)"
    1.18  by unfold_locales
    1.19    (simp add: less_le, auto intro: antisym order_trans simp add: linear)
    1.20  
    1.21 @@ -597,15 +597,6 @@
    1.22  lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
    1.23  lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
    1.24  
    1.25 -lemmas min_le_iff_disj = linorder_class.min_le_iff_disj
    1.26 -lemmas le_max_iff_disj = linorder_class.le_max_iff_disj
    1.27 -lemmas min_less_iff_disj = linorder_class.min_less_iff_disj
    1.28 -lemmas less_max_iff_disj = linorder_class.less_max_iff_disj
    1.29 -lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj
    1.30 -lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj
    1.31 -lemmas split_min = linorder_class.split_min
    1.32 -lemmas split_max = linorder_class.split_max
    1.33 -
    1.34  
    1.35  subsection {* Bounded quantifiers *}
    1.36  
     2.1 --- a/src/Pure/Isar/class.ML	Fri Oct 19 19:45:29 2007 +0200
     2.2 +++ b/src/Pure/Isar/class.ML	Fri Oct 19 19:45:31 2007 +0200
     2.3 @@ -664,7 +664,7 @@
     2.4    |> synchronize_syntax thy sups base_sort
     2.5    |> Context.proof_map (
     2.6        Syntax.add_term_check 0 "class" sort_term_check
     2.7 -      #> Syntax.add_term_uncheck (~10) "class" sort_term_uncheck)
     2.8 +      #> Syntax.add_term_uncheck 0 "class" sort_term_uncheck)
     2.9  
    2.10  fun init class ctxt =
    2.11    let
    2.12 @@ -821,8 +821,6 @@
    2.13      thy'
    2.14      |> Sign.hide_consts_i false [c''] (*FIXME*)
    2.15      |> Sign.declare_const pos (c, ty'', mx) |> snd
    2.16 -    |> Sign.parent_path
    2.17 -    |> Sign.sticky_prefix prfx
    2.18      |> Thm.add_def false (c, def_eq)
    2.19      |>> Thm.symmetric
    2.20      |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
    2.21 @@ -847,14 +845,19 @@
    2.22        |> map (Pattern.rewrite_term thy rews []);
    2.23    in Term.betapplys (head', ts') end;
    2.24  
    2.25 -fun add_syntactic_const class prmode pos ((c, mx), dict) thy =
    2.26 +fun fold_aux_defs thy class =
    2.27 +  let
    2.28 +    val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy [class])
    2.29 +  in Pattern.rewrite_term thy rews [] end;
    2.30 +
    2.31 +fun add_syntactic_const class prmode pos ((c, mx), rhs) thy =
    2.32    let
    2.33      val prfx = class_prefix class;
    2.34      val thy' = thy |> Sign.add_path prfx;
    2.35      val phi = morphism thy class;
    2.36  
    2.37      val c' = Sign.full_name thy' c;
    2.38 -    val dict' = (expand_aux_abbrev thy' class o Morphism.term phi) dict;
    2.39 +    val dict' = (expand_aux_abbrev thy' class o Morphism.term phi) rhs;
    2.40      val dict'' = map_types Logic.unvarifyT dict';
    2.41      val ty' = Term.fastype_of dict'';
    2.42  
    2.43 @@ -867,7 +870,7 @@
    2.44      |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts dict') |> snd
    2.45      |> Sign.add_const_constraint (c', SOME ty')
    2.46      |> Sign.notation true prmode [(Const (c', ty'), mx)]
    2.47 -    |> register_operation class ((c', (dict, dict'')), NONE)
    2.48 +    |> register_operation class ((c', (dict', dict'')), NONE)
    2.49      |> Sign.restore_naming thy
    2.50      |> pair c'
    2.51    end;
     3.1 --- a/src/Tools/code/code_funcgr.ML	Fri Oct 19 19:45:29 2007 +0200
     3.2 +++ b/src/Tools/code/code_funcgr.ML	Fri Oct 19 19:45:31 2007 +0200
     3.3 @@ -302,7 +302,7 @@
     3.4      val drop = drop_classes thy tfrees;
     3.5      val instdefs = instances_of_consts thy algebra funcgr' c_exprs;
     3.6      val funcgr'' = ensure_consts thy algebra instdefs funcgr';
     3.7 -  in (f drop thm5 funcgr'' ct'' , funcgr'') end;
     3.8 +  in (f drop thm5 funcgr'' ct'', funcgr'') end;
     3.9  
    3.10  fun raw_eval_conv thy conv =
    3.11    let