8 val t' = ((list2isalist HOLogic.realT) o vars) t; |
8 val t' = ((list2isalist HOLogic.realT) o vars) t; |
9 val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg); |
9 val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg); |
10 in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end |
10 in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end |
11 | eval_var _ _ _ _ = raise GO_ON; |
11 | eval_var _ _ _ _ = raise GO_ON; |
12 (* |
12 (* |
13 > val t = (term_of o the o (parse thy)) "Var (A=a*(b::real))"; |
13 > val t = (Thm.term_of o the o (parse thy)) "Var (A=a*(b::real))"; |
14 > val op_ = "Var"; |
14 > val op_ = "Var"; |
15 > val eval_fn = the (assoc (!eval_list, op_)); |
15 > val eval_fn = the (assoc (!eval_list, op_)); |
16 > get_pair op_ eval_fn t; |
16 > get_pair op_ eval_fn t; |
17 > val (t as (Const(op0,t0) $ arg)) = t; |
17 > val (t as (Const(op0,t0) $ arg)) = t; |
18 > eval_fn op0 t; |
18 > eval_fn op0 t; |
25 val it = "Var ((A::real) = (a::real) * (b::real)) = [A, a, b]" : string |
25 val it = "Var ((A::real) = (a::real) * (b::real)) = [A, a, b]" : string |
26 *) |
26 *) |
27 fun eval_Length (thmid:string) (op_:string) |
27 fun eval_Length (thmid:string) (op_:string) |
28 (t as (Const(op0,t0) $ arg)) thy = |
28 (t as (Const(op0,t0) $ arg)) thy = |
29 let |
29 let |
30 val t' = ((term_of_num HOLogic.realT) o length o isalist2list) arg; |
30 val t' = ((Thm.term_of_num HOLogic.realT) o length o isalist2list) arg; |
31 val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg); |
31 val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg); |
32 in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end |
32 in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end |
33 | eval_Length _ _ _ _ = raise GO_ON; |
33 | eval_Length _ _ _ _ = raise GO_ON; |
34 (* |
34 (* |
35 > val thmid = "#Length_"; val op_ = "Length"; |
35 > val thmid = "#Length_"; val op_ = "Length"; |
36 > val s = "Length [A = a * b, a // #2 = #2]"; |
36 > val s = "Length [A = a * b, a // #2 = #2]"; |
37 > val (t as (Const(op0,t0) $ arg)) = (term_of o the o (parse thy)) s; |
37 > val (t as (Const(op0,t0) $ arg)) = (Thm.term_of o the o (parse thy)) s; |
38 > val (SOME (id,t')) = eval_Length thmid op_ t; |
38 > val (SOME (id,t')) = eval_Length thmid op_ t; |
39 val id = "#Length_[A = a * b, a // #2 = #2]" : string |
39 val id = "#Length_[A = a * b, a // #2 = #2]" : string |
40 val t' = Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#)) |
40 val t' = Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#)) |
41 val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm |
41 val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm |
42 --------------------------------------------- |
42 --------------------------------------------- |
45 "if #1 < Length [A = a * b, a // #2 = #2] \ |
45 "if #1 < Length [A = a * b, a // #2 = #2] \ |
46 \then make_fun (R, [make, function], no_met) A a_ [A = a * b, a // #2 = #2]\ |
46 \then make_fun (R, [make, function], no_met) A a_ [A = a * b, a // #2 = #2]\ |
47 \else hd [A = a * b, a // #2 = #2]"; |
47 \else hd [A = a * b, a // #2 = #2]"; |
48 |
48 |
49 > (Thm.global_cterm_of thy) t'; |
49 > (Thm.global_cterm_of thy) t'; |
50 > val t = (term_of o the o (parse thy)) s; |
50 > val t = (Thm.term_of o the o (parse thy)) s; |
51 > val eval_fn = the (assoc (!eval_list, op_)); |
51 > val eval_fn = the (assoc (!eval_list, op_)); |
52 > val (SOME(_,t')) = get_pair op_ eval_fn t; |
52 > val (SOME(_,t')) = get_pair op_ eval_fn t; |
53 val t' = Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#)) |
53 val t' = Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#)) |
54 val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm |
54 val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm |
55 |
55 |
85 ) |
85 ) |
86 | eval_Nth _ _ _ _ = raise GO_ON; |
86 | eval_Nth _ _ _ _ = raise GO_ON; |
87 (* |
87 (* |
88 > val thmid = "#Nth_"; val op_ = "Nth"; |
88 > val thmid = "#Nth_"; val op_ = "Nth"; |
89 > val s = "Nth #2 [A = a * b, a // #2 = #2]"; |
89 > val s = "Nth #2 [A = a * b, a // #2 = #2]"; |
90 > val t = (term_of o the o (parse thy)) s; |
90 > val t = (Thm.term_of o the o (parse thy)) s; |
91 > eval_Nth thmid op_ t; |
91 > eval_Nth thmid op_ t; |
92 |
92 |
93 > val eval_fn = the (assoc (!eval_list, op_)); |
93 > val eval_fn = the (assoc (!eval_list, op_)); |
94 > val (SOME(id,t')) = get_pair op_ eval_fn t; |
94 > val (SOME(id,t')) = get_pair op_ eval_fn t; |
95 > (Thm.global_cterm_of thy) t'; |
95 > (Thm.global_cterm_of thy) t'; |