equal
deleted
inserted
replaced
1 (* theorems.ML |
1 (* theorems.ML |
2 Author : David von Oheimb |
2 Author : David von Oheimb |
3 Created: 06-Jun-95 |
3 Created: 06-Jun-95 |
4 Updated: 08-Jun-95 first proof from cterms |
4 Updated: 08-Jun-95 first proof from cterms |
5 Updated: 26-Jun-95 proofs for exhaustion thms |
5 Updated: 26-Jun-95 proofs for exhaustion thms |
6 Updated: 27-Jun-95 proofs for discriminators, constructors and selectors |
6 Updated: 27-Jun-95 proofs for discriminators, constructors and selectors |
37 fun pg' thy defs t tacsf=pg'' thy defs t (fn [] => tacsf |
37 fun pg' thy defs t tacsf=pg'' thy defs t (fn [] => tacsf |
38 | prems=> (cut_facts_tac prems 1)::tacsf); |
38 | prems=> (cut_facts_tac prems 1)::tacsf); |
39 |
39 |
40 fun REPEAT_DETERM_UNTIL p tac = |
40 fun REPEAT_DETERM_UNTIL p tac = |
41 let fun drep st = if p st then Sequence.single st |
41 let fun drep st = if p st then Sequence.single st |
42 else (case Sequence.pull(tapply(tac,st)) of |
42 else (case Sequence.pull(tac st) of |
43 None => Sequence.null |
43 None => Sequence.null |
44 | Some(st',_) => drep st') |
44 | Some(st',_) => drep st') |
45 in Tactic drep end; |
45 in drep end; |
46 val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1); |
46 val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1); |
47 |
47 |
48 local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn prems=>[rtac TrueI 1])in |
48 local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn prems=>[rtac TrueI 1])in |
49 val kill_neq_tac = dtac trueI2 end; |
49 val kill_neq_tac = dtac trueI2 end; |
50 fun case_UU_tac rews i v = res_inst_tac [("Q",v^"=UU")] classical2 i THEN |
50 fun case_UU_tac rews i v = res_inst_tac [("Q",v^"=UU")] classical2 i THEN |