ad 967c8a1eb6b1 (2): add functions accessing Theory_Data in parallel to those accessing 'mets = Unsynchronized.ref'
1 (* 6.8.02 change to Isabelle2002 caused error -- thy excluded !
3 Proving equations for primrec function(s) "InsSort.foldr" ...
4 GC #1.17.30.54.345.21479: (10 ms)
5 *** Definition of InsSort.ins :: "['a::ord list, 'a::ord] => 'a::ord list"
6 *** imposes additional sort constraints on the declared type of the constant
7 *** The error(s) above occurred in definition "InsSort.ins.ins_list_def (@@@)"
10 (* insertion sort, would need lists different from script-lists WN.11.00
11 WN.7.5.03: -"- started with someList :: 'a list => unl, fun dest_list
12 WN.8.5.03: error (@@@) remained with outcommenting foldr ?!?
16 theory InsSort imports "../ProgLang/Script" begin
20 (*foldr :: [['a,'b] => 'a, 'b list, 'a] => 'a
21 WN.8.5.03: already defined in Isabelle2002 (instantiated by Typefix):
22 "[[real, real] => real, real list, real] => real") : term
24 val t = str2term "foldr";
28 "[[RealDef.real, RealDef.real] => RealDef.real, RealDef.real List.list,
29 RealDef.real] => RealDef.real") : term
31 ins :: ['a list,'a] => 'a list
32 sort :: 'a list => 'a list
34 (*descriptions, script-id*)
35 unsorted :: 'a list => unl
36 sorted :: 'a list => unl
38 (*subproblem and script-name*)
39 Ins'_sort :: "['a list,
41 ("((Script Ins'_sort (_ =))//
45 ("((Script Sort (_ =))//
49 foldr_base "foldr f [] a = a"
50 foldr_rec "foldr f (x#xs) a = foldr f xs (f a x)"
55 (*primrec .. outcommented analoguous to ListC.thy*)
56 ins_base "ins [] a = [a]"
57 ins_rec "ins (x#xs) a = (if x < a then x#(ins xs a) else a#(x#xs))"
59 sort_def "sort ls = foldr ins ls []"
62 setup {* KEStore_Elems.add_pbts
63 [(prep_pbt @{theory "InsSort"}
64 (["functional"]:pblID,
65 [("#Given" ,["unsorted u_"]), ("#Find" ,["sorted s_"])], [])),
66 (prep_pbt @{theory "InsSort"}
67 (["inssort","functional"]:pblID,
68 [("#Given" ,["unsorted u_"]), ("#Find" ,["sorted s_"])], []))] *}
72 todo: implementation needs extra object-level lists **)
75 (prep_met @{theory "Diff"}
78 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
79 crls = Atools_rls, errpats = [], nrls = norm_Rational
80 (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
82 (prep_met @{theory "InsSort"} (*test-version for [#1,#3,#2] only: see *.sml*)
83 (["InsSort","sort"]:metID,
84 [("#Given" ,["unsorted u_"]),
85 ("#Find" ,["sorted s_"])
87 {rew_ord'="tless_true",rls'=eval_rls,calc = [], srls = e_rls, prls=e_rls,
88 crls = eval_rls, errpats = [], nrls = norm_Rational},
89 "Script Sort (u_::'a list) = (Rewrite_Set ins_sort False) u_"
92 setup {* KEStore_Elems.add_mets
93 [prep_met @{theory "Diff"}
95 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
96 crls = Atools_rls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
98 prep_met @{theory "InsSort"} (*test-version for [#1,#3,#2] only: see *.sml*)
99 (["InsSort","sort"]:metID,
100 [("#Given" ,["unsorted u_"]), ("#Find" ,["sorted s_"])],
101 {rew_ord'="tless_true",rls'=eval_rls,calc = [], srls = e_rls, prls=e_rls, crls = eval_rls,
102 errpats = [], nrls = norm_Rational},
103 "Script Sort (u_::'a list) = (Rewrite_Set ins_sort False) u_")]
105 setup {* KEStore_Elems.add_rlss [("ins_sort", (Context.theory_name @{theory}, ins_sort))] *}