[STATEMENT]
theorem doublep_infinite_params:
  \<open>infinite (- (\<Union>p \<in> psubst (\<lambda>n::nat. 2 * n) ` S. params p))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (- \<Union> (params ` psubst ((*) 2) ` S))
[PROOF STEP]
proof (rule infinite_super)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?S \<subseteq> - \<Union> (params ` psubst ((*) 2) ` S)
 2. infinite ?S
[PROOF STEP]
show \<open>infinite (range (\<lambda>n::nat. 2 * n + 1))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (range (\<lambda>n. 2 * n + 1))
[PROOF STEP]
using inj_onI Suc_1 Suc_mult_cancel1 add_right_imp_eq finite_imageD infinite_UNIV_char_0
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. \<lbrakk>x \<in> ?A; y \<in> ?A; ?f x = ?f y\<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> inj_on ?f ?A
Suc 1 = 2
(Suc ?k * ?m = Suc ?k * ?n) = (?m = ?n)
?b + ?a = ?c + ?a \<Longrightarrow> ?b = ?c
\<lbrakk>finite (?f ` ?A); inj_on ?f ?A\<rbrakk> \<Longrightarrow> finite ?A
infinite UNIV

goal (1 subgoal):
 1. infinite (range (\<lambda>n. 2 * n + 1))
[PROOF STEP]
by (metis (no_types, lifting))
[PROOF STATE]
proof (state)
this:
infinite (range (\<lambda>n. 2 * n + 1))

goal (1 subgoal):
 1. range (\<lambda>n. 2 * n + 1) \<subseteq> - \<Union> (params ` psubst ((*) 2) ` S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. range (\<lambda>n. 2 * n + 1) \<subseteq> - \<Union> (params ` psubst ((*) 2) ` S)
[PROOF STEP]
have \<open>\<And>m n. Suc (2 * m) \<noteq> 2 * n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m n. Suc (2 * m) \<noteq> 2 * n
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
Suc (2 * ?m) \<noteq> 2 * ?n

goal (1 subgoal):
 1. range (\<lambda>n. 2 * n + 1) \<subseteq> - \<Union> (params ` psubst ((*) 2) ` S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Suc (2 * ?m) \<noteq> 2 * ?n
[PROOF STEP]
show \<open>range (\<lambda>n. 2 * n + 1)
    \<subseteq> - (\<Union>p::(nat, 'a) form \<in> psubst (\<lambda>n . 2 * n) ` S. params p)\<close>
[PROOF STATE]
proof (prove)
using this:
Suc (2 * ?m) \<noteq> 2 * ?n

goal (1 subgoal):
 1. range (\<lambda>n. 2 * n + 1) \<subseteq> - \<Union> (params ` psubst ((*) 2) ` S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
range (\<lambda>n. 2 * n + 1) \<subseteq> - \<Union> (params ` psubst ((*) 2) ` S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem loewenheim_skolem:
  assumes evalS: \<open>\<forall>p \<in> S. eval e f g p\<close>
  shows \<open>\<forall>p \<in> S. closed 0 p \<longrightarrow> eval e' (\<lambda>n. HApp (2*n)) (\<lambda>a ts.
      Pred a (terms_of_hterms ts) \<in> Extend (psubst (\<lambda>n. 2 * n) ` S)
        (mk_finite_char (mk_alt_consistency (close
          {S. infinite (- (\<Union>p \<in> S. params p)) \<and> (\<exists>f. \<forall>p \<in> S. eval e f g p)}))) from_nat) p\<close>
    (is \<open>\<forall>_ \<in> _. _ _ _ \<longrightarrow> eval _ _ ?g _\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>S. closed 0 p \<longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
using evalS
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>S. eval e f g p

goal (1 subgoal):
 1. \<forall>p\<in>S. closed 0 p \<longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
proof (intro ballI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p\<in>S. eval e f g p; p \<in> S; closed 0 p\<rbrakk> \<Longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p\<in>S. eval e f g p; p \<in> S; closed 0 p\<rbrakk> \<Longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
let ?C = \<open>{S. infinite (- (\<Union>p \<in> S. params p)) \<and> (\<exists>f. \<forall>x \<in> S. eval e f g x)}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p\<in>S. eval e f g p; p \<in> S; closed 0 p\<rbrakk> \<Longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
assume \<open>p \<in> S\<close>
    and \<open>closed 0 p\<close>
[PROOF STATE]
proof (state)
this:
p \<in> S
closed 0 p

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p\<in>S. eval e f g p; p \<in> S; closed 0 p\<rbrakk> \<Longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> S
closed 0 p
[PROOF STEP]
have \<open>eval e f g p\<close>
[PROOF STATE]
proof (prove)
using this:
p \<in> S
closed 0 p

goal (1 subgoal):
 1. eval e f g p
[PROOF STEP]
using evalS
[PROOF STATE]
proof (prove)
using this:
p \<in> S
closed 0 p
\<forall>p\<in>S. eval e f g p

goal (1 subgoal):
 1. eval e f g p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval e f g p

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p\<in>S. eval e f g p; p \<in> S; closed 0 p\<rbrakk> \<Longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval e f g p
[PROOF STEP]
have \<open>\<forall>x \<in> S. eval e f g x\<close>
[PROOF STATE]
proof (prove)
using this:
eval e f g p

goal (1 subgoal):
 1. \<forall>x\<in>S. eval e f g x
[PROOF STEP]
using evalS
[PROOF STATE]
proof (prove)
using this:
eval e f g p
\<forall>p\<in>S. eval e f g p

goal (1 subgoal):
 1. \<forall>x\<in>S. eval e f g x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. eval e f g x

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p\<in>S. eval e f g p; p \<in> S; closed 0 p\<rbrakk> \<Longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>S. eval e f g x
[PROOF STEP]
have \<open>\<forall>p \<in> psubst (\<lambda>n. 2 * n) ` S. eval e (\<lambda>n. f (n div 2)) g p\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. eval e f g x

goal (1 subgoal):
 1. \<forall>p\<in>psubst ((*) 2) ` S. eval e (\<lambda>n. f (n div 2)) g p
[PROOF STEP]
by (simp add: psubst_eval)
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>psubst ((*) 2) ` S. eval e (\<lambda>n. f (n div 2)) g p

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p\<in>S. eval e f g p; p \<in> S; closed 0 p\<rbrakk> \<Longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>psubst ((*) 2) ` S. eval e (\<lambda>n. f (n div 2)) g p
[PROOF STEP]
have \<open>psubst (\<lambda>n. 2 * n) ` S \<in> ?C\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>psubst ((*) 2) ` S. eval e (\<lambda>n. f (n div 2)) g p

goal (1 subgoal):
 1. psubst ((*) 2) ` S \<in> {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>x\<in>S. eval e f g x)}
[PROOF STEP]
using doublep_infinite_params
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>psubst ((*) 2) ` S. eval e (\<lambda>n. f (n div 2)) g p
infinite (- \<Union> (params ` psubst ((*) 2) ` ?S))

goal (1 subgoal):
 1. psubst ((*) 2) ` S \<in> {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>x\<in>S. eval e f g x)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
psubst ((*) 2) ` S \<in> {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>x\<in>S. eval e f g x)}

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p\<in>S. eval e f g p; p \<in> S; closed 0 p\<rbrakk> \<Longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
psubst ((*) 2) ` S \<in> {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>x\<in>S. eval e f g x)}

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p\<in>S. eval e f g p; p \<in> S; closed 0 p\<rbrakk> \<Longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
have \<open>psubst (\<lambda>n. 2 * n) p \<in> psubst (\<lambda>n. 2 * n) ` S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst ((*) 2) p \<in> psubst ((*) 2) ` S
[PROOF STEP]
using \<open>p \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
p \<in> S

goal (1 subgoal):
 1. psubst ((*) 2) p \<in> psubst ((*) 2) ` S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
psubst ((*) 2) p \<in> psubst ((*) 2) ` S

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p\<in>S. eval e f g p; p \<in> S; closed 0 p\<rbrakk> \<Longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
psubst ((*) 2) p \<in> psubst ((*) 2) ` S

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p\<in>S. eval e f g p; p \<in> S; closed 0 p\<rbrakk> \<Longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
have \<open>closed 0 (psubst (\<lambda>n. 2 * n) p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed 0 (psubst ((*) 2) p)
[PROOF STEP]
using \<open>closed 0 p\<close>
[PROOF STATE]
proof (prove)
using this:
closed 0 p

goal (1 subgoal):
 1. closed 0 (psubst ((*) 2) p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
closed 0 (psubst ((*) 2) p)

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p\<in>S. eval e f g p; p \<in> S; closed 0 p\<rbrakk> \<Longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
closed 0 (psubst ((*) 2) p)

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p\<in>S. eval e f g p; p \<in> S; closed 0 p\<rbrakk> \<Longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
have \<open>consistency ?C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistency {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>x\<in>S. eval e f g x)}
[PROOF STEP]
using sat_consistency
[PROOF STATE]
proof (prove)
using this:
consistency {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval ?e f ?g p)}

goal (1 subgoal):
 1. consistency {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>x\<in>S. eval e f g x)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
consistency {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>x\<in>S. eval e f g x)}

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p\<in>S. eval e f g p; p \<in> S; closed 0 p\<rbrakk> \<Longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
psubst ((*) 2) ` S \<in> {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>x\<in>S. eval e f g x)}
psubst ((*) 2) p \<in> psubst ((*) 2) ` S
closed 0 (psubst ((*) 2) p)
consistency {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>x\<in>S. eval e f g x)}
[PROOF STEP]
have \<open>eval e' HApp ?g (psubst (\<lambda>n. 2 * n) p)\<close>
[PROOF STATE]
proof (prove)
using this:
psubst ((*) 2) ` S \<in> {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>x\<in>S. eval e f g x)}
psubst ((*) 2) p \<in> psubst ((*) 2) ` S
closed 0 (psubst ((*) 2) p)
consistency {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>x\<in>S. eval e f g x)}

goal (1 subgoal):
 1. eval e' HApp (\<lambda>a b. Pred a (terms_of_hterms b) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) (psubst ((*) 2) p)
[PROOF STEP]
using model_existence
[PROOF STATE]
proof (prove)
using this:
psubst ((*) 2) ` S \<in> {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>x\<in>S. eval e f g x)}
psubst ((*) 2) p \<in> psubst ((*) 2) ` S
closed 0 (psubst ((*) 2) p)
consistency {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>x\<in>S. eval e f g x)}
\<lbrakk>consistency ?C; ?S \<in> ?C; infinite (- \<Union> (params ` ?S)); ?p \<in> ?S; closed 0 ?p\<rbrakk> \<Longrightarrow> eval ?e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend ?S (mk_finite_char (mk_alt_consistency (close ?C))) from_nat) ?p

goal (1 subgoal):
 1. eval e' HApp (\<lambda>a b. Pred a (terms_of_hterms b) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) (psubst ((*) 2) p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval e' HApp (\<lambda>a b. Pred a (terms_of_hterms b) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) (psubst ((*) 2) p)

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p\<in>S. eval e f g p; p \<in> S; closed 0 p\<rbrakk> \<Longrightarrow> eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval e' HApp (\<lambda>a b. Pred a (terms_of_hterms b) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) (psubst ((*) 2) p)
[PROOF STEP]
show \<open>eval e' (\<lambda>n. HApp (2 * n)) ?g p\<close>
[PROOF STATE]
proof (prove)
using this:
eval e' HApp (\<lambda>a b. Pred a (terms_of_hterms b) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) (psubst ((*) 2) p)

goal (1 subgoal):
 1. eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a b. Pred a (terms_of_hterms b) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
using psubst_eval
[PROOF STATE]
proof (prove)
using this:
eval e' HApp (\<lambda>a b. Pred a (terms_of_hterms b) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) (psubst ((*) 2) p)
eval ?e ?f ?g (psubst ?h ?p) = eval ?e (\<lambda>p. ?f (?h p)) ?g ?p

goal (1 subgoal):
 1. eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a b. Pred a (terms_of_hterms b) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval e' (\<lambda>n. HApp (2 * n)) (\<lambda>a b. Pred a (terms_of_hterms b) \<in> Extend (psubst ((*) 2) ` S) (mk_finite_char (mk_alt_consistency (close {S. infinite (- \<Union> (params ` S)) \<and> (\<exists>f. \<forall>p\<in>S. eval e f g p)}))) from_nat) p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma new_psubst_image':
  \<open>new_term c t \<Longrightarrow> d \<notin> image f (paramst t) \<Longrightarrow> new_term d (psubstt (f(c := d)) t)\<close>
  \<open>new_list c l \<Longrightarrow> d \<notin> image f (paramsts l) \<Longrightarrow> new_list d (psubstts (f(c := d)) l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>new_term c t; d \<notin> f ` paramst t\<rbrakk> \<Longrightarrow> new_term d (psubstt (f(c := d)) t)) &&& (\<lbrakk>new_list c l; d \<notin> f ` paramsts l\<rbrakk> \<Longrightarrow> new_list d (psubstts (f(c := d)) l))
[PROOF STEP]
by (induct t and l rule: paramst.induct paramsts.induct) auto


[STATEMENT]
lemma new_psubst_image: \<open>new c p \<Longrightarrow> d \<notin> image f (params p) \<Longrightarrow> new d (psubst (f(c := d)) p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>new c p; d \<notin> f ` params p\<rbrakk> \<Longrightarrow> new d (psubst (f(c := d)) p)
[PROOF STEP]
using new_psubst_image'
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>new_term ?c ?t; ?d \<notin> ?f ` paramst ?t\<rbrakk> \<Longrightarrow> new_term ?d (psubstt (?f(?c := ?d)) ?t)
\<lbrakk>new_list ?c ?l; ?d \<notin> ?f ` paramsts ?l\<rbrakk> \<Longrightarrow> new_list ?d (psubstts (?f(?c := ?d)) ?l)

goal (1 subgoal):
 1. \<lbrakk>new c p; d \<notin> f ` params p\<rbrakk> \<Longrightarrow> new d (psubst (f(c := d)) p)
[PROOF STEP]
by (induct p) auto


[STATEMENT]
lemma news_psubst: \<open>news c z \<Longrightarrow> d \<notin> image f (\<Union>p \<in> set z. params p) \<Longrightarrow>
    news d (map (psubst (f(c := d))) z)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>news c z; d \<notin> f ` \<Union> (params ` set z)\<rbrakk> \<Longrightarrow> news d (map (psubst (f(c := d))) z)
[PROOF STEP]
using new_psubst_image
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>new ?c ?p; ?d \<notin> ?f ` params ?p\<rbrakk> \<Longrightarrow> new ?d (psubst (?f(?c := ?d)) ?p)

goal (1 subgoal):
 1. \<lbrakk>news c z; d \<notin> f ` \<Union> (params ` set z)\<rbrakk> \<Longrightarrow> news d (map (psubst (f(c := d))) z)
[PROOF STEP]
by (induct z) auto


[STATEMENT]
lemma member_psubst: \<open>p \<in> set z \<Longrightarrow> psubst f p \<in> set (map (psubst f) z)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> set z \<Longrightarrow> psubst f p \<in> set (map (psubst f) z)
[PROOF STEP]
by (induct z) auto