28 |
28 |
29 fun pull_ites_conv ct = |
29 fun pull_ites_conv ct = |
30 (Conv.rewr_conv pull_ite then_conv |
30 (Conv.rewr_conv pull_ite then_conv |
31 Conv.binop_conv (Conv.try_conv pull_ites_conv)) ct |
31 Conv.binop_conv (Conv.try_conv pull_ites_conv)) ct |
32 |
32 |
33 val prove_ite = |
33 fun prove_ite ctxt = |
34 Z3_Proof_Tools.by_tac ( |
34 Z3_Proof_Tools.by_tac ctxt ( |
35 CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv)) |
35 CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv)) |
36 THEN' rtac @{thm refl}) |
36 THEN' rtac @{thm refl}) |
37 |
37 |
38 |
38 |
39 |
39 |
66 val disjE = @{lemma "~P | Q ==> P ==> Q" by fast} |
66 val disjE = @{lemma "~P | Q ==> P ==> Q" by fast} |
67 |
67 |
68 fun prove_inj_prop ctxt def lhs = |
68 fun prove_inj_prop ctxt def lhs = |
69 let |
69 let |
70 val (ct, ctxt') = SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt |
70 val (ct, ctxt') = SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt |
71 val rule = disjE OF [Object_Logic.rulify ctxt (Thm.assume lhs)] |
71 val rule = disjE OF [Object_Logic.rulify ctxt' (Thm.assume lhs)] |
72 in |
72 in |
73 Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct)) |
73 Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct)) |
74 |> apply (rtac @{thm injI}) |
74 |> apply (rtac @{thm injI}) |
75 |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}]) |
75 |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}]) |
76 |> Goal.norm_result o Goal.finish ctxt' |
76 |> Goal.norm_result ctxt' o Goal.finish ctxt' |
77 |> singleton (Variable.export ctxt' ctxt) |
77 |> singleton (Variable.export ctxt' ctxt) |
78 end |
78 end |
79 |
79 |
80 fun prove_rhs ctxt def lhs = |
80 fun prove_rhs ctxt def lhs = |
81 Z3_Proof_Tools.by_tac ( |
81 Z3_Proof_Tools.by_tac ctxt ( |
82 CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt) |
82 CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt) |
83 THEN' REPEAT_ALL_NEW (match_tac @{thms allI}) |
83 THEN' REPEAT_ALL_NEW (match_tac @{thms allI}) |
84 THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) |
84 THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) |
85 |
85 |
86 |
86 |
95 fun prove_lhs ctxt rhs = |
95 fun prove_lhs ctxt rhs = |
96 let |
96 let |
97 val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify ctxt (Thm.assume rhs))) |
97 val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify ctxt (Thm.assume rhs))) |
98 val conv = SMT_Utils.binders_conv (K (expand eq)) ctxt |
98 val conv = SMT_Utils.binders_conv (K (expand eq)) ctxt |
99 in |
99 in |
100 Z3_Proof_Tools.by_tac ( |
100 Z3_Proof_Tools.by_tac ctxt ( |
101 CONVERSION (SMT_Utils.prop_conv conv) |
101 CONVERSION (SMT_Utils.prop_conv conv) |
102 THEN' Simplifier.simp_tac (put_simpset HOL_ss ctxt)) |
102 THEN' Simplifier.simp_tac (put_simpset HOL_ss ctxt)) |
103 end |
103 end |
104 |
104 |
105 |
105 |
138 Conv.arg_conv (SMT_Utils.binders_conv (K swap_eq_conv) ctxt) |
138 Conv.arg_conv (SMT_Utils.binders_conv (K swap_eq_conv) ctxt) |
139 |
139 |
140 in |
140 in |
141 |
141 |
142 fun prove_injectivity ctxt = |
142 fun prove_injectivity ctxt = |
143 Z3_Proof_Tools.by_tac ( |
143 Z3_Proof_Tools.by_tac ctxt ( |
144 CONVERSION (SMT_Utils.prop_conv (norm_conv ctxt)) |
144 CONVERSION (SMT_Utils.prop_conv (norm_conv ctxt)) |
145 THEN' CSUBGOAL (uncurry (rtac o prove_inj_eq ctxt))) |
145 THEN' CSUBGOAL (uncurry (rtac o prove_inj_eq ctxt))) |
146 |
146 |
147 end |
147 end |
148 |
148 |