12 "----------- Pattern.match ------------------------------"; |
12 "----------- Pattern.match ------------------------------"; |
13 "----------- fun TermC.matches --------------------------------"; |
13 "----------- fun TermC.matches --------------------------------"; |
14 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------------------"; |
14 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------------------"; |
15 "----------- fun TermC.vars_of -----------------------------------------------------------------"; |
15 "----------- fun TermC.vars_of -----------------------------------------------------------------"; |
16 "----------- fun TermC.vars --------------------------------------------------------------------"; |
16 "----------- fun TermC.vars --------------------------------------------------------------------"; |
17 "----------- uminus_to_string ---------------------------"; |
|
18 "----------- *** Problem.prep_input: syntax error in '#Where' of [v"; |
17 "----------- *** Problem.prep_input: syntax error in '#Where' of [v"; |
19 "----------- check writeln, tracing for string markup ---"; |
18 "----------- check writeln, tracing for string markup ---"; |
20 "----------- build fun TermC.is_bdv_subst ------------------------------------------------------------"; |
19 "----------- build fun TermC.is_bdv_subst ------------------------------------------------------------"; |
21 "----------- fun str_of_int --------------------------------------------------------------------"; |
20 "----------- fun str_of_int --------------------------------------------------------------------"; |
22 "----------- fun TermC.scala_of_term -----------------------------------------------------------------"; |
21 "----------- fun TermC.scala_of_term -----------------------------------------------------------------"; |
28 "----------- fun TermC.ins_concl ---------------------------------------------------------------------"; |
27 "----------- fun TermC.ins_concl ---------------------------------------------------------------------"; |
29 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------"; |
28 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------"; |
30 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------"; |
29 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------"; |
31 "----------- fun TermC.is_list -----------------------------------------------------------------------"; |
30 "----------- fun TermC.is_list -----------------------------------------------------------------------"; |
32 "----------- fun inst_abs ----------------------------------------------------------------------"; |
31 "----------- fun inst_abs ----------------------------------------------------------------------"; |
33 "----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------"; |
|
34 "--------------------------------------------------------"; |
32 "--------------------------------------------------------"; |
35 "--------------------------------------------------------"; |
33 "--------------------------------------------------------"; |
36 |
34 |
37 "----------- numerals in Isabelle2011/12/13 -------------"; |
35 "----------- numerals in Isabelle2011/12/13 -------------"; |
38 "----------- numerals in Isabelle2011/12/13 -------------"; |
36 "----------- numerals in Isabelle2011/12/13 -------------"; |
182 (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const ("...", "num"))))*) |
180 (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const ("...", "num"))))*) |
183 |
181 |
184 "----------- inst_bdv -----------------------------------"; |
182 "----------- inst_bdv -----------------------------------"; |
185 "----------- inst_bdv -----------------------------------"; |
183 "----------- inst_bdv -----------------------------------"; |
186 "----------- inst_bdv -----------------------------------"; |
184 "----------- inst_bdv -----------------------------------"; |
187 if (UnparseC.term o Thm.prop_of o ThmC.numerals_to_Free) @{thm d1_isolate_add2} = |
185 if (UnparseC.term o Thm.prop_of) @{thm d1_isolate_add2} = |
188 "\<not> ?bdv occurs_in ?a \<Longrightarrow>\n(?a + ?bdv = 0) = (?bdv = - 1 * ?a)" |
186 "\<not> ?bdv occurs_in ?a \<Longrightarrow>\n(?a + ?bdv = 0) = (?bdv = - 1 * ?a)" |
189 then () |
187 then () |
190 else error "termC.sml d1_isolate_add2"; |
188 else error "termC.sml d1_isolate_add2"; |
191 val subst = [(TermC.str2term "bdv", TermC.str2term "x")]; |
189 val subst = [(TermC.str2term "bdv", TermC.str2term "x")]; |
192 val t = (Eval.norm o Thm.prop_of) (ThmC.numerals_to_Free @{thm d1_isolate_add2}); |
190 val t = (Eval.norm o Thm.prop_of) @{thm d1_isolate_add2}; |
193 val t' = TermC.inst_bdv subst t; |
191 val t' = TermC.inst_bdv subst t; |
194 if UnparseC.term t' = "\<not> x occurs_in ?a \<Longrightarrow> (?a + x = 0) = (x = - 1 * ?a)" |
192 if UnparseC.term t' = "\<not> x occurs_in ?a \<Longrightarrow> (?a + x = 0) = (x = - 1 * ?a)" |
195 then () |
193 then () |
196 else error "termC.sml inst_bdv 1"; |
194 else error "termC.sml inst_bdv 1"; |
197 if (UnparseC.term o Thm.prop_of o ThmC.numerals_to_Free) @{thm separate_bdvs_add} = |
195 if (UnparseC.term o Thm.prop_of) @{thm separate_bdvs_add} = |
198 "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0,\n " ^ |
196 "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0,\n " ^ |
199 "?bdv_4.0] occur_exactly_in ?a \<Longrightarrow>\n(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)" |
197 "?bdv_4.0] occur_exactly_in ?a \<Longrightarrow>\n(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)" |
200 then () else error "termC.sml separate_bdvs_add"; |
198 then () else error "termC.sml separate_bdvs_add"; |
201 (*default_print_depth 5;*) |
199 (*default_print_depth 5;*) |
202 |
200 |
203 val subst = |
201 val subst = |
204 [(TermC.str2term "bdv_1", TermC.str2term "c"), |
202 [(TermC.str2term "bdv_1", TermC.str2term "c"), |
205 (TermC.str2term "bdv_2", TermC.str2term "c_2"), |
203 (TermC.str2term "bdv_2", TermC.str2term "c_2"), |
206 (TermC.str2term "bdv_3", TermC.str2term "c_3"), |
204 (TermC.str2term "bdv_3", TermC.str2term "c_3"), |
207 (TermC.str2term "bdv_4", TermC.str2term "c_4")]; |
205 (TermC.str2term "bdv_4", TermC.str2term "c_4")]; |
208 val t = (Eval.norm o Thm.prop_of) (ThmC.numerals_to_Free @{thm separate_bdvs_add}); |
206 val t = (Eval.norm o Thm.prop_of) @{thm separate_bdvs_add}; |
209 val t' = TermC.inst_bdv subst t; |
207 val t' = TermC.inst_bdv subst t; |
210 |
208 |
211 if UnparseC.term t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a \<Longrightarrow>\n" ^ |
209 if UnparseC.term t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a \<Longrightarrow>\n" ^ |
212 "(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)" |
210 "(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)" |
213 then () else error "termC.sml inst_bdv 2"; |
211 then () else error "termC.sml inst_bdv 2"; |
415 |
412 |
416 case TermC.vars_of t of [Const (\<^const_name>\<open>AA\<close>, _), Const (\<^const_name>\<open>HOL.eq\<close>, _)] => () |
413 case TermC.vars_of t of [Const (\<^const_name>\<open>AA\<close>, _), Const (\<^const_name>\<open>HOL.eq\<close>, _)] => () |
417 | _ => error "TermC.vars_of (3 = 3 * AA / 4) ..changed (! use only for polynomials, not equations!)"; |
414 | _ => error "TermC.vars_of (3 = 3 * AA / 4) ..changed (! use only for polynomials, not equations!)"; |
418 |
415 |
419 |
416 |
420 "----------- uminus_to_string ---------------------------"; |
|
421 "----------- uminus_to_string ---------------------------"; |
|
422 "----------- uminus_to_string ---------------------------"; |
|
423 val t1 = ThmC_Def.num_to_Free @{term "-2::real"}; |
|
424 val t2 = ThmC_Def.num_to_Free @{term "- 2::real"}; |
|
425 if TermC.uminus_to_string t2 = t1 |
|
426 then () |
|
427 else error "termC.sml diff.behav. in uminus_to_string"; |
|
428 |
|
429 "----------- *** Problem.prep_input: syntax error in '#Where' of [v"; |
417 "----------- *** Problem.prep_input: syntax error in '#Where' of [v"; |
430 "----------- *** Problem.prep_input: syntax error in '#Where' of [v"; |
418 "----------- *** Problem.prep_input: syntax error in '#Where' of [v"; |
431 "----------- *** Problem.prep_input: syntax error in '#Where' of [v"; |
419 "----------- *** Problem.prep_input: syntax error in '#Where' of [v"; |
432 "===== deconstruct datatype typ ==="; |
420 "===== deconstruct datatype typ ==="; |
433 val str = "?a"; |
421 val str = "?a"; |
434 val t = (thy, str) |>> ThyC.to_ctxt |
422 val t = (thy, str) |>> ThyC.to_ctxt |
435 |-> Proof_Context.read_term_pattern |
423 |-> Proof_Context.read_term_pattern; |
436 |> ThmC_Def.num_to_Free; |
|
437 val Var (("a", 0), ty) = t; |
424 val Var (("a", 0), ty) = t; |
438 val TVar ((str, i), srt) = ty; |
425 val TVar ((str, i), srt) = ty; |
439 if str = "'a" andalso i = 1 andalso srt = [] |
426 if str = "'a" andalso i = 1 andalso srt = [] |
440 then () |
427 then () |
441 else error "termC.sml type-structure of \"?a\" changed"; |
428 else error "termC.sml type-structure of \"?a\" changed"; |
442 |
429 |
443 "----- real type in pattern ---"; |
430 "----- real type in pattern ---"; |
444 val str = "?a :: real"; |
431 val str = "?a :: real"; |
445 val t = (thy, str) |>> ThyC.to_ctxt |
432 val t = (thy, str) |>> ThyC.to_ctxt |
446 |-> Proof_Context.read_term_pattern |
433 |-> Proof_Context.read_term_pattern; |
447 |> ThmC_Def.num_to_Free; |
|
448 val Var (("a", 0), ty) = t; |
434 val Var (("a", 0), ty) = t; |
449 val Type (str, tys) = ty; |
435 val Type (str, tys) = ty; |
450 if str = \<^type_name>\<open>real\<close> andalso tys = [] andalso ty = HOLogic.realT |
436 if str = \<^type_name>\<open>real\<close> andalso tys = [] andalso ty = HOLogic.realT |
451 then () |
437 then () |
452 else error "termC.sml type-structure of \"?a :: real\" changed"; |
438 else error "termC.sml type-structure of \"?a :: real\" changed"; |
458 " matchsub (?a + (?b - ?c)) t_t )"); |
444 " matchsub (?a + (?b - ?c)) t_t )"); |
459 val ctxt = Proof_Context.init_global thy; |
445 val ctxt = Proof_Context.init_global thy; |
460 val ctxt = Config.put show_types true ctxt; |
446 val ctxt = Config.put show_types true ctxt; |
461 "----- read_term_pattern ---"; |
447 "----- read_term_pattern ---"; |
462 val t = (thy, str) |>> ThyC.to_ctxt |
448 val t = (thy, str) |>> ThyC.to_ctxt |
463 |-> Proof_Context.read_term_pattern |
449 |-> Proof_Context.read_term_pattern; |
464 |> ThmC_Def.num_to_Free; |
|
465 val t_real = TermC.typ_a2real t; |
450 val t_real = TermC.typ_a2real t; |
466 if UnparseC.term_in_ctxt ctxt t_real = |
451 if UnparseC.term_in_ctxt ctxt t_real = |
467 "\<not> (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) \<or>\n " |
452 "\<not> (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) \<or>\n " |
468 ^ "matchsub (?a + (?b - ?c)) t_t \<or>\n " |
453 ^ "matchsub (?a + (?b - ?c)) t_t \<or>\n " |
469 ^ "matchsub (?a - (?b + ?c)) t_t \<or> matchsub (?a + (?b - ?c)) t_t)" then () |
454 ^ "matchsub (?a - (?b + ?c)) t_t \<or> matchsub (?a + (?b - ?c)) t_t)" then () |
644 (Const (\<^const_name>\<open>times\<close>, _) $ Var (("n", 0), _) $ Var (("k", 0), _))) $ |
629 (Const (\<^const_name>\<open>times\<close>, _) $ Var (("n", 0), _) $ Var (("k", 0), _))) $ |
645 (Const (\<^const_name>\<open>divide\<close>, _) $ Var (("m", 0), _) $ Var (("n", 0), _)))) = prop; |
630 (Const (\<^const_name>\<open>divide\<close>, _) $ Var (("m", 0), _) $ Var (("n", 0), _)))) = prop; |
646 val SOME t' = TermC.strip_imp_prems' t; |
631 val SOME t' = TermC.strip_imp_prems' t; |
647 if UnparseC.term t' = "(\<Longrightarrow>) (?k \<noteq> 0)" then () else error "TermC.strip_imp_prems' changed"; |
632 if UnparseC.term t' = "(\<Longrightarrow>) (?k \<noteq> 0)" then () else error "TermC.strip_imp_prems' changed"; |
648 |
633 |
649 val thm = ThmC.numerals_to_Free @{thm frac_sym_conv}; |
634 val thm = @{thm frac_sym_conv}; |
650 val prop = Thm.prop_of thm; |
635 val prop = Thm.prop_of thm; |
651 val concl = Logic.strip_imp_concl prop; |
636 val concl = Logic.strip_imp_concl prop; |
652 val SOME prems = TermC.strip_imp_prems' prop; |
637 val SOME prems = TermC.strip_imp_prems' prop; |
653 val prop' = TermC.ins_concl prems concl; |
638 val prop' = TermC.ins_concl prems concl; |
654 if prop = prop' then () else error "TermC.ins_concl o strip_imp_concl"; |
639 if prop = prop' then () else error "TermC.ins_concl o strip_imp_concl"; |
682 if TermC.is_list t = false then () else error "TermC.is_list lll::real list"; |
667 if TermC.is_list t = false then () else error "TermC.is_list lll::real list"; |
683 |
668 |
684 val t = TermC.str2term "[a, b, c]"; |
669 val t = TermC.str2term "[a, b, c]"; |
685 val ty = (Term.type_of o Thm.term_of) ct; |
670 val ty = (Term.type_of o Thm.term_of) ct; |
686 if TermC.is_list t = true then () else error "TermC.is_list [a, b, c]"; |
671 if TermC.is_list t = true then () else error "TermC.is_list [a, b, c]"; |
687 |
|
688 "----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------"; |
|
689 "----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------"; |
|
690 "----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------"; |
|
691 case ThmC_Def.num_to_Free @{term "123::real"} of |
|
692 Const (\<^const_name>\<open>numeral\<close>, _) $ |
|
693 (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ |
|
694 (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ |
|
695 (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))))))) => () |
|
696 | _ => error "ThmC_Def.num_to_Free '123' changed"; |
|
697 |
|
698 case ThmC_Def.num_to_Free @{term "1::real"} of |
|
699 Const (\<^const_name>\<open>one_class.one\<close>, _) => () |
|
700 | _ => error "ThmC_Def.num_to_Free '1' changed"; |
|
701 |
|
702 case ThmC_Def.num_to_Free @{term "0::real"} of |
|
703 Const (\<^const_name>\<open>zero_class.zero\<close>, _) => () |
|
704 | _ => error "ThmC_Def.num_to_Free '0' changed"; |
|
705 |
672 |
706 "----------- fun mk_frac, proper term with uminus ----------------------------------------------"; |
673 "----------- fun mk_frac, proper term with uminus ----------------------------------------------"; |
707 "----------- fun mk_frac, proper term with uminus ----------------------------------------------"; |
674 "----------- fun mk_frac, proper term with uminus ----------------------------------------------"; |
708 "----------- fun mk_frac, proper term with uminus ----------------------------------------------"; |
675 "----------- fun mk_frac, proper term with uminus ----------------------------------------------"; |
709 TermC.mk_frac: typ -> int * (int * int) -> term; |
676 TermC.mk_frac: typ -> int * (int * int) -> term; |