43 subsection \<open>ML code for functions in pre-conditions and program-expressions\<close> |
43 subsection \<open>ML code for functions in pre-conditions and program-expressions\<close> |
44 ML \<open> |
44 ML \<open> |
45 signature PROG_EXPR = |
45 signature PROG_EXPR = |
46 sig |
46 sig |
47 val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option |
47 val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option |
48 val eval_matches: string -> string -> term -> theory -> (string * term) option |
48 val eval_matches: string -> string -> term -> Proof.context -> (string * term) option |
49 val matchsub: theory -> term -> term -> bool |
49 val matchsub: theory -> term -> term -> bool |
50 val eval_matchsub: string -> string -> term -> theory -> (string * term) option |
50 val eval_matchsub: string -> string -> term -> Proof.context -> (string * term) option |
51 val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option |
51 val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option |
52 val eval_var: string -> string -> term -> theory -> (string * term) option |
52 val eval_var: string -> string -> term -> Proof.context -> (string * term) option |
53 |
53 |
54 val or2list: term -> term |
54 val or2list: term -> term |
55 |
55 |
56 val occurs_in: term -> term -> bool |
56 val occurs_in: term -> term -> bool |
57 val eval_occurs_in: 'a -> string -> term -> 'b -> (string * term) option |
57 val eval_occurs_in: 'a -> string -> term -> 'b -> (string * term) option |
60 val eval_is_atom: string -> string -> term -> 'a -> (string * term) option |
60 val eval_is_atom: string -> string -> term -> 'a -> (string * term) option |
61 val eval_is_num: string -> string -> term -> 'a -> (string * term) option |
61 val eval_is_num: string -> string -> term -> 'a -> (string * term) option |
62 val even: int -> bool |
62 val even: int -> bool |
63 val eval_is_even: string -> string -> term -> 'a -> (string * term) option |
63 val eval_is_even: string -> string -> term -> 'a -> (string * term) option |
64 val eval_equ: string -> string -> term -> 'a -> (string * term) option |
64 val eval_equ: string -> string -> term -> 'a -> (string * term) option |
65 val eval_ident: string -> string -> term -> theory -> (string * term) option |
65 val eval_ident: string -> string -> term -> Proof.context -> (string * term) option |
66 val eval_equal: string -> string -> term -> theory -> (string * term) option |
66 val eval_equal: string -> string -> term -> Proof.context -> (string * term) option |
67 val eval_cancel: string -> string -> term -> 'a -> (string * term) option |
67 val eval_cancel: string -> string -> term -> 'a -> (string * term) option |
68 val eval_argument_in: string -> string -> term -> 'a -> (string * term) option |
68 val eval_argument_in: string -> string -> term -> 'a -> (string * term) option |
69 val same_funid: term -> term -> bool |
69 val same_funid: term -> term -> bool |
70 val eval_sameFunId: string -> string -> term -> 'a -> (string * term) option |
70 val eval_sameFunId: string -> string -> term -> 'a -> (string * term) option |
71 val eval_filter_sameFunId: string -> string -> term -> 'a -> (string * term) option |
71 val eval_filter_sameFunId: string -> string -> term -> 'a -> (string * term) option |
96 |
96 |
97 (** evaluation on the meta-level **) |
97 (** evaluation on the meta-level **) |
98 |
98 |
99 (*. evaluate the predicate matches (match on whole term only) .*) |
99 (*. evaluate the predicate matches (match on whole term only) .*) |
100 (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*) |
100 (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*) |
101 fun eval_matches (_:string) "Prog_Expr.matches" (t as Const (\<^const_name>\<open>Prog_Expr.matches\<close>, _) $ pat $ tst) thy = |
101 fun eval_matches (_:string) "Prog_Expr.matches" |
102 if TermC.matches thy tst pat |
102 (t as Const (\<^const_name>\<open>Prog_Expr.matches\<close>, _) $ pat $ tst) ctxt = |
|
103 if TermC.matches (Proof_Context.theory_of ctxt) tst pat |
103 then |
104 then |
104 let |
105 let |
105 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})) |
106 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})) |
106 in SOME (UnparseC.term_in_thy thy prop, prop) end |
107 in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end |
107 else |
108 else |
108 let |
109 let |
109 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})) |
110 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})) |
110 in SOME (UnparseC.term_in_thy thy prop, prop) end |
111 in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end |
111 | eval_matches _ _ _ _ = NONE; |
112 | eval_matches _ _ _ _ = NONE; |
112 |
113 |
113 (*.does a pattern match some subterm ?.*) |
114 (*.does a pattern match some subterm ?.*) |
114 fun matchsub thy t pat = |
115 fun matchsub thy t pat = |
115 let |
116 let |
124 else if matchs f1 then true else matchs f2 |
125 else if matchs f1 then true else matchs f2 |
125 in matchs t end; |
126 in matchs t end; |
126 |
127 |
127 (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*) |
128 (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*) |
128 fun eval_matchsub (_:string) "Prog_Expr.matchsub" |
129 fun eval_matchsub (_:string) "Prog_Expr.matchsub" |
129 (t as Const (\<^const_name>\<open>Prog_Expr.matchsub\<close>, _) $ pat $ tst) thy = |
130 (t as Const (\<^const_name>\<open>Prog_Expr.matchsub\<close>, _) $ pat $ tst) ctxt = |
130 if matchsub thy tst pat |
131 if matchsub (Proof_Context.theory_of ctxt) tst pat |
131 then |
132 then |
132 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})) |
133 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})) |
133 in SOME (UnparseC.term_in_thy thy prop, prop) end |
134 in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end |
134 else |
135 else |
135 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})) |
136 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})) |
136 in SOME (UnparseC.term_in_thy thy prop, prop) end |
137 in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end |
137 | eval_matchsub _ _ _ _ = NONE; |
138 | eval_matchsub _ _ _ _ = NONE; |
138 |
139 |
139 (*get the variables in an isabelle-term*) |
140 (*get the variables in an isabelle-term*) |
140 (*("Vars" ,("Prog_Expr.Vars" , eval_var "#Vars_")):calc*) |
141 (*("Vars" ,("Prog_Expr.Vars" , eval_var "#Vars_")):calc*) |
141 fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) thy = |
142 fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) ctxt = |
142 let |
143 let |
143 val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t; |
144 val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t; |
144 val thmId = thmid ^ UnparseC.term_in_thy thy arg; |
145 val thmId = thmid ^ UnparseC.term_in_ctxt ctxt arg; |
145 in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end |
146 in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end |
146 | eval_var _ _ _ _ = NONE; |
147 | eval_var _ _ _ _ = NONE; |
147 |
148 |
148 (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*) |
149 (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*) |
149 fun eval_lhs _ "Prog_Expr.lhs" (t as (Const (\<^const_name>\<open>lhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _))) _ = |
150 fun eval_lhs _ "Prog_Expr.lhs" (t as (Const (\<^const_name>\<open>lhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _))) _ = |
156 (*("rhs" ,("Prog_Expr.rhs" , eval_rhs "")):calc*) |
157 (*("rhs" ,("Prog_Expr.rhs" , eval_rhs "")):calc*) |
157 fun eval_rhs _ "Prog_Expr.rhs" (t as (Const (\<^const_name>\<open>rhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r))) _ = |
158 fun eval_rhs _ "Prog_Expr.rhs" (t as (Const (\<^const_name>\<open>rhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r))) _ = |
158 SOME (UnparseC.term t ^ " = " ^ UnparseC.term r, |
159 SOME (UnparseC.term t ^ " = " ^ UnparseC.term r, |
159 HOLogic.Trueprop $ (TermC.mk_equality (t, r))) |
160 HOLogic.Trueprop $ (TermC.mk_equality (t, r))) |
160 | eval_rhs _ _ _ _ = NONE; |
161 | eval_rhs _ _ _ _ = NONE; |
161 (*\\------------------------- from Prog_Expr.thy-------------------------------------------------//*) |
162 |
162 |
163 |
163 (*//------------------------- from Atools.thy------------------------------------------------\\*) |
|
164 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v); |
164 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v); |
165 |
|
166 (*("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""))*) |
165 (*("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""))*) |
167 fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const (\<^const_name>\<open>occurs_in\<close>, _) $ v $ t)) _ = |
166 fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const (\<^const_name>\<open>occurs_in\<close>, _) $ v $ t)) _ = |
168 ((*tracing("#>@ eval_occurs_in: v= "^(UnparseC.term v)); |
167 ((*tracing("#>@ eval_occurs_in: v= "^(UnparseC.term v)); |
169 tracing("#>@ eval_occurs_in: t= "^(UnparseC.term t));*) |
168 tracing("#>@ eval_occurs_in: t= "^(UnparseC.term t));*) |
170 if occurs_in v t |
169 if occurs_in v t |
285 |
284 |
286 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of |
285 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of |
287 the arguments: thus special handling by 'fun eval_binop'*) |
286 the arguments: thus special handling by 'fun eval_binop'*) |
288 (*("ident" ,("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")):calc*) |
287 (*("ident" ,("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")):calc*) |
289 fun eval_ident (thmid:string) "Prog_Expr.ident" (t as |
288 fun eval_ident (thmid:string) "Prog_Expr.ident" (t as |
290 (Const _(*op0, t0*) $ t1 $ t2 )) thy = |
289 (Const _(*op0, t0*) $ t1 $ t2 )) ctxt = |
291 if t1 = t2 |
290 if t1 = t2 |
292 then SOME (TermC.mk_thmid thmid |
291 then SOME (TermC.mk_thmid thmid |
293 ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")") |
292 ("(" ^ (UnparseC.term_in_ctxt ctxt t1) ^ ")") |
294 ("(" ^ (UnparseC.term_in_thy thy t2) ^ ")"), |
293 ("(" ^ (UnparseC.term_in_ctxt ctxt t2) ^ ")"), |
295 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) |
294 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) |
296 else SOME (TermC.mk_thmid thmid |
295 else SOME (TermC.mk_thmid thmid |
297 ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")") |
296 ("(" ^ (UnparseC.term_in_ctxt ctxt t1) ^ ")") |
298 ("(" ^ (UnparseC.term_in_thy thy t2) ^ ")"), |
297 ("(" ^ (UnparseC.term_in_ctxt ctxt t2) ^ ")"), |
299 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) |
298 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) |
300 | eval_ident _ _ _ _ = NONE; |
299 | eval_ident _ _ _ _ = NONE; |
301 (* TODO |
300 (* TODO |
302 > val t = str2term "x =!= 0"; |
301 > val t = str2term "x =!= 0"; |
303 > val SOME (str, t') = eval_ident "ident_" "b" t thy; |
302 > val SOME (str, t') = eval_ident "ident_" "b" t thy; |
318 |
317 |
319 |
318 |
320 (* evaluate identity of terms, which stay ready for further evaluation; |
319 (* evaluate identity of terms, which stay ready for further evaluation; |
321 thus returns False only for atoms *) |
320 thus returns False only for atoms *) |
322 (*("equal" ,(\<^const_name>\<open>HOL.eq\<close>, Prog_Expr.eval_equal "#equal_")):calc*) |
321 (*("equal" ,(\<^const_name>\<open>HOL.eq\<close>, Prog_Expr.eval_equal "#equal_")):calc*) |
323 fun eval_equal (thmid : string) \<^const_name>\<open>HOL.eq\<close> (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy = |
322 fun eval_equal (thmid : string) \<^const_name>\<open>HOL.eq\<close> (t as (Const _(*op0,t0*) $ t1 $ t2 )) ctxt = |
324 if t1 = t2 |
323 if t1 = t2 |
325 then |
324 then |
326 SOME (TermC.mk_thmid thmid |
325 SOME (TermC.mk_thmid thmid |
327 ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy t2 ^ ")"), |
326 ("(" ^ UnparseC.term_in_ctxt ctxt t1 ^ ")") ("(" ^ UnparseC.term_in_ctxt ctxt t2 ^ ")"), |
328 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) |
327 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))) |
329 else |
328 else |
330 (case (TermC.is_atom t1, TermC.is_atom t2) of |
329 (case (TermC.is_atom t1, TermC.is_atom t2) of |
331 (true, true) => |
330 (true, true) => |
332 if TermC.variable_constant_pair (t1, t2) |
331 if TermC.variable_constant_pair (t1, t2) |
333 then NONE |
332 then NONE |
334 else SOME (TermC.mk_thmid thmid |
333 else SOME (TermC.mk_thmid thmid |
335 ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy t2 ^ ")"), |
334 ("(" ^ UnparseC.term_in_ctxt ctxt t1 ^ ")") ("(" ^ UnparseC.term_in_ctxt ctxt t2 ^ ")"), |
336 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) |
335 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) |
337 | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *) |
336 | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *) |
338 | eval_equal _ _ _ _ = NONE; (* error-exit *) |
337 | eval_equal _ _ _ _ = NONE; (* error-exit *) |
339 |
338 |
340 (*. evaluate HOL.divide .*) |
339 (*. evaluate HOL.divide .*) |