11 atom_decl name |
11 atom_decl name |
12 |
12 |
13 nominal_datatype lam = Var "name" |
13 nominal_datatype lam = Var "name" |
14 | App "lam" "lam" |
14 | App "lam" "lam" |
15 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
15 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
16 |
|
17 section {* Strong induction principles for lam *} |
|
18 |
|
19 lemma lam_induct'[case_names Fin Var App Lam]: |
|
20 fixes P :: "'a \<Rightarrow> lam \<Rightarrow> bool" |
|
21 and f :: "'a \<Rightarrow> 'a" |
|
22 assumes fs: "\<And>x. finite ((supp (f x))::name set)" |
|
23 and h1: "\<And>a x. P x (Var a)" |
|
24 and h2: "\<And>t1 t2 x. (\<And>z. P z t1) \<Longrightarrow> (\<And>z. P z t2) \<Longrightarrow> P x (App t1 t2)" |
|
25 and h3: "\<And>a t x. a\<sharp>f x \<Longrightarrow> (\<And>z. P z t) \<Longrightarrow> P x (Lam [a].t)" |
|
26 shows "P x t" |
|
27 proof - |
|
28 have "\<And>(pi::name prm) x. P x (pi\<bullet>t)" |
|
29 proof (induct rule: lam.induct_weak) |
|
30 case (Lam a t) |
|
31 have ih: "\<And>(pi::name prm) x. P x (pi\<bullet>t)" by fact |
|
32 show "\<And>(pi::name prm) x. P x (pi\<bullet>(Lam [a].t))" |
|
33 proof (simp) |
|
34 fix x::"'a" and pi::"name prm" |
|
35 have "\<exists>c::name. c\<sharp>(f x,pi\<bullet>a,pi\<bullet>t)" |
|
36 by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1 fs) |
|
37 then obtain c::"name" |
|
38 where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(f x)" and f3: "c\<sharp>(pi\<bullet>t)" |
|
39 by (force simp add: fresh_prod fresh_atm) |
|
40 have "Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t)) = Lam [(pi\<bullet>a)].(pi\<bullet>t)" using f1 f3 |
|
41 by (simp add: lam.inject alpha) |
|
42 moreover |
|
43 from ih have "\<And>x. P x (([(c,pi\<bullet>a)]@pi)\<bullet>t)" by force |
|
44 hence "\<And>x. P x ([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t))" by (simp add: pt_name2[symmetric]) |
|
45 hence "P x (Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t)))" using h3 f2 |
|
46 by (auto simp add: fresh_def at_fin_set_supp[OF at_name_inst, OF fs]) |
|
47 ultimately show "P x (Lam [(pi\<bullet>a)].(pi\<bullet>t))" by simp |
|
48 qed |
|
49 qed (auto intro: h1 h2) |
|
50 hence "P x (([]::name prm)\<bullet>t)" by blast |
|
51 thus "P x t" by simp |
|
52 qed |
|
53 |
|
54 lemma lam_induct[case_names Var App Lam]: |
|
55 fixes P :: "('a::fs_name) \<Rightarrow> lam \<Rightarrow> bool" |
|
56 and x :: "'a::fs_name" |
|
57 and t :: "lam" |
|
58 assumes h1: "\<And>a x. P x (Var a)" |
|
59 and h2: "\<And>t1 t2 x. (\<And>z. P z t1)\<Longrightarrow>(\<And>z. P z t2)\<Longrightarrow>P x (App t1 t2)" |
|
60 and h3: "\<And>a t x. a\<sharp>x \<Longrightarrow> (\<And>z. P z t)\<Longrightarrow> P x (Lam [a].t)" |
|
61 shows "P x t" |
|
62 apply(rule lam_induct'[of "\<lambda>x. x" "P"]) |
|
63 apply(simp add: fs_name1) |
|
64 apply(auto intro: h1 h2 h3) |
|
65 done |
|
66 |
16 |
67 types 'a f1_ty = "name\<Rightarrow>('a::pt_name)" |
17 types 'a f1_ty = "name\<Rightarrow>('a::pt_name)" |
68 'a f2_ty = "'a\<Rightarrow>'a\<Rightarrow>('a::pt_name)" |
18 'a f2_ty = "'a\<Rightarrow>'a\<Rightarrow>('a::pt_name)" |
69 'a f3_ty = "name\<Rightarrow>'a\<Rightarrow>('a::pt_name)" |
19 'a f3_ty = "name\<Rightarrow>'a\<Rightarrow>('a::pt_name)" |
70 |
20 |
913 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
863 and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" |
914 and a1: "\<forall>c. fun (Var c) = f1 c" |
864 and a1: "\<forall>c. fun (Var c) = f1 c" |
915 and a2: "\<forall>t1 t2. fun (App t1 t2) = f2 (fun t1) (fun t2)" |
865 and a2: "\<forall>t1 t2. fun (App t1 t2) = f2 (fun t1) (fun t2)" |
916 and a3: "\<forall>a t. a\<sharp>(f1,f2,f3) \<longrightarrow> fun (Lam [a].t) = f3 a (fun t)" |
866 and a3: "\<forall>a t. a\<sharp>(f1,f2,f3) \<longrightarrow> fun (Lam [a].t) = f3 a (fun t)" |
917 shows "fun t = rfun f1 f2 f3 t" |
867 shows "fun t = rfun f1 f2 f3 t" |
918 apply (rule lam_induct'[of "\<lambda>_. (f1,f2,f3)" "\<lambda>_ t. fun t = rfun f1 f2 f3 t"]) |
868 apply (rule lam.induct'[of "\<lambda>_. ((supp (f1,f2,f3))::name set)" "\<lambda>_ t. fun t = rfun f1 f2 f3 t"]) |
|
869 apply(fold fresh_def) |
919 (* finite support *) |
870 (* finite support *) |
920 apply(rule f) |
871 apply(rule f) |
921 (* VAR *) |
872 (* VAR *) |
922 apply(simp add: a1 rfun_Var[OF f, OF c, symmetric]) |
873 apply(simp add: a1 rfun_Var[OF f, OF c, symmetric]) |
923 (* APP *) |
874 (* APP *) |
1027 and f2::"('a::pt_name) f2_ty'" |
978 and f2::"('a::pt_name) f2_ty'" |
1028 and f3::"('a::pt_name) f3_ty'" |
979 and f3::"('a::pt_name) f3_ty'" |
1029 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
980 assumes f: "finite ((supp (f1,f2,f3))::name set)" |
1030 and c: "(\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y))" |
981 and c: "(\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y))" |
1031 shows "fst (rfun_gen' f1 f2 f3 t) = t" |
982 shows "fst (rfun_gen' f1 f2 f3 t) = t" |
1032 apply(rule lam_induct'[of "\<lambda>_. (f1,f2,f3)" "\<lambda>_ t. fst (rfun_gen' f1 f2 f3 t) = t"]) |
983 apply(rule lam.induct'[of "\<lambda>_. ((supp (f1,f2,f3))::name set)" "\<lambda>_ t. fst (rfun_gen' f1 f2 f3 t) = t"]) |
|
984 apply(fold fresh_def) |
1033 apply(simp add: f) |
985 apply(simp add: f) |
1034 apply(unfold rfun_gen'_def) |
986 apply(unfold rfun_gen'_def) |
1035 apply(simp only: rfun_Var[OF fsupp'[OF f],OF fcb'[OF f, OF c]]) |
987 apply(simp only: rfun_Var[OF fsupp'[OF f],OF fcb'[OF f, OF c]]) |
1036 apply(simp) |
988 apply(simp) |
1037 apply(simp only: rfun_App[OF fsupp'[OF f],OF fcb'[OF f, OF c]]) |
989 apply(simp only: rfun_App[OF fsupp'[OF f],OF fcb'[OF f, OF c]]) |
1360 fixes pi:: "name prm" |
1312 fixes pi:: "name prm" |
1361 and t1:: "lam" |
1313 and t1:: "lam" |
1362 and t2:: "lam" |
1314 and t2:: "lam" |
1363 and a :: "name" |
1315 and a :: "name" |
1364 shows "pi\<bullet>(t1[b::=t2]) = (pi\<bullet>t1)[(pi\<bullet>b)::=(pi\<bullet>t2)]" |
1316 shows "pi\<bullet>(t1[b::=t2]) = (pi\<bullet>t1)[(pi\<bullet>b)::=(pi\<bullet>t2)]" |
1365 apply(nominal_induct t1 avoiding: b t2 rule: lam_induct) |
1317 apply(nominal_induct t1 avoiding: b t2 rule: lam.induct) |
1366 apply(auto simp add: perm_bij fresh_prod fresh_atm) |
1318 apply(auto simp add: perm_bij fresh_prod fresh_atm) |
1367 apply(subgoal_tac "(pi\<bullet>a)\<sharp>(pi\<bullet>b,pi\<bullet>t2)")(*A*) |
1319 apply(subgoal_tac "(pi\<bullet>name)\<sharp>(pi\<bullet>b,pi\<bullet>t2)")(*A*) |
1368 apply(simp) |
1320 apply(simp) |
|
1321 (*A*) |
1369 apply(simp add: perm_bij fresh_prod fresh_atm pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) |
1322 apply(simp add: perm_bij fresh_prod fresh_atm pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) |
1370 done |
1323 done |
1371 |
1324 |
1372 lemma subst_supp: "supp(t1[a::=t2])\<subseteq>(((supp(t1)-{a})\<union>supp(t2))::name set)" |
1325 lemma subst_supp: "supp(t1[a::=t2])\<subseteq>(((supp(t1)-{a})\<union>supp(t2))::name set)" |
1373 apply(nominal_induct t1 avoiding: a t2 rule: lam_induct) |
1326 apply(nominal_induct t1 avoiding: a t2 rule: lam.induct) |
1374 apply(auto simp add: lam.supp supp_atm fresh_prod abs_supp) |
1327 apply(auto simp add: lam.supp supp_atm fresh_prod abs_supp) |
1375 apply(blast) |
1328 apply(blast) |
1376 apply(blast) |
1329 apply(blast) |
1377 done |
1330 done |
1378 |
1331 |