simplified Abel_Cancel setup;
authorwenzelm
Wed Jun 18 18:54:57 2008 +0200 (2008-06-18)
changeset 272507eef2b183032
parent 27249 f339dc43ce9f
child 27251 121991a4884d
simplified Abel_Cancel setup;
src/HOL/OrderedGroup.thy
src/Provers/Arith/abel_cancel.ML
     1.1 --- a/src/HOL/OrderedGroup.thy	Wed Jun 18 16:55:44 2008 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Wed Jun 18 18:54:57 2008 +0200
     1.3 @@ -1372,8 +1372,8 @@
     1.4  lemmas diff_le_0_iff_le [simp] = le_iff_diff_le_0 [symmetric]
     1.5  
     1.6  ML {*
     1.7 -structure ab_group_add_cancel = Abel_Cancel(
     1.8 -struct
     1.9 +structure ab_group_add_cancel = Abel_Cancel
    1.10 +(
    1.11  
    1.12  (* term order for abelian groups *)
    1.13  
    1.14 @@ -1400,25 +1400,25 @@
    1.15      "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
    1.16  end;
    1.17  
    1.18 +val eq_reflection = @{thm eq_reflection};
    1.19 +  
    1.20 +val T = @{typ "'a::ab_group_add"};
    1.21 +
    1.22  val cancel_ss = HOL_basic_ss settermless termless_agrp
    1.23    addsimprocs [add_ac_proc] addsimps
    1.24    [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def},
    1.25     @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
    1.26     @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
    1.27     @{thm minus_add_cancel}];
    1.28 -  
    1.29 -val eq_reflection = @{thm eq_reflection};
    1.30 +
    1.31 +val sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}];
    1.32    
    1.33 -val thy_ref = Theory.check_thy @{theory};
    1.34 -
    1.35 -val T = @{typ "'a\<Colon>ab_group_add"};
    1.36 -
    1.37  val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
    1.38  
    1.39  val dest_eqI = 
    1.40    fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
    1.41  
    1.42 -end);
    1.43 +);
    1.44  *}
    1.45  
    1.46  ML {*
     2.1 --- a/src/Provers/Arith/abel_cancel.ML	Wed Jun 18 16:55:44 2008 +0200
     2.2 +++ b/src/Provers/Arith/abel_cancel.ML	Wed Jun 18 18:54:57 2008 +0200
     2.3 @@ -12,10 +12,10 @@
     2.4  
     2.5  signature ABEL_CANCEL =
     2.6  sig
     2.7 +  val eq_reflection   : thm           (*object-equality to meta-equality*)
     2.8 +  val T               : typ           (*the type of group elements*)
     2.9    val cancel_ss       : simpset       (*abelian group cancel simpset*)
    2.10 -  val thy_ref         : theory_ref    (*signature of the theory of the group*)
    2.11 -  val T               : typ           (*the type of group elements*)
    2.12 -  val eq_reflection   : thm           (*object-equality to meta-equality*)
    2.13 +  val sum_pats        : cterm list
    2.14    val eqI_rules       : thm list
    2.15    val dest_eqI        : thm -> term
    2.16  end;
    2.17 @@ -89,9 +89,7 @@
    2.18  
    2.19  val sum_conv =
    2.20    Simplifier.mk_simproc "cancel_sums"
    2.21 -    (map (Drule.cterm_fun Logic.varify o Thm.read_cterm (Theory.deref thy_ref))
    2.22 -      [("x + y", Data.T), ("x - y", Data.T)])  (* FIXME depends on concrete syntax *)
    2.23 -    (K sum_proc);
    2.24 +    (map (Drule.cterm_fun Logic.varify) Data.sum_pats) (K sum_proc);
    2.25  
    2.26  
    2.27  (*A simproc to cancel like terms on the opposite sides of relations:
    2.28 @@ -109,6 +107,6 @@
    2.29  
    2.30  val rel_conv =
    2.31    Simplifier.mk_simproc "cancel_relations"
    2.32 -    (map (Thm.cterm_of (Theory.deref thy_ref) o Data.dest_eqI) eqI_rules) (K rel_proc);
    2.33 +    (map (fn th => Thm.cterm_of (Thm.theory_of_thm th) (Data.dest_eqI th)) eqI_rules) (K rel_proc);
    2.34  
    2.35  end;