1016 val SOME (t,asm) = rewrite_set_inst_ ctxt true inst rls t; |
1016 val SOME (t,asm) = rewrite_set_inst_ ctxt true inst rls t; |
1017 if UnparseC.term t = "- 8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2" |
1017 if UnparseC.term t = "- 8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2" |
1018 then () else error "rls complete_square CHANGED"; |
1018 then () else error "rls complete_square CHANGED"; |
1019 |
1019 |
1020 val thm = @{thm square_explicit1}; |
1020 val thm = @{thm square_explicit1}; |
1021 val SOME (t,asm) = rewrite_ ctxt dummy_ord Rule_Set.Empty true thm t; |
1021 val SOME (t,asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true thm t; |
1022 if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8" |
1022 if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8" |
1023 then () else error "thm square_explicit1 CHANGED"; |
1023 then () else error "thm square_explicit1 CHANGED"; |
1024 |
1024 |
1025 val thm = @{thm root_plus_minus}; |
1025 val thm = @{thm root_plus_minus}; |
1026 val SOME (t,asm) = rewrite_ ctxt dummy_ord PolyEq_erls true thm t; |
1026 val SOME (t,asm) = rewrite_ ctxt Rewrite_Ord.function_empty PolyEq_erls true thm t; |
1027 if UnparseC.term t = |
1027 if UnparseC.term t = |
1028 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)" |
1028 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)" |
1029 then () else error "thm root_plus_minus CHANGED"; |
1029 then () else error "thm root_plus_minus CHANGED"; |
1030 |
1030 |
1031 (*the thm bdv_explicit2* here required to be constrained to ::real*) |
1031 (*the thm bdv_explicit2* here required to be constrained to ::real*) |
1032 val thm = @{thm bdv_explicit2}; |
1032 val thm = @{thm bdv_explicit2}; |
1033 val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t; |
1033 val SOME (t,asm) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true inst thm t; |
1034 if UnparseC.term t = |
1034 if UnparseC.term t = |
1035 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)" |
1035 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)" |
1036 then () else error "thm bdv_explicit2 CHANGED"; |
1036 then () else error "thm bdv_explicit2 CHANGED"; |
1037 |
1037 |
1038 val thm = @{thm bdv_explicit3}; |
1038 val thm = @{thm bdv_explicit3}; |
1039 val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t; |
1039 val SOME (t,asm) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true inst thm t; |
1040 if UnparseC.term t = |
1040 if UnparseC.term t = |
1041 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))" |
1041 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))" |
1042 then () else error "thm bdv_explicit3 CHANGED"; |
1042 then () else error "thm bdv_explicit3 CHANGED"; |
1043 |
1043 |
1044 val thm = @{thm bdv_explicit2}; |
1044 val thm = @{thm bdv_explicit2}; |
1045 val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t; |
1045 val SOME (t,asm) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true inst thm t; |
1046 if UnparseC.term t = |
1046 if UnparseC.term t = |
1047 "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))" |
1047 "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))" |
1048 then () else error "thm bdv_explicit2 CHANGED"; |
1048 then () else error "thm bdv_explicit2 CHANGED"; |
1049 |
1049 |
1050 val rls = calculate_RootRat; |
1050 val rls = calculate_RootRat; |