equal
deleted
inserted
replaced
107 have "P 0 (f 0)" "\<And>n. P n (f n) \<Longrightarrow> P (Suc n) (f (Suc n)) \<and> Q n (f n) (f (Suc n))" |
107 have "P 0 (f 0)" "\<And>n. P n (f n) \<Longrightarrow> P (Suc n) (f (Suc n)) \<and> Q n (f n) (f (Suc n))" |
108 using someI_ex[OF 1] someI_ex[OF 2] by (simp_all add: f_def) |
108 using someI_ex[OF 1] someI_ex[OF 2] by (simp_all add: f_def) |
109 then show "P n (f n)" "Q n (f n) (f (Suc n))" |
109 then show "P n (f n)" "Q n (f n) (f (Suc n))" |
110 by (induct n) auto |
110 by (induct n) auto |
111 qed |
111 qed |
112 |
|
113 |
|
114 subsection {* A skolemization tactic and proof method *} |
|
115 |
|
116 ML {* |
|
117 fun moura_tac ctxt = |
|
118 Atomize_Elim.atomize_elim_tac ctxt THEN' |
|
119 SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice bchoice}) THEN ALLGOALS (blast_tac ctxt)); |
|
120 *} |
|
121 |
|
122 method_setup moura = {* |
|
123 Scan.succeed (SIMPLE_METHOD' o moura_tac) |
|
124 *} "solve skolemization goals, especially those arising from Z3 proofs" |
|
125 |
112 |
126 |
113 |
127 subsection {*Function Inverse*} |
114 subsection {*Function Inverse*} |
128 |
115 |
129 lemma inv_def: "inv f = (%y. SOME x. f x = y)" |
116 lemma inv_def: "inv f = (%y. SOME x. f x = y)" |