1445 lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d" |
1445 lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d" |
1446 by auto |
1446 by auto |
1447 |
1447 |
1448 (* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *) |
1448 (* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *) |
1449 ML {* |
1449 ML {* |
1450 fun uint_arith_ss_of ss = |
1450 fun uint_arith_simpset ctxt = |
1451 ss addsimps @{thms uint_arith_simps} |
1451 ctxt addsimps @{thms uint_arith_simps} |
1452 delsimps @{thms word_uint.Rep_inject} |
1452 delsimps @{thms word_uint.Rep_inject} |
1453 |> fold Splitter.add_split @{thms split_if_asm} |
1453 |> fold Splitter.add_split @{thms split_if_asm} |
1454 |> fold Simplifier.add_cong @{thms power_False_cong} |
1454 |> fold Simplifier.add_cong @{thms power_False_cong} |
1455 |
1455 |
1456 fun uint_arith_tacs ctxt = |
1456 fun uint_arith_tacs ctxt = |
1458 fun arith_tac' n t = |
1458 fun arith_tac' n t = |
1459 Arith_Data.verbose_arith_tac ctxt n t |
1459 Arith_Data.verbose_arith_tac ctxt n t |
1460 handle Cooper.COOPER _ => Seq.empty; |
1460 handle Cooper.COOPER _ => Seq.empty; |
1461 in |
1461 in |
1462 [ clarify_tac ctxt 1, |
1462 [ clarify_tac ctxt 1, |
1463 full_simp_tac (uint_arith_ss_of (simpset_of ctxt)) 1, |
1463 full_simp_tac (uint_arith_simpset ctxt) 1, |
1464 ALLGOALS (full_simp_tac (HOL_ss |> fold Splitter.add_split @{thms uint_splits} |
1464 ALLGOALS (full_simp_tac |
1465 |> fold Simplifier.add_cong @{thms power_False_cong})), |
1465 (put_simpset HOL_ss ctxt |
|
1466 |> fold Splitter.add_split @{thms uint_splits} |
|
1467 |> fold Simplifier.add_cong @{thms power_False_cong})), |
1466 rewrite_goals_tac @{thms word_size}, |
1468 rewrite_goals_tac @{thms word_size}, |
1467 ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN |
1469 ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN |
1468 REPEAT (etac conjE n) THEN |
1470 REPEAT (etac conjE n) THEN |
1469 REPEAT (dtac @{thm word_of_int_inverse} n |
1471 REPEAT (dtac @{thm word_of_int_inverse} n |
1470 THEN atac n |
1472 THEN atac n |
1944 unat_sub_if' unat_plus_if' unat_div unat_mod |
1946 unat_sub_if' unat_plus_if' unat_div unat_mod |
1945 |
1947 |
1946 (* unat_arith_tac: tactic to reduce word arithmetic to nat, |
1948 (* unat_arith_tac: tactic to reduce word arithmetic to nat, |
1947 try to solve via arith *) |
1949 try to solve via arith *) |
1948 ML {* |
1950 ML {* |
1949 fun unat_arith_ss_of ss = |
1951 fun unat_arith_simpset ctxt = |
1950 ss addsimps @{thms unat_arith_simps} |
1952 ctxt addsimps @{thms unat_arith_simps} |
1951 delsimps @{thms word_unat.Rep_inject} |
1953 delsimps @{thms word_unat.Rep_inject} |
1952 |> fold Splitter.add_split @{thms split_if_asm} |
1954 |> fold Splitter.add_split @{thms split_if_asm} |
1953 |> fold Simplifier.add_cong @{thms power_False_cong} |
1955 |> fold Simplifier.add_cong @{thms power_False_cong} |
1954 |
1956 |
1955 fun unat_arith_tacs ctxt = |
1957 fun unat_arith_tacs ctxt = |
1957 fun arith_tac' n t = |
1959 fun arith_tac' n t = |
1958 Arith_Data.verbose_arith_tac ctxt n t |
1960 Arith_Data.verbose_arith_tac ctxt n t |
1959 handle Cooper.COOPER _ => Seq.empty; |
1961 handle Cooper.COOPER _ => Seq.empty; |
1960 in |
1962 in |
1961 [ clarify_tac ctxt 1, |
1963 [ clarify_tac ctxt 1, |
1962 full_simp_tac (unat_arith_ss_of (simpset_of ctxt)) 1, |
1964 full_simp_tac (unat_arith_simpset ctxt) 1, |
1963 ALLGOALS (full_simp_tac (HOL_ss |> fold Splitter.add_split @{thms unat_splits} |
1965 ALLGOALS (full_simp_tac |
1964 |> fold Simplifier.add_cong @{thms power_False_cong})), |
1966 (put_simpset HOL_ss ctxt |
|
1967 |> fold Splitter.add_split @{thms unat_splits} |
|
1968 |> fold Simplifier.add_cong @{thms power_False_cong})), |
1965 rewrite_goals_tac @{thms word_size}, |
1969 rewrite_goals_tac @{thms word_size}, |
1966 ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN |
1970 ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN |
1967 REPEAT (etac conjE n) THEN |
1971 REPEAT (etac conjE n) THEN |
1968 REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)), |
1972 REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)), |
1969 TRYALL arith_tac' ] |
1973 TRYALL arith_tac' ] |