src/HOL/ex/meson.ML
 changeset 1820 e381e1c51689 parent 1764 69b93ffc29ec child 2031 03a843f0f447
equal inserted replaced
1819:245721624c8d 1820:e381e1c51689
`    14 writeln"File HOL/ex/meson.";`
`    14 writeln"File HOL/ex/meson.";`
`    15 `
`    15 `
`    16 (*Prove theorems using fast_tac*)`
`    16 (*Prove theorems using fast_tac*)`
`    17 fun prove_fun s = `
`    17 fun prove_fun s = `
`    18     prove_goal HOL.thy s`
`    18     prove_goal HOL.thy s`
`    19          (fn prems => [ cut_facts_tac prems 1, fast_tac HOL_cs 1 ]);`
`    19          (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]);`
`    20 `
`    20 `
`    21 (**** Negation Normal Form ****)`
`    21 (**** Negation Normal Form ****)`
`    22 `
`    22 `
`    23 (*** de Morgan laws ***)`
`    23 (*** de Morgan laws ***)`
`    24 `
`    24 `
`    61 `
`    61 `
`    62 (*"Axiom" of Choice, proved using the description operator*)`
`    62 (*"Axiom" of Choice, proved using the description operator*)`
`    63 val [major] = goal HOL.thy`
`    63 val [major] = goal HOL.thy`
`    64     "! x. ? y. Q x y ==> ? f. ! x. Q x (f x)";`
`    64     "! x. ? y. Q x y ==> ? f. ! x. Q x (f x)";`
`    65 by (cut_facts_tac [major] 1);`
`    65 by (cut_facts_tac [major] 1);`
`    66 by (fast_tac (HOL_cs addEs [selectI]) 1);`
`    66 by (fast_tac (!claset addEs [selectI]) 1);`
`    67 qed "choice";`
`    67 qed "choice";`
`    68 `
`    68 `
`    69 `
`    69 `
`    70 (***** Generating clauses for the Meson Proof Procedure *****)`
`    70 (***** Generating clauses for the Meson Proof Procedure *****)`
`    71 `
`    71 `
`   428                          (has_fewer_prems 1, sizef)`
`   428                          (has_fewer_prems 1, sizef)`
`   429 			 (prolog_step_tac (make_horns cls) 1));`
`   429 			 (prolog_step_tac (make_horns cls) 1));`
`   430 `
`   430 `
`   431 (*First, breaks the goal into independent units*)`
`   431 (*First, breaks the goal into independent units*)`
`   432 val safe_best_meson_tac =`
`   432 val safe_best_meson_tac =`
`   433      SELECT_GOAL (TRY (safe_tac HOL_cs) THEN `
`   433      SELECT_GOAL (TRY (safe_tac (!claset)) THEN `
`   434                   TRYALL (best_meson_tac size_of_subgoals));`
`   434                   TRYALL (best_meson_tac size_of_subgoals));`
`   435 `
`   435 `
`   436 (** Depth-first search version **)`
`   436 (** Depth-first search version **)`
`   437 `
`   437 `
`   438 val depth_meson_tac =`
`   438 val depth_meson_tac =`
`   462          (THEN_ITER_DEEPEN (resolve_tac (gocls cls) 1)`
`   462          (THEN_ITER_DEEPEN (resolve_tac (gocls cls) 1)`
`   463 	                   (has_fewer_prems 1)`
`   463 	                   (has_fewer_prems 1)`
`   464 	                   (prolog_step_tac' (make_horns cls))));`
`   464 	                   (prolog_step_tac' (make_horns cls))));`
`   465 `
`   465 `
`   466 val safe_meson_tac =`
`   466 val safe_meson_tac =`
`   467      SELECT_GOAL (TRY (safe_tac HOL_cs) THEN `
`   467      SELECT_GOAL (TRY (safe_tac (!claset)) THEN `
`   468                   TRYALL (iter_deepen_meson_tac));`
`   468                   TRYALL (iter_deepen_meson_tac));`
`   469 `
`   469 `
`   470 `
`   470 `
`   471 writeln"Reached end of file.";`
`   471 writeln"Reached end of file.";`