equal
deleted
inserted
replaced
30 val xsko25 = Meson.skolemize ctxt nnf25; |
30 val xsko25 = Meson.skolemize ctxt nnf25; |
31 *} |
31 *} |
32 apply (tactic {* cut_tac xsko25 1 THEN REPEAT (etac exE 1) *}) |
32 apply (tactic {* cut_tac xsko25 1 THEN REPEAT (etac exE 1) *}) |
33 ML_val {* |
33 ML_val {* |
34 val ctxt = @{context}; |
34 val ctxt = @{context}; |
35 val [_, sko25] = #prems (#1 (Subgoal.focus ctxt 1 (#goal @{Isar.goal}))); |
35 val [_, sko25] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal}))); |
36 val clauses25 = Meson.make_clauses ctxt [sko25]; (*7 clauses*) |
36 val clauses25 = Meson.make_clauses ctxt [sko25]; (*7 clauses*) |
37 val horns25 = Meson.make_horns clauses25; (*16 Horn clauses*) |
37 val horns25 = Meson.make_horns clauses25; (*16 Horn clauses*) |
38 val go25 :: _ = Meson.gocls clauses25; |
38 val go25 :: _ = Meson.gocls clauses25; |
39 |
39 |
40 val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt; |
40 val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt; |
54 val xsko26 = Meson.skolemize ctxt nnf26; |
54 val xsko26 = Meson.skolemize ctxt nnf26; |
55 *} |
55 *} |
56 apply (tactic {* cut_tac xsko26 1 THEN REPEAT (etac exE 1) *}) |
56 apply (tactic {* cut_tac xsko26 1 THEN REPEAT (etac exE 1) *}) |
57 ML_val {* |
57 ML_val {* |
58 val ctxt = @{context}; |
58 val ctxt = @{context}; |
59 val [_, sko26] = #prems (#1 (Subgoal.focus ctxt 1 (#goal @{Isar.goal}))); |
59 val [_, sko26] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal}))); |
60 val clauses26 = Meson.make_clauses ctxt [sko26]; |
60 val clauses26 = Meson.make_clauses ctxt [sko26]; |
61 val _ = @{assert} (length clauses26 = 9); |
61 val _ = @{assert} (length clauses26 = 9); |
62 val horns26 = Meson.make_horns clauses26; |
62 val horns26 = Meson.make_horns clauses26; |
63 val _ = @{assert} (length horns26 = 24); |
63 val _ = @{assert} (length horns26 = 24); |
64 val go26 :: _ = Meson.gocls clauses26; |
64 val go26 :: _ = Meson.gocls clauses26; |
81 val xsko43 = Meson.skolemize ctxt nnf43; |
81 val xsko43 = Meson.skolemize ctxt nnf43; |
82 *} |
82 *} |
83 apply (tactic {* cut_tac xsko43 1 THEN REPEAT (etac exE 1) *}) |
83 apply (tactic {* cut_tac xsko43 1 THEN REPEAT (etac exE 1) *}) |
84 ML_val {* |
84 ML_val {* |
85 val ctxt = @{context}; |
85 val ctxt = @{context}; |
86 val [_, sko43] = #prems (#1 (Subgoal.focus ctxt 1 (#goal @{Isar.goal}))); |
86 val [_, sko43] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal}))); |
87 val clauses43 = Meson.make_clauses ctxt [sko43]; |
87 val clauses43 = Meson.make_clauses ctxt [sko43]; |
88 val _ = @{assert} (length clauses43 = 6); |
88 val _ = @{assert} (length clauses43 = 6); |
89 val horns43 = Meson.make_horns clauses43; |
89 val horns43 = Meson.make_horns clauses43; |
90 val _ = @{assert} (length horns43 = 16); |
90 val _ = @{assert} (length horns43 = 16); |
91 val go43 :: _ = Meson.gocls clauses43; |
91 val go43 :: _ = Meson.gocls clauses43; |