equal
deleted
inserted
replaced
8 (** tools setup **) |
8 (** tools setup **) |
9 |
9 |
10 structure Quantifier1 = Quantifier1Fun |
10 structure Quantifier1 = Quantifier1Fun |
11 (struct |
11 (struct |
12 (*abstract syntax*) |
12 (*abstract syntax*) |
13 fun dest_eq ((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME (c, s, t) |
13 fun dest_eq ((c as Const(@{const_name HOL.eq},_)) $ s $ t) = SOME (c, s, t) |
14 | dest_eq _ = NONE; |
14 | dest_eq _ = NONE; |
15 fun dest_conj ((c as Const(@{const_name HOL.conj},_)) $ s $ t) = SOME (c, s, t) |
15 fun dest_conj ((c as Const(@{const_name HOL.conj},_)) $ s $ t) = SOME (c, s, t) |
16 | dest_conj _ = NONE; |
16 | dest_conj _ = NONE; |
17 fun dest_imp ((c as Const(@{const_name HOL.implies},_)) $ s $ t) = SOME (c, s, t) |
17 fun dest_imp ((c as Const(@{const_name HOL.implies},_)) $ s $ t) = SOME (c, s, t) |
18 | dest_imp _ = NONE; |
18 | dest_imp _ = NONE; |
42 fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; |
42 fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; |
43 |
43 |
44 fun mk_eq th = case concl_of th |
44 fun mk_eq th = case concl_of th |
45 (*expects Trueprop if not == *) |
45 (*expects Trueprop if not == *) |
46 of Const (@{const_name "=="},_) $ _ $ _ => th |
46 of Const (@{const_name "=="},_) $ _ $ _ => th |
47 | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => mk_meta_eq th |
47 | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th |
48 | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI} |
48 | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI} |
49 | _ => th RS @{thm Eq_TrueI} |
49 | _ => th RS @{thm Eq_TrueI} |
50 |
50 |
51 fun mk_eq_True (_: simpset) r = |
51 fun mk_eq_True (_: simpset) r = |
52 SOME (r RS @{thm meta_eq_to_obj_eq} RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE; |
52 SOME (r RS @{thm meta_eq_to_obj_eq} RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE; |