1.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Fri Sep 13 18:35:51 2019 +0200
1.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Sat Sep 14 16:15:05 2019 +0200
1.3 @@ -6,9 +6,10 @@
1.4 theory Auto_Prog imports Program Prog_Tac Tactical begin
1.5
1.6 text \<open>Abstract:
1.7 - Rewrite_Set* create ONE step in a calculation.
1.8 - However, students can request steps in detail, which led to the rewrite by a rule-set.
1.9 - For meeting such requests, a program is auto-generated from the items of the rule-set.
1.10 + The tactics Rewrite_Set* create ONE step in a calculation by application of usually
1.11 + MORE than one theorem (here called "rule").
1.12 + However, students can request details of rewriting down to single applications of theorems.
1.13 + For accomplishing such requests, a program is auto-generated from the items of a rule-set.
1.14 \<close>
1.15
1.16 subsection \<open>consts for programs automatically built from rules\<close>
2.1 --- a/src/Tools/isac/ProgLang/Calculate.thy Fri Sep 13 18:35:51 2019 +0200
2.2 +++ b/src/Tools/isac/ProgLang/Calculate.thy Sat Sep 14 16:15:05 2019 +0200
2.3 @@ -1,136 +1,41 @@
2.4 -(* auxiliary functions used in programs
2.5 - author: Walther Neuper 000301
2.6 - WN0509 shift into Atools ?!? (because used also in where of models !)
2.7 -
2.8 +(* Title: ProgLang/Calculate.thy
2.9 + Author: Walther Neuper 000301
2.10 (c) copyright due to lincense terms.
2.11 *)
2.12
2.13 theory Calculate
2.14 imports "~~/src/Tools/isac/CalcElements/CalcElements"
2.15 begin
2.16 -(*//------------------------- from Atools ---------------------------------------------------\\*)
2.17 +
2.18 +text \<open>Abstract:
2.19 + The Isac project required floating point numbers and complex numbers in early 2000,
2.20 + before these numbers were available in Isabelle.
2.21 + Since that time numeral calculations are done by ML functions, all named eval_
2.22 + and integrated into rewriting. eval_binop below is not bound to a specific constant
2.23 + (like in Prog_Expr.thy), rather calculates results of Isabelle's binary operations + - * / ^.
2.24 + Nowadays the code in Calculate.thy and calculate.sml should be replaced by native Isabelle
2.25 + code.
2.26 + A specialty are the ad-hoc theorems for numeral calculations created in order to provide
2.27 + the rewrite engine with theorems as done in general.
2.28 +\<close>
2.29 +
2.30 ML_file calculate.sml
2.31
2.32 ML \<open>
2.33 \<close> ML \<open>
2.34 -\<close> ML \<open>
2.35 -\<close> ML \<open>
2.36 -(* convert int and float to internal floatingpoint prepresentation.*)
2.37 -fun numeral (Free (str, _)) =
2.38 - (case TermC.int_of_str_opt str of
2.39 - SOME i => SOME ((i, 0), (0, 0))
2.40 - | NONE => NONE)
2.41 - | numeral (Const ("Float.Float", _) $
2.42 - (Const ("Product_Type.Pair", _) $
2.43 - (Const ("Product_Type.Pair", _) $ Free (v1, _) $ Free (v2,_)) $
2.44 - (Const ("Product_Type.Pair", _) $ Free (p1, _) $ Free (p2,_))))=
2.45 - (case (TermC.int_of_str_opt v1, TermC.int_of_str_opt v2, TermC.int_of_str_opt p1, TermC.int_of_str_opt p2) of
2.46 - (SOME v1', SOME v2', SOME p1', SOME p2') =>
2.47 - SOME ((v1', v2'), (p1', p2'))
2.48 - | _ => NONE)
2.49 - | numeral _ = NONE;
2.50 +(*** evaluate binary associative operations ***)
2.51
2.52 -(*** handle numerals in eval_binop ***)
2.53 -(* TODO rebuild fun calcul, fun term_of_float,fun var_op_float, fun float_op_var:
2.54 - Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *)
2.55 -
2.56 -\<close> ML \<open>
2.57 -(* used for calculating built in binary operations in Isabelle2002.
2.58 - integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0) *)
2.59 -fun calcul "Groups.plus_class.plus" ((a, b), _:int * int) ((c, d), _:int * int) = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*)
2.60 - if b < d
2.61 - then ((a + c * Calc.power 10 (d - b), b), (0, 0))(*FIXXXME precision*)
2.62 - else ((a * Calc.power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
2.63 - | calcul "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
2.64 - ((a - c,0),(0,0))
2.65 - | calcul "Groups.times_class.times" ((a, b), _) ((c, d), _) = (*FIXXXME precision*)
2.66 - ((a * c, b + d), (0, 0))
2.67 - | calcul "Rings.divide_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
2.68 - ((a div c, 0), (0, 0))
2.69 - | calcul "Prog_Expr.pow" ((a, _), _) ((c, _), _) = (*FIXXXME Float + prec.*)
2.70 - ((Calc.power a c, 0), (0, 0))
2.71 - | calcul op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) =
2.72 - error ("calcul: not impl. for Float (("^
2.73 - (string_of_int a )^","^(string_of_int b )^"), ("^
2.74 - (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^
2.75 - (string_of_int c )^","^(string_of_int d )^"), ("^
2.76 - (string_of_int p21)^","^(string_of_int p22)^"))");
2.77 -(*> calcul "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0));
2.78 -val it = ((1,0),(0,0))*)
2.79 -\<close> ML \<open>
2.80 -(*.convert internal floatingpoint prepresentation to int and float.*)
2.81 -fun term_of_float T ((val1, 0), ( 0, 0)) =
2.82 - TermC.term_of_num T val1
2.83 - | term_of_float T ((val1, val2), (precision1, precision2)) =
2.84 - let val pT = TermC.pairT T T
2.85 - in Const ("Float.Float", (TermC.pairT pT pT) --> T)
2.86 - $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int val1, T))
2.87 - (Free (TermC.str_of_int val2, T)))
2.88 - (TermC.pairt (Free (TermC.str_of_int precision1, T))
2.89 - (Free (TermC.str_of_int precision2, T))))
2.90 - end;
2.91 -(*> val t = str2term "Float ((1,2),(0,0))";
2.92 -> val Const ("Float.Float", fT) $ _ = t;
2.93 -> atomtyp fT;
2.94 -> val ffT = (pairT (pairT HOLogic.realT HOLogic.realT)
2.95 -> (pairT HOLogic.realT HOLogic.realT)) --> HOLogic.realT;
2.96 -> atomtyp ffT;
2.97 -> fT = ffT;
2.98 -val it = true : bool
2.99 -
2.100 -t = float_term_of_num HOLogic.realT ((1,2),(0,0));
2.101 -val it = true : bool*)
2.102 -
2.103 -(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
2.104 -fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) =
2.105 - TermC.mk_var_op_num v op_ optype ntyp v1
2.106 - | var_op_float v op_ optype T ((v1, v2), (p1, p2)) =
2.107 - let val pT = TermC.pairT T T
2.108 - in Const (op_, optype) $ v $
2.109 - (Const ("Float.Float", (TermC.pairT pT pT) --> T)
2.110 - $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int v1, T))
2.111 - (Free (TermC.str_of_int v2, T)))
2.112 - (TermC.pairt (Free (TermC.str_of_int p1, T))
2.113 - (Free (TermC.str_of_int p2, T)))))
2.114 - end;
2.115 -(*> val t = str2term "a + b";
2.116 -> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
2.117 -> val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";
2.118 -> t = var_op_float v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
2.119 -val it = true : bool*)
2.120 -
2.121 -(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
2.122 -fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) =
2.123 - TermC.mk_num_op_var v op_ optype ntyp v1
2.124 - | float_op_var v op_ optype T ((v1, v2), (p1, p2)) =
2.125 - let val pT = TermC.pairT T T
2.126 - in Const (op_, optype) $
2.127 - (Const ("Float.Float", (TermC.pairT pT pT) --> T)
2.128 - $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int v1, T))
2.129 - (Free (TermC.str_of_int v2, T)))
2.130 - (TermC.pairt (Free (TermC.str_of_int p1, T))
2.131 - (Free (TermC.str_of_int p2, T))))) $ v
2.132 - end;
2.133 -(*> val t = str2term "a + b";
2.134 -> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
2.135 -> val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";
2.136 -> t = float_op_var v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
2.137 -val it = true : bool*)
2.138 -\<close>
2.139 -
2.140 -(*** evaluate binary associative operations ***)
2.141 -ML \<open>
2.142 -fun eval_binop (_(*thmid*) : string) (op_: string)
2.143 +fun eval_binop (_(*thmid*) : string) (op_: string)
2.144 (t as (Const (op0, t0) $ (Const (op0', _) $ v $ t1) $ t2)) _ = (* binary . (v.n1).n2 *)
2.145 if op0 = op0' then
2.146 - case (numeral t1, numeral t2) of
2.147 + case (Calc.numeral t1, Calc.numeral t2) of
2.148 (SOME n1, SOME n2) =>
2.149 let
2.150 val (T1, _, _) = TermC.dest_binop_typ t0
2.151 val res =
2.152 - calcul (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0)n1 n2
2.153 + Calc.calcul (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0)n1 n2
2.154 (*WN071229 "Rings.divide_class.divide" never tried*)
2.155 - val rhs = var_op_float v op_ t0 T1 res
2.156 + val rhs = Calc.var_op_float v op_ t0 T1 res
2.157 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
2.158 in SOME ("#: " ^ Rule.term2str prop, prop) end
2.159 | _ => NONE
2.160 @@ -138,24 +43,24 @@
2.161 | eval_binop _ (op_ : string)
2.162 (t as (Const (op0, t0) $ t1 $ (Const (op0', _) $ t2 $ v))) _ = (* binary . n1.(n2.v) *)
2.163 if op0 = op0' then
2.164 - case (numeral t1, numeral t2) of
2.165 + case (Calc.numeral t1, Calc.numeral t2) of
2.166 (SOME n1, SOME n2) =>
2.167 if op0 = "Groups.minus_class.minus" then NONE
2.168 else let
2.169 val (T1, _, _) = TermC.dest_binop_typ t0
2.170 - val res = calcul op0 n1 n2
2.171 - val rhs = float_op_var v op_ t0 T1 res
2.172 + val res = Calc.calcul op0 n1 n2
2.173 + val rhs = Calc.float_op_var v op_ t0 T1 res
2.174 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
2.175 in SOME ("#: " ^ Rule.term2str prop, prop) end
2.176 | _ => NONE
2.177 else NONE
2.178 | eval_binop _ _ (t as (Const (op0, t0) $ t1 $ t2)) _ = (* binary . n1.n2 *)
2.179 - (case (numeral t1, numeral t2) of
2.180 + (case (Calc.numeral t1, Calc.numeral t2) of
2.181 (SOME n1, SOME n2) =>
2.182 let
2.183 val (_, _, Trange) = TermC.dest_binop_typ t0;
2.184 - val res = calcul op0 n1 n2;
2.185 - val rhs = term_of_float Trange res;
2.186 + val res = Calc.calcul op0 n1 n2;
2.187 + val rhs = Calc.term_of_float Trange res;
2.188 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs));
2.189 in SOME ("#: " ^ Rule.term2str prop, prop) end
2.190 | _ => NONE)
2.191 @@ -170,12 +75,6 @@
2.192 val it = "-1 * (-1 * a) = 1 * a"*)
2.193 \<close> ML \<open>
2.194 \<close> ML \<open>
2.195 -\<close> ML \<open>
2.196 -\<close>
2.197 -(*\\------------------------- from Atools ---------------------------------------------------//*)
2.198 -ML \<open>
2.199 -\<close> ML \<open>
2.200 -\<close> ML \<open>
2.201 \<close>
2.202
2.203 end
2.204 \ No newline at end of file
3.1 --- a/src/Tools/isac/ProgLang/ProgLang.thy Fri Sep 13 18:35:51 2019 +0200
3.2 +++ b/src/Tools/isac/ProgLang/ProgLang.thy Sat Sep 14 16:15:05 2019 +0200
3.3 @@ -2,9 +2,16 @@
3.4 Author: Walther Neuper 100831
3.5 (c) due to copyright terms
3.6 *)
3.7 -theory ProgLang imports Prog_Expr Auto_Prog
3.8 +theory ProgLang
3.9 + imports Prog_Expr Auto_Prog
3.10 begin
3.11
3.12 +text \<open>Abstract:
3.13 + Here the language is defined, which extends Isabelle's functions to Isac's programs
3.14 + for Lucas-Interpretation.
3.15 + The language is interpreted by use of Isac's rewrite engine, defined in the ML-file below.
3.16 +\<close>
3.17 +
3.18 ML_file rewrite.sml
3.19
3.20 ML \<open>
4.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Fri Sep 13 18:35:51 2019 +0200
4.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Sat Sep 14 16:15:05 2019 +0200
4.3 @@ -4,36 +4,32 @@
4.4 (c) copyright due to lincense terms.
4.5 *)
4.6
4.7 -theory Prog_Expr imports Calculate
4.8 +theory Prog_Expr
4.9 + imports Calculate
4.10 begin
4.11
4.12 -subsection \<open>General constants\<close>
4.13 +text \<open>Abstract:
4.14 + Specific constants are defined for pre-conditions of programs and for program-expressions.
4.15 + The constants are connected with ML functions for evaluation of respective expressions
4.16 + (all named eval_*), such that Isac's rewrite engine can handle it.
4.17 +\<close>
4.18 +
4.19 +subsection \<open>Power re-defined for a specific type\<close>
4.20 consts
4.21 -(*//------------------------- from Tools .thy-------------------------------------------------\\*)
4.22 - EmptyList :: "bool list"
4.23 - UniversalList :: "bool list"
4.24 -(*\\------------------------- from Tools .thy ------------------------------------------------//*)
4.25 -(*\\------------------------- from Atools .thy -----------------------------------------------//*)
4.26 - Arbfix :: "real"
4.27 - Undef :: "real" (* WN190823 probably an outdated design for DiffApp *)
4.28 -
4.29 pow :: "[real, real] => real" (infixr "^^^" 80)
4.30 -(*\\------------------------- from Atools.thy -----------------------------------------------//*)
4.31
4.32 subsection \<open>consts of functions in pre-conditions and program-expressions\<close>
4.33 -(*//------------------------- from Tools .thy-------------------------------------------------\\*)
4.34 consts
4.35 lhs :: "bool => real" (*of an equality*)
4.36 rhs :: "bool => real" (*of an equality*)
4.37 Vars :: "'a => real list" (*get the variables of a term *)
4.38 matches :: "['a, 'a] => bool"
4.39 matchsub :: "['a, 'a] => bool"
4.40 -(*\\------------------------- from Tools .thy-------------------------------------------------//*)
4.41 some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
4.42 occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
4.43
4.44 abs :: "real => real" ("(|| _ ||)")
4.45 -(* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
4.46 + (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
4.47 absset :: "real set => real" ("(||| _ |||)")
4.48 (*is numeral constant ?*)
4.49 is'_const :: "real => bool" ("_ is'_const" 10)
4.50 @@ -43,27 +39,14 @@
4.51
4.52 (* identity on term level*)
4.53 ident :: "['a, 'a] => bool" ("(_ =!=/ _)" [51, 51] 50)
4.54 -
4.55 argument'_in :: "real => real" ("argument'_in _" 10)
4.56 - sameFunId :: "[real, bool] => bool" (**"same'_funid _ _" 10
4.57 - WN0609 changed the id, because ".. _ _" inhibits currying**)
4.58 + sameFunId :: "[real, bool] => bool" (* "same'_funid _ _" 10
4.59 + WN0609 changed the id, because ".. _ _" inhibits currying *)
4.60 filter'_sameFunId:: "[real, bool list] => bool list"
4.61 ("filter'_sameFunId _ _" 10)
4.62 boollist2sum :: "bool list => real"
4.63 lastI :: "'a list \<Rightarrow> 'a"
4.64
4.65 -subsection \<open>Theorems for rule-sets TODO: find a better location in code\<close>
4.66 -axiomatization where
4.67 - rle_refl: "(n::real) <= n" and
4.68 - not_true: "(~ True) = False" and
4.69 - not_false: "(~ False) = True" and
4.70 - and_true: "(a & True) = a" and
4.71 - and_false: "(a & False) = False" and
4.72 - or_true: "(a | True) = True" and
4.73 - or_false: "(a | False) = a" and
4.74 - and_commute: "(a & b) = (b & a)" and
4.75 - or_commute: "(a | b) = (b | a)"
4.76 -
4.77 subsection \<open>ML code for functions in pre-conditions and program-expressions\<close>
4.78 ML \<open>
4.79 signature PROG_EXPR =
4.80 @@ -574,9 +557,6 @@
4.81 \<close> text \<open>
4.82 open Prog_Expr
4.83 \<close> ML \<open>
4.84 -
4.85 -\<close> ML \<open>
4.86 -\<close> ML \<open>
4.87 \<close> ML \<open>
4.88 \<close>
4.89
5.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Fri Sep 13 18:35:51 2019 +0200
5.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Sat Sep 14 16:15:05 2019 +0200
5.3 @@ -7,6 +7,13 @@
5.4 imports "~~/src/Tools/isac/CalcElements/CalcElements"
5.5 begin
5.6
5.7 +text \<open>Abstract:
5.8 + Specific constants for tactics in programs, which each create a step in a calculation
5.9 + as a side effect.
5.10 + These program-tactics are related to Tactic.input for use in calculations and
5.11 + Tactic.T for internal use by lucas-interpretation.
5.12 +\<close>
5.13 +
5.14 subsection \<open>arguments of tactic SubProblem\<close>
5.15
5.16 typedecl
5.17 @@ -24,8 +31,6 @@
5.18
5.19 subsection \<open>tactics in programs\<close>
5.20 text \<open>
5.21 - For tactics as input by students and for tactics used by the MathEngine see
5.22 - type Tactic.input and type Tactic.T, respectively.
5.23 Note: the items below MUST ALL be recorded in xxx TODO
5.24 \<close>
5.25 consts
6.1 --- a/src/Tools/isac/ProgLang/Program.thy Fri Sep 13 18:35:51 2019 +0200
6.2 +++ b/src/Tools/isac/ProgLang/Program.thy Sat Sep 14 16:15:05 2019 +0200
6.3 @@ -8,9 +8,30 @@
6.4 begin
6.5
6.6 text \<open>Abstract:
6.7 - TODO
6.8 + Theorems required by Isac's rewrite engine for evaluating assumptions of theorems/rules.
6.9 + Basic functions for Isac programs and theorems
6.10 \<close>
6.11
6.12 +subsection \<open>General constants: TODO shift to appropriate files\<close>
6.13 +consts
6.14 + EmptyList :: "bool list"
6.15 + UniversalList :: "bool list"
6.16 + Arbfix :: "real"
6.17 + Undef :: "real" (* WN190823 probably an outdated design for DiffApp *)
6.18 +
6.19 +subsection \<open>Theorems specific for evaluation of assumptions of theorems/rules\<close>
6.20 +axiomatization where
6.21 + rle_refl: "(n::real) <= n" and
6.22 + not_true: "(~ True) = False" and
6.23 + not_false: "(~ False) = True" and
6.24 + and_true: "(a & True) = a" and
6.25 + and_false: "(a & False) = False" and
6.26 + or_true: "(a | True) = True" and
6.27 + or_false: "(a | False) = a" and
6.28 + and_commute: "(a & b) = (b & a)" and
6.29 + or_commute: "(a | b) = (b | a)"
6.30 +
6.31 +subsection \<open>TODO\<close>
6.32 ML \<open>
6.33 \<close> ML \<open>
6.34 signature PROGRAM =
6.35 @@ -35,7 +56,7 @@
6.36 struct
6.37 (**)
6.38
6.39 -(* the lucas-interpreter requires programs in a specific format *)
6.40 +(* the lucas-interpreter requires programs in this specific format *)
6.41 fun prep_program thm = (thm
6.42 |> Thm.prop_of
6.43 |> HOLogic.dest_Trueprop
7.1 --- a/src/Tools/isac/ProgLang/Tactical.thy Fri Sep 13 18:35:51 2019 +0200
7.2 +++ b/src/Tools/isac/ProgLang/Tactical.thy Sat Sep 14 16:15:05 2019 +0200
7.3 @@ -6,6 +6,10 @@
7.4 imports "~~/src/Tools/isac/CalcElements/CalcElements"
7.5 begin
7.6
7.7 +text \<open>Abstract:
7.8 + Define specific constants for tacticals, which determine the flow of evaluation in programs.
7.9 + Tacticals are not visible in calculations, which are generated by programs as a side effect.
7.10 +\<close>
7.11 subsection \<open>Consts for tacticals\<close>
7.12 consts
7.13 Seq :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10) (*@ used*)
8.1 --- a/src/Tools/isac/ProgLang/calculate.sml Fri Sep 13 18:35:51 2019 +0200
8.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Sat Sep 14 16:15:05 2019 +0200
8.3 @@ -4,6 +4,7 @@
8.4
8.5 signature NUMERAL_CALCULATION =
8.6 sig
8.7 + type float
8.8 val calc_equ: string -> int * int -> bool
8.9 val power: int -> int -> int
8.10 val sign_mult: int -> int -> int
8.11 @@ -14,6 +15,11 @@
8.12 val adhoc_thm1_: theory -> Rule.cal -> term -> (string * thm) option
8.13 val norm: term -> term
8.14 val popt2str: ('a * term) option -> string
8.15 + val numeral: term -> ((int * int) * (int * int)) option
8.16 + val calcul: string -> float -> float -> float
8.17 + val term_of_float: typ -> float -> term
8.18 + val var_op_float: term -> string -> typ -> typ ->float -> term
8.19 + val float_op_var: term -> string -> typ -> typ -> float -> term
8.20 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.21 (* NONE *)
8.22 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.23 @@ -29,6 +35,10 @@
8.24 struct
8.25 (**)
8.26
8.27 +type float =
8.28 + (int * int) (* value: significand * exponent *)
8.29 + * (int * int) (* precision: significand * exponent *)
8.30 +
8.31 (** calculate integers **)
8.32
8.33 fun calc_equ "less" (n1, n2) = n1 < n2
8.34 @@ -180,6 +190,107 @@
8.35 else (*3*) mk_rule (prems, concl, @{term True})
8.36 end;
8.37
8.38 +(* convert int and float to internal floatingpoint prepresentation.*)
8.39 +fun numeral (Free (str, _)) =
8.40 + (case TermC.int_of_str_opt str of
8.41 + SOME i => SOME ((i, 0), (0, 0))
8.42 + | NONE => NONE)
8.43 + | numeral (Const ("Float.Float", _) $
8.44 + (Const ("Product_Type.Pair", _) $
8.45 + (Const ("Product_Type.Pair", _) $ Free (v1, _) $ Free (v2,_)) $
8.46 + (Const ("Product_Type.Pair", _) $ Free (p1, _) $ Free (p2,_))))=
8.47 + (case (TermC.int_of_str_opt v1, TermC.int_of_str_opt v2, TermC.int_of_str_opt p1, TermC.int_of_str_opt p2) of
8.48 + (SOME v1', SOME v2', SOME p1', SOME p2') =>
8.49 + SOME ((v1', v2'), (p1', p2'))
8.50 + | _ => NONE)
8.51 + | numeral _ = NONE;
8.52 +
8.53 +(*** handle numerals in eval_binop ***)
8.54 +(* TODO rebuild fun calcul, fun term_of_float,fun var_op_float, fun float_op_var:
8.55 + Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *)
8.56 +
8.57 +(* used for calculating built in binary operations in Isabelle2002.
8.58 + integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0) *)
8.59 +fun calcul "Groups.plus_class.plus" ((a, b), _:int * int) ((c, d), _:int * int) = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*)
8.60 + if b < d
8.61 + then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)
8.62 + else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
8.63 + | calcul "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
8.64 + ((a - c,0),(0,0))
8.65 + | calcul "Groups.times_class.times" ((a, b), _) ((c, d), _) = (*FIXXXME precision*)
8.66 + ((a * c, b + d), (0, 0))
8.67 + | calcul "Rings.divide_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
8.68 + ((a div c, 0), (0, 0))
8.69 + | calcul "Prog_Expr.pow" ((a, _), _) ((c, _), _) = (*FIXXXME Float + prec.*)
8.70 + ((power a c, 0), (0, 0))
8.71 + | calcul op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) =
8.72 + error ("calcul: not impl. for Float (("^
8.73 + (string_of_int a )^","^(string_of_int b )^"), ("^
8.74 + (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^
8.75 + (string_of_int c )^","^(string_of_int d )^"), ("^
8.76 + (string_of_int p21)^","^(string_of_int p22)^"))");
8.77 +(*> calcul "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0));
8.78 +val it = ((1,0),(0,0))*)
8.79 +
8.80 +(*.convert internal floatingpoint prepresentation to int and float.*)
8.81 +fun term_of_float T ((val1, 0), ( 0, 0)) =
8.82 + TermC.term_of_num T val1
8.83 + | term_of_float T ((val1, val2), (precision1, precision2)) =
8.84 + let val pT = TermC.pairT T T
8.85 + in Const ("Float.Float", (TermC.pairT pT pT) --> T)
8.86 + $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int val1, T))
8.87 + (Free (TermC.str_of_int val2, T)))
8.88 + (TermC.pairt (Free (TermC.str_of_int precision1, T))
8.89 + (Free (TermC.str_of_int precision2, T))))
8.90 + end;
8.91 +(*> val t = str2term "Float ((1,2),(0,0))";
8.92 +> val Const ("Float.Float", fT) $ _ = t;
8.93 +> atomtyp fT;
8.94 +> val ffT = (pairT (pairT HOLogic.realT HOLogic.realT)
8.95 +> (pairT HOLogic.realT HOLogic.realT)) --> HOLogic.realT;
8.96 +> atomtyp ffT;
8.97 +> fT = ffT;
8.98 +val it = true : bool
8.99 +
8.100 +t = float_term_of_num HOLogic.realT ((1,2),(0,0));
8.101 +val it = true : bool*)
8.102 +
8.103 +(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
8.104 +fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) =
8.105 + TermC.mk_var_op_num v op_ optype ntyp v1
8.106 + | var_op_float v op_ optype T ((v1, v2), (p1, p2)) =
8.107 + let val pT = TermC.pairT T T
8.108 + in Const (op_, optype) $ v $
8.109 + (Const ("Float.Float", (TermC.pairT pT pT) --> T)
8.110 + $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int v1, T))
8.111 + (Free (TermC.str_of_int v2, T)))
8.112 + (TermC.pairt (Free (TermC.str_of_int p1, T))
8.113 + (Free (TermC.str_of_int p2, T)))))
8.114 + end;
8.115 +(*> val t = str2term "a + b";
8.116 +> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
8.117 +> val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";
8.118 +> t = var_op_float v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
8.119 +val it = true : bool*)
8.120 +
8.121 +(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
8.122 +fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) =
8.123 + TermC.mk_num_op_var v op_ optype ntyp v1
8.124 + | float_op_var v op_ optype T ((v1, v2), (p1, p2)) =
8.125 + let val pT = TermC.pairT T T
8.126 + in Const (op_, optype) $
8.127 + (Const ("Float.Float", (TermC.pairT pT pT) --> T)
8.128 + $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int v1, T))
8.129 + (Free (TermC.str_of_int v2, T)))
8.130 + (TermC.pairt (Free (TermC.str_of_int p1, T))
8.131 + (Free (TermC.str_of_int p2, T))))) $ v
8.132 + end;
8.133 +(*> val t = str2term "a + b";
8.134 +> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
8.135 +> val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";
8.136 +> t = float_op_var v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
8.137 +val it = true : bool*)
8.138 +
8.139 end
8.140
8.141