21 

    22 ML {*

    23   Outer_Syntax.local_theory_to_proof;

    24   Proof.theorem

    25 *}

    26 

    27 ML {*

    28 fun prove_strong_ind pred_name avoids ctxt =

    29   let

    30     val _ = ()

    31   in

    32     Proof.theorem NONE (fn thss => fn ctxt => ctxt) [] ctxt

    33   end

    34 

    35 (* outer syntax *)

    36 local

    37   structure P = Parse;

    38   structure S = Scan

    39 

    40 in

    41 val _ =

    42   Outer_Syntax.local_theory_to_proof "nominal_inductive"

    43     "prove strong induction theorem for inductive predicate involving nominal datatypes"

    44     Keyword.thy_goal

    45     (Parse.xname -- 

    46      (Scan.optional (Parse.$$$ "avoids" |-- Parse.enum1 "|" (Parse.name --

    47       (Parse.$$$ ":" |-- Parse.and_list1 Parse.term))) []) >> (fn (pred_name, avoids) =>

    48         prove_strong_ind pred_name avoids))

    49 

    50 end

    51 *}

    52 

    53 

    54 section {* Typing *}

    55 

    56 nominal_datatype ty =

    57   TVar string

    58 | TFun ty ty ("_ \<rightarrow> _") 

    59 

    60 

    61 inductive

    62   valid :: "(name \<times> ty) list \<Rightarrow> bool"

    63 where

    64   "valid []"

    65 | "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)"

    66 

    67 inductive

    68   typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 

    69 where

    70     t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"

    71   | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"

    72   | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"

    73 

    74 equivariance valid

    75 equivariance typing

    76 

    77 thm valid.eqvt

    78 thm typing.eqvt

    79 thm eqvts

    80 thm eqvts_raw

    81 

    82 thm typing.induct[of "\<Gamma>" "t" "T", no_vars]

    83 

    84 (*

    85 lemma

    86   fixes c::"'a::fs"

    87   assumes a: "\<Gamma> \<turnstile> t : T" 

    88   and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T"

    89   and a2: "\<And>\<Gamma> t1 T1 T2 t2 c. \<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<And>d. P d \<Gamma> t1 T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1; \<And>d. P d \<Gamma> t2 T1\<rbrakk> 

    90            \<Longrightarrow> P c \<Gamma> (App t1 t2) T2"

    91   and a3: "\<And>x \<Gamma> T1 t T2 c. \<lbrakk>atom x \<sharp> c; atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2; \<And>d. P d ((x, T1) # \<Gamma>) t T2\<rbrakk> 

    92            \<Longrightarrow> P c \<Gamma> (Lam x t) T1 \<rightarrow> T2"

    93   shows "P c \<Gamma> t T"

    94 proof -

    95   from a have "\<And>p c. P c (p \<bullet> \<Gamma>) (p \<bullet> t) (p \<bullet> T)"

    96   proof (induct)

    97     case (t_Var \<Gamma> x T p c)

    98     then show ?case

    99       apply -

   100       apply(perm_strict_simp)

   101       apply(rule a1)

   102       apply(drule_tac p="p" in permute_boolI)

   103       apply(perm_strict_simp add: permute_minus_cancel)

   104       apply(assumption)

   105       apply(rotate_tac 1)

   106       apply(drule_tac p="p" in permute_boolI)

   107       apply(perm_strict_simp add: permute_minus_cancel)

   108       apply(assumption)

   109       done

   110   next

   111     case (t_App \<Gamma> t1 T1 T2 t2 p c)

   112     then show ?case

   113       apply -

   114       apply(perm_strict_simp)

   115       apply(rule a2)

   116       apply(drule_tac p="p" in permute_boolI)

   117       apply(perm_strict_simp add: permute_minus_cancel)

   118       apply(assumption)

   119       apply(assumption)

   120       apply(rotate_tac 2)

   121       apply(drule_tac p="p" in permute_boolI)

   122       apply(perm_strict_simp add: permute_minus_cancel)

   123       apply(assumption)

   124       apply(assumption)

   125       done

   126   next

   127     case (t_Lam x \<Gamma> T1 t T2 p c)

   128     then show ?case

   129       apply -

   130       apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom x}) \<sharp>* c \<and> 

   131         supp (p \<bullet> \<Gamma>, p \<bullet> Lam x t, p \<bullet> (T1 \<rightarrow> T2)) \<sharp>* q")

   132       apply(erule exE)

   133       apply(rule_tac t="p \<bullet> \<Gamma>" and  s="(q + p) \<bullet> \<Gamma>" in subst)

   134       apply(simp only: permute_plus)

   135       apply(rule supp_perm_eq)

   136       apply(simp add: supp_Pair fresh_star_union)

   137       apply(rule_tac t="p \<bullet> Lam x t" and  s="(q + p) \<bullet> Lam x t" in subst)

   138       apply(simp only: permute_plus)

   139       apply(rule supp_perm_eq)

   140       apply(simp add: supp_Pair fresh_star_union)

   141       apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and  s="(q + p) \<bullet> (T1 \<rightarrow> T2)" in subst)

   142       apply(simp only: permute_plus)

   143       apply(rule supp_perm_eq)

   144       apply(simp add: supp_Pair fresh_star_union)

   145       apply(simp (no_asm) only: eqvts)

   146       apply(rule a3)

   147       apply(simp only: eqvts permute_plus)

   148       apply(simp add: fresh_star_def)

   149       apply(drule_tac p="q + p" in permute_boolI)

   150       apply(perm_strict_simp add: permute_minus_cancel)

   151       apply(assumption)

   152       apply(rotate_tac 1)

   153       apply(drule_tac p="q + p" in permute_boolI)

   154       apply(perm_strict_simp add: permute_minus_cancel)

   155       apply(assumption)

   156       apply(drule_tac x="d" in meta_spec)

   157       apply(drule_tac x="q + p" in meta_spec)

   158       apply(perm_strict_simp add: permute_minus_cancel)

   159       apply(assumption)

   160       apply(rule at_set_avoiding2)

   161       apply(simp add: finite_supp)

   162       apply(simp add: finite_supp)

   163       apply(simp add: finite_supp)

   164       apply(rule_tac p="-p" in permute_boolE)

   165       apply(perm_strict_simp add: permute_minus_cancel)

   166 	--"supplied by the user"

   167       apply(simp add: fresh_star_prod)

   168       apply(simp add: fresh_star_def)

   169       sorry

   170   qed

   171   then have "P c (0 \<bullet> \<Gamma>) (0 \<bullet> t) (0 \<bullet> T)" .

   172   then show "P c \<Gamma> t T" by simp

   173 qed

   174 

   175 *)