# HG changeset patch # User blanchet # Date 1305206959 -7200 # Node ID 6b7ef9b724fdf40edf77e4ac42e9f9a74e3fbe74 # Parent 4603154a301858c252b1d43ec2ed26554a280738 added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around diff -r 4603154a3018 -r 6b7ef9b724fd src/HOL/Metis_Examples/Clausify.thy --- a/src/HOL/Metis_Examples/Clausify.thy Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Metis_Examples/Clausify.thy Thu May 12 15:29:19 2011 +0200 @@ -12,36 +12,6 @@ declare [[unify_search_bound = 100]] declare [[unify_trace_bound = 100]] -sledgehammer_params [prover = e, blocking, timeout = 10] - - -text {* Extensionality *} - -lemma plus_1_not_0: "n + (1\nat) \ 0" -by simp - -definition inc :: "nat \ nat" where -"inc x = x + 1" - -lemma "inc \ (\y. 0)" -sledgehammer [expect = some] (inc_def plus_1_not_0) -by (metis inc_def plus_1_not_0) - -lemma "inc = (\y. y + 1)" -sledgehammer [expect = some] (inc_def) -by (metis inc_def) - -lemma "(\y. y + 1) = inc" -sledgehammer [expect = some] (inc_def) -by (metis inc_def) - -definition add_swap :: "nat \ nat \ nat" where -"add_swap = (\x y. y + x)" - -lemma "add_swap m n = n + m" -sledgehammer [expect = some] (add_swap_def) -by (metis add_swap_def) - text {* Definitional CNF for facts *} diff -r 4603154a3018 -r 6b7ef9b724fd src/HOL/Metis_Examples/HO_Reas.thy --- a/src/HOL/Metis_Examples/HO_Reas.thy Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Metis_Examples/HO_Reas.thy Thu May 12 15:29:19 2011 +0200 @@ -12,13 +12,56 @@ sledgehammer_params [prover = e, blocking, timeout = 10] +text {* Extensionality and set constants *} + +lemma plus_1_not_0: "n + (1\nat) \ 0" +by simp + +definition inc :: "nat \ nat" where +"inc x = x + 1" + +lemma "inc \ (\y. 0)" +sledgehammer [expect = some] (inc_def plus_1_not_0) +by (metis inc_def plus_1_not_0) + +lemma "inc = (\y. y + 1)" +sledgehammer [expect = some] (inc_def) +by (metis inc_def) + +lemma "(\y. y + 1) = inc" +sledgehammer [expect = some] (inc_def) +by (metis inc_def) + +definition add_swap :: "nat \ nat \ nat" where +"add_swap = (\x y. y + x)" + +lemma "add_swap m n = n + m" +sledgehammer [expect = some] (add_swap_def) +by (metis add_swap_def) + +definition "A = {xs\'a list. True}" + +lemma "xs \ A" +sledgehammer [expect = some] +by (metis A_def Collect_def mem_def) + +definition "B (y::int) \ y \ 0" +definition "C (y::int) \ y \ 1" + +lemma int_le_0_imp_le_1: "x \ (0::int) \ x \ 1" +by linarith + +lemma "B \ C" +sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some] +by (metis B_def C_def int_le_0_imp_le_1 predicate1I) + + +text {* Proxies for logical constants *} + lemma "id True" sledgehammer [type_sys = erased, expect = some] (id_apply) sledgehammer [type_sys = poly_tags!, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds!, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) @@ -28,10 +71,7 @@ lemma "\ id False" sledgehammer [type_sys = erased, expect = some] (id_apply) sledgehammer [type_sys = poly_tags!, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds!, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) @@ -41,11 +81,8 @@ lemma "x = id True \ x = id False" sledgehammer [type_sys = erased, expect = some] (id_apply) sledgehammer [type_sys = poly_tags!, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) sledgehammer [type_sys = poly_tags, expect = some] (id_apply) sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds!, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -54,10 +91,7 @@ lemma "id x = id True \ id x = id False" sledgehammer [type_sys = erased, expect = some] (id_apply) sledgehammer [type_sys = poly_tags!, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds!, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) @@ -68,10 +102,7 @@ sledgehammer [type_sys = erased, expect = none] () sledgehammer [type_sys = poly_args, expect = none] () sledgehammer [type_sys = poly_tags!, expect = some] () -sledgehammer [type_sys = poly_tags?, expect = some] () sledgehammer [type_sys = poly_tags, expect = some] () -sledgehammer [type_sys = poly_preds!, expect = some] () -sledgehammer [type_sys = poly_preds?, expect = some] () sledgehammer [type_sys = poly_preds, expect = some] () sledgehammer [type_sys = mangled_preds!, expect = some] () sledgehammer [type_sys = mangled_preds?, expect = some] () @@ -81,10 +112,7 @@ lemma "id (\ a) \ \ id a" sledgehammer [type_sys = erased, expect = some] (id_apply) sledgehammer [type_sys = poly_tags!, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds!, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) @@ -94,10 +122,7 @@ lemma "id (\ \ a) \ id a" sledgehammer [type_sys = erased, expect = some] (id_apply) sledgehammer [type_sys = poly_tags!, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds!, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) @@ -107,10 +132,7 @@ lemma "id (\ (id (\ a))) \ id a" sledgehammer [type_sys = erased, expect = some] (id_apply) sledgehammer [type_sys = poly_tags!, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds!, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) @@ -120,10 +142,7 @@ lemma "id (a \ b) \ id a" sledgehammer [type_sys = erased, expect = some] (id_apply) sledgehammer [type_sys = poly_tags!, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds!, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) @@ -133,10 +152,7 @@ lemma "id (a \ b) \ id b" sledgehammer [type_sys = erased, expect = some] (id_apply) sledgehammer [type_sys = poly_tags!, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds!, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) @@ -146,10 +162,7 @@ lemma "id a \ id b \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) sledgehammer [type_sys = poly_tags!, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds!, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) @@ -159,10 +172,7 @@ lemma "id a \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) sledgehammer [type_sys = poly_tags!, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds!, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) @@ -172,10 +182,7 @@ lemma "id b \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) sledgehammer [type_sys = poly_tags!, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds!, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) @@ -185,10 +192,7 @@ lemma "id (\ a) \ id (\ b) \ id (\ (a \ b))" sledgehammer [type_sys = erased, expect = some] (id_apply) sledgehammer [type_sys = poly_tags!, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds!, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) @@ -198,11 +202,8 @@ lemma "id (\ a) \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) sledgehammer [type_sys = poly_tags!, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) sledgehammer [type_sys = poly_tags, expect = some] (id_apply) sledgehammer [type_sys = poly_preds, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds!, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -211,10 +212,7 @@ lemma "id (a \ b) \ id (\ a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) sledgehammer [type_sys = poly_tags!, expect = some] (id_apply) -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply) sledgehammer [type_sys = poly_tags, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds!, expect = some] (id_apply) -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)