equal
deleted
inserted
replaced
60 |
60 |
61 lemma induct: |
61 lemma induct: |
62 assumes a1: "\<And>name b. P b (Var name)" |
62 assumes a1: "\<And>name b. P b (Var name)" |
63 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |
63 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |
64 and a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)" |
64 and a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)" |
65 shows "P a t \<and> P' d ts " |
65 shows "P (a :: 'a :: pt) t \<and> P' d ts " |
66 proof - |
66 proof - |
67 have " (\<forall>p. P a (p \<bullet> t)) \<and> (\<forall>p. P' d (p \<bullet> ts))" |
67 have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))" |
68 apply (rule t_tyS.induct) |
68 apply (rule t_tyS.induct) |
69 apply (simp add: a1) |
69 apply (simp add: a1) |
70 apply (simp_all) |
70 apply (simp) |
|
71 apply (rule allI)+ |
|
72 apply (rule a2) |
|
73 apply simp |
|
74 apply simp |
71 apply (rule allI) |
75 apply (rule allI) |
72 apply (rule a2) |
|
73 defer defer |
|
74 apply (rule allI) |
76 apply (rule allI) |
|
77 apply(subgoal_tac "\<exists>new::name fset. fset_to_set (fmap atom new) \<sharp>* (d, All (p \<bullet> fset) (p \<bullet> t)) |
|
78 \<and> fcard new = fcard fset") |
|
79 apply clarify |
|
80 (*apply(rule_tac t="p \<bullet> All fset t" and |
|
81 s="(((p \<bullet> fset) \<leftrightarrow> new) + p) \<bullet> All fset t" in subst) |
75 apply (rule a3) |
82 apply (rule a3) |
76 apply simp_all |
83 apply simp_all*) |
77 sorry |
84 sorry |
78 then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast |
85 then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast |
79 then show ?thesis by simp |
86 then show ?thesis by simp |
80 qed |
87 qed |
81 |
88 |