1 (* Title: collect all defitions for the Lucas-Interpreter
2 Author: Walther Neuper 110226
3 (c) due to copyright terms
6 theory Input_Descript imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
9 subsection \<open>typedecl for descriptions of input in specify-phase\<close>
11 The typedecl below MUST ALL be registered in "fun is_dsc"
13 typedecl nam (* named variables *)
14 typedecl una (* unnamed variables *)
15 typedecl unl (* unnamed variables of type list, elementwise input prohibited*)
16 typedecl str (* structured variables *)
17 typedecl toreal (* var with undef real value: forces typing *)
18 typedecl toreall (* var with undef real list value: forces typing *)
19 typedecl tobooll (* var with undef bool list value: forces typing *)
20 typedecl unknow (* input without dsc in fmz=[] *)
21 typedecl cpy (* copy-named variables identified by .._0, .._i .._' in pbt *)
23 subsection \<open>consts for general descriptions of input in specify-phase\<close>
26 (*TODO.180331: review for localisation of model-patterns and of method's guards*)
27 someList :: "'a list => unl" (*not for elementwise input, eg. inssort*)
29 additionalRels :: "bool list => una"
30 boundVariable :: "real => una"
31 derivative :: "real => una"
32 equalities :: "bool list => tobooll" (*WN071228 see fixedValues*)
33 equality :: "bool => una"
34 errorBound :: "bool => nam"
36 fixedValues :: "bool list => nam"
37 functionEq :: "bool => una" (*6.5.03: functionTerm -> functionEq*)
38 antiDerivative :: "bool => una"
39 functionOf :: "real => una"
40 (*functionTerm :: 'a => toreal 28.11.00*)
41 functionTerm :: "real => una" (*6.5.03: functionTerm -> functionEq*)
42 functionName :: "real => una"
43 interval :: "real set => una"
44 maxArgument :: "bool => toreal"
45 maximum :: "real => toreal"
47 relations :: "bool list => una"
48 solutions :: "bool list => toreall"
49 (*solution :: bool => toreal WN0509 bool list=> toreall --->EqSystem*)
50 solveFor :: "real => una"
51 differentiateFor:: "real => una"
52 unknown :: "'a => unknow"
53 valuesFor :: "real list => toreall"
55 intTestGiven :: "int => una"
56 realTestGiven :: "real => una"
57 realTestFind :: "real => una"
58 boolTestGiven :: "bool => una"
59 boolTestFind :: "bool => una"
61 subsection \<open>Functions decking for descriptions of input in specify-phase\<close>
64 signature INPUT_DESCRIPT =
66 val is_reall_dsc: term -> bool
67 val is_booll_dsc: term -> bool
68 val is_list_dsc: term -> bool
69 val is_unl: term -> bool
70 val is_dsc: term -> bool
71 val pbl_ids: Proof.context -> term -> term -> term list
72 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
74 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
76 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
80 structure Input_Descript(**): INPUT_DESCRIPT =(**)
83 (* distinguish input to Model (deep embedding of terms as Isac's object language) *)
84 fun is_reall_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("Real.real", [])]), _]))) = true
85 | is_reall_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("Real.real", [])]),_])) $ _) = true
86 | is_reall_dsc _ = false;
87 fun is_booll_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _]))) = true
88 | is_booll_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("HOL.bool", [])]),_])) $ _) = true
89 | is_booll_dsc _ = false;
90 fun is_list_dsc (Const (_, Type("fun", [Type("List.list", _), _]))) = true
91 | is_list_dsc (Const (_, Type("fun", [Type("List.list", _), _])) $ _) = true
92 (*WN:8.5.03: ??? TODO test/../scrtools.sml ~~~~ ???*)
93 | is_list_dsc _ = false;
94 fun is_unl (Const (_, Type("fun", [_, Type("Input_Descript.unl", _)]))) = true
96 fun is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.nam",_)]))) = true
97 | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.una",_)]))) = true
98 | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.unl",_)]))) = true
99 | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.str",_)]))) = true
100 | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.toreal",_)]))) = true
101 | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.toreall",_)])))= true
102 | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.tobooll",_)])))= true
103 | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.unknow",_)])))= true
104 | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.cpy",_)])))= true
107 (* given the input value (from split_dts)
108 make the value in a problem-env according to description-type
109 28.8.01: .nam and .una impl. properly, others copied .. TODO.
110 19/03/15 17:33, Makarius wrote:
111 >>> val i = case HOLogic.dest_number t of
112 >>> (Type ("Nat.nat", []), i) => i
113 >> Formal names should never be hardwired as ML string constants. Use
114 >> @{type_name nat} above, or better @{typ nat} for the whole type *)
115 fun pbl_ids ctxt (Const(_, Type ("fun", [_, Type ("Input_Descript.nam", _)]))) v =
117 then [v] (*eg. [r=Arbfix]*)
119 (case v of (*eg. eps=#0*) (Const ("HOL.eq", _) $ l $ r) => [r, l]
120 | _ => error ("pbl_ids Input_Descript.nam: no equality " ^ UnparseC.term_to_string' ctxt v))
121 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.una", _)]))) v = [v]
122 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.unl", _)]))) v = [v]
123 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.str", _)]))) v = [v]
124 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.toreal", _)]))) v = [v]
125 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.toreall", _)])))v = [v]
126 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.unknown" ,_)])))v = [v]
127 | pbl_ids _ _ v = error ("pbl_ids: not implemented for " ^ UnparseC.term2str v);
129 (* given an already input itm, ((14.9.01: no difference to pbl_ids jet!!))
130 make the value in a problem-env according to description-type.
131 28.8.01: .nam and .una impl. properly, others copied .. TODO
132 fun pbl_ids' (Const(_, Type ("fun", [_, Type ("Input_Descript.nam", _)]))) vs =
134 [] => error ("pbl_ids' Input_Descript.nam called with []")
136 (case t of (*eg. eps=#0*)
137 (Const ("HOL.eq",_) $ l $ r) => [r,l]
138 | _ => error ("pbl_ids' Input_Descript.nam: no equality " ^ term2str t))
139 | _ => vs (*14.9.01: ???TODO *))
140 | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.una", _)]))) vs = vs
141 | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.unl", _)]))) vs = vs
142 | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.str", _)]))) vs = vs
143 | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.toreal", _)]))) vs = vs
144 | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.toreall", _)])))vs = vs
145 | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.unknown", _)])))vs = vs
146 | pbl_ids' _ vs = error ("pbl_ids': not implemented for " ^ terms2str vs);*)