79 (Free ("P",varsT --> boolT) $ mk_bodyC vars)); |
79 (Free ("P",varsT --> boolT) $ mk_bodyC vars)); |
80 val small_Collect = mk_CollectC (Abs("x",varsT, |
80 val small_Collect = mk_CollectC (Abs("x",varsT, |
81 Free ("P",varsT --> boolT) $ Bound 0)); |
81 Free ("P",varsT --> boolT) $ Bound 0)); |
82 val impl = implies $ (Mset_incl big_Collect) $ |
82 val impl = implies $ (Mset_incl big_Collect) $ |
83 (Mset_incl small_Collect); |
83 (Mset_incl small_Collect); |
84 in Goal.prove (ProofContext.init (Thm.sign_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end; |
84 in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end; |
85 |
85 |
86 end; |
86 end; |
87 |
87 |
88 |
88 |
89 (*****************************************************************************) |
89 (*****************************************************************************) |
115 (** transformed. **) |
115 (** transformed. **) |
116 (** This transformation may solve very easy subgoals due to a ligth **) |
116 (** This transformation may solve very easy subgoals due to a ligth **) |
117 (** simplification done by (split_all_tac) **) |
117 (** simplification done by (split_all_tac) **) |
118 (*****************************************************************************) |
118 (*****************************************************************************) |
119 |
119 |
120 fun set2pred i thm = let fun mk_string [] = "" |
120 fun set2pred i thm = |
121 | mk_string (x::xs) = x^" "^mk_string xs; |
121 let val var_names = map (fst o dest_Free) (get_vars thm) in |
122 val vars=get_vars(thm); |
122 ((before_set2pred_simp_tac i) THEN_MAYBE |
123 val var_string = mk_string (map (fst o dest_Free) vars); |
123 (EVERY [rtac subsetI i, |
124 in ((before_set2pred_simp_tac i) THEN_MAYBE |
124 rtac CollectI i, |
125 (EVERY [rtac subsetI i, |
125 dtac CollectD i, |
126 rtac CollectI i, |
126 (TRY(split_all_tac i)) THEN_MAYBE |
127 dtac CollectD i, |
127 ((rename_params_tac var_names i) THEN |
128 (TRY(split_all_tac i)) THEN_MAYBE |
128 (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm |
129 ((rename_tac var_string i) THEN |
129 end; |
130 (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm |
|
131 end; |
|
132 |
130 |
133 (*****************************************************************************) |
131 (*****************************************************************************) |
134 (** BasicSimpTac is called to simplify all verification conditions. It does **) |
132 (** BasicSimpTac is called to simplify all verification conditions. It does **) |
135 (** a light simplification by applying "mem_Collect_eq", then it calls **) |
133 (** a light simplification by applying "mem_Collect_eq", then it calls **) |
136 (** MaxSimpTac, which solves subgoals of the form "A <= A", **) |
134 (** MaxSimpTac, which solves subgoals of the form "A <= A", **) |