40 in Pretty.writeln (Pretty.big_list "Algebraic structures:" (map pretty_struct structs)) end; |
40 in Pretty.writeln (Pretty.big_list "Algebraic structures:" (map pretty_struct structs)) end; |
41 |
41 |
42 |
42 |
43 (** Method **) |
43 (** Method **) |
44 |
44 |
45 fun struct_tac ((s, ts), simps) = |
45 fun struct_tac ctxt ((s, ts), simps) = |
46 let |
46 let |
47 val ops = map (fst o Term.strip_comb) ts; |
47 val ops = map (fst o Term.strip_comb) ts; |
48 fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops |
48 fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops |
49 | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops; |
49 | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops; |
50 fun less (a, b) = (Term_Ord.term_lpo ord (a, b) = LESS); |
50 fun less (a, b) = (Term_Ord.term_lpo ord (a, b) = LESS); |
51 in asm_full_simp_tac (HOL_ss addsimps simps |> Simplifier.set_termless less) end; |
51 in asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps simps |> Simplifier.set_termless less) end; |
52 |
52 |
53 fun algebra_tac ctxt = |
53 fun algebra_tac ctxt = |
54 EVERY' (map (fn s => TRY o struct_tac s) (Data.get (Context.Proof ctxt))); |
54 EVERY' (map (fn s => TRY o struct_tac ctxt s) (Data.get (Context.Proof ctxt))); |
55 |
55 |
56 |
56 |
57 (** Attribute **) |
57 (** Attribute **) |
58 |
58 |
59 fun add_struct_thm s = |
59 fun add_struct_thm s = |