equal
deleted
inserted
replaced
25 |
25 |
26 fun mk_case_certificate thy raw_thms = |
26 fun mk_case_certificate thy raw_thms = |
27 let |
27 let |
28 val thms as thm1 :: _ = raw_thms |
28 val thms as thm1 :: _ = raw_thms |
29 |> Conjunction.intr_balanced |
29 |> Conjunction.intr_balanced |
30 |> Thm.unvarify_global |
30 |> Thm.unvarify_global thy |
31 |> Conjunction.elim_balanced (length raw_thms) |
31 |> Conjunction.elim_balanced (length raw_thms) |
32 |> map Simpdata.mk_meta_eq |
32 |> map Simpdata.mk_meta_eq |
33 |> map Drule.zero_var_indexes; |
33 |> map Drule.zero_var_indexes; |
34 val params = Term.add_free_names (Thm.prop_of thm1) []; |
34 val params = Term.add_free_names (Thm.prop_of thm1) []; |
35 val rhs = thm1 |
35 val rhs = thm1 |
51 let |
51 let |
52 fun mk_fcT_eq (t, u) = Const (@{const_name HOL.equal}, fcT --> fcT --> HOLogic.boolT) $ t $ u; |
52 fun mk_fcT_eq (t, u) = Const (@{const_name HOL.equal}, fcT --> fcT --> HOLogic.boolT) $ t $ u; |
53 fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term True}); |
53 fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term True}); |
54 fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term False}); |
54 fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term False}); |
55 |
55 |
56 val monomorphic_prop_of = Thm.prop_of o Thm.unvarify_global o Drule.zero_var_indexes; |
56 val monomorphic_prop_of = Thm.prop_of o Thm.unvarify_global thy o Drule.zero_var_indexes; |
57 |
57 |
58 fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs); |
58 fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs); |
59 fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)]; |
59 fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)]; |
60 |
60 |
61 val triv_inject_goals = |
61 val triv_inject_goals = |