Re: [isabelle] HTML string of term



Thanks Peter!

But still, it is not obvious to me how to obtain a similar
html_string_of_term function in Isabelle 2016.

fun html_string_of_term ctxt t =
    let
      val ctxt' = ctxt |> Config.put show_markup false
                       |> Config.put show_question_marks false
    in HTML.html_mode (Syntax.string_of_term ctxt') t end

Should I try to get 'keywords' and 'spans' from a term? What I am trying to
do is to report the performance of an inductive prover in html format (I
attach a report generated with Isabelle 2015).

Best,


2016-06-30 19:35 GMT-05:00 Peter Gammie <peteg42 at gmail.com>:

> Omar,
>
> Digging into the hg repo, I found:
>
> changeset:   61379:c57820ceead3
> user:        wenzelm
> date:        Fri Oct 09 21:16:00 2015 +0200
> summary:     more direct HTML presentation, without print mode;
>
> and this part of that patch may answer your question:
>
> diff --git a/src/Pure/PIDE/resources.ML b/src/Pure/PIDE/resources.ML
> --- a/src/Pure/PIDE/resources.ML
> +++ b/src/Pure/PIDE/resources.ML
> @@ -159,7 +159,7 @@
>      fun init () =
>        begin_theory master_dir header parents
>        |> Present.begin_theory update_time
> -          (fn () => HTML.html_mode (implode o map
> (Thy_Syntax.present_span keywords)) spans);
> +        (fn () => implode (map (HTML.present_span keywords) spans));
>
>      val (results, thy) =
>        cond_timeit true (âtheory " ^ quote name)
>
> cheers,
> peter
>
> > On 1 Jul 2016, at 04:14, Omar Montano Rivas <omarmrivas at gmail.com>
> wrote:
> >
> > Hi,
> >
> > Is there a way to obtain a string from a term ready to be presented in a
> > html page in Isabelle 2016?
> >
> > I have the following code which works in Isabelle 2015:
> >
> > fun html_string_of_term ctxt t =
> >    let
> >      val ctxt' = ctxt |> Config.put show_markup false
> >                       |> Config.put show_question_marks false
> >    in HTML.html_mode (Syntax.string_of_term ctxt') t end
> >
> > but it seems that the method HTML.html_mode no longer exists in isabelle
> > 2016.
> >
> > Thanks,
> > --
> > Dr. Omar MontaÃo Rivas
> > Profesor-Investigador UPSLP
> > e-mail: omar.montano at upslp.edu.mx
> > Tel. +52 (444) 8126367 ext. 225
> > URL: http://atit.upslp.edu.mx/index.php/omarmrivas
>
> --
> http://peteg.org/
>
>


-- 
Dr. Omar MontaÃo Rivas
Profesor-Investigador UPSLP
e-mail: omar.montano at upslp.edu.mx
Tel. +52 (444) 8126367 ext. 225
URL: http://atit.upslp.edu.mx/index.php/omarmrivas
Title: Results for induct_auto_breadth_first (Isabelle2015: May 2015)

Results for induct_auto_breadth_first

Proved Not proved Proved % Not proved % Avg cpu time Avg proved Avg not proved
61 234 20.6779661017% 79.3220338983% 47.2203268746s 11.3121780984s 56.5809981368s
No. Conjecture File Proved Time
0 (!!x y z. bin_distrib.times x (bin_distrib.plus y z) = bin_distrib.plus (bin_distrib.times x y) (bin_distrib.times x z)) ==> (!!x y z. bin_distrib.times x (bin_distrib.plus y z) = bin_distrib.plus (bin_distrib.times x y) (bin_distrib.times x z)) bin_distrib.thy 70.620187
1 (!!x y. toNat (bin_plus.plus x y) = plus2 (toNat x) (toNat y)) ==> (!!x y. toNat (bin_plus.plus x y) = plus2 (toNat x) (toNat y)) bin_plus.thy 71.056965
2 (!!x y z. bin_plus_assoc.plus x (bin_plus_assoc.plus y z) = bin_plus_assoc.plus (bin_plus_assoc.plus x y) z) ==> (!!x y z. bin_plus_assoc.plus x (bin_plus_assoc.plus y z) = bin_plus_assoc.plus (bin_plus_assoc.plus x y) z) bin_plus_assoc.thy 70.355378
3 (!!x y. bin_plus_comm.plus x y = bin_plus_comm.plus y x) ==> (!!x y. bin_plus_comm.plus x y = bin_plus_comm.plus y x) bin_plus_comm.thy 13.407736
4 (!!n. toNat (s n) = S (toNat n)) ==> (!!n. toNat (s n) = S (toNat n)) bin_s.thy 70.432041
5 (!!x y. toNat (bin_times.times x y) = mult (toNat x) (toNat y)) ==> (!!x y. toNat (bin_times.times x y) = mult (toNat x) (toNat y)) bin_times.thy 71.212275
6 (!!x y z. bin_times_assoc.times x (bin_times_assoc.times y z) = bin_times_assoc.times (bin_times_assoc.times x y) z) ==> (!!x y z. bin_times_assoc.times x (bin_times_assoc.times y z) = bin_times_assoc.times (bin_times_assoc.times x y) z) bin_times_assoc.thy 70.20727
7 (!!x y. bin_times_comm.times x y = bin_times_comm.times y x) ==> (!!x y. bin_times_comm.times x y = bin_times_comm.times y x) bin_times_comm.thy 70.367421
8 (!!xs ys. escape xs = escape ys ==> xs = ys) ==> (!!xs ys. escape xs = escape ys ==> xs = ys) escape_Injective.thy 11.337252
9 (!!xs. all (λxa. ok xa) (escape xs)) ==> (!!xs. all (λxa. ok xa) (escape xs)) escape_NoSpecial.thy 10.200143
10 (!!n x y z. fermat_last.plus (pow (S x) (S (S (S n)))) (pow (S y) (S (S (S n)))) pow (S z) (S (S (S n)))) ==> (!!n x y z. fermat_last.plus (pow (S x) (S (S (S n)))) (pow (S y) (S (S (S n)))) pow (S z) (S (S (S n)))) fermat_last.thy 8.443014
11 (!!h. heap h ==> listDeleteMinimum (toList2 h) = maybeToList (deleteMinimum h)) ==> (!!h. heap h ==> listDeleteMinimum (toList2 h) = maybeToList (deleteMinimum h)) heap_deleteMinimum.thy 71.986352
12 (!!x h. heap h ==> toList2 (insert2 x h) = listInsert x (toList2 h)) ==> (!!x h. heap h ==> toList2 (insert2 x h) = listInsert x (toList2 h)) heap_insert.thy 71.240061
13 (!!x y. [| heap x; heap y |] ==> toList2 (merge x y) = mergeLists (toList2 x) (toList2 y)) ==> (!!x y. [| heap x; heap y |] ==> toList2 (merge x y) = mergeLists (toList2 x) (toList2 y)) heap_merge.thy 71.822258
14 (!!h. heap h ==> listMinimum (toList2 h) = minimum h) ==> (!!h. heap h ==> listMinimum (toList2 h) = minimum h) heap_minimum.thy 12.599195
15 (!!x y. count x (hsort y) = count x y) ==> (!!x y. count x (hsort y) = count x y) heap_SortPermutes.thy 71.734746
16 (!!x. ordered (hsort x)) ==> (!!x. ordered (hsort x)) heap_SortSorts.thy 71.17349
17 (!!x y z. int_add_assoc.plus x (int_add_assoc.plus y z) = int_add_assoc.plus (int_add_assoc.plus x y) z) ==> (!!x y z. int_add_assoc.plus x (int_add_assoc.plus y z) = int_add_assoc.plus (int_add_assoc.plus x y) z) int_add_assoc.thy 69.228879
18 (!!x y. int_add_comm.plus x y = int_add_comm.plus y x) ==> (!!x y. int_add_comm.plus x y = int_add_comm.plus y x) int_add_comm.thy 69.209178
19 (!!x. x = int_add_ident_left.plus zero x) ==> (!!x. x = int_add_ident_left.plus zero x) int_add_ident_left.thy 9.072363
20 (!!x. x = int_add_ident_right.plus x zero) ==> (!!x. x = int_add_ident_right.plus x zero) int_add_ident_right.thy 9.124087
21 (!!x. int_add_inv_left.plus (neg x) x = zero) ==> (!!x. int_add_inv_left.plus (neg x) x = zero) int_add_inv_left.thy 12.38298
22 (!!x. int_add_inv_right.plus x (neg x) = zero) ==> (!!x. int_add_inv_right.plus x (neg x) = zero) int_add_inv_right.thy 12.325678
23 (!!x y z. int_left_distrib.times x (int_left_distrib.plus y z) = int_left_distrib.plus (int_left_distrib.times x y) (int_left_distrib.times x z)) ==> (!!x y z. int_left_distrib.times x (int_left_distrib.plus y z) = int_left_distrib.plus (int_left_distrib.times x y) (int_left_distrib.times x z)) int_left_distrib.thy 70.154126
24 (!!x y z. int_mul_assoc.times x (int_mul_assoc.times y z) = int_mul_assoc.times (int_mul_assoc.times x y) z) ==> (!!x y z. int_mul_assoc.times x (int_mul_assoc.times y z) = int_mul_assoc.times (int_mul_assoc.times x y) z) int_mul_assoc.thy 69.83637
25 (!!x y. int_mul_comm.times x y = int_mul_comm.times y x) ==> (!!x y. int_mul_comm.times x y = int_mul_comm.times y x) int_mul_comm.thy 69.786701
26 (!!x. x = int_mul_ident_left.times one x) ==> (!!x. x = int_mul_ident_left.times one x) int_mul_ident_left.thy 9.97141
27 (!!x. x = int_mul_ident_right.times x one) ==> (!!x. x = int_mul_ident_right.times x one) int_mul_ident_right.thy 10.077942
28 (!!x y z. int_right_distrib.times (int_right_distrib.plus x y) z = int_right_distrib.plus (int_right_distrib.times x z) (int_right_distrib.times y z)) ==> (!!x y z. int_right_distrib.times (int_right_distrib.plus x y) z = int_right_distrib.plus (int_right_distrib.times x z) (int_right_distrib.times y z)) int_right_distrib.thy 70.178103
29 (!!xs ys zs. list_append_inj_1.append xs zs = list_append_inj_1.append ys zs ==> xs = ys) ==> (!!xs ys zs. list_append_inj_1.append xs zs = list_append_inj_1.append ys zs ==> xs = ys) list_append_inj_1.thy 8.683961
30 (!!xs ys zs. list_append_inj_2.append xs ys = list_append_inj_2.append xs zs ==> ys = zs) ==> (!!xs ys zs. list_append_inj_2.append xs ys = list_append_inj_2.append xs zs ==> ys = zs) list_append_inj_2.thy 8.692828
31 (!!m f g. bind (bind m f) g = bind m (λxa. bind (f xa) g)) ==> (!!m f g. bind (bind m f) g = bind m (λxa. bind (f xa) g)) list_assoc.thy 68.507862
32 (!!f xs. concat2 (map2 f xs) = bind xs f) ==> (!!f xs. concat2 (map2 f xs) = bind xs f) list_concat_map_bind.thy 9.293828
33 (!!x xs. elem x xs ==> count x (nub xs) = S Z) ==> (!!x xs. elem x xs ==> count x (nub xs) = S Z) list_count_nub.thy 11.727907
34 (!!x xs. deleteAll x xs = delete x xs ==> le (count x xs) (S Z)) ==> (!!x xs. deleteAll x xs = delete x xs ==> le (count x xs) (S Z)) list_deleteAll_count.thy 9.815629
35 (!!x xs. elem x xs ==> elem x (nub xs)) ==> (!!x xs. elem x xs ==> elem x (nub xs)) list_elem_nub_l.thy 9.462946
36 (!!x xs. elem x (nub xs) ==> elem x xs) ==> (!!x xs. elem x (nub xs) ==> elem x xs) list_elem_nub_r.thy 9.447416
37 (!!xs. interleave (evens xs) (odds xs) = xs) ==> (!!xs. interleave (evens xs) (odds xs) = xs) list_Interleave.thy 8.765551
38 (!!xs. nub (nub xs) = nub xs) ==> (!!xs. nub (nub xs) = nub xs) list_nub_nub.thy 69.325228
39 (!!xs. list_PairEvens.even (list_PairEvens.length xs) ==> map2 (λxa. list_PairEvens.fst xa) (pairs xs) = evens xs) ==> (!!xs. list_PairEvens.even (list_PairEvens.length xs) ==> map2 (λxa. list_PairEvens.fst xa) (pairs xs) = evens xs) list_PairEvens.thy 10.689935
40 (!!xs. map2 (λxa. list_PairOdds.snd xa) (pairs xs) = odds xs) ==> (!!xs. map2 (λxa. list_PairOdds.snd xa) (pairs xs) = odds xs) list_PairOdds.thy 9.858202
41 (!!xs. list_PairUnpair.even (list_PairUnpair.length xs) ==> unpair (pairs xs) = xs) ==> (!!xs. list_PairUnpair.even (list_PairUnpair.length xs) ==> unpair (pairs xs) = xs) list_PairUnpair.thy 10.892624
42 (!!x xs ys. [| elem x xs; isPermutation xs ys |] ==> elem x ys) ==> (!!x xs ys. [| elem x xs; isPermutation xs ys |] ==> elem x ys) list_perm_elem.thy 9.586743
43 (!!xs. isPermutation xs xs) ==> (!!xs. isPermutation xs xs) list_perm_refl.thy 69.568857
44 (!!xs ys. isPermutation xs ys ==> isPermutation ys xs) ==> (!!xs ys. isPermutation xs ys ==> isPermutation ys xs) list_perm_symm.thy 69.605929
45 (!!xs ys zs. [| isPermutation xs ys; isPermutation ys zs |] ==> isPermutation xs zs) ==> (!!xs ys zs. [| isPermutation xs ys; isPermutation ys zs |] ==> isPermutation xs zs) list_perm_trans.thy 69.543859
46 (!!x f. bind (return x) f = f x) ==> (!!x f. bind (return x) f = f x) list_return_1.thy 8.778336
47 (!!xs. bind xs (λxa. return xa) = xs) ==> (!!xs. bind xs (λxa. return xa) = xs) list_return_2.thy 8.720329
48 (!!xs. map2 (λxa. list_Select.fst xa) (select2 xs) = xs) ==> (!!xs. map2 (λxa. list_Select.fst xa) (select2 xs) = xs) list_Select.thy 9.742031
49 (!!xs. all (λxa. zisPermutation xa xs) (propSelectPermutations (select2 xs))) ==> (!!xs. all (λxa. zisPermutation xa xs) (propSelectPermutations (select2 xs))) list_SelectPermutations.thy 10.492546
50 (!!f xs. weirdconcat (map2 f xs) = bind xs f) ==> (!!f xs. weirdconcat (map2 f xs) = bind xs f) list_weird_concat_map_bind.thy 69.309976
51 (!!x. concat2 x = weirdconcat x) ==> (!!x. concat2 x = weirdconcat x) list_weird_is_normal.thy 9.131987
52 (!!x xs. zelem x xs ==> zcount x (znub xs) = S Z) ==> (!!x xs. zelem x xs ==> zcount x (znub xs) = S Z) list_z_count_nub.thy 69.536755
53 (!!x xs. zdeleteAll x xs = zdelete x xs ==> le (zcount x xs) (S Z)) ==> (!!x xs. zdeleteAll x xs = zdelete x xs ==> le (zcount x xs) (S Z)) list_z_deleteAll_count.thy 69.494176
54 (!!x xs. zelem x xs ==> zelem x (znub xs)) ==> (!!x xs. zelem x xs ==> zelem x (znub xs)) list_z_elem_nub_l.thy 52.480422
55 (!!x xs. zelem x (znub xs) ==> zelem x xs) ==> (!!x xs. zelem x (znub xs) ==> zelem x xs) list_z_elem_nub_r.thy 11.829751
56 (!!xs. znub (znub xs) = znub xs) ==> (!!xs. znub (znub xs) = znub xs) list_z_nub_nub.thy 68.748424
57 (!!x xs ys. [| zelem x xs; zisPermutation xs ys |] ==> zelem x ys) ==> (!!x xs ys. [| zelem x xs; zisPermutation xs ys |] ==> zelem x ys) list_z_perm_elem.thy 12.325247
58 (!!xs. zisPermutation xs xs) ==> (!!xs. zisPermutation xs xs) list_z_perm_refl.thy 9.072856
59 (!!xs ys. zisPermutation xs ys ==> zisPermutation ys xs) ==> (!!xs ys. zisPermutation xs ys ==> zisPermutation ys xs) list_z_perm_symm.thy 69.047113
60 (!!xs ys zs. [| zisPermutation xs ys; zisPermutation ys zs |] ==> zisPermutation xs zs) ==> (!!xs ys zs. [| zisPermutation xs ys; zisPermutation ys zs |] ==> zisPermutation xs zs) list_z_perm_trans.thy 68.870038
61 (!!n. [| m_dom n; n 100 |] ==> m n = 91) ==> (!!n. [| m_dom n; n 100 |] ==> m n = 91) mccarthy91_M1.thy 7.330986
62 (!!n. [| m_dom n; 101 n |] ==> m n = n - 10) ==> (!!n. [| m_dom n; 101 n |] ==> m n = n - 10) mccarthy91_M2.thy 7.339755
63 (!!m n. mod2_dom (m, n) ==> mod2 m n = modstructural m n) ==> (!!m n. mod2_dom (m, n) ==> mod2 m n = modstructural m n) mod_same.thy 27.959979
64 (!!x y z. accaltmul x (accaltmul y z) = accaltmul (accaltmul x y) z) ==> (!!x y z. accaltmul x (accaltmul y z) = accaltmul (accaltmul x y) z) nat_acc_alt_mul_assoc.thy 68.084091
65 (!!x y. accaltmul x y = accaltmul y x) ==> (!!x y. accaltmul x y = accaltmul y x) nat_acc_alt_mul_comm.thy 68.126302
66 (!!x y. accaltmul x y = mult x y) ==> (!!x y. accaltmul x y = mult x y) nat_acc_alt_mul_same.thy 68.397341
67 (!!x y z. accplus x (accplus y z) = accplus (accplus x y) z) ==> (!!x y z. accplus x (accplus y z) = accplus (accplus x y) z) nat_acc_plus_assoc.thy 67.978796
68 (!!x y. accplus x y = accplus y x) ==> (!!x y. accplus x y = accplus y x) nat_acc_plus_comm.thy 67.893249
69 (!!x y. nat_acc_plus_same.plus x y = accplus x y) ==> (!!x y. nat_acc_plus_same.plus x y = accplus x y) nat_acc_plus_same.thy 8.297949
70 (!!x y z. altmul x (altmul y z) = altmul (altmul x y) z) ==> (!!x y z. altmul x (altmul y z) = altmul (altmul x y) z) nat_alt_mul_assoc.thy 68.024493
71 (!!x y. altmul x y = altmul y x) ==> (!!x y. altmul x y = altmul y x) nat_alt_mul_comm.thy 68.020639
72 (!!x y. altmul x y = mult x y) ==> (!!x y. altmul x y = mult x y) nat_alt_mul_same.thy 68.077371
73 (!!x y. [| ge x y; ge y x |] ==> x = y) ==> (!!x y. [| ge x y; ge y x |] ==> x = y) nat_boring_ge_antisym.thy 7.934434
74 (!!x. ge x x) ==> (!!x. ge x x) nat_boring_ge_reflexive.thy 7.934319
75 (!!x y z. [| ge x y; ge y z |] ==> ge x z) ==> (!!x y z. [| ge x y; ge y z |] ==> ge x z) nat_boring_ge_trans.thy 7.945294
76 (!!x y. gt x y ==> ¬ gt y x) ==> (!!x y. gt x y ==> ¬ gt y x) nat_boring_gt_asymmetric.thy 7.873347
77 (!!x. ¬ gt x x) ==> (!!x. ¬ gt x x) nat_boring_gt_irreflexive.thy 7.960158
78 (!!x y z. [| gt x y; gt y z |] ==> gt x z) ==> (!!x y z. [| gt x y; gt y z |] ==> gt x z) nat_boring_gt_trans.thy 7.917797
79 (!!x y. max2 x (min2 x y) = x) ==> (!!x y. max2 x (min2 x y) = x) nat_boring_max_min_abs.thy 8.023902
80 (!!x y z. min2 x (max2 y z) = max2 (min2 x y) (min2 x z)) ==> (!!x y z. min2 x (max2 y z) = max2 (min2 x y) (min2 x z)) nat_boring_max_min_distrib.thy 68.059366
81 (!!x y z. min2 x (min2 y z) = min2 (min2 x y) z) ==> (!!x y z. min2 x (min2 y z) = min2 (min2 x y) z) nat_boring_min_assoc.thy 67.901125
82 (!!x y. min2 x y = min2 y x) ==> (!!x y. min2 x y = min2 y x) nat_boring_min_comm.thy 8.176305
83 (!!x. min2 x x = x) ==> (!!x. min2 x x = x) nat_boring_min_idem.thy 8.198159
84 (!!x. equal2 x x) ==> (!!x. equal2 x x) nat_eq_refl.thy 7.901538
85 (!!x y. equal2 x y ==> equal2 y x) ==> (!!x y. equal2 x y ==> equal2 y x) nat_eq_sym.thy 7.889388
86 (!!x y z. [| equal2 x y; equal2 y z |] ==> equal2 x z) ==> (!!x y z. [| equal2 x y; equal2 y z |] ==> equal2 x z) nat_eq_trans.thy 7.846504
87 (!!x y. [| le x y; le y x |] ==> x = y) ==> (!!x y. [| le x y; le y x |] ==> x = y) nat_le_antisym.thy 7.927613
88 (!!x y. [| ge x y; le x y |] ==> equal2 x y) ==> (!!x y. [| ge x y; le x y |] ==> equal2 x y) nat_le_ge_eq.thy 8.250954
89 (!!x y. [| le x y; unequal x y |] ==> lt x y) ==> (!!x y. [| le x y; unequal x y |] ==> lt x y) nat_le_ne_lt.thy 8.601857
90 (!!x. le x x) ==> (!!x. le x x) nat_le_reflexive.thy 7.922905
91 (!!x y z. [| le x y; le y z |] ==> le x z) ==> (!!x y z. [| le x y; le y z |] ==> le x z) nat_le_trans.thy 7.903054
92 (!!x y. lt x y ==> ¬ lt y x) ==> (!!x y. lt x y ==> ¬ lt y x) nat_lt_asymmetric.thy 7.8529
93 (!!x. ¬ lt x x) ==> (!!x. ¬ lt x x) nat_lt_irreflexive.thy 7.896736
94 (!!x y. lt y x ==> unequal x y) ==> (!!x y. lt y x ==> unequal x y) nat_lt_ne.thy 8.141907
95 (!!x y z. [| lt x y; lt y z |] ==> lt x z) ==> (!!x y z. [| lt x y; lt y z |] ==> lt x z) nat_lt_trans.thy 7.907236
96 (!!x y z. max2 x (max2 y z) = max2 (max2 x y) z) ==> (!!x y z. max2 x (max2 y z) = max2 (max2 x y) z) nat_max_assoc.thy 67.89223
97 (!!x y. max2 x y = max2 y x) ==> (!!x y. max2 x y = max2 y x) nat_max_comm.thy 7.981254
98 (!!x. max2 x x = x) ==> (!!x. max2 x x = x) nat_max_idem.thy 7.782576
99 (!!x y. min2 x (max2 x y) = x) ==> (!!x y. min2 x (max2 x y) = x) nat_min_max_abs.thy 8.434682
100 (!!x y z. max2 x (min2 y z) = min2 (max2 x y) (max2 x z)) ==> (!!x y z. max2 x (min2 y z) = min2 (max2 x y) (max2 x z)) nat_min_max_distrib.thy 68.021566
101 (!!n. lt (pow (S (S Z)) (S (S (S (S n))))) (factorial (S (S (S (S n)))))) ==> (!!n. lt (pow (S (S Z)) (S (S (S (S n))))) (factorial (S (S (S (S n)))))) nat_pow_le_factorial.thy 68.369217
102 (!!x. pow (S Z) x = S Z) ==> (!!x. pow (S Z) x = S Z) nat_pow_one.thy 7.971004
103 (!!x y z. pow x (mult y z) = pow (pow x y) z) ==> (!!x y z. pow x (mult y z) = pow (pow x y) z) nat_pow_pow.thy 68.019903
104 (!!x y z. pow x (nat_pow_times.plus y z) = mult (pow x y) (pow x z)) ==> (!!x y z. pow x (nat_pow_times.plus y z) = mult (pow x y) (pow x z)) nat_pow_times.thy 68.083406
105 (!!n. cubes n = mult (sum n) (sum n)) ==> (!!n. cubes n = mult (sum n) (sum n)) nicomachus_theorem.thy 68.187348
106 (!!u v. linS u = linS v ==> u = v) ==> (!!u v. linS u = linS v ==> u = v) packrat_unambigPackrat.thy 11.689671
107 (!!n xs. prop_01.append (prop_01.take n xs) (prop_01.drop n xs) = xs) ==> (!!n xs. prop_01.append (prop_01.take n xs) (prop_01.drop n xs) = xs) prop_01.thy 9.289484
108 (!!x y. prop_02.length (prop_02.append x y) = prop_02.length (prop_02.append y x)) ==> (!!x y. prop_02.length (prop_02.append x y) = prop_02.length (prop_02.append y x)) prop_02.thy 10.247044
109 (!!x y. prop_03.length (prop_03.append x y) = prop_03.plus (prop_03.length y) (prop_03.length x)) ==> (!!x y. prop_03.length (prop_03.append x y) = prop_03.plus (prop_03.length y) (prop_03.length x)) prop_03.thy 10.971601
110 (!!x. prop_04.length (prop_04.append x x) = double (prop_04.length x)) ==> (!!x. prop_04.length (prop_04.append x x) = double (prop_04.length x)) prop_04.thy 69.051087
111 (!!x. prop_05.length (prop_05.rev x) = prop_05.length x) ==> (!!x. prop_05.length (prop_05.rev x) = prop_05.length x) prop_05.thy 69.227024
112 (!!x y. prop_06.length (prop_06.rev (prop_06.append x y)) = prop_06.plus (prop_06.length x) (prop_06.length y)) ==> (!!x y. prop_06.length (prop_06.rev (prop_06.append x y)) = prop_06.plus (prop_06.length x) (prop_06.length y)) prop_06.thy 69.235099
113 (!!x y. prop_07.length (qrev x y) = prop_07.plus (prop_07.length x) (prop_07.length y)) ==> (!!x y. prop_07.length (qrev x y) = prop_07.plus (prop_07.length x) (prop_07.length y)) prop_07.thy 10.841273
114 (!!x y z. prop_08.drop x (prop_08.drop y z) = prop_08.drop y (prop_08.drop x z)) ==> (!!x y z. prop_08.drop x (prop_08.drop y z) = prop_08.drop y (prop_08.drop x z)) prop_08.thy 68.968932
115 (!!x y z w. prop_09.drop w (prop_09.drop x (prop_09.drop y z)) = prop_09.drop y (prop_09.drop x (prop_09.drop w z))) ==> (!!x y z w. prop_09.drop w (prop_09.drop x (prop_09.drop y z)) = prop_09.drop y (prop_09.drop x (prop_09.drop w z))) prop_09.thy 68.942085
116 (!!x. prop_10.rev (prop_10.rev x) = x) ==> (!!x. prop_10.rev (prop_10.rev x) = x) prop_10.thy 68.498543
117 (!!x y. prop_11.rev (prop_11.append (prop_11.rev x) (prop_11.rev y)) = prop_11.append y x) ==> (!!x y. prop_11.rev (prop_11.append (prop_11.rev x) (prop_11.rev y)) = prop_11.append y x) prop_11.thy 68.396319
118 (!!x y. qrev x y = prop_12.append (prop_12.rev x) y) ==> (!!x y. qrev x y = prop_12.append (prop_12.rev x) y) prop_12.thy 68.608521
119 (!!x. half (prop_13.plus x x) = x) ==> (!!x. half (prop_13.plus x x) = x) prop_13.thy 67.961629
120 (!!x. prop_14.sorted (isort x)) ==> (!!x. prop_14.sorted (isort x)) prop_14.thy 69.287165
121 (!!x. prop_15.plus x (S x) = S (prop_15.plus x x)) ==> (!!x. prop_15.plus x (S x) = S (prop_15.plus x x)) prop_15.thy 67.895212
122 (!!x. prop_16.even (prop_16.plus x x)) ==> (!!x. prop_16.even (prop_16.plus x x)) prop_16.thy 67.941648
123 (!!x y. prop_17.rev (prop_17.rev (prop_17.append x y)) = prop_17.append (prop_17.rev (prop_17.rev x)) (prop_17.rev (prop_17.rev y))) ==> (!!x y. prop_17.rev (prop_17.rev (prop_17.append x y)) = prop_17.append (prop_17.rev (prop_17.rev x)) (prop_17.rev (prop_17.rev y))) prop_17.thy 68.465462
124 (!!x y. prop_18.rev (prop_18.append (prop_18.rev x) y) = prop_18.append (prop_18.rev y) x) ==> (!!x y. prop_18.rev (prop_18.append (prop_18.rev x) y) = prop_18.append (prop_18.rev y) x) prop_18.thy 68.426053
125 (!!x y. prop_19.append (prop_19.rev (prop_19.rev x)) y = prop_19.rev (prop_19.rev (prop_19.append x y))) ==> (!!x y. prop_19.append (prop_19.rev (prop_19.rev x)) y = prop_19.rev (prop_19.rev (prop_19.append x y))) prop_19.thy 68.450846
126 (!!x. prop_20.even (prop_20.length (prop_20.append x x))) ==> (!!x. prop_20.even (prop_20.length (prop_20.append x x))) prop_20.thy 69.101568
127 (!!x y. prop_21.rotate (prop_21.length x) (prop_21.append x y) = prop_21.append y x) ==> (!!x y. prop_21.rotate (prop_21.length x) (prop_21.append x y) = prop_21.append y x) prop_21.thy 69.21474
128 (!!x y. prop_22.even (prop_22.length (prop_22.append x y)) = prop_22.even (prop_22.length (prop_22.append y x))) ==> (!!x y. prop_22.even (prop_22.length (prop_22.append x y)) = prop_22.even (prop_22.length (prop_22.append y x))) prop_22.thy 69.181752
129 (!!x y. half (prop_23.length (prop_23.append x y)) = half (prop_23.length (prop_23.append y x))) ==> (!!x y. half (prop_23.length (prop_23.append x y)) = half (prop_23.length (prop_23.append y x))) prop_23.thy 69.203588
130 (!!x y. prop_24.even (prop_24.plus x y) = prop_24.even (prop_24.plus y x)) ==> (!!x y. prop_24.even (prop_24.plus x y) = prop_24.even (prop_24.plus y x)) prop_24.thy 68.042863
131 (!!x y. prop_25.even (prop_25.length (prop_25.append x y)) = prop_25.even (prop_25.plus (prop_25.length y) (prop_25.length x))) ==> (!!x y. prop_25.even (prop_25.length (prop_25.append x y)) = prop_25.even (prop_25.plus (prop_25.length y) (prop_25.length x))) prop_25.thy 69.296705
132 (!!x y. half (prop_26.plus x y) = half (prop_26.plus y x)) ==> (!!x y. half (prop_26.plus x y) = half (prop_26.plus y x)) prop_26.thy 67.989569
133 (!!x. prop_27.rev x = qrev x nil2) ==> (!!x. prop_27.rev x = qrev x nil2) prop_27.thy 68.616078
134 (!!x. revflat x = qrevflat x nil2) ==> (!!x. revflat x = qrevflat x nil2) prop_28.thy 68.745544
135 (!!x. prop_29.rev (qrev x nil2) = x) ==> (!!x. prop_29.rev (qrev x nil2) = x) prop_29.thy 68.596944
136 (!!x. prop_30.rev (prop_30.append (prop_30.rev x) nil2) = x) ==> (!!x. prop_30.rev (prop_30.append (prop_30.rev x) nil2) = x) prop_30.thy 68.386551
137 (!!x. qrev (qrev x nil2) nil2 = x) ==> (!!x. qrev (qrev x nil2) nil2 = x) prop_31.thy 68.267778
138 (!!x. prop_32.rotate (prop_32.length x) x = x) ==> (!!x. prop_32.rotate (prop_32.length x) x = x) prop_32.thy 69.17261
139 (!!x. fac x = qfac x one) ==> (!!x. fac x = qfac x one) prop_33.thy 68.141077
140 (!!x y. mult x y = mult2 x y Z) ==> (!!x y. mult x y = mult2 x y Z) prop_34.thy 68.029303
141 (!!x y. prop_35.exp x y = qexp x y one) ==> (!!x y. prop_35.exp x y = qexp x y one) prop_35.thy 68.1074
142 (!!x y z. elem x y ==> elem x (prop_36.append y z)) ==> (!!x y z. elem x y ==> elem x (prop_36.append y z)) prop_36.thy 11.695822
143 (!!x y z. elem x z ==> elem x (prop_37.append y z)) ==> (!!x y z. elem x z ==> elem x (prop_37.append y z)) prop_37.thy 9.23722
144 (!!x y z. [| elem x y; elem x z |] ==> elem x (prop_38.append y z)) ==> (!!x y z. [| elem x y; elem x z |] ==> elem x (prop_38.append y z)) prop_38.thy 9.235734
145 (!!x y z. elem x (prop_39.drop y z) ==> elem x z) ==> (!!x y z. elem x (prop_39.drop y z) ==> elem x z) prop_39.thy 9.240559
146 (!!x y. subset2 x y ==> union2 x y = y) ==> (!!x y. subset2 x y ==> union2 x y = y) prop_40.thy 9.700314
147 (!!x y. subset2 x y ==> intersect2 x y = x) ==> (!!x y. subset2 x y ==> intersect2 x y = x) prop_41.thy 9.749594
148 (!!x y z. elem x y ==> elem x (union2 y z)) ==> (!!x y z. elem x y ==> elem x (union2 y z)) prop_42.thy 11.824833
149 (!!x y z. elem x y ==> elem x (union2 z y)) ==> (!!x y z. elem x y ==> elem x (union2 z y)) prop_43.thy 9.203883
150 (!!x y z. [| elem x y; elem x z |] ==> elem x (intersect2 y z)) ==> (!!x y z. [| elem x y; elem x z |] ==> elem x (intersect2 y z)) prop_44.thy 9.231152
151 (!!x y. elem x (insert2 x y)) ==> (!!x y. elem x (insert2 x y)) prop_45.thy 11.026447
152 (!!x y z. x = y ==> elem x (insert2 y z)) ==> (!!x y z. x = y ==> elem x (insert2 y z)) prop_46.thy 24.010158
153 (!!x y z. unequal x y ==> elem x (insert2 y z) = elem x z) ==> (!!x y z. unequal x y ==> elem x (insert2 y z) = elem x z) prop_47.thy 9.436047
154 (!!x. prop_48.length (isort x) = prop_48.length x) ==> (!!x. prop_48.length (isort x) = prop_48.length x) prop_48.thy 69.185693
155 (!!x y. elem x (isort y) ==> elem x y) ==> (!!x y. elem x (isort y) ==> elem x y) prop_49.thy 9.321643
156 (!!x y. count x (isort y) = count x y) ==> (!!x y. count x (isort y) = count x y) prop_50.thy 69.270736
157 (!!xs x. prop_51.butlast (prop_51.append xs (cons2 x nil2)) = xs) ==> (!!xs x. prop_51.butlast (prop_51.append xs (cons2 x nil2)) = xs) prop_51.thy 8.401105
158 (!!n xs. count n xs = count n (prop_52.rev xs)) ==> (!!n xs. count n xs = count n (prop_52.rev xs)) prop_52.thy 69.243424
159 (!!n xs. count n xs = count n (prop_53.sort xs)) ==> (!!n xs. count n xs = count n (prop_53.sort xs)) prop_53.thy 69.277786
160 (!!n m. prop_54.minus (prop_54.plus m n) n = m) ==> (!!n m. prop_54.minus (prop_54.plus m n) n = m) prop_54.thy 67.888591
161 (!!n xs ys. prop_55.drop n (prop_55.append xs ys) = prop_55.append (prop_55.drop n xs) (prop_55.drop (prop_55.minus n (len xs)) ys)) ==> (!!n xs ys. prop_55.drop n (prop_55.append xs ys) = prop_55.append (prop_55.drop n xs) (prop_55.drop (prop_55.minus n (len xs)) ys)) prop_55.thy 9.49764
162 (!!n m xs. prop_56.drop n (prop_56.drop m xs) = prop_56.drop (prop_56.plus n m) xs) ==> (!!n m xs. prop_56.drop n (prop_56.drop m xs) = prop_56.drop (prop_56.plus n m) xs) prop_56.thy 69.014319
163 (!!n m xs. prop_57.drop n (prop_57.take m xs) = prop_57.take (prop_57.minus m n) (prop_57.drop n xs)) ==> (!!n m xs. prop_57.drop n (prop_57.take m xs) = prop_57.take (prop_57.minus m n) (prop_57.drop n xs)) prop_57.thy 69.187645
164 (!!n xs ys. prop_58.drop n (prop_58.zip xs ys) = prop_58.zip (prop_58.drop n xs) (prop_58.drop n ys)) ==> (!!n xs ys. prop_58.drop n (prop_58.zip xs ys) = prop_58.zip (prop_58.drop n xs) (prop_58.drop n ys)) prop_58.thy 69.970374
165 (!!xs ys. ys = nil2 ==> prop_59.last (prop_59.append xs ys) = prop_59.last xs) ==> (!!xs ys. ys = nil2 ==> prop_59.last (prop_59.append xs ys) = prop_59.last xs) prop_59.thy 9.069762
166 (!!xs ys. ¬ null ys ==> prop_60.last (prop_60.append xs ys) = prop_60.last ys) ==> (!!xs ys. ¬ null ys ==> prop_60.last (prop_60.append xs ys) = prop_60.last ys) prop_60.thy 69.056249
167 (!!xs ys. prop_61.last (prop_61.append xs ys) = lastOfTwo xs ys) ==> (!!xs ys. prop_61.last (prop_61.append xs ys) = lastOfTwo xs ys) prop_61.thy 69.266978
168 (!!xs x. ¬ null xs ==> prop_62.last (cons2 x xs) = prop_62.last xs) ==> (!!xs x. ¬ null xs ==> prop_62.last (cons2 x xs) = prop_62.last xs) prop_62.thy 8.998722
169 (!!n xs. lt n (len xs) ==> prop_63.last (prop_63.drop n xs) = prop_63.last xs) ==> (!!n xs. lt n (len xs) ==> prop_63.last (prop_63.drop n xs) = prop_63.last xs) prop_63.thy 69.194899
170 (!!x xs. prop_64.last (prop_64.append xs (cons2 x nil2)) = x) ==> (!!x xs. prop_64.last (prop_64.append xs (cons2 x nil2)) = x) prop_64.thy 68.975457
171 (!!i m. lt i (S (prop_65.plus m i))) ==> (!!i m. lt i (S (prop_65.plus m i))) prop_65.thy 68.011283
172 (!!q xs. le (len (prop_66.filter q xs)) (len xs)) ==> (!!q xs. le (len (prop_66.filter q xs)) (len xs)) prop_66.thy 69.160426
173 (!!xs. len (prop_67.butlast xs) = prop_67.minus (len xs) (S Z)) ==> (!!xs. len (prop_67.butlast xs) = prop_67.minus (len xs) (S Z)) prop_67.thy 9.241709
174 (!!n xs. le (len (delete n xs)) (len xs)) ==> (!!n xs. le (len (delete n xs)) (len xs)) prop_68.thy 69.30053
175 (!!n m. le n (prop_69.plus m n)) ==> (!!n m. le n (prop_69.plus m n)) prop_69.thy 67.991654
176 (!!m n. le m n ==> le m (S n)) ==> (!!m n. le m n ==> le m (S n)) prop_70.thy 8.038062
177 (!!x y xs. ¬ equal2 x y ==> elem x (ins y xs) = elem x xs) ==> (!!x y xs. ¬ equal2 x y ==> elem x (ins y xs) = elem x xs) prop_71.thy 9.525973
178 (!!i xs. prop_72.rev (prop_72.drop i xs) = prop_72.take (prop_72.minus (len xs) i) (prop_72.rev xs)) ==> (!!i xs. prop_72.rev (prop_72.drop i xs) = prop_72.take (prop_72.minus (len xs) i) (prop_72.rev xs)) prop_72.thy 69.506906
179 (!!p xs. prop_73.rev (prop_73.filter p xs) = prop_73.filter p (prop_73.rev xs)) ==> (!!p xs. prop_73.rev (prop_73.filter p xs) = prop_73.filter p (prop_73.rev xs)) prop_73.thy 68.632123
180 (!!i xs. prop_74.rev (prop_74.take i xs) = prop_74.drop (prop_74.minus (len xs) i) (prop_74.rev xs)) ==> (!!i xs. prop_74.rev (prop_74.take i xs) = prop_74.drop (prop_74.minus (len xs) i) (prop_74.rev xs)) prop_74.thy 69.539922
181 (!!n m xs. prop_75.plus (count n xs) (count n (cons2 m nil2)) = count n (cons2 m xs)) ==> (!!n m xs. prop_75.plus (count n xs) (count n (cons2 m nil2)) = count n (cons2 m xs)) prop_75.thy 9.380522
182 (!!n m xs. ¬ equal2 n m ==> count n (prop_76.append xs (cons2 m nil2)) = count n xs) ==> (!!n m xs. ¬ equal2 n m ==> count n (prop_76.append xs (cons2 m nil2)) = count n xs) prop_76.thy 9.233988
183 (!!x xs. prop_77.sorted xs ==> prop_77.sorted (prop_77.insort x xs)) ==> (!!x xs. prop_77.sorted xs ==> prop_77.sorted (prop_77.insort x xs)) prop_77.thy 69.169566
184 (!!xs. prop_78.sorted (prop_78.sort xs)) ==> (!!xs. prop_78.sorted (prop_78.sort xs)) prop_78.thy 69.311313
185 (!!m n k. prop_79.minus (prop_79.minus (S m) n) (S k) = prop_79.minus (prop_79.minus m n) k) ==> (!!m n k. prop_79.minus (prop_79.minus (S m) n) (S k) = prop_79.minus (prop_79.minus m n) k) prop_79.thy 15.166993
186 (!!n xs ys. prop_80.take n (prop_80.append xs ys) = prop_80.append (prop_80.take n xs) (prop_80.take (prop_80.minus n (len xs)) ys)) ==> (!!n xs ys. prop_80.take n (prop_80.append xs ys) = prop_80.append (prop_80.take n xs) (prop_80.take (prop_80.minus n (len xs)) ys)) prop_80.thy 9.394922
187 (!!n m xs. prop_81.take n (prop_81.drop m xs) = prop_81.drop m (prop_81.take (prop_81.plus n m) xs)) ==> (!!n m xs. prop_81.take n (prop_81.drop m xs) = prop_81.drop m (prop_81.take (prop_81.plus n m) xs)) prop_81.thy 69.20161
188 (!!n xs ys. prop_82.take n (prop_82.zip xs ys) = prop_82.zip (prop_82.take n xs) (prop_82.take n ys)) ==> (!!n xs ys. prop_82.take n (prop_82.zip xs ys) = prop_82.zip (prop_82.take n xs) (prop_82.take n ys)) prop_82.thy 70.086745
189 (!!xs ys zs. prop_83.zip (prop_83.append xs ys) zs = prop_83.append (prop_83.zip xs (prop_83.take (len xs) zs)) (prop_83.zip ys (prop_83.drop (len xs) zs))) ==> (!!xs ys zs. prop_83.zip (prop_83.append xs ys) zs = prop_83.append (prop_83.zip xs (prop_83.take (len xs) zs)) (prop_83.zip ys (prop_83.drop (len xs) zs))) prop_83.thy 70.390512
190 (!!xs ys zs. prop_84.zip xs (prop_84.append ys zs) = prop_84.append (prop_84.zip (prop_84.take (len ys) xs) ys) (prop_84.zip (prop_84.drop (len ys) xs) zs)) ==> (!!xs ys zs. prop_84.zip xs (prop_84.append ys zs) = prop_84.append (prop_84.zip (prop_84.take (len ys) xs) ys) (prop_84.zip (prop_84.drop (len ys) xs) zs)) prop_84.thy 70.585719
191 (!!xs ys. len xs = len ys ==> prop_85.zip (prop_85.rev xs) (prop_85.rev ys) = prop_85.rev (prop_85.zip xs ys)) ==> (!!xs ys. len xs = len ys ==> prop_85.zip (prop_85.rev xs) (prop_85.rev ys) = prop_85.rev (prop_85.zip xs ys)) prop_85.thy 70.390209
192 (!!x y xs. lt x y ==> elem x (ins y xs) = elem x xs) ==> (!!x y xs. lt x y ==> elem x (ins y xs) = elem x xs) prop_86.thy 69.407964
193 (!!p s. recognise (Star p) s = recognise (Star (deeps p)) s) ==> (!!p s. recognise (Star p) s = recognise (Star (deeps p)) s) regexp_Deeps.thy 72.51526
194 (!!p q r s. recognise (Plus p (Plus q r)) s = recognise (Plus (Plus p q) r) s) ==> (!!p q r s. recognise (Plus p (Plus q r)) s = recognise (Plus (Plus p q) r) s) regexp_PlusAssociative.thy 72.558854
195 (!!p q s. recognise (Plus p q) s = recognise (Plus q p) s) ==> (!!p q s. recognise (Plus p q) s = recognise (Plus q p) s) regexp_PlusCommutative.thy 72.634871
196 (!!p s. recognise (Plus p p) s = recognise p s) ==> (!!p s. recognise (Plus p p) s = recognise p s) regexp_PlusIdempotent.thy 72.880255
197 (!!a s. recognise (Atom a) s = eqList s (cons2 a nil2)) ==> (!!a s. recognise (Atom a) s = eqList s (cons2 a nil2)) regexp_RecAtom.thy 72.807583
198 (!!s. recognise R.Eps s = null s) ==> (!!s. recognise R.Eps s = null s) regexp_RecEps.thy 13.083918
199 (!!s. ¬ recognise Nil2 s) ==> (!!s. ¬ recognise Nil2 s) regexp_RecNil.thy 12.922417
200 (!!p q s. recognise (Plus p q) s = (recognise p s recognise q s)) ==> (!!p q s. recognise (Plus p q) s = (recognise p s recognise q s)) regexp_RecPlus.thy 72.959011
201 (!!p q s. recognise (Seq p q) s = or2 (propRecSeq p q (regexp_RecSeq.split s))) ==> (!!p q s. recognise (Seq p q) s = or2 (propRecSeq p q (regexp_RecSeq.split s))) regexp_RecSeq.thy 74.418307
202 (!!p s. recognise (Star p) s = (null s recognise (Seq p (Star p)) s)) ==> (!!p s. recognise (Star p) s = (null s recognise (Seq p (Star p)) s)) regexp_RecStar.thy 73.202396
203 (!!r s. recognise (regexp_Reverse.rev r) s = recognise r (reverse s)) ==> (!!r s. recognise (regexp_Reverse.rev r) s = recognise r (reverse s)) regexp_Reverse.thy 73.208955
204 (!!p q r s. recognise (Seq p (Seq q r)) s = recognise (Seq (Seq p q) r) s) ==> (!!p q r s. recognise (Seq p (Seq q r)) s = recognise (Seq (Seq p q) r) s) regexp_SeqAssociative.thy 72.910936
205 (!!p q r s. recognise (Seq p (Plus q r)) s = recognise (Plus (Seq p q) (Seq p r)) s) ==> (!!p q r s. recognise (Seq p (Plus q r)) s = recognise (Plus (Seq p q) (Seq p r)) s) regexp_SeqDistrPlus.thy 73.412353
206 (!!p s. recognise (Star p) s = recognise (Plus R.Eps (Seq p (Star p))) s) ==> (!!p s. recognise (Star p) s = recognise (Plus R.Eps (Seq p (Star p))) s) regexp_Star.thy 73.743609
207 (!!xs ys. isRelaxedPrefix xs ys = spec xs ys) ==> (!!xs ys. isRelaxedPrefix xs ys = spec xs ys) relaxedprefix_correct.thy 71.102908
208 (!!xs ys. isRelaxedPrefix xs (relaxedprefix_is_prefix_1.append xs ys)) ==> (!!xs ys. isRelaxedPrefix xs (relaxedprefix_is_prefix_1.append xs ys)) relaxedprefix_is_prefix_1.thy 70.397262
209 (!!x xs ys zs. isRelaxedPrefix (relaxedprefix_is_prefix_2.append (relaxedprefix_is_prefix_2.append xs (cons2 x nil2)) ys) (relaxedprefix_is_prefix_2.append (relaxedprefix_is_prefix_2.append xs ys) zs)) ==> (!!x xs ys zs. isRelaxedPrefix (relaxedprefix_is_prefix_2.append (relaxedprefix_is_prefix_2.append xs (cons2 x nil2)) ys) (relaxedprefix_is_prefix_2.append (relaxedprefix_is_prefix_2.append xs ys) zs)) relaxedprefix_is_prefix_2.thy 70.277739
210 (!!x xs ys. isRelaxedPrefix (relaxedprefix_is_prefix_3.append xs (cons2 x nil2)) (relaxedprefix_is_prefix_3.append xs ys)) ==> (!!x xs ys. isRelaxedPrefix (relaxedprefix_is_prefix_3.append xs (cons2 x nil2)) (relaxedprefix_is_prefix_3.append xs ys)) relaxedprefix_is_prefix_3.thy 70.23452
211 (!!x xs ys. isRelaxedPrefix (cons2 x xs) (relaxedprefix_is_prefix_4.append xs ys)) ==> (!!x xs ys. isRelaxedPrefix (cons2 x xs) (relaxedprefix_is_prefix_4.append xs ys)) relaxedprefix_is_prefix_4.thy 70.19854
212 (!!n xs. mod2_dom (n, rotate_mod.length xs) ==> rotate_mod.rotate n xs = rotate_mod.append (rotate_mod.drop (mod2 n (rotate_mod.length xs)) xs) (rotate_mod.take (mod2 n (rotate_mod.length xs)) xs)) ==> (!!n xs. mod2_dom (n, rotate_mod.length xs) ==> rotate_mod.rotate n xs = rotate_mod.append (rotate_mod.drop (mod2 n (rotate_mod.length xs)) xs) (rotate_mod.take (mod2 n (rotate_mod.length xs)) xs)) rotate_mod.thy 70.470309
213 (!!n xs. rotate_self.rotate n (rotate_self.append xs xs) = rotate_self.append (rotate_self.rotate n xs) (rotate_self.rotate n xs)) ==> (!!n xs. rotate_self.rotate n (rotate_self.append xs xs) = rotate_self.append (rotate_self.rotate n xs) (rotate_self.rotate n xs)) rotate_self.thy 69.776196
214 (!!xs. rotate_snoc.rotate (rotate_snoc.length xs) xs = xs) ==> (!!xs. rotate_snoc.rotate (rotate_snoc.length xs) xs = xs) rotate_snoc.thy 69.507846
215 (!!n xs. rotate_snoc_self.rotate n (rotate_snoc_self.append xs xs) = rotate_snoc_self.append (rotate_snoc_self.rotate n xs) (rotate_snoc_self.rotate n xs)) ==> (!!n xs. rotate_snoc_self.rotate n (rotate_snoc_self.append xs xs) = rotate_snoc_self.append (rotate_snoc_self.rotate n xs) (rotate_snoc_self.rotate n xs)) rotate_snoc_self.thy 69.647239
216 (!!n xs. rotate_structural_mod.rotate n xs = rotate_structural_mod.append (rotate_structural_mod.drop (modstructural n (rotate_structural_mod.length xs)) xs) (rotate_structural_mod.take (modstructural n (rotate_structural_mod.length xs)) xs)) ==> (!!n xs. rotate_structural_mod.rotate n xs = rotate_structural_mod.append (rotate_structural_mod.drop (modstructural n (rotate_structural_mod.length xs)) xs) (rotate_structural_mod.take (modstructural n (rotate_structural_mod.length xs)) xs)) rotate_structural_mod.thy 70.451897
217 (!!u v. lin u = lin v ==> u = v) ==> (!!u v. lin u = lin v ==> u = v) simp_expr_unambig1.thy 10.572635
218 (!!u v. lin u = lin v ==> u = v) ==> (!!u v. lin u = lin v ==> u = v) simp_expr_unambig2.thy 10.602825
219 (!!u v. lin u = lin v ==> u = v) ==> (!!u v. lin u = lin v ==> u = v) simp_expr_unambig3.thy 10.668774
220 (!!u v. lin u = lin v ==> u = v) ==> (!!u v. lin u = lin v ==> u = v) simp_expr_unambig4.thy 10.632997
221 (!!u v. lin u = lin v ==> u = v) ==> (!!u v. lin u = lin v ==> u = v) simp_expr_unambig5.thy 11.647516
222 (!!x y. zcount x (isort y) = zcount x y) ==> (!!x y. zcount x (isort y) = zcount x y) sort_ISortCount.thy 69.603022
223 (!!x. zisPermutation (isort x) x) ==> (!!x. zisPermutation (isort x) x) sort_ISortPermutes.thy 69.354619
224 (!!x. zordered (isort x)) ==> (!!x. zordered (isort x)) sort_ISortSorts.thy 68.924567
225 (!!x y. zcount x (nstoogesort2 y) = zcount x y) ==> (!!x y. zcount x (nstoogesort2 y) = zcount x y) sort_NStoogeSort2Count.thy 71.762378
226 (!!x. nstoogesort2 x = isort x) ==> (!!x. nstoogesort2 x = isort x) sort_NStoogeSort2IsSort.thy 11.855424
227 (!!x. zisPermutation (nstoogesort2 x) x) ==> (!!x. zisPermutation (nstoogesort2 x) x) sort_NStoogeSort2Permutes.thy 72.121381
228 (!!x. zordered (nstoogesort2 x)) ==> (!!x. zordered (nstoogesort2 x)) sort_NStoogeSort2Sorts.thy 71.725171
229 (!!x y. zcount x (nstoogesort y) = zcount x y) ==> (!!x y. zcount x (nstoogesort y) = zcount x y) sort_NStoogeSortCount.thy 71.791066
230 (!!x. nstoogesort x = isort x) ==> (!!x. nstoogesort x = isort x) sort_NStoogeSortIsSort.thy 11.89711
231 (!!x. zisPermutation (nstoogesort x) x) ==> (!!x. zisPermutation (nstoogesort x) x) sort_NStoogeSortPermutes.thy 72.05802
232 (!!x. zordered (nstoogesort x)) ==> (!!x. zordered (nstoogesort x)) sort_NStoogeSortSorts.thy 71.706379
233 (!!x y. zcount x (stoogesort2 y) = zcount x y) ==> (!!x y. zcount x (stoogesort2 y) = zcount x y) sort_StoogeSort2Count.thy 71.70904
234 (!!x. stoogesort2 x = isort x) ==> (!!x. stoogesort2 x = isort x) sort_StoogeSort2IsSort.thy 11.208312
235 (!!x. zisPermutation (stoogesort2 x) x) ==> (!!x. zisPermutation (stoogesort2 x) x) sort_StoogeSort2Permutes.thy 71.3558
236 (!!x. zordered (stoogesort2 x)) ==> (!!x. zordered (stoogesort2 x)) sort_StoogeSort2Sorts.thy 71.011346
237 (!!x y. zcount x (stoogesort y) = zcount x y) ==> (!!x y. zcount x (stoogesort y) = zcount x y) sort_StoogeSortCount.thy 71.689783
238 (!!x. stoogesort x = isort x) ==> (!!x. stoogesort x = isort x) sort_StoogeSortIsSort.thy 11.379635
239 (!!x. zisPermutation (stoogesort x) x) ==> (!!x. zisPermutation (stoogesort x) x) sort_StoogeSortPermutes.thy 71.507972
240 (!!x. zordered (stoogesort x)) ==> (!!x. zordered (stoogesort x)) sort_StoogeSortSorts.thy 71.034318
241 (!!x y. zcount x (tsort y) = zcount x y) ==> (!!x y. zcount x (tsort y) = zcount x y) sort_TSortCount.thy 70.923388
242 (!!x. tsort x = isort x) ==> (!!x. tsort x = isort x) sort_TSortIsSort.thy 70.427277
243 (!!x. zisPermutation (tsort x) x) ==> (!!x. zisPermutation (tsort x) x) sort_TSortPermutes.thy 70.75927
244 (!!x. zordered (tsort x)) ==> (!!x. zordered (tsort x)) sort_TSortSorts.thy 70.372144
245 (!!p. flatten2 p nil2 = flatten0 p) ==> (!!p. flatten2 p nil2 = flatten0 p) tree_Flatten2.thy 70.15765
246 (!!x y t. ¬ equal2 x y ==> count y (flatten (add x t) nil2) = count y (flatten t nil2)) ==> (!!x y t. ¬ equal2 x y ==> count y (flatten (add x t) nil2) = count y (flatten t nil2)) tree_sort_AddDifferent.thy 58.247859
247 (!!x t. count x (flatten (add x t) nil2) = S (count x (flatten t nil2))) ==> (!!x t. count x (flatten (add x t) nil2) = S (count x (flatten t nil2))) tree_sort_AddSame.thy 71.110769
248 (!!x y. count x (tsort y) = count x y) ==> (!!x y. count x (tsort y) = count x y) tree_sort_SortPermutes.thy 71.298702
249 (!!x. ordered (tsort x)) ==> (!!x. ordered (tsort x)) tree_sort_SortSorts.thy 71.107968
250 (!!p a b. [| zelem a (flatten0 p); zelem b (flatten0 p) |] ==> zelem a (flatten0 (swap a b p)) zelem b (flatten0 (swap a b p))) ==> (!!p a b. [| zelem a (flatten0 p); zelem b (flatten0 p) |] ==> zelem a (flatten0 (swap a b p)) zelem b (flatten0 (swap a b p))) tree_SwapAB.thy 70.433401
251 (!!x1 x2 x3 x4 x5. add3 (add3 x1 x2 x3) x4 x5 = add3 x1 x2 (add3 x3 x4 x5)) ==> (!!x1 x2 x3 x4 x5. add3 (add3 x1 x2 x3) x4 x5 = add3 x1 x2 (add3 x3 x4 x5)) weird_nat_add3_assoc1.thy 8.345732
252 (!!x1 x2 x3 x4 x5. add3 (add3 x1 x2 x3) x4 x5 = add3 x1 (add3 x2 x3 x4) x5) ==> (!!x1 x2 x3 x4 x5. add3 (add3 x1 x2 x3) x4 x5 = add3 x1 (add3 x2 x3 x4) x5) weird_nat_add3_assoc2.thy 32.84501
253 (!!x1 x2 x3 x4 x5. add3 x1 (add3 x2 x3 x4) x5 = add3 x1 x2 (add3 x3 x4 x5)) ==> (!!x1 x2 x3 x4 x5. add3 x1 (add3 x2 x3 x4) x5 = add3 x1 x2 (add3 x3 x4 x5)) weird_nat_add3_assoc3.thy 49.001601
254 (!!x y z. add3 x y z = add3 y x z) ==> (!!x y z. add3 x y z = add3 y x z) weird_nat_add3_comm12.thy 9.450155
255 (!!x y z. add3 x y z = add3 z y x) ==> (!!x y z. add3 x y z = add3 z y x) weird_nat_add3_comm13.thy 10.955537
256 (!!x y z. add3 x y z = add3 x z y) ==> (!!x y z. add3 x y z = add3 x z y) weird_nat_add3_comm23.thy 9.264705
257 (!!x y z. add3 x y z = add3 y x z) ==> (!!x y z. add3 x y z = add3 y x z) weird_nat_add3_rot.thy 9.317288
258 (!!x y z. add3 x y z = add3 z x y) ==> (!!x y z. add3 x y z = add3 z x y) weird_nat_add3_rrot.thy 10.0389
259 (!!x y z. add3 x y z = add3acc x y z) ==> (!!x y z. add3 x y z = add3acc x y z) weird_nat_add3_same.thy 68.393321
260 (!!x y z. add3 x y z = weird_nat_add3_spec.plus x (weird_nat_add3_spec.plus y z)) ==> (!!x y z. add3 x y z = weird_nat_add3_spec.plus x (weird_nat_add3_spec.plus y z)) weird_nat_add3_spec.thy 8.261464
261 (!!x1 x2 x3 x4 x5. add3acc (add3acc x1 x2 x3) x4 x5 = add3acc x1 x2 (add3acc x3 x4 x5)) ==> (!!x1 x2 x3 x4 x5. add3acc (add3acc x1 x2 x3) x4 x5 = add3acc x1 x2 (add3acc x3 x4 x5)) weird_nat_add3acc_assoc1.thy 25.403472
262 (!!x1 x2 x3 x4 x5. add3acc (add3acc x1 x2 x3) x4 x5 = add3acc x1 (add3acc x2 x3 x4) x5) ==> (!!x1 x2 x3 x4 x5. add3acc (add3acc x1 x2 x3) x4 x5 = add3acc x1 (add3acc x2 x3 x4) x5) weird_nat_add3acc_assoc2.thy 36.638099
263 (!!x1 x2 x3 x4 x5. add3acc x1 (add3acc x2 x3 x4) x5 = add3acc x1 x2 (add3acc x3 x4 x5)) ==> (!!x1 x2 x3 x4 x5. add3acc x1 (add3acc x2 x3 x4) x5 = add3acc x1 x2 (add3acc x3 x4 x5)) weird_nat_add3acc_assoc3.thy 68.205264
264 (!!x y z. add3acc x y z = add3acc y x z) ==> (!!x y z. add3acc x y z = add3acc y x z) weird_nat_add3acc_comm12.thy 68.191903
265 (!!x y z. add3acc x y z = add3acc z y x) ==> (!!x y z. add3acc x y z = add3acc z y x) weird_nat_add3acc_comm13.thy 68.329493
266 (!!x y z. add3acc x y z = add3acc x z y) ==> (!!x y z. add3acc x y z = add3acc x z y) weird_nat_add3acc_comm23.thy 68.274878
267 (!!x y z. add3acc x y z = add3acc y x z) ==> (!!x y z. add3acc x y z = add3acc y x z) weird_nat_add3acc_rot.thy 68.253045
268 (!!x y z. add3acc x y z = add3acc z x y) ==> (!!x y z. add3acc x y z = add3acc z x y) weird_nat_add3acc_rrot.thy 68.283508
269 (!!x y z. add3acc x y z = weird_nat_add3acc_spec.plus x (weird_nat_add3acc_spec.plus y z)) ==> (!!x y z. add3acc x y z = weird_nat_add3acc_spec.plus x (weird_nat_add3acc_spec.plus y z)) weird_nat_add3acc_spec.thy 10.813298
270 (!!x y z. mul2 x (mul2 y z) = mul2 (mul2 x y) z) ==> (!!x y z. mul2 x (mul2 y z) = mul2 (mul2 x y) z) weird_nat_mul2_assoc.thy 68.348566
271 (!!x y. mul2 x y = mul2 y x) ==> (!!x y. mul2 x y = mul2 y x) weird_nat_mul2_comm.thy 68.351782
272 (!!x1 x2 x3 x4 x5. mul3 (mul3 x1 x2 x3) x4 x5 = mul3 x1 x2 (mul3 x3 x4 x5)) ==> (!!x1 x2 x3 x4 x5. mul3 (mul3 x1 x2 x3) x4 x5 = mul3 x1 x2 (mul3 x3 x4 x5)) weird_nat_mul3_assoc1.thy 68.97589
273 (!!x1 x2 x3 x4 x5. mul3 (mul3 x1 x2 x3) x4 x5 = mul3 x1 (mul3 x2 x3 x4) x5) ==> (!!x1 x2 x3 x4 x5. mul3 (mul3 x1 x2 x3) x4 x5 = mul3 x1 (mul3 x2 x3 x4) x5) weird_nat_mul3_assoc2.thy 69.011361
274 (!!x1 x2 x3 x4 x5. mul3 x1 (mul3 x2 x3 x4) x5 = mul3 x1 x2 (mul3 x3 x4 x5)) ==> (!!x1 x2 x3 x4 x5. mul3 x1 (mul3 x2 x3 x4) x5 = mul3 x1 x2 (mul3 x3 x4 x5)) weird_nat_mul3_assoc3.thy 69.392498
275 (!!x y z. mul3 x y z = mul3 y x z) ==> (!!x y z. mul3 x y z = mul3 y x z) weird_nat_mul3_comm12.thy 69.011996
276 (!!x y z. mul3 x y z = mul3 z y x) ==> (!!x y z. mul3 x y z = mul3 z y x) weird_nat_mul3_comm13.thy 68.963751
277 (!!x y z. mul3 x y z = mul3 x z y) ==> (!!x y z. mul3 x y z = mul3 x z y) weird_nat_mul3_comm23.thy 69.07085
278 (!!x y z. mul3 x y z = mul3 y x z) ==> (!!x y z. mul3 x y z = mul3 y x z) weird_nat_mul3_rot.thy 68.964568
279 (!!x y z. mul3 x y z = mul3 z x y) ==> (!!x y z. mul3 x y z = mul3 z x y) weird_nat_mul3_rrot.thy 68.994129
280 (!!x y z. mul3 x y z = mul3acc x y z) ==> (!!x y z. mul3 x y z = mul3acc x y z) weird_nat_mul3_same.thy 69.717675
281 (!!x y z. mul3 x y z = mult (mult x y) z) ==> (!!x y z. mul3 x y z = mult (mult x y) z) weird_nat_mul3_spec.thy 69.291949
282 (!!x1 x2 x3acc x4 x5. mul3acc (mul3acc x1 x2 x3acc) x4 x5 = mul3acc x1 x2 (mul3acc x3acc x4 x5)) ==> (!!x1 x2 x3acc x4 x5. mul3acc (mul3acc x1 x2 x3acc) x4 x5 = mul3acc x1 x2 (mul3acc x3acc x4 x5)) weird_nat_mul3acc_assoc1.thy 69.151581
283 (!!x1 x2 x3acc x4 x5. mul3acc (mul3acc x1 x2 x3acc) x4 x5 = mul3acc x1 (mul3acc x2 x3acc x4) x5) ==> (!!x1 x2 x3acc x4 x5. mul3acc (mul3acc x1 x2 x3acc) x4 x5 = mul3acc x1 (mul3acc x2 x3acc x4) x5) weird_nat_mul3acc_assoc2.thy 69.033559
284 (!!x1 x2 x3acc x4 x5. mul3acc x1 (mul3acc x2 x3acc x4) x5 = mul3acc x1 x2 (mul3acc x3acc x4 x5)) ==> (!!x1 x2 x3acc x4 x5. mul3acc x1 (mul3acc x2 x3acc x4) x5 = mul3acc x1 x2 (mul3acc x3acc x4 x5)) weird_nat_mul3acc_assoc3.thy 69.123922
285 (!!x y z. mul3acc x y z = mul3acc y x z) ==> (!!x y z. mul3acc x y z = mul3acc y x z) weird_nat_mul3acc_comm12.thy 69.021613
286 (!!x y z. mul3acc x y z = mul3acc z y x) ==> (!!x y z. mul3acc x y z = mul3acc z y x) weird_nat_mul3acc_comm13.thy 69.065365
287 (!!x y z. mul3acc x y z = mul3acc x z y) ==> (!!x y z. mul3acc x y z = mul3acc x z y) weird_nat_mul3acc_comm23.thy 69.086191
288 (!!x y z. mul3acc x y z = mul3acc y x z) ==> (!!x y z. mul3acc x y z = mul3acc y x z) weird_nat_mul3acc_rot.thy 69.103617
289 (!!x y z. mul3acc x y z = mul3acc z x y) ==> (!!x y z. mul3acc x y z = mul3acc z x y) weird_nat_mul3acc_rrot.thy 69.095496
290 (!!x y z. mul3acc x y z = mult (mult x y) z) ==> (!!x y z. mul3acc x y z = mult (mult x y) z) weird_nat_mul3acc_spec.thy 69.162028
291 (!!a b c d e. opp (opp a b Z Z) c d e = opp a (opp b c Z Z) d e) ==> (!!a b c d e. opp (opp a b Z Z) c d e = opp a (opp b c Z Z) d e) weird_nat_op_assoc.thy 68.300298
292 (!!x a b c d. opp (opp x a a a) b c d = opp a (opp b x b b) c d) ==> (!!x a b c d. opp (opp x a a a) b c d = opp a (opp b x b b) c d) weird_nat_op_assoc2.thy 68.250017
293 (!!a b c d. opp a b c d = opp b a d c) ==> (!!a b c d. opp a b c d = opp b a d c) weird_nat_op_comm_comm.thy 68.224757
294 (!!a b c d. opp a b c d = weird_nat_op_spec.plus (weird_nat_op_spec.plus (mult a b) c) d) ==> (!!a b c d. opp a b c d = weird_nat_op_spec.plus (weird_nat_op_spec.plus (mult a b) c) d) weird_nat_op_spec.thy 68.630564


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.