978 SubProblem (DiffApp_, [univar, equation], [no_met]) |
978 SubProblem (DiffApp_, [univar, equation], [no_met]) |
979 [BOOL e_1 BOUND_2, REAL v_1 BOUND_0] |
979 [BOOL e_1 BOUND_2, REAL v_1 BOUND_0] |
980 in Substitute [(v_1 BOUND_1 = (rhs o hd) s_1 BOUND_0)] h_ BOUND_4 |
980 in Substitute [(v_1 BOUND_1 = (rhs o hd) s_1 BOUND_0)] h_ BOUND_4 |
981 *) |
981 *) |
982 |
982 |
983 |
983 (* for parse and parse_patt: fix all types to real *) |
984 fun T_a2real (Type (s, [])) = |
984 fun T_a2real (Type (s, [])) = |
985 if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else Type (s, []) |
985 if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT |
|
986 else Type (s, []) |
986 | T_a2real (Type (s, Ts)) = Type (s, map T_a2real Ts) |
987 | T_a2real (Type (s, Ts)) = Type (s, map T_a2real Ts) |
987 | T_a2real (TFree (s, srt)) = |
988 | T_a2real (TFree (s, srt)) = |
988 if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TFree (s, srt) |
989 if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT |
989 | T_a2real (TVar (("DUMMY",_),srt)) = HOLogic.realT; |
990 else TFree (s, srt) |
|
991 | T_a2real (TVar ((s, i), srt)) = |
|
992 if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT |
|
993 else TVar ((s, i), srt) |
|
994 | T_a2real (TVar (("DUMMY",_), srt)) = HOLogic.realT; |
990 |
995 |
991 (*FIXME .. fixes the type (+see Typefix.thy*) |
996 (*FIXME .. fixes the type (+see Typefix.thy*) |
992 fun typ_a2real (Const( s, T)) = (Const( s, T_a2real T)) |
997 fun typ_a2real (Const( s, T)) = (Const( s, T_a2real T)) |
993 | typ_a2real (Free( s, T)) = (Free( s, T_a2real T)) |
998 | typ_a2real (Free( s, T)) = (Free( s, T_a2real T)) |
994 | typ_a2real (Var( n, T)) = (Var( n, T_a2real T)) |
999 | typ_a2real (Var( n, T)) = (Var( n, T_a2real T)) |
995 | typ_a2real (Bound i) = (Bound i) |
1000 | typ_a2real (Bound i) = (Bound i) |
996 | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t) |
1001 | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t) |
997 | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2); |
1002 | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2); |
998 (* |
1003 |
999 ----------------6.8.02--------------------------------------------------- |
1004 |
1000 val str = "1"; |
1005 (* before 2002 *) |
1001 val t = read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[]))); |
|
1002 atomty (term_of t); |
|
1003 *** ------------- |
|
1004 *** Const ( 1, 'a) |
|
1005 val t = (app_num_tr' o term_of) t; |
|
1006 atomty t; |
|
1007 *** ------------- |
|
1008 *** Const ( 1, 'a) |
|
1009 val t = typ_a2real t; |
|
1010 atomty t; |
|
1011 *** ------------- |
|
1012 *** Const ( 1, real) |
|
1013 |
|
1014 val str = "2"; |
|
1015 val t = read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[]))); |
|
1016 atomty (term_of t); |
|
1017 *** ------------- |
|
1018 *** Const ( Numeral.number_of, bin => 'a) |
|
1019 *** . Const ( Numeral.bin.Bit, [bin, bool] => bin) |
|
1020 *** . . Const ( Numeral.bin.Bit, [bin, bool] => bin) |
|
1021 *** . . . Const ( Numeral.bin.Pls, bin) |
|
1022 *** . . . Const ( True, bool) |
|
1023 *** . . Const ( False, bool) |
|
1024 val t = (app_num_tr' o term_of) t; |
|
1025 atomty t; |
|
1026 *** ------------- |
|
1027 *** Free ( 2, 'a) |
|
1028 val t = typ_a2real t; |
|
1029 atomty t; |
|
1030 *** ------------- |
|
1031 *** Free ( 2, real) |
|
1032 ----------------6.8.02--------------------------------------------------- |
|
1033 |
|
1034 |
|
1035 > val str = "R"; |
|
1036 > val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[])))); |
|
1037 val t = Free ("R","?DUMMY") : term |
|
1038 > val t' = typ_a2real t; |
|
1039 > (cterm_of thy) t'; |
|
1040 val it = "R::RealDef.real" : cterm |
|
1041 |
|
1042 > val str = "R=R"; |
|
1043 > val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[])))); |
|
1044 > atomty (typ_a2real t); |
|
1045 *** ------------- |
|
1046 *** Const ( op =, [RealDef.real, RealDef.real] => bool) |
|
1047 *** Free ( R, RealDef.real) |
|
1048 *** Free ( R, RealDef.real) |
|
1049 > val t' = typ_a2real t; |
|
1050 > (cterm_of thy) t'; |
|
1051 val it = "(R::RealDef.real) = R" : cterm |
|
1052 |
|
1053 > val str = "fixed_values [R=R]"; |
|
1054 > val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[])))); |
|
1055 > val t' = typ_a2real t; |
|
1056 > (cterm_of thy) t'; |
|
1057 val it = "fixed_values [(R::RealDef.real) = R]" : cterm |
|
1058 *) |
|
1059 |
|
1060 (*TODO.WN0609: parse should return a term or a string |
|
1061 (or even more comprehensive datastructure for error-messages) |
|
1062 i.e. in wrapping with SOME term or NONE the latter is not sufficient*) |
|
1063 (*2002 fun parseold thy str = |
|
1064 (let |
|
1065 val sgn = sign_of thy; |
|
1066 val t = ((*typ_a2real o*) app_num_tr'1 o term_of) |
|
1067 (read_cterm sgn (str,(TVar(("DUMMY",0),[])))); |
|
1068 in SOME (cterm_of sgn t) end) |
|
1069 handle _ => NONE;*) |
|
1070 |
|
1071 |
|
1072 |
|
1073 fun parseold thy str = |
1006 fun parseold thy str = |
1074 (let val t = ((*typ_a2real o*) numbers_to_string) |
1007 (let val t = ((*typ_a2real o*) numbers_to_string) |
1075 (Syntax.read_term_global thy str) |
1008 (Syntax.read_term_global thy str) |
1076 in SOME (cterm_of thy t) end) |
1009 in SOME (cterm_of thy t) end) |
1077 handle _ => NONE; |
1010 handle _ => NONE; |
1122 *** ------------- |
1055 *** ------------- |
1123 *** Const ( op =, [RealDef.real, RealDef.real] => bool) |
1056 *** Const ( op =, [RealDef.real, RealDef.real] => bool) |
1124 *** Free ( R, RealDef.real) |
1057 *** Free ( R, RealDef.real) |
1125 *** Free ( R, RealDef.real) *) |
1058 *** Free ( R, RealDef.real) *) |
1126 |
1059 |
1127 (*fun parse_patt thy str = |
1060 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation*) |
1128 (**** prep_pbt: syntax error in '#Where' of ["equation"] |
1061 fun parse_patt thy str = (thy, str) |>> thy2ctxt |
1129 *** Exception- TOPLEVEL_ERROR raised |
|
1130 *** At command "ML" (line 172 of "/usr/local/isabisac/src/Tools/isac/Knowledge/Poly.thy").*) |
|
1131 (typ_a2real o numbers_to_string o |
|
1132 ProofContext.read_term_pattern (thy2ctxt thy)) str;*) |
|
1133 fun parse_patt thy str = |
|
1134 ProofContext.read_term_pattern (thy2ctxt thy) str; |
|
1135 (*fun parse_patt thy str = (thy, str) |>> thy2ctxt |
|
1136 |-> ProofContext.read_term_pattern |
1062 |-> ProofContext.read_term_pattern |
1137 |> numbers_to_string |
1063 |> numbers_to_string |
1138 |> typ_a2real;*) |
1064 |> typ_a2real; |
|
1065 (* |
|
1066 fun parse_patt thy str = (thy, str) |>> thy2ctxt |
|
1067 |-> ProofContext.read_term_pattern; |
|
1068 *) |
1139 |
1069 |
1140 (*version for testing local to theories*) |
1070 (*version for testing local to theories*) |
1141 fun str2term_ thy str = (term_of o the o (parse thy)) str; |
1071 fun str2term_ thy str = (term_of o the o (parse thy)) str; |
1142 fun str2term str = (term_of o the o (parse (theory "Isac"))) str; |
1072 fun str2term str = (term_of o the o (parse (theory "Isac"))) str; |
1143 fun strs2terms ss = map str2term ss; |
1073 fun strs2terms ss = map str2term ss; |