Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Nominal2.thy
changeset 2616 dd7490fdd998
parent 2613 1803104d76c9
child 2617 e44551d067e6
equal deleted inserted replaced
2615:d5713db7e146 2616:dd7490fdd998 
   114   end
 
   114   end
 
   115 *} 
   115 *} 
   116 
   116 
   117 ML {*
 
   117 ML {*
 
   118 (* derives abs_eq theorems of the form Exists s. [as].t = [p o as].s *)
 
   118 (* derives abs_eq theorems of the form Exists s. [as].t = [p o as].s *)
 
   119 fun abs_eq_thm ctxt fprops p parms bn_finite_thms (BC (bmode, binders, bodies)) =
 
   119 fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns
 
       
   120   (bclause as (BC (bmode, binders, bodies))) =
 
   120   case binders of
 
   121   case binders of
 
   121     [] => [] 
   122     [] => [] 
   122   | _ =>
 
   123   | _ =>
 
   123       let
 
   124       let
 
   124         val binder_trm = comb_binders ctxt bmode parms binders
 
   125         val binder_trm = comb_binders ctxt bmode parms binders
 
   131           | Set => (@{const_name "Abs_set"}, @{typ "atom set"},  @{type_name abs_set})
 
   132           | Set => (@{const_name "Abs_set"}, @{typ "atom set"},  @{type_name abs_set})
 
   132           | Res => (@{const_name "Abs_res"}, @{typ "atom set"},  @{type_name abs_res})
 
   133           | Res => (@{const_name "Abs_res"}, @{typ "atom set"},  @{type_name abs_res})
 
   133 
   134 
   134         val abs = Const (abs_name, [binder_ty, body_ty] ---> Type (abs_ty, [body_ty]))
 
   135         val abs = Const (abs_name, [binder_ty, body_ty] ---> Type (abs_ty, [body_ty]))
 
   135         val abs_lhs = abs $ binder_trm $ body_trm
 
   136         val abs_lhs = abs $ binder_trm $ body_trm
 
   136         val abs_rhs = abs $ mk_perm p binder_trm $ Bound 0
 
   137         val abs_rhs = abs $ mk_perm p binder_trm $ mk_perm (Bound 0) body_trm
 
   137         val goal = HOLogic.mk_eq (abs_lhs, abs_rhs)
 
   138         val abs_rhs' = abs $ mk_perm (Bound 0) binder_trm $ mk_perm (Bound 0) body_trm
 
   138           |> (fn t => HOLogic.mk_exists ("y", body_ty, t))
 
   139         val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs)
 
       
   140         val abs_eq' = HOLogic.mk_eq (abs_lhs, abs_rhs')
 
       
   141         val eq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) 
       
   142 
       
   143         val goal = HOLogic.mk_conj (abs_eq, eq)
 
       
   144           |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))
 
   139           |> HOLogic.mk_Trueprop  
   145           |> HOLogic.mk_Trueprop  
       
   146 
       
   147         val goal' = HOLogic.mk_conj (abs_eq', eq)
 
       
   148           |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))
 
       
   149           |> HOLogic.mk_Trueprop   
   140  
   150  
   141         val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt}
 
   151         val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt}
 
   142           @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
 
   152           @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
 
   143           fresh_star_set} @ @{thms finite.intros finite_fset}  
   153           fresh_star_set} @ @{thms finite.intros finite_fset}
 
   144      in
 
   154      in
 
   145        [Goal.prove ctxt [] [] goal
 
   155        if is_recursive_binder bclause
 
   146           (K (HEADGOAL (resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst}
 
   156        then
 
   147               THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss))))] 
   157          (tracing "recursive";
 
       
   158          [ Goal.prove ctxt [] [] goal'
 
       
   159              (K (HEADGOAL (resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
 
       
   160                  THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss))))
 
       
   161            |> Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []
 
       
   162          ])
 
       
   163        else
 
       
   164          (tracing "non-recursive";
 
       
   165          [ Goal.prove ctxt [] [] goal
 
       
   166              (K (HEADGOAL (resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst}
 
       
   167                  THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss))))
 
       
   168            |> Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []
 
       
   169          ]) 
   148      end
 
   170      end
 
   149 *}
 
   171 *}
 
   150 
   172 
   151 
   173 ML {*
 
   152 (* FIXME: use pure cterm functions *)
 
   174 fun conj_tac tac i =
 
   153 ML {*
 
   175   let
 
   154 fun mk_cperm ctxt p ctrm =
 
   176      fun select (t, i) =
 
   155   mk_perm (term_of p) (term_of ctrm)
 
   177        case t of
 
   156   |> cterm_of (ProofContext.theory_of ctxt)
 
   178          @{term "Trueprop"} $ t' => select (t', i)
 
   157 *}
 
   179        | @{term "op \<and>"} $ _ $ _ => (rtac @{thm conjI} THEN' RANGE [conj_tac tac, conj_tac tac]) i
 
   158 
   180        | _ => tac i
 
   159 
   181   in
 
   160 ML {*
 
   182     SUBGOAL select i
 
   161 fun case_tac ctxt c bn_finite_thms (prems, bclausess) thm =
 
   183   end
 
       
   184 *}
 
       
   185 
       
   186 ML {*
 
       
   187 fun is_abs_eq thm =
 
       
   188   let
 
       
   189     fun is_abs trm =
 
       
   190       case (head_of trm) of
 
       
   191         Const (@{const_name "Abs_set"}, _) => true
 
       
   192       | Const (@{const_name "Abs_lst"}, _) => true
 
       
   193       | Const (@{const_name "Abs_res"}, _) => true
 
       
   194       | _ => false
 
       
   195   in 
       
   196     thm |> prop_of 
       
   197         |> HOLogic.dest_Trueprop
 
       
   198         |> HOLogic.dest_eq
 
       
   199         |> fst
 
       
   200         |> is_abs
 
       
   201   end
 
       
   202 *}
 
       
   203 
       
   204 lemma setify:
 
       
   205   shows "xs = ys \<Longrightarrow> set xs = set ys" 
       
   206   by simp
 
       
   207 
       
   208 ML {*
 
       
   209 fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas 
       
   210   (prems, bclausess) qexhaust_thm =
 
   162   let
 
   211   let
 
   163     fun aux_tac prem bclauses =
 
   212     fun aux_tac prem bclauses =
 
   164       case (get_all_binders bclauses) of
 
   213       case (get_all_binders bclauses) of
 
   165         [] => EVERY' [rtac prem, atac]
 
   214         [] => EVERY' [rtac prem, atac]
 
   166       | binders => Subgoal.FOCUS (fn {params, prems, context = ctxt, ...} =>  
   215       | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} =>  
   167           let
 
   216           let
 
   168             val parms = map (term_of o snd) params
 
   217             val parms = map (term_of o snd) params
 
   169             val fthm = fresh_thm ctxt c parms binders bn_finite_thms 
   218             val fthm = fresh_thm ctxt c parms binders bn_finite_thms 
   170   
   219   
   171             val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}
 
   220             val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}
 
   172             val (([(_, fperm)], fprops), ctxt') = Obtain.result
 
   221             val (([(_, fperm)], fprops), ctxt') = Obtain.result
 
   173               (K (EVERY1 [etac exE, 
   222               (K (EVERY1 [etac exE, 
   174                           full_simp_tac (HOL_basic_ss addsimps ss), 
   223                           full_simp_tac (HOL_basic_ss addsimps ss), 
   175                           REPEAT o (etac conjE)])) [fthm] ctxt 
   224                           REPEAT o (etac @{thm conjE})])) [fthm] ctxt 
   176   
   225   
   177             val abs_eqs = flat (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms) bclauses)
 
   226             val abs_eq_thms = flat 
   178 
   227              (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms bn_eqvt permute_bns) bclauses)
 
   179             val _ = tracing ("test")
 
   228 
   180             (*
 
   229             val ((_, eqs), ctxt'') = Obtain.result
 
   181             val _ = tracing ("fprop:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) fprops))
 
   230               (K (EVERY1 
   182             *)    
   231                    [ REPEAT o (etac @{thm exE}), 
   183             (* 
   232                      REPEAT o (etac @{thm conjE}),
 
   184             val _ = tracing ("abs_eqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) abs_eqs))
 
   233                      REPEAT o (dtac @{thm setify}),
 
   185             *)
 
   234                      full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt' 
       
   235 
       
   236             val (abs_eqs, peqs) = split_filter is_abs_eq eqs
 
       
   237 
       
   238             val fprops' = map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops
 
       
   239             val fprops'' = map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops
 
       
   240 
       
   241             val _ = tracing ("prem:\n" ^ (Syntax.string_of_term ctxt'' o prop_of) prem)
 
       
   242             val _ = tracing ("prems:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) prems))
 
       
   243             val _ = tracing ("fprop':\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) fprops'))
 
       
   244             val _ = tracing ("fprop'':\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) fprops''))
 
       
   245             val _ = tracing ("abseq:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) abs_eqs))
 
       
   246             val _ = tracing ("peqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) peqs))
 
       
   247               
       
   248  
       
   249             val tac1 = EVERY'
 
       
   250               [ simp_tac (HOL_basic_ss addsimps peqs),
 
       
   251                 rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}),
 
       
   252                 K (print_tac "before solving freshness"), 
       
   253                 conj_tac (TRY o DETERM o resolve_tac (fprops' @ fprops'')) ] 
       
   254 
       
   255             val tac2 = EVERY' 
       
   256               [ rtac (@{thm ssubst} OF prems),
 
       
   257                 rewrite_goal_tac (map safe_mk_equiv eq_iff_thms),
 
       
   258                 K (print_tac "before substituting"),
 
       
   259                 rewrite_goal_tac (map safe_mk_equiv abs_eqs),
 
       
   260                 K (print_tac "after substituting"),
 
       
   261                 conj_tac (TRY o DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)),
 
       
   262                 K (print_tac "end") 
       
   263               ] 
       
   264 
       
   265             val side_thm = Goal.prove ctxt'' [] [] (term_of concl)
 
       
   266               (fn _ => (* Skip_Proof.cheat_tac (ProofContext.theory_of ctxt'') *)
 
       
   267                        EVERY 
       
   268                         [ rtac prem 1,
 
       
   269                           print_tac "after applying prem",
 
       
   270                           RANGE [SOLVED' tac1, SOLVED' tac2] 1,
 
       
   271                           print_tac "final" ] )
 
       
   272               |> singleton (ProofContext.export ctxt'' ctxt)  
       
   273 
       
   274             val _ = tracing ("side_thm:\n" ^ (Syntax.string_of_term ctxt o prop_of) side_thm)
 
   186           in
 
   275           in
 
   187             (*HEADGOAL (rtac prem THEN' RANGE [K all_tac, simp_tac (HOL_basic_ss addsimps prems)])*)
 
   276             rtac side_thm 1 
   188             Skip_Proof.cheat_tac (ProofContext.theory_of ctxt')
 
       
   189           end) ctxt
 
   277           end) ctxt
 
   190   in
 
   278   in
 
   191     rtac thm THEN' RANGE (map2 aux_tac prems bclausess)
 
   279     rtac qexhaust_thm THEN' RANGE (map2 aux_tac prems bclausess)
 
   192   end
 
   280   end
 
   193 *}
 
   281 *}
 
   194 
   282 
   195 
   283 
   196 ML {*
 
   284 ML {*
 
   197 fun prove_strong_exhausts lthy qexhausts qtrms bclausesss bn_finite_thms =
 
   285 fun prove_strong_exhausts lthy exhausts qtrms bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns 
       
   286   perm_bn_alphas =
 
   198   let
 
   287   let
 
   199     val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy 
   288     val ((_, exhausts'), lthy') = Variable.import true exhausts lthy 
   200 
   289 
   201     val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
 
   290     val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
 
   202     val c = Free (c, TFree (a, @{sort fs}))
 
   291     val c = Free (c, TFree (a, @{sort fs}))
 
   203 
   292 
   204     val (ecases, main_concls) = qexhausts' (* ecases or of the form (params, prems, concl) *)
 
   293     val (ecases, main_concls) = exhausts' (* ecases or of the form (params, prems, concl) *)
 
   205       |> map prop_of
 
   294       |> map prop_of
 
   206       |> map Logic.strip_horn
 
   295       |> map Logic.strip_horn
 
   207       |> split_list
 
   296       |> split_list
 
   208       |>> (map o map) strip_params_prems_concl     
   297       |>> (map o map) strip_params_prems_concl     
   209 
   298 
   213      (fn {prems:thm list, context} =>
 
   302      (fn {prems:thm list, context} =>
 
   214         let
 
   303         let
 
   215            val prems' = partitions prems (map length bclausesss)
 
   304            val prems' = partitions prems (map length bclausesss)
 
   216         in
 
   305         in
 
   217           EVERY1 [Goal.conjunction_tac,
 
   306           EVERY1 [Goal.conjunction_tac,
 
   218             RANGE (map2 (case_tac context c bn_finite_thms) (prems' ~~ bclausesss) qexhausts')]
 
   307             RANGE (map2 (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas) 
       
   308                       (prems' ~~ bclausesss) exhausts')]
 
   219         end)
 
   309         end)
 
   220   end
 
   310   end
 
   221 *}
 
   311 *}
 
   222 
   312 
   223 
   313 
   580   val qty_names = map Long_Name.base_name qty_full_names             
   670   val qty_names = map Long_Name.base_name qty_full_names             
   581 
   671 
   582   (* defining of quotient term-constructors, binding functions, free vars functions *)
 
   672   (* defining of quotient term-constructors, binding functions, free vars functions *)
 
   583   val _ = warning "Defining the quotient constants"
 
   673   val _ = warning "Defining the quotient constants"
 
   584   val qconstrs_descrs =
 
   674   val qconstrs_descrs =
 
   585     map2 (map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx))) (get_cnstrs dts) raw_constrs
 
   675     (map2 o map2) (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) (get_cnstrs dts) raw_constrs
 
   586 
   676 
   587   val qbns_descr =
 
   677   val qbns_descr =
 
   588     map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns
 
   678     map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns
 
   589 
   679 
   590   val qfvs_descr = 
   680   val qfvs_descr = 
   732   val qpermute_bn_thms = 
   822   val qpermute_bn_thms = 
   733     if get_STEPS lthy > 33
 
   823     if get_STEPS lthy > 33
 
   734     then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC
 
   824     then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC
 
   735     else []
 
   825     else []
 
   736 
   826 
   737   val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses qbn_finite_thms
 
   827   val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses qbn_finite_thms qeq_iffs'
 
       
   828     qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms
 
       
   829 
   738 
   830 
   739   (* noting the theorems *)  
   831   (* noting the theorems *)  
   740 
   832 
   741   (* generating the prefix for the theorem names *)
 
   833   (* generating the prefix for the theorem names *)
 
   742   val thms_name = 
   834   val thms_name = 
   915     fun add bcs i = (if included i bcs then [] else [BC (Lst, [], [i])]) 
  1007     fun add bcs i = (if included i bcs then [] else [BC (Lst, [], [i])]) 
   916   in
 
  1008   in
 
   917     bcs @ (flat (map_range (add bcs) n))
 
  1009     bcs @ (flat (map_range (add bcs) n))
 
   918   end
 
  1010   end
 
   919 in
 
  1011 in
 
   920   map2 (map2 complt) args bclauses
 
  1012   (map2 o map2) complt args bclauses
 
   921 end
 
  1013 end
 
   922 *}
 
  1014 *}
 
   923 
  1015 
   924 ML {*
 
  1016 ML {*
 
   925 fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = 
  1017 fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy =
nominal2