1.1 --- a/src/Tools/isac/Build_Isac.thy Mon Jul 15 08:28:50 2013 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Jul 17 07:32:53 2013 +0200
1.3 @@ -2,9 +2,10 @@
1.4 Author: Walther Neuper, TU Graz, 100808
1.5 (c) due to copyright terms
1.6
1.7 -create a new Isac heap (via ~~/src/Tools/isac/ROOT.ML) by
1.8 -$ cd /usr/local/isabisac/src/Tools/isac
1.9 -$ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac
1.10 +For creating a heap image of isac see ~~/ROOT.
1.11 +
1.12 +ATTENTION: no errors in this theory do not mean that there are no errors in Isac;
1.13 +errors are rigorously detected when creating a heap.
1.14 *)
1.15
1.16 header {* Loading the isac mathengine *}
1.17 @@ -21,7 +22,7 @@
1.18 "use_thy ProgLang/Tools"
1.19 "use_thy ProgLang/Script"
1.20 use "ProgLang/scrtools.sml"
1.21 -*) "~~/src/Tools/isac/ProgLang/ProgLang"
1.22 +*) "ProgLang/ProgLang"
1.23
1.24 (* use "Interpret/mstools.sml"
1.25 use "Interpret/ctree.sml"
1.26 @@ -34,23 +35,23 @@
1.27 use "Interpret/solve.sml"
1.28 use "Interpret/inform.sml"
1.29 use "Interpret/mathengine.sml"
1.30 -*) "~~/src/Tools/isac/Interpret/Interpret"
1.31 +*) "Interpret/Interpret"
1.32
1.33 -(* use "xmlsrc/mathml.sml"1491
1.34 +(* use "xmlsrc/mathml.sml"
1.35 use "xmlsrc/datatypes.sml"
1.36 use "xmlsrc/pbl-met-hierarchy.sml"
1.37 use "xmlsrc/thy-hierarchy.sml"
1.38 use "xmlsrc/interface-xml.sml"
1.39 -*) "~~/src/Tools/isac/xmlsrc/xmlsrc"
1.40 +*) "xmlsrc/xmlsrc"
1.41
1.42 (* use "Frontend/messages.sml"
1.43 use "Frontend/states.sml"
1.44 use "Frontend/interface.sml"
1.45
1.46 use "print_exn_G.sml"
1.47 -*) "~~/src/Tools/isac/Frontend/Frontend"
1.48 +*) "Frontend/Frontend"
1.49
1.50 - "~~/src/Tools/isac/Knowledge/Build_Thydata" (*imports Isac etc*)
1.51 + "Knowledge/Build_Thydata" (*imports Isac.thy etc*)
1.52
1.53 begin
1.54
2.1 --- a/src/Tools/isac/Build_Test_Isac.thy Mon Jul 15 08:28:50 2013 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,49 +0,0 @@
2.4 -(* Title: build and test isac
2.5 - Author: Walther Neuper, TU Graz, 100808
2.6 - (c) due to copyright terms
2.7 -
2.8 -$ cd /usr/local/Isabelle2009-1/src/Tools/isac
2.9 -$ /usr/local/isabisac/bin/isabelle emacs Build_Test_Isac.thy &
2.10 -$ /usr/local/isabisac/bin/isabelle jedit Build_Test_Isac.thy &
2.11 -
2.12 -create a new Isac heap (via ~~/ROOT.ML) with
2.13 -$ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac
2.14 -
2.15 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
2.16 - 10 20 30 40 50 60 70 80
2.17 -*)
2.18 -
2.19 -header {* Loading the isac mathengine *}
2.20 -
2.21 -theory Build_Test_Isac
2.22 -imports Complex_Main "ProgLang/ProgLang" "Knowledge/Isac" "Test_Isac"
2.23 -begin
2.24 -
2.25 -use_thy "Build_Isac"
2.26 -
2.27 -(* PROCEEDING WITH 'use testfile.sml" HERE DOESN'T WORK,
2.28 - because the 'imports "Knowledge/Isac" (in Test_Isac.thy) is required;
2.29 - the following kind of errors are raised:
2.30 -use "../../../test/Tools/isac/Interpret/calchead.sml"
2.31 -*** get_pbt not found: ["linear","system"]
2.32 -use"../../../test/Tools/isac/Knowledge/integrate.sml";
2.33 -*)
2.34 -
2.35 -use_thy "Test_Isac"
2.36 -
2.37 -end
2.38 -
2.39 -(*=== inhibit exn ?=============================================================
2.40 -===== inhibit exn ?===========================================================*)
2.41 -
2.42 -
2.43 -(*========== inhibit exn =======================================================
2.44 -
2.45 -"########### testcode inserted vvv ###########################################";
2.46 -"########### testcode inserted ^^^ ###########################################";
2.47 -
2.48 -============ inhibit exn =====================================================*)
2.49 -
2.50 -
2.51 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
2.52 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
3.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Mon Jul 15 08:28:50 2013 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Wed Jul 17 07:32:53 2013 +0200
3.3 @@ -63,8 +63,8 @@
3.4 ("List.if_True", (prop_of o num_str) @{thm if_True}),
3.5 ("HOL.if_False", (prop_of o num_str) @{thm if_False}),
3.6 (*###("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")*)
3.7 - ("Rings.semiring_class.left_distrib", (prop_of o num_str) @{thm left_distrib}),
3.8 - ("Rings.semiring_class.right_distrib", (prop_of o num_str) @{thm right_distrib}),
3.9 + ("Rings.semiring_class.distrib_right", (prop_of o num_str) @{thm distrib_right}),
3.10 + ("Rings.semiring_class.distrib_left", (prop_of o num_str) @{thm distrib_left}),
3.11 (*###("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2")*)
3.12 (*###("sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)")*)
3.13 ("Groups.monoid_mult_class.mult_1_right", (prop_of o num_str) @{thm mult_1_right}),
4.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Mon Jul 15 08:28:50 2013 +0200
4.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Jul 17 07:32:53 2013 +0200
4.3 @@ -262,7 +262,7 @@
4.4 Seq {id = "simplify_System_parenthesized", preconds = []:term list,
4.5 rew_ord = ("dummy_ord", dummy_ord),
4.6 erls = Atools_erls, srls = Erls, calc = [], errpatts = [],
4.7 - rules = [Thm ("left_distrib",num_str @{thm left_distrib}),
4.8 + rules = [Thm ("distrib_right",num_str @{thm distrib_right}),
4.9 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
4.10 Thm ("add_divide_distrib",num_str @{thm add_divide_distrib}),
4.11 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
5.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Mon Jul 15 08:28:50 2013 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Jul 17 07:32:53 2013 +0200
5.3 @@ -254,7 +254,7 @@
5.4 rew_ord = ("dummy_ord", dummy_ord),
5.5 erls = Atools_erls, srls = Erls,
5.6 calc = [], errpatts = [],
5.7 - rules = [Thm ("left_distrib",num_str @{thm left_distrib}),
5.8 + rules = [Thm ("distrib_right",num_str @{thm distrib_right}),
5.9 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
5.10 Thm ("add_divide_distrib",num_str @{thm add_divide_distrib}),
5.11 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
6.1 --- a/src/Tools/isac/Knowledge/Poly.thy Mon Jul 15 08:28:50 2013 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Jul 17 07:32:53 2013 +0200
6.3 @@ -498,9 +498,9 @@
6.4 val expand =
6.5 Rls{id = "expand", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
6.6 erls = e_rls,srls = Erls, calc = [], errpatts = [],
6.7 - rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
6.8 + rules = [Thm ("distrib_right" ,num_str @{thm distrib_right}),
6.9 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
6.10 - Thm ("right_distrib",num_str @{thm right_distrib})
6.11 + Thm ("distrib_left",num_str @{thm distrib_left})
6.12 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
6.13 ], scr = EmptyScr}:rls;
6.14
6.15 @@ -541,9 +541,9 @@
6.16 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
6.17 (*WN071229 changed/removed for Schaerding -----^^^*)
6.18
6.19 - Thm ("left_distrib" ,num_str @{thm left_distrib}),
6.20 + Thm ("distrib_right" ,num_str @{thm distrib_right}),
6.21 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
6.22 - Thm ("right_distrib",num_str @{thm right_distrib}),
6.23 + Thm ("distrib_left",num_str @{thm distrib_left}),
6.24 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
6.25
6.26 Thm ("realpow_multI", num_str @{thm realpow_multI}),
6.27 @@ -783,11 +783,11 @@
6.28 erls = e_rls,srls = Erls,
6.29 calc = [], errpatts = [],
6.30 (*asm_thm = [],*)
6.31 - rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
6.32 + rules = [Thm ("distrib_right" ,num_str @{thm distrib_right}),
6.33 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
6.34 - Thm ("right_distrib",num_str @{thm right_distrib}),
6.35 + Thm ("distrib_left",num_str @{thm distrib_left}),
6.36 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
6.37 - (*Thm ("left_distrib1",num_str @{thm left_distrib}1),
6.38 + (*Thm ("distrib_right1",num_str @{thm distrib_right}1),
6.39 ....... 18.3.03 undefined???*)
6.40
6.41 Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
6.42 @@ -937,8 +937,8 @@
6.43 "(Repeat " ^
6.44 "((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
6.45
6.46 -" (Try (Repeat (Rewrite left_distrib False))) @@ " ^
6.47 -" (Try (Repeat (Rewrite right_distrib False))) @@ " ^
6.48 +" (Try (Repeat (Rewrite distrib_right False))) @@ " ^
6.49 +" (Try (Repeat (Rewrite distrib_left False))) @@ " ^
6.50 " (Try (Repeat (Rewrite left_diff_distrib False))) @@ " ^
6.51 " (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^
6.52
6.53 @@ -1063,9 +1063,9 @@
6.54 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
6.55
6.56
6.57 - (*Thm ("left_distrib" ,num_str @{thm left_distrib}),
6.58 + (*Thm ("distrib_right" ,num_str @{thm distrib_right}),
6.59 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
6.60 - Thm ("right_distrib",num_str @{thm right_distrib}),
6.61 + Thm ("distrib_left",num_str @{thm distrib_left}),
6.62 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
6.63 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
6.64 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
6.65 @@ -1528,9 +1528,9 @@
6.66
6.67 Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*)
6.68
6.69 - Thm ("left_distrib" ,num_str @{thm left_distrib}),
6.70 + Thm ("distrib_right" ,num_str @{thm distrib_right}),
6.71 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
6.72 - Thm ("right_distrib",num_str @{thm right_distrib}),
6.73 + Thm ("distrib_left",num_str @{thm distrib_left}),
6.74 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
6.75
6.76 Thm ("mult_assoc", num_str @{thm mult_assoc}),
7.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Mon Jul 15 08:28:50 2013 +0200
7.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Wed Jul 17 07:32:53 2013 +0200
7.3 @@ -331,9 +331,9 @@
7.4 val klammern_ausmultiplizieren =
7.5 Rls{id = "klammern_ausmultiplizieren", preconds = [],
7.6 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], errpatts = [], erls = Erls,
7.7 - rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
7.8 + rules = [Thm ("distrib_right" ,num_str @{thm distrib_right}),
7.9 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
7.10 - Thm ("right_distrib",num_str @{thm right_distrib}),
7.11 + Thm ("distrib_left",num_str @{thm distrib_left}),
7.12 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
7.13
7.14 Thm ("klammer_mult_minus",num_str @{thm klammer_mult_minus}),
8.1 --- a/src/Tools/isac/Knowledge/Root.thy Mon Jul 15 08:28:50 2013 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Jul 17 07:32:53 2013 +0200
8.3 @@ -199,9 +199,9 @@
8.4 rules = [Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
8.5 (*"a - b = a + (-1) * b"*)
8.6
8.7 - Thm ("left_distrib" ,num_str @{thm left_distrib}),
8.8 + Thm ("distrib_right" ,num_str @{thm distrib_right}),
8.9 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
8.10 - Thm ("right_distrib",num_str @{thm right_distrib}),
8.11 + Thm ("distrib_left",num_str @{thm distrib_left}),
8.12 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
8.13 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
8.14 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
9.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Mon Jul 15 08:28:50 2013 +0200
9.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Wed Jul 17 07:32:53 2013 +0200
9.3 @@ -16,7 +16,7 @@
9.4 (*.calculate numeral groundterms.*)
9.5 val calculate_RootRat =
9.6 append_rls "calculate_RootRat" calculate_Rational
9.7 - [Thm ("right_distrib",num_str @{thm right_distrib}),
9.8 + [Thm ("distrib_left",num_str @{thm distrib_left}),
9.9 (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
9.10 Thm ("mult_1_left",num_str @{thm mult_1_left}),
9.11 (* 1 * z = z *)
10.1 --- a/src/Tools/isac/Knowledge/Test.thy Mon Jul 15 08:28:50 2013 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Jul 17 07:32:53 2013 +0200
10.3 @@ -1291,8 +1291,8 @@
10.4 "(Repeat " ^
10.5 "((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
10.6
10.7 -" (Try (Repeat (Rewrite left_distrib False))) @@ " ^
10.8 -" (Try (Repeat (Rewrite right_distrib False))) @@ " ^
10.9 +" (Try (Repeat (Rewrite distrib_right False))) @@ " ^
10.10 +" (Try (Repeat (Rewrite distrib_left False))) @@ " ^
10.11 " (Try (Repeat (Rewrite left_diff_distrib False))) @@ " ^
10.12 " (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^
10.13
10.14 @@ -1334,9 +1334,9 @@
10.15 ], errpatts = [],
10.16 rules = [Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
10.17 (*"a - b = a + (-1) * b"*)
10.18 - Thm ("left_distrib" ,num_str @{thm left_distrib}),
10.19 + Thm ("distrib_right" ,num_str @{thm distrib_right}),
10.20 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
10.21 - Thm ("right_distrib",num_str @{thm right_distrib}),
10.22 + Thm ("distrib_left",num_str @{thm distrib_left}),
10.23 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
10.24 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
10.25 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
10.26 @@ -1467,9 +1467,9 @@
10.27 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
10.28
10.29
10.30 - (* Thm ("left_distrib" ,num_str @{thm left_distrib}),
10.31 + (* Thm ("distrib_right" ,num_str @{thm distrib_right}),
10.32 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
10.33 - Thm ("right_distrib",num_str @{thm right_distrib}),
10.34 + Thm ("distrib_left",num_str @{thm distrib_left}),
10.35 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
10.36 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
10.37 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
11.1 --- a/src/Tools/isac/MAKE-ISAC-bundle.txt Mon Jul 15 08:28:50 2013 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,19 +0,0 @@
11.4 -# transfer a new version to the wiki for download:
11.5 -# WN 101231
11.6 -
11.7 -cd /usr/local
11.8 -
11.9 -sudo rm -r Isabelle2009-2/src/Tools/isac/$ cp Isabelle2009-2-ISAC_bundle_x86-cygwin.tar.gz /home/neuper/www/download/
11.10 -sudo rm -r Isabelle2009-2/test
11.11 -
11.12 -sudo cp -r isabisac/src/Tools/isac/ Isabelle2009-2/src/Tools/isac/
11.13 -sudo cp -r isabisac/test/ Isabelle2009-2/test/
11.14 -
11.15 -sudo cp /home/neuper/.isabelle/heaps/polyml-5.3.0_x86-linux/Isac Isabelle2009-2/heaps/polyml-5.3.0_x86-cygwin/
11.16 -
11.17 -cp Isabelle2009-2-ISAC_bundle_x86-cygwin.tar.gz /home/neuper/www/download/
11.18 -
11.19 -#scp /home/neuper/www/download/* wneuper@soy.ist.intra:/netshares/www/htdocs/projects/isac/www/download/
11.20 -
11.21 -scp /home/neuper/www/download/* wneuper@gw.ist.tugraz.at:/netshares/www/htdocs/projects/isac/www/download/
11.22 -
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/Tools/isac/ROOT Wed Jul 17 07:32:53 2013 +0200
12.3 @@ -0,0 +1,19 @@
12.4 +(* Title: create a heap image for isac on Isabelle2013
12.5 + Author: Walther Neuper, TU Graz, 130715
12.6 + (c) due to copyright terms
12.7 +
12.8 +$ cd /usr/local/isabisac/
12.9 +$ ./bin/isabelle build -d src/Tools/isac/ -v -b Isac
12.10 +*)
12.11 +
12.12 +session Isac in "~~/src/Tools/isac" = HOL +
12.13 + description {*
12.14 + Isac core, prototype of a math-engine and knowledge
12.15 + for a TP-based educational mathematics assistant.
12.16 +
12.17 + The java front-end is under development at TU Graz,
12.18 + the PolyML math-engine and Isabelle knowledge at RISC Linz.
12.19 + See http://www.ist.tugraz.at/isac/.
12.20 + *}
12.21 + options [document = false]
12.22 + theories Build_Isac
13.1 --- a/src/Tools/isac/ROOT.ML Mon Jul 15 08:28:50 2013 +0200
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,13 +0,0 @@
13.4 -(*
13.5 -$ cd /usr/local/isabisac/src/Tools/isac
13.6 -$ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac
13.7 -$ ls -l /home/neuper/.isabelle/heaps/polyml-5.4.0_x86-linux/Isac
13.8 -
13.9 -https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-June/msg00053.html:
13.10 -use 'isabelle build' instead !
13.11 -
13.12 -in Knowledge/Isac.thy set:
13.13 -ML {* val version_isac = "isac version 121014 21:00"; *}
13.14 -*)
13.15 -
13.16 -use_thys ["Build_Isac"];
14.1 --- a/src/Tools/isac/coding-standard.txt Mon Jul 15 08:28:50 2013 +0200
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,2 +0,0 @@
14.4 -these string patterns serve 'grep -R "SEE BELOW" *':
14.5 -# " thmid: "
15.1 --- a/test/Tools/isac/Interpret/rewtools.sml Mon Jul 15 08:28:50 2013 +0200
15.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Wed Jul 17 07:32:53 2013 +0200
15.3 @@ -40,7 +40,7 @@
15.4 map #1 (rlsthmsNOTisac : (string * term) list) = (*WN101011, Isabelle2009-2*)
15.5 ["refl", "o_apply", "del_base", "del_rec", "LENGTH_CONS", "LENGTH_NIL",
15.6 "list_diff_def", "take_Nil", "take_Cons", "if_True", "if_False",
15.7 - "sym_real_mult_minus1", "left_distrib", "right_distrib",
15.8 + "sym_real_mult_minus1", "distrib_right", "distrib_left",
15.9 "sym_realpow_twoI", "sym_realpow_addI", "mult_1_right",
15.10 "sym_real_mult_2", "mult_1_left", "mult_zero_left", "mult_zero_right",
15.11 "add_0_left", "add_0_right", "divide_zero_left", "sym_mult_assoc",
16.1 --- a/test/Tools/isac/Knowledge/Isac.thy Mon Jul 15 08:28:50 2013 +0200
16.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
16.3 @@ -1,116 +0,0 @@
16.4 -(* Title: test/Tools/isac/Isac.thy
16.5 - Author: Walther Neuper, TU Graz, 2010
16.6 - (c) due to copyright terms
16.7 -
16.8 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
16.9 - 10 20 30 40 50 60 70 80
16.10 -*)
16.11 -
16.12 -(*WN110319 theory Isac imports Complex_Main (*TODO Build_Isac*) begin*)
16.13 -theory isac imports Isac
16.14 -imports "Frontend/Frontend"
16.15 - PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin (*InsSort +*) DiophantEq Test
16.16 -begin
16.17 -
16.18 -
16.19 -text {* rlsthmsNOTisac from Isabelle2002-isac are all applicable to reals;
16.20 - the leading parts of longnames can be dropped with some exceptions. *}
16.21 -
16.22 -lemma "take n (x # xs) = (case n of 0 => [] | Suc m => x # take m xs)" by (rule List.take_Cons)
16.23 -lemma "t = (t::real)" by (rule HOL.refl)
16.24 -lemma "take n [] = []" by (rule List.take_Nil)
16.25 -lemma "(f o g) x = f (g x)" by (rule Fun.o_apply)
16.26 -lemma "(if True then x else y) = x" by (rule HOL.if_True)
16.27 -lemma "(if False then x else y) = y" by (rule HOL.if_False)
16.28 -(*lemma "- z1 = -1 * z1" by (rule \*)
16.29 -lemma "(z1 + z2) * w = z1 * w + z2 * (w::real)" by (rule Rings.semiring_class.left_distrib)
16.30 -lemma "w * (z1 + z2) = w * z1 + w * (z2::real)" by (rule Rings.semiring_class.right_distrib)
16.31 -lemma "r1 * r1 = (r1::real) ^ 2" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29))
16.32 -lemma "r1 ^ n1 * r1 ^ m1 = (r1::real) ^ (n1 + m1)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(26))
16.33 -lemma "z * 1 = (z::real)" by (rule Groups.monoid_mult_class.mult_1_right)
16.34 -(*lemma "z1 + z1 = 2 * z1::real)" by (rule !!!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(4)): m + m = ((1::'a) + (1::'a)) * m*)
16.35 -lemma "1 * z = (z::real)" by (rule Groups.monoid_mult_class.mult_1_left)
16.36 -lemma "0 * z = (0::real)" by (rule Rings.mult_zero_class.mult_zero_left)
16.37 -lemma "z * 0 = (0::real)" by (rule Rings.mult_zero_class.mult_zero_right)
16.38 -lemma "0 + z = (z::real)" by (rule Groups.monoid_add_class.add_0_left)
16.39 -lemma "z + 0 = (z::real)" by (rule Groups.monoid_add_class.add_0_right)
16.40 -lemma "0 / x = (0::real)" by (rule Rings.division_ring_class.divide_zero_left)
16.41 -lemma "z1 * (z2 * z3) = z1 * z2 * (z3::real)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18))
16.42 -lemma "n <= (n::real)" by (rule RealDef.order_refl)
16.43 -lemma "- (- z) = (z::real)" by (rule Groups.group_add_class.minus_minus)
16.44 -lemma "z * w = w * (z::real)" by (rule RealDef.mult_commute)
16.45 -lemma "z1 * (z2 * z3) = z2 * (z1 * (z3::real))" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19))
16.46 -lemma "z1 * z2 * z3 = z1 * (z2 * (z3::real))" by (rule RealDef.mult_assoc)
16.47 -lemma "z + w = w + (z::real)" by (rule Groups.ab_semigroup_add_class.add_commute)
16.48 -lemma "x + (y + z) = y + (x + (z::real))" by (rule Groups.ab_semigroup_add_class.add_left_commute)
16.49 -lemma "z1 + z2 + z3 = z1 + (z2 + (z3::real))" by (rule Groups.semigroup_add_class.add_assoc)
16.50 -lemma "- (x1 * y1) = - x1 * (y1::real)" by (rule Rings.ring_class.minus_mult_left)
16.51 -lemma "z + - z = (0::real)" by (rule Groups.group_add_class.right_minus)
16.52 -lemma "z1 + (z2 + z3) = z1 + z2 + (z3::real)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25))
16.53 -lemma "- (x1 / y1) = - x1 / (y1::real)" by (rule Rings.division_ring_class.minus_divide_left)
16.54 -
16.55 -lemma "x * (y / z) = x * y / (z::real)" by (rule Fields.field_class.times_divide_eq(1))
16.56 -lemma "x * (y / z) = x * y / (z::real)" by (rule Rings.division_ring_class.times_divide_eq_right) (*without (1)*)
16.57 -
16.58 -lemma "y / z * x = y * x / (z::real)" by (rule Fields.field_class.times_divide_eq_left)
16.59 -lemma "x / y / z = x / (y * (z::real))" by (rule Fields.field_inverse_zero_class.divide_divide_eq_left)
16.60 -lemma "x / (y / z) = x * z / (y::real)" by (rule Fields.field_inverse_zero_class.divide_divide_eq_right)
16.61 -lemma "x / 1 = (x::real)" by (rule Rings.division_ring_class.divide_1)
16.62 -lemma "(z1 - z2) * w = z1 * w - z2 * (w::real)" by (rule Rings.ring_class.left_diff_distrib)
16.63 -lemma "w * (z1 - z2) = w * z1 - w * (z2::real)" by (rule Rings.ring_class.right_diff_distrib)
16.64 -lemma "(x + y) / z = x / z + y / (z::real)" by (rule Rings.division_ring_class.add_divide_distrib)
16.65 -
16.66 -section {* comments on the above *}
16.67 -subsection {* these are twice: *}
16.68 -text {*
16.69 -(*lemma "m1 + (n1 + k1) = m1 + n1 + k1" + see sym_real_add_assoc *)
16.70 -(*lemma "m1 * (n1 * k1) = m1 * n1 * k1" )] + see sym_mult_assoc*)
16.71 -*}
16.72 -
16.73 -subsection {* leading parts of long.names can be omitted, except *_class.*(n)*}
16.74 -lemma "take n (x # xs) = (case n of 0 => [] | Suc m => x # take m xs)" by (rule take_Cons)
16.75 -lemma "t = (t::real)" by (rule refl)
16.76 -lemma "take n [] = []" by (rule take_Nil)
16.77 -lemma "(f o g) x = f (g x)" by (rule o_apply)
16.78 -lemma "(if True then x else y) = x" by (rule if_True)
16.79 -lemma "(if False then x else y) = y" by (rule if_False)
16.80 -(*lemma "- z1 = -1 * z1" by (rule \*)
16.81 -lemma "(z1 + z2) * w = z1 * w + z2 * (w::real)" by (rule left_distrib)
16.82 -lemma "w * (z1 + z2) = w * z1 + w * (z2::real)" by (rule right_distrib)
16.83 -lemma "r1 * r1 = (r1::real) ^ 2" by (rule comm_semiring_1_class.normalizing_semiring_rules(29))
16.84 -lemma "r1 ^ n1 * r1 ^ m1 = (r1::real) ^ (n1 + m1)" by (rule comm_semiring_1_class.normalizing_semiring_rules(26))
16.85 -lemma "z * 1 = (z::real)" by (rule mult_1_right)
16.86 -(*lemma "z1 + z1 = 2 * z1::real)" by (rule !!!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(4)): m + m = ((1::'a) + (1::'a)) * m*)
16.87 -lemma "1 * z = (z::real)" by (rule mult_1_left)
16.88 -lemma "0 * z = (0::real)" by (rule mult_zero_left)
16.89 -lemma "z * 0 = (0::real)" by (rule mult_zero_right)
16.90 -lemma "0 + z = (z::real)" by (rule add_0_left)
16.91 -lemma "z + 0 = (z::real)" by (rule add_0_right)
16.92 -lemma "0 / x = (0::real)" by (rule divide_zero_left)
16.93 -lemma "z1 * (z2 * z3) = z1 * z2 * (z3::real)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18))
16.94 -lemma "n <= (n::real)" by (rule order_refl)
16.95 -lemma "- (- z) = (z::real)" by (rule minus_minus)
16.96 -lemma "z * w = w * (z::real)" by (rule mult_commute)
16.97 -lemma "z1 * (z2 * z3) = z2 * (z1 * (z3::real))" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19))
16.98 -lemma "z1 * z2 * z3 = z1 * (z2 * (z3::real))" by (rule mult_assoc)
16.99 -lemma "z + w = w + (z::real)" by (rule add_commute)
16.100 -lemma "x + (y + z) = y + (x + (z::real))" by (rule add_left_commute)
16.101 -lemma "z1 + z2 + z3 = z1 + (z2 + (z3::real))" by (rule add_assoc)
16.102 -lemma "- (x1 * y1) = - x1 * (y1::real)" by (rule minus_mult_left)
16.103 -lemma "z + - z = (0::real)" by (rule right_minus)
16.104 -lemma "z1 + (z2 + z3) = z1 + z2 + (z3::real)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25))
16.105 -lemma "- (x1 / y1) = - x1 / (y1::real)" by (rule minus_divide_left)
16.106 -
16.107 -lemma "x * (y / z) = x * y / (z::real)" by (rule Fields.field_class.times_divide_eq(1))
16.108 -lemma "x * (y / z) = x * y / (z::real)" by (rule times_divide_eq_right)
16.109 -
16.110 -lemma "y / z * x = y * x / (z::real)" by (rule times_divide_eq_left)
16.111 -lemma "x / y / z = x / (y * (z::real))" by (rule divide_divide_eq_left)
16.112 -lemma "x / (y / z) = x * z / (y::real)" by (rule divide_divide_eq_right)
16.113 -lemma "x / 1 = (x::real)" by (rule divide_1)
16.114 -lemma "(z1 - z2) * w = z1 * w - z2 * (w::real)" by (rule left_diff_distrib)
16.115 -lemma "w * (z1 - z2) = w * z1 - w * (z2::real)" by (rule right_diff_distrib)
16.116 -lemma "(x + y) / z = x / z + y / (z::real)" by (rule add_divide_distrib)
16.117 -
16.118 -
16.119 -end
16.120 \ No newline at end of file
17.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Mon Jul 15 08:28:50 2013 +0200
17.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Wed Jul 17 07:32:53 2013 +0200
17.3 @@ -68,8 +68,8 @@
17.4 ("if_True", "(if True then ?x else ?y) = ?x"),
17.5 ("if_False", "(if False then ?x else ?y) = ?y"),
17.6 (*###*)("sym_real_mult_minus1", "- ?z1 = -1 * ?z1"),
17.7 - ("left_distrib", "(?a + ?b) * ?c = ?a * ?c + ?b * ?c"),
17.8 - ("right_distrib", "?a * (?b + ?c) = ?a * ?b + ?a * ?c"),
17.9 + ("distrib_right", "(?a + ?b) * ?c = ?a * ?c + ?b * ?c"),
17.10 + ("distrib_left", "?a * (?b + ?c) = ?a * ?b + ?a * ?c"),
17.11 (*###*)(sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2"),
17.12 (*###*)(sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)"),
17.13 ("mult_1_right", "?a * 1 = ?a"),
17.14 @@ -297,8 +297,8 @@
17.15 ("List.if_True", (prop_of o num_str) @{thm if_True}),
17.16 ("HOL.if_False", (prop_of o num_str) @{thm if_False}),
17.17 (*###("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")*)
17.18 - ("Rings.semiring_class.left_distrib", (prop_of o num_str) @{thm left_distrib}),
17.19 - ("Rings.semiring_class.right_distrib", (prop_of o num_str) @{thm right_distrib}),
17.20 + ("Rings.semiring_class.distrib_right", (prop_of o num_str) @{thm distrib_right}),
17.21 + ("Rings.semiring_class.distrib_left", (prop_of o num_str) @{thm distrib_left}),
17.22 (*###("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2")*)
17.23 (*###("sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)")*)
17.24 ("Groups.monoid_mult_class.mult_1_right", (prop_of o num_str) @{thm mult_1_right}),
17.25 @@ -362,8 +362,8 @@
17.26 *** insert: preserved ["Isabelle","List","Theorems","if_True"]
17.27 Thm.get_name_hint @{t^^^^^^True} = "HOL.if_True";
17.28 *** insert: preserved ["Isabelle","HOL","Theorems","if_False"]
17.29 - *** insert: preserved ["Isabelle","Rings","Theorems","left_distrib"]
17.30 - *** insert: preserved ["Isabelle","Rings","Theorems","right_distrib"]
17.31 + *** insert: preserved ["Isabelle","Rings","Theorems","distrib_right"]
17.32 + *** insert: preserved ["Isabelle","Rings","Theorems","distrib_left"]
17.33 *** insert: preserved ["Isabelle","Groups","Theorems","mult_1_right"]
17.34 *** insert: preserved ["Isabelle","Groups","Theorems","mult_1_left"]
17.35 *** insert: preserved ["Isabelle","Rings","Theorems","mult_zero_left"]
18.1 --- a/test/Tools/isac/Test_Some2.thy Mon Jul 15 08:28:50 2013 +0200
18.2 +++ b/test/Tools/isac/Test_Some2.thy Wed Jul 17 07:32:53 2013 +0200
18.3 @@ -3,28 +3,11 @@
18.4 imports "/usr/local/isabisac/src/Tools/isac/Knowledge/GCD_Poly"
18.5 begin
18.6 ML_file "/usr/local/isabisac/test/Tools/isac/Knowledge/gcd_poly.sml"
18.7 -ML_file "/usr/local/isabisac/test/Tools/isac/Knowledge/gcd_poly_winkler.sml"
18.8 +(* gcd_poly_winkler.sml overwrites definitions from GCD_Poly.thy;
18.9 + thus it must be evaluated *after* gcd_poly.sml.
18.10 +ML_file "/usr/local/isabisac/test/Tools/isac/Knowledge/gcd_poly_winkler.sml"*)
18.11
18.12 ML {*
18.13 -(*http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*)
18.14 -fun pat_to_term ctxt t =
18.15 - let
18.16 - fun new_var vs T = case Variable.variant_frees ctxt vs [("x", T)] of
18.17 - v::_ => (Free v :: vs, Free v);
18.18 - fun go (v as Var (_,T)) (vs,assocs) =
18.19 - (case AList.lookup op= assocs v of
18.20 - NONE => (case new_var vs T of
18.21 - (vs', v') => (vs', (v,v') :: assocs))
18.22 - | _ => (vs,assocs))
18.23 - | go _ (vs,assocs) = (vs,assocs);
18.24 - val assocs = snd (Term.fold_aterms go t
18.25 - (map Free (Term.add_frees t []), []));
18.26 - in fst (yield_singleton (Variable.import_terms true)
18.27 - (subst_atomic assocs t) ctxt)
18.28 - end;
18.29 -
18.30 -*}
18.31 -ML {*
18.32 *}
18.33 ML {*
18.34 *}
19.1 --- a/test/Tools/isac/thms-survey-Isa02-Isa09-2.sml Mon Jul 15 08:28:50 2013 +0200
19.2 +++ b/test/Tools/isac/thms-survey-Isa02-Isa09-2.sml Wed Jul 17 07:32:53 2013 +0200
19.3 @@ -27,9 +27,9 @@
19.4 -----------------------------------------------------------------------------------------------------------------
19.5 ("if_False", "(if False then ?x else ?y) = ?y"), HOL.if_False
19.6 ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1" [.]), \???
19.7 - ("real_add_mult_distrib", Rings.semiring_class.left_distrib
19.8 + ("real_add_mult_distrib", Rings.semiring_class.distrib_right
19.9 "(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"),
19.10 - ("real_add_mult_distrib2", Rings.semiring_class.right_distrib
19.11 + ("real_add_mult_distrib2", Rings.semiring_class.distrib_left
19.12 "?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"),
19.13 ("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2" [.]), !^!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29)
19.14 Poly.realpow_two_atom: ?r is_atom \<Longrightarrow> ?r * ?r = ?r ^^^ 2